In English: “This sentence is not true”.
Liar_Paradox  ≡  ∃X ~Provable(X, Liar_Paradox)

Minimal Type Theory (MTT) Knowledge Tree of the Liar Paradox:
Translated into a directed acyclic graph (DAG) by the MTT compiler
[01] Liar_Paradox        (02)(04)
[02] THERE_EXISTS   (03)
[03] X
[04] NOT                           (05)
[05] Provable                  (03)(01)  // cycle indicates infinite evaluation loop

Minimal Type Theory Directed Acyclic Graph

The above formalism shows that the Liar Paradox gets stuck in an infinite evaluation loop and is thus not a Truth Bearer. Any expression that is impossibly true and impossibly false is not a truth bearer and therefore not a member of any Formal System even though it may otherwise be a syntactically WFF.

Copyright 2016 and 2017 Pete Olcott