∃X (X ⊢ Y) asserts that there is a set of connected WFF from X to Y.

If G is an alias (sentential variable) for ∃X (X ⊢ Y), then G is either True or False, even if both X and Y are gibberish.

If G is an alias (sentential variable) for ~∃X (X ⊢ G) we have pathological self-reference creating infinite recursion. This prevents G from ever evaluating to either True or False, thus making G semantically ill-formed.

copyright 2017 Pete Olcott (Created Friday October 13, 2017)

**Originally posted material is shown below**

If the 1931 Incompleteness Theorem is correct then the much simpler expression at the end of this post equally proves that there are some sentences of predicate logic that are neither provable nor refutable.

Syntactic_Logical_Consequence (Γ proves A)

A formula A is a syntactic consequence within some formal system FS of a set Γ of formulas if there is a formal proof in FS of A from the set Γ:

**Γ ⊢ _{FS} A**

Translation to Minimal Type Theory notational conventions

**Γ ⊢ _{FS} A ≡ ( Γ ⊂ FS (Γ ⊢ A) )**

Named predicate (of predicate logic PL) impossible to prove and impossible to refute:** G( ~∃Γ ⊂ PL (Γ ⊢ G) )**