When-so-ever a formal proof from any closed WFF** to a semantic value in {True, False} cannot be completed then this closed WFF is necessarily semantically incorrect.

∀L ∈ Formal_Systems

∀X ∈ Closed-WFF(L)

~True(L, X) ∧ ~False(L, X) → Incorrect(L, X)

**Backward-chaining inference. (Truth Predicate Defined Here)

**In English: “This sentence is not true”.**

**In Higher Order Logic:**

** ∀L ∈ Formal_Systems**

**LP ≡ ~∃Γ ⊆ BaseFact(L) (Γ ⊢ LP)**

**Minimal Type Theory (MTT) Knowledge Tree of the Liar Paradox:**

Translated into a directed acyclic graph (DAG) by the MTT compiler

[00] LP (01)(07)

[01] NOT (02)

[02] THERE_EXISTS (03)

[03] SUBSET_OF (04)(05)

[04] Γ

[05] BaseFacts (06)

[06] L

[07] PROVES (04)(00) // **cycle indicates infinite evaluation loop**

**∀L ∈ Formal_Systems**

** ∀X ∈ Closed-WFF(L)**

** ~True(L, X) ∧ ~False(L, X) → Incorrect(L, X)**

**∴ ~True(L, LP) ∧ ~False(L, LP) → Incorrect(L, LP)**

Because the evaluation of the above **formalized Liar Paradox** has the semantic error of

pathological self-reference(Olcott 2004) (indicated by the infinite evaluation loop)

the **formal proof from LP** never reaches a semantic value of {True, False}.

Copyright 2016 and 2017 Pete Olcott