Prolog detects [and rejects] pathological self reference in the Gödel sentence + Wittgenstein

[olcott]

The conventional definition of incompleteness:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ))

When we see that the following Prolog expressions satisfy the above
definition of incompleteness then we can see that they are equivalent to
the Gödel sentence in the 1931 incompleteness proof.

?- G = not(provable(F, G)). % G = ¬(F ⊢ G)
?- G = not(provable(F, not(G))). % G = ¬(F ⊢ ¬G)

When we test the above pair of expressions we find that neither of them
are provable in the Prolog formal system:
(SWI-Prolog (threaded, 64 bits, version 7.6.4)

?- unify_with_occurs_check(G, not(provable(F, G))).false.
?- unify_with_occurs_check(G, not(provable(F, not(G)))).false.

https://www.liarparadox.org/Wittgenstein.pdf
Within Wittgenstein's controversial formalization of true and false:

'True in Russell's system' means, as was said:
proved in Russell's system; and

'false in Russell's system' means:
the opposite has been proved in Russell's system.

Then the above minimal essence of Gödel's logic sentence: φ is construed
as neither true nor false thus (like the liar paradox) simply not a
truth bearer. Gödel would construe this same case as Incomplete(T).

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence


--
Copyright 2022 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

[olcott]

The conventional definition of incompleteness:
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ))

When we see that the following Prolog expressions satisfy the above
definition of incompleteness then we can see that they are equivalent to
the Gödel sentence in the 1931 incompleteness proof.

?- G = not(provable(F, G)). % G = ¬(F ⊢ G)
?- G = not(provable(F, not(G))). % G = ¬(F ⊢ ¬G)

When we test the above pair of expressions we find that neither of them
are provable in the Prolog formal system:
(SWI-Prolog (threaded, 64 bits, version 7.6.4)

?- unify_with_occurs_check(G, not(provable(F, G))).false.
?- unify_with_occurs_check(G, not(provable(F, not(G)))).false.

*I forgot to include these two paragraphs*
Thus fulfilling the conventional definition of incompleteness, and
proving equivalence to the 1931 Gödel “Incompleteness” sentence. The
1931 Gödel Incompleteness theorem correctly concludes that neither G nor
¬G are provable in F.

The key detail that it leaves out is that neither G nor ¬G are provable
in F because both are erroneous cyclic terms that cannot be resolved in
any formal system what-so-ever.