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

Minimal Type Theory Directed Acyclic Graph

∀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