From Newsgroup: comp.theory

olcott kirjoitti 1.12.2025 klo 14.45:

On 12/1/2025 4:18 AM, Mikko wrote:

olcott kirjoitti 29.11.2025 klo 20.01:

On 11/29/2025 4:31 AM, Mikko wrote:

olcott kirjoitti 28.11.2025 klo 17.21:

On 11/28/2025 2:40 AM, Mikko wrote:

olcott kirjoitti 27.11.2025 klo 17.48:

On 11/27/2025 2:17 AM, Mikko wrote:

olcott kirjoitti 26.11.2025 klo 17.20:

On 11/26/2025 4:17 AM, Mikko wrote:

olcott kirjoitti 14.11.2025 klo 16.49:

On 11/14/2025 3:09 AM, Mikko wrote:

On 2025-11-14 00:56:17 +0000, Tristan Wibberley said:

On 13/11/2025 09:05, Mikko wrote:

On 2025-11-12 14:45:34 +0000, olcott said:

... formalized in Minimal
Type Theory as LP := ~True(LP).
(where A := B means A is defined as B).

https://philpapers.org/rec/OLCREO

Can someone review my actual reasoning
elaborated in the paper?

If you want to use the term "formal language" you must >>>>>>>>>>>>>> prove that
there is a Turing machine that can determine whether a >>>>>>>>>>>>>> string is a
valid sentence of your language. If no such Turing machine >>>>>>>>>>>>>> exists
you have no justifiction for the use of the word "formal". >>>>>>>>>>>>>

It looks, at a glance, like his system has no theorems with >>>>>>>>>>>>> loops in
them. The system is "safe" and very small.

It does not look small. It seems to have very many
postulates, perhaps
infinitely many. The intent is that it be complete so it >>>>>>>>>>>> probably is
only paraconsistent or perhaps even inconsistent.

My system rejects expressions of language that cannot
possibly be resolved to a truth value because they have
pathological self-reference(Olcott 2004)

G ↔ ¬Prov(⌜G⌝)

That can be evaluated ir sufficient defitions are given. In >>>>>>>>>> particular,

Directed Graph of evaluation sequence
00 ↔               01 02
01 G
02 ¬               03
03 Prov            04
04 Gödel_Number_of 01  // cycle

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

You do not understand the deep meaning of
unify_with_occurs_check()

That you need to lie about other people indicates that you are >>>>>>>> not sure
whether what you say is true but you want anyway that others
believe it.

Of course I do understand the meaning of
unify_with_occurs_check/2. It

That is not what I said. I said the deep meaning

There is no deep meaning that is not a part of the meaning.

That the directly graph of the evaluation sequence
of a formal expression contains a cycle

LP := ~True(LP)
that expands to ~True(~True(~True(~True(~True(~True(...))))))
means that it is semantically unsound.

Irrelevant to the fact that there is no deep meaning that is not a part >>>> of the meaning.

Also irrelevant the meaning and deep meaning of the library predicate
unify_with_occurs_check/2.

unify_with_occurs_check() does not mean only the
Prolog doesn't like it. It means that Prolog has
proved that it is semantically unsound.

That unify_with_occurs_check(X, Y) succeeds means that X and Y can be
unified and that such unification does not create any loop that is not
already in X or Y. Whether Prolog likes it or not is irrelevant, and
so is whether the resulting structure is semantically sound.

% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.

LP is not semantically sound thus the Liar Paradox
has finally been unequivocally proven to not be a
proposition.

Irrelevant to the Prolog semantics discussed above. That your Prolog implenmentation accepts LP = not(true(LP)) as a correct Prolog query
and knows what to do with it is all that matters.
--
Mikko
--- Synchronet 3.21a-Linux NewsLink 1.2