Re: April Fools Day Challenge (Liar Paradox specifies an unsatisfiable cyclic structure)

[olcott]

On 4/1/2021 12:39 PM, olcott wrote:
> On 3/31/2021 6:15 PM, Mostowski Collapse wrote:
>>
>>
>> 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
>>
>
> 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
>

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

--
Copyright 2021 Pete Olcott

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