From Newsgroup: comp.ai.philosophy

On 1/12/26 9:05 AM, olcott wrote:

On 1/12/2026 5:56 AM, Richard Damon wrote:

On 1/11/26 11:33 PM, olcott wrote:

On 1/11/2026 10:00 PM, Richard Damon wrote:

On 1/11/26 10:42 PM, olcott wrote:

On 1/11/2026 9:37 PM, Richard Damon wrote:

On 1/11/26 5:52 PM, olcott wrote:

On 1/11/2026 11:52 AM, Richard Damon wrote:

On 1/11/26 9:25 AM, olcott wrote:

On 1/11/2026 4:26 AM, Mikko wrote:

On 10/01/2026 18:11, olcott wrote:

On 1/10/2026 3:02 AM, Mikko wrote:

On 09/01/2026 17:53, olcott wrote:

On 1/9/2026 4:03 AM, Mikko wrote:

On 09/01/2026 01:28, olcott wrote:

Non-programmers and non-Prolog programmers only
understand Occurs‑check failure as “Prolog doesn’t like it”.

I don't know about non-programmers but everyone who knows >>>>>>>>>>>>>> enough about
programming to be able to read the definition of the >>>>>>>>>>>>>> predicate
unify_with_occurs_check/2 can understand that its failure >>>>>>>>>>>>>> means that
the programmer does not like a cyclic structure at that >>>>>>>>>>>>>> point.

That is so stupidly wrong that it must be dishonest.

Prolog is what the standard says it is. You don't show any >>>>>>>>>>>> contradiction
with the Prolog standard but dishonesstly say "dishonest" >>>>>>>>>>>> anyway.

I could not get a copy of the standard to prove
that I am correct its costs $600.

Here is the Clocksin & Mellish page
https://www.liarparadox.org/Clocksin&Mellish.pdf

“In proof-theoretic semantics, as reflected in
the well-founded semantics of logic programming,
the Liar is rejected as a non-well-founded goal.”

That is about the proof-theoretic semantics, not about Prolog >>>>>>>>>> semantics.
Only Prolog semantics is defined in the standard.

“Prolog is an operational implementation of proof-theoretic >>>>>>>>> semantics: truth is derivability, and only well-founded proofs >>>>>>>>> count.”

“In proof-theoretic semantics, as reflected in the well-founded >>>>>>>>> semantics of logic programming, the Liar is rejected as a non- >>>>>>>>> well- founded goal.”

In proof-theoretic semantics, the Liar Paradox is not a genuine >>>>>>>>> contradiction but a non-well-founded construct, and thus not >>>>>>>>> truth- apt.

Proof Theoretic Semantics is not the same as Truth Conditional >>>>>>>>> Semantics.

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

This is similar to semantically ungrounded (Kripke 1975) at the >>>>>>>>> Tarski object language level thus cannot be resolved to a truth >>>>>>>>> value. Outline of a Theory of Truth --- Saul Kripke

And the problem is that your "Proof Theoretic Semantics" isn't >>>>>>>> the logic domain of the problems you want to talk about.

It turns out that [Proof Theoretic Semantics] anchored in

   A theory (over {E}) is defined as a conceptual class of
   these elementary statements. Let {T} be such a theory.
   Then the elementary statements which belong to {T} we
   shall call the elementary theorems of {T}; we also say
   that these elementary statements are true for {T}. Thus,
   given {T}, an elementary theorem is an elementary
   statement which is true. A theory is thus a way of
   picking out from the statements of {E} a certain
   subclass of true statements…
Curry, Haskell 1977. Foundations of Mathematical
Logic. New York: Dover Publications, 45

Is the foundation of the system that I have been
talking about all of these years making
∀x ∈ T ((True(T, x) ≡ (T ⊢ x))
and Gödel Incompleteness impossible.

Nope. Read the last line, it say it allows picking out a certain
SUBCLASS of true statemensts, not that it picks out ALL true
statements.

Proof SHOWS the statement to be true.

“The system adopts Proof-Theoretic Semantics: meaning is determined >>>>> by inferential role, and truth is internal to the theory. A theory
T is defined by a finite set of stipulated atomic statements
together with all expressions derivable from them under the
inference rules. The statements belonging to T constitute its
theorems, and these are exactly the statements that are true-in-T.” >>>>> ∀x ∈ T ((True(T, x) ≡ (T ⊢ x))

I think the issue is that this "Proof-Theoretic Semantics" can't
actually handle systems like Peano Arithmatic.

It turns out that they can and much much more. So what
I have been saying all these years is about Gödel is
essentially "Proof-Theoretic Semantics".

Considering your history, you got anything that supports that claim?

Why PA is fully expressible in this system
Peano Arithmetic (PA) fits perfectly into this framework because:
PA is a recursively axiomatized theory with a finite set of primitive symbols.

Its axioms and inference rules are finitary and syntactic, exactly the
kind of rules this system treats as meaning-giving.

Every PA proof is a finite, well-founded derivation, so PA’s theorems
are automatically “true-in-PA” in this sense.

PA’s refutations (proofs of negations) are likewise finite, so PA’s falsehoods are “false-in-PA”.

PA’s independent sentences (Gödel, Rosser, Paris–Harrington, etc.) naturally fall into the non-well-founded category, since their
inferential roles cannot be grounded within PA’s proof system.

No they don't. Where did Godel, etc break the inferential rules of PA?

(Not where does a side comment not follow the rules, where in the ACTUAL PROOF, does Godel break the inference rules.)

Your inability to understand the logic doesn't make it invalid, it just
shows that you are limited in your understanding.

One issue with your claim, is that if Godel is breaking the rules, then
the relationship between proofs and programs is also invalid, and thus
you whole idea of "computing truth" has to be thrown out.

Nothing in PA requires model-theoretic truth, infinite structures, or semantic notions beyond what this system provides. PA’s entire content — its syntax, its proofs, its derivations, and its independence phenomena
— is fully captured by these three proof-theoretic statuses.

Sure it does. It is a FACT that either a number exists or doesn't exist
that satisfies some criteria. There can not be something in between. The determination of this, might require looking at the whole model of the
number system.

An example would be does an even number, greater than 2, exist that
isn't the sum of two primes. Perfectly valid quiestion in PA. We haven't
been able to prove that it exists or that it doesn't, and thus the truth
may only be determined by looking at the full infinite model.

Your stupidity in not seeing this, doesn't make it not true.

In short: PA is fully expressible because everything PA does is already proof-theoretic, and this system’s semantics is defined entirely in proof-theoretic terms.

But, there are truths in PA that are not provable, so your claim just
shows you don't actually know what you are talking about.

In that case, it doesn't refute Godel's incompleteness Theorem, as
that had as its precondition that ability to support the defintions
of the Natural Numbers.

So, your problem is that, since you don't actually understand what
any of these fields are actually doing, you don't know which ones
are actualy applicable to the problem you want to deal with.

Since "Computation Theory" has at its foundation things that need to
have the properties of the Natural Numbers available, your systems
that can't handle them are just not applicable.

--- Synchronet 3.21a-Linux NewsLink 1.2