April Fools Day Challenge

[Mostowski Collapse]

Currently fiddling around with truth tellers and liars.
Take this sentence which we label S:

S : This sentence is false.

A truth teller can be translate into this:

S <=> ~S

A liar can be translate into this:

S <=/=> ~S

Both formulation can be checked for satisfiablity via
CLP(B) as found in SWI-Prolog or Jekejeke Prolog:

?- use_module(library(clpb)).

?- sat(S=:= ~S).
false.

?- sat(S=\= ~S), labeling([S]).
S = 0 ;
S = 1.

Can we use Prolog CLP(B) similarly to solve the below riddle.

Two doors with two guards - one lies, one tells the truth
https://puzzling.stackexchange.com/q/2188/66207

[olcott]

Occurs check: Application in theorem proving
In theorem proving, unification without the occurs check can lead to
unsound inference. For example, the Prolog goal X = ƒ(X) will succeed,
binding X to a cyclic structure which has no counterpart in the Herbrand
universe. https://en.wikipedia.org/wiki/Occurs_check

∴ LP = ¬True(LP)
and (its negation)
TT = True(TT) are both unsatisfiable

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

[olcott]

On 4/1/2021 12:58 PM, Richard Damon wrote:

> Be sure to remember this when you presume that Halts will answer all
> halting questions correctly.
>

In this case regular ordinary Prolog code correctly decides that both
the Liar Paradox and its negation are unsatisfiable.

I did not notice that Prolog does this until long after I created
Minimal Type Theory that provides the syntax for specifying cyclical
expressions and translates input expressions into directed graphs.

https://www.researchgate.net/publication/315367846_Minimal_Type_Theory_MTT

[olcott]

Here it is in actual Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP,not(true(LP))).
false.

[Chris M. Thomasson]

Olcott is a moron.

Is this sentence true, false, or a mixture of both?

[olcott]

Even a bot could have provided a better critique.
Any jackass can be a mindless naysayer.

Here it is in actual Prolog:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP,not(true(LP))).
false.

[Peter]

That paper has a section titled 'Formalizing (the semantics of) Gödel’s
(1931) incompleteness theorem using MTT' but nowhere do you mention
Gödel’s (1931) incompleteness theorem.
>


--
Just as 'beautiful' points the way for aesthetics and 'good' for ethics,
so do words like 'true' for logic. All sciences have truth as their
goal; but logic is also concerned with it in a quite different way:
logic has much the same relation to truth as physics has to weight or
heat. Frege in 'Thoughts' (Der Gedanke)

[R Kym Horsell]

In comp.lang.prolog olcott <No...@nowhere.com> wrote:
> Even a bot could have provided a better critique.
> Any jackass can be a mindless naysayer.

Invalid self reference.

--
[Complainer's syndrome:]
What, exactly, are you complaining about. [...] So, what's the complaint?
-- John Stafford <nh...@droffats.net>, 09 Dec 2010 16:30:53 -0600

[olcott]

Actual Prolog representing the Liar Paradox:

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

Thus proving that the Prolog Liar Paradox has an
“uninstantiated subterm of itself”
we can know that unification will fail because it specifies
“some kind of infinite structure.”

The quotes come from: (Clocksin and Mellish 2003:255)
Clocksin, W.F. and Mellish, C.S. 2003. Programming in Prolog Using the
ISO Standard Fifth Edition, 254. Berlin Heidelberg: Springer-Verlag.



Prolog detects pathological self reference in the Gödel sentence
April 2021 PL Olcott

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