XPost: comp.theory, comp.lang.prolog

On 5/3/2022 11:52 AM, André G. Isaak wrote:

On 2022-05-03 10:08, olcott wrote:

On 5/3/2022 10:18 AM, André G. Isaak wrote:

On 2022-05-02 18:57, olcott wrote:

On 5/2/2022 6:43 PM, Ben wrote:

Aleksy Grabowski <hurufu@gmail.com> writes:

IF you are defining that your logic system is limited to what
Prolog can "Prove", that is fine. Just realize that you have just >>>>>>> defined that your
logic system can't handle a lot of the real problems in the
world, and in particular, it is very limited in the mathematics
it can handle.
I am pretty sure that Prolog is NOT up to handling the logic
needed to
handle the mathematics needed to express Godel's G, or the
Halting Problem.
Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you >>>>>>> have only proven that your limited logic system can't reach them >>>>>>> in expressibility.

Thanks for confirmation, that's what exactly what I was trying to
tell
to topic poster in one of my previous posts. Prolog in it's bare form >>>>>> is a bad theorem solver. It wasn't designed a such.

If you want to deal with such problems maybe it is better to use Coq >>>>>> theorem prover, I've never used it by myself, but it looks like
one of
the best proving assistants out there.

And indeed there is a fully formalised proof of GIT in Coq (though I >>>>> think it's the slightly tighter Gödel-Rosser version).

It is true that G is not provable. G is not provable because it is
semantically incorrect in the exactly same way that the Liar Paradox
is semantically incorrect.

Gödel says:
14 Every epistemological antinomy can likewise be used for a similar
undecidability proof

André denied this six times yesterday
The Liar Paradox is an epistemological antinomy, thus can likewise
be used for a similar undecidability proof.

No. The Liar can be used to construct an *identical* proof.

Really?

Of course really.

His original proof drew on The Liar for inspiration. So a proof which
draws on The Liar would be the same proof.

OK, then I am very happy to say that my accusation that you lied was not justified, we were simply talking past each other.

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)