Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics" https://plato.stanford.edu/entries/proof-theoretic-semantics/ #InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL. Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but
whether it is for any purpose more useful than alternatives.
For example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is already in the usual metalanguage semantics.
Which expression becomes shorter or simpler if Has_Meaning_PTS is
used instead of Provable ?
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
For example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is
already in the usual metalanguage semantics.
KnownTrue := Γ ⊂ PA(Γ ⊣ φ)
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it.
For example, if a sentence is known to be undecidable then it can be
added to the postulates. Conversely, if a sentence is known to be
decidable it should not be added to the postulates as the set of the postulates would become either inconsistent or redundant.
For example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is
There should be an existential quantifier above expression that should
be a copy of the expression defining Probable.
already in the usual metalanguage semantics.
KnownTrue := Γ ⊂ PA(Γ ⊣ φ)
It is a syntax error to use open variables φ in a definition.Besides KnownTrue is a bad name for a symbol that does not refer to knowledge.
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it.
For example, if a sentence is known to be undecidable then it can be
Such as "What time is it (yes or no)?"
Now the right side is as in the definition of Provable but the variableadded to the postulates. Conversely, if a sentence is known to be
decidable it should not be added to the postulates as the set of the
postulates would become either inconsistent or redundant.
There should be an existential quantifier above expression that shouldFor example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is >>
be a copy of the expression defining Probable.
already in the usual metalanguage semantics.
KnownTrue := Γ ⊂ PA(Γ ⊣ φ)
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
On 22/04/2026 10:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ >>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but >>>>> whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it.
For example, if a sentence is known to be undecidable then it can be
Such as "What time is it (yes or no)?"
A question is neither true nor false and there is no way to prove
a question. But usually "undecidability" refers to affirmative
sentences only, as they only are in the scope of logic.
Now the right side is as in the definition of Provable but the variableadded to the postulates. Conversely, if a sentence is known to be
decidable it should not be added to the postulates as the set of the
postulates would become either inconsistent or redundant.
For example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is
There should be an existential quantifier above expression that should
be a copy of the expression defining Probable.
already in the usual metalanguage semantics.
KnownTrue := Γ ⊂ PA(Γ ⊣ φ)
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
φ is still free on the right side making KnownTrue ill-defined.
There still is no connection to knowledge so KnownTrue is a bad name.
Note that the Common Language phrase "known true" is not a noun phrase
and therefore does not denote any being.
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-chained inference steps from that proposition to the axioms of Peano Arithmetic.
I'm not saying I agree with the above, but at least it is more clear
than your attempts at formalism.
André
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-chained inference steps from that proposition to the axioms of Peano Arithmetic.
I'm not saying I agree with the above, but at least it is more clear
than your attempts at formalism.
André
On 04/22/2026 04:06 PM, André G. Isaak wrote:
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge. >>>>
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the
formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-chained
inference steps from that proposition to the axioms of Peano Arithmetic.
I'm not saying I agree with the above, but at least it is more clear
than your attempts at formalism.
André
Perhaps something like the band "Faith No More" the song "Empire".
On 4/22/2026 3:19 AM, Mikko wrote:
On 22/04/2026 10:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ >>>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL. >>>>>>> Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but >>>>>> whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it.
For example, if a sentence is known to be undecidable then it can be
Such as "What time is it (yes or no)?"
A question is neither true nor false and there is no way to prove
a question. But usually "undecidability" refers to affirmative
sentences only, as they only are in the scope of logic.
This sentence is not true. // It is semantically incoherent
On 22/04/2026 16:17, olcott wrote:
On 4/22/2026 3:19 AM, Mikko wrote:
On 22/04/2026 10:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>> #InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ >>>>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL. >>>>>>>> Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is >>>>>>> but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it. >>>>> For example, if a sentence is known to be undecidable then it can be
Such as "What time is it (yes or no)?"
A question is neither true nor false and there is no way to prove
a question. But usually "undecidability" refers to affirmative
sentences only, as they only are in the scope of logic.
This sentence is not true. // It is semantically incoherent
Can you think any reason why typical formal languages have no symbol analogous to "this" in that sentence ?
On 4/22/2026 6:06 PM, André G. Isaak wrote:
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge. >>>>
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the
formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of
back-chained inference steps from that proposition to the axioms of
Peano Arithmetic.
That certainly is more clear.
On 4/23/2026 2:06 AM, Mikko wrote:
On 22/04/2026 16:17, olcott wrote:
On 4/22/2026 3:19 AM, Mikko wrote:
On 22/04/2026 10:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:Such as "What time is it (yes or no)?"
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs. >>>>>>>>> ...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>>> #InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ >>>>>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL. >>>>>>>>> Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics >>>>>>>> is but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it. >>>>>> For example, if a sentence is known to be undecidable then it can be >>>>>
A question is neither true nor false and there is no way to prove
a question. But usually "undecidability" refers to affirmative
sentences only, as they only are in the scope of logic.
This sentence is not true. // It is semantically incoherent
Can you think any reason why typical formal languages have no symbol
analogous to "this" in that sentence ?
To keep reasoning about these things
so convoluted that they can never be
resolved?
I invented one that does
LP := ~True(LP)
On 2026-04-22 19:21, olcott wrote:
On 4/22/2026 6:06 PM, André G. Isaak wrote:
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides >>>>> KnownTrue is a bad name for a symbol that does not refer to knowledge. >>>>>
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the
formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-
chained inference steps from that proposition to the axioms of Peano
Arithmetic.
That certainly is more clear.
The point I want to make is that clarity and formalism are two different things. You do not excel at formalism. But that doesn't mean that you
cannot be clear. Just worry about the English for the time being and
worry about the formalism later.
On 4/23/2026 11:19 PM, André G. Isaak wrote:
On 2026-04-22 19:21, olcott wrote:
On 4/22/2026 6:06 PM, André G. Isaak wrote:
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides >>>>>> KnownTrue is a bad name for a symbol that does not refer to
knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the
formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-
chained inference steps from that proposition to the axioms of Peano
Arithmetic.
That certainly is more clear.
The point I want to make is that clarity and formalism are two
different things. You do not excel at formalism. But that doesn't mean
that you cannot be clear. Just worry about the English for the time
being and worry about the formalism later.
Can he take your good advise? Humm...
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics" https://plato.stanford.edu/entries/proof-theoretic-semantics/ #InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL. Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
On 2026-04-20, olcott <polcott333@gmail.com> wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
Twenty years ago (under my sixth-grade-adopted nickname "Mike"),
I posted in sci.math that Gödel's G was meaningless due to the
infinite regression toward infinity on the basis of which its
meaning was supposedly obtained.
The correct interpretation was, I argued, not "This sentence is
unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
As regards semantics, I could call statement (1) the "unencoded
sentence," sentence (2) the "first encoded sentence," the concept
under which all sentences (1)-(∞) belong the "formally abstracted sentence," and the concept under which all sentences (2)-(∞)
belong the "encoding-abstracted sentence."
Then, I could argue that:
1. The /unencoded sentence/ is /true and meaningful/. It's a
statement about numbers.
2. The /formally abstracted/ and /encoding-abstracted/ sentences
are both /meaningless/.
Does this seem in agreement with your view? If so, how would you
describe my concepts in your own terms?
--Scott Hoge
On 4/26/2026 3:01 PM, Scott Hoge wrote:
On 2026-04-20, olcott <polcott333@gmail.com> wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
Twenty years ago (under my sixth-grade-adopted nickname "Mike"),
I posted in sci.math that Gödel's G was meaningless due to the
infinite regression toward infinity on the basis of which its
meaning was supposedly obtained.
The correct interpretation was, I argued, not "This sentence is
unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
As regards semantics, I could call statement (1) the "unencoded
sentence," sentence (2) the "first encoded sentence," the concept
under which all sentences (1)-(∞) belong the "formally abstracted
sentence," and the concept under which all sentences (2)-(∞)
belong the "encoding-abstracted sentence."
Then, I could argue that:
1. The /unencoded sentence/ is /true and meaningful/. It's a
statement about numbers.
2. The /formally abstracted/ and /encoding-abstracted/ sentences
are both /meaningless/.
Does this seem in agreement with your view? If so, how would you
describe my concepts in your own terms?
--Scott Hoge
F ⊢ GF ↔ ¬ProvF(⌜GF⌝) https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Olcott's Minimal Type Theory
G ↔ ¬Prov_PA(⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov_PA 04
04 Gödel_Number_of 01 // cycle
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first incompleteness theorem sentence
has a cycle in the directed graph of its
evaluation sequence making it semantically
incoherent.
This kind of semantically incoherence is
foundational in proof theoretic semantics.
On 4/26/2026 3:01 PM, Scott Hoge wrote:
On 2026-04-20, olcott <polcott333@gmail.com> wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
Twenty years ago (under my sixth-grade-adopted nickname "Mike"),
I posted in sci.math that Gödel's G was meaningless due to the
infinite regression toward infinity on the basis of which its
meaning was supposedly obtained.
The correct interpretation was, I argued, not "This sentence is
unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
As regards semantics, I could call statement (1) the "unencoded
sentence," sentence (2) the "first encoded sentence," the concept
under which all sentences (1)-(∞) belong the "formally abstracted
sentence," and the concept under which all sentences (2)-(∞)
belong the "encoding-abstracted sentence."
Then, I could argue that:
1. The /unencoded sentence/ is /true and meaningful/. It's a
statement about numbers.
2. The /formally abstracted/ and /encoding-abstracted/ sentences
are both /meaningless/.
Does this seem in agreement with your view? If so, how would you
describe my concepts in your own terms?
--Scott Hoge
F ⊢ GF ↔ ¬ProvF(⌜GF⌝) https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Olcott's Minimal Type Theory
G ↔ ¬Prov_PA(⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov_PA 04
04 Gödel_Number_of 01 // cycle
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first incompleteness theorem sentence
has a cycle in the directed graph of its
evaluation sequence making it semantically
incoherent.
This kind of semantically incoherence is
foundational in proof theoretic semantics.
On 26/04/2026 23:54, olcott wrote:
On 4/26/2026 3:01 PM, Scott Hoge wrote:
On 2026-04-20, olcott <polcott333@gmail.com> wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
Twenty years ago (under my sixth-grade-adopted nickname "Mike"),
I posted in sci.math that Gödel's G was meaningless due to the
infinite regression toward infinity on the basis of which its
meaning was supposedly obtained.
The correct interpretation was, I argued, not "This sentence is
unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
As regards semantics, I could call statement (1) the "unencoded
sentence," sentence (2) the "first encoded sentence," the concept
under which all sentences (1)-(∞) belong the "formally abstracted
sentence," and the concept under which all sentences (2)-(∞)
belong the "encoding-abstracted sentence."
Then, I could argue that:
1. The /unencoded sentence/ is /true and meaningful/. It's a
statement about numbers.
2. The /formally abstracted/ and /encoding-abstracted/ sentences
are both /meaningless/.
Does this seem in agreement with your view? If so, how would you
describe my concepts in your own terms?
--Scott Hoge
F ⊢ GF ↔ ¬ProvF(⌜GF⌝)
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Olcott's Minimal Type Theory
G ↔ ¬Prov_PA(⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov_PA 04
04 Gödel_Number_of 01 // cycle
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first incompleteness theorem sentence
has a cycle in the directed graph of its
evaluation sequence making it semantically
incoherent.
This kind of semantically incoherence is
foundational in proof theoretic semantics.
Olcott's usual reaction is to say something unrelated to any asked
question instead of answering. Perhaps he hopes to hide his ignorance
and incompetens. But it does not work.
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G
has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will
never get this. If you always knew what directed graphs
of evaluation sequences that contain cycles are then
you rebuttal has always been pure dishonesty.
As regards semantics, I could call statement (1) the
"unencoded sentence," sentence (2) the "first encoded
sentence," the concept under which all sentences (1)-(∞)
belong the "formally abstracted sentence," and the concept
under which all sentences (2)-(∞) belong the
"encoding-abstracted sentence."
On 2026-04-27, olcott <polcott333@gmail.com> wrote:
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G
has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will
never get this. If you always knew what directed graphs
of evaluation sequences that contain cycles are then
you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
Yours appears to look like this, where its semantic (?)
evaluation contains a cycle:
(D2)
· ─┐
↑ ↓
└─ ·
(This may be an oversimplification of the actual cycle, but it's
for illustrative purposes.)
I'll requote my proposed division of concepts:
As regards semantics, I could call statement (1) the
"unencoded sentence," sentence (2) the "first encoded
sentence," the concept under which all sentences (1)-(∞)
belong the "formally abstracted sentence," and the concept
under which all sentences (2)-(∞) belong the
"encoding-abstracted sentence."
If we're speaking of the /infinite sequence of nth-encoded
sentences/, the graph would be D1. However, we may still be able
to argue that for the /formally abstracted/ sentence, the graph
would be D2.
The formally abstracted sentence is closer in concept to "This
sentence is unprovable."
Does this view sound tenable?
-- Scott Hoge
On 2026-04-27, olcott <polcott333@gmail.com> wrote:I strongly urge you to read and understand an actual proof of Gödel's incompleteness theorem[*]. There are no looping or endless directed
[...]
I learned what directed graphs were in high school.The directed graph of the evaluation sequence of GOn 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will
never get this. If you always knew what directed graphs
of evaluation sequences that contain cycles are then
you rebuttal has always been pure dishonesty.
It seems our views are somewhat in agreement, but my directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
-- Scott Hoge--
In sci.math Scott Hoge <nospam@nospam.com> wrote:
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of
Gödel's incompleteness theorem[*]. There are no looping or
endless directed graphs in these. Such notions result from
misunderstandings by those lacking formal training in
mathematics.
On 2026-04-27, Alan Mackenzie <acm@muc.de> wrote:
In sci.math Scott Hoge <nospam@nospam.com> wrote:
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of
Gödel's incompleteness theorem[*]. There are no looping or
endless directed graphs in these. Such notions result from
misunderstandings by those lacking formal training in
mathematics.
I own a copy of Gödel's /On Formally Undecidable Propositions of
Principia Mathematica and Related Systems/ and have read the
original proof.
You're correct that the proof does not refer to directed graphs.
What I want to argue, rather, is that such graphs can be used to
/visualize the meaning/ of the Gödel sentence. That meaning
exists for the first unencoded sentence, which (as Gödel showed)
is true. But for what I'm calling the "formally abstracted
sentence" -- that is, the concept of being any sentence
represented by some node in the graph -- perhaps there is no such
meaning.
-- Scott Hoge
On 4/27/2026 5:01 PM, Scott Hoge wrote:
On 2026-04-27, Alan Mackenzie <acm@muc.de> wrote:
In sci.math Scott Hoge <nospam@nospam.com> wrote:
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of
Gödel's incompleteness theorem[*]. There are no looping or
endless directed graphs in these. Such notions result from
misunderstandings by those lacking formal training in
mathematics.
I own a copy of Gödel's /On Formally Undecidable Propositions of
Principia Mathematica and Related Systems/ and have read the
original proof.
You're correct that the proof does not refer to directed graphs.
What I want to argue, rather, is that such graphs can be used to
/visualize the meaning/ of the Gödel sentence. That meaning
exists for the first unencoded sentence, which (as Gödel showed)
is true. But for what I'm calling the "formally abstracted
sentence" -- that is, the concept of being any sentence
represented by some node in the graph -- perhaps there is no such
meaning.
Olcott's Minimal Type Theory
G ↔ ¬Prov_PA(⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov_PA 04
04 Gödel_Number_of 01 // cycle
On 2026-04-27, Alan Mackenzie <acm@muc.de> wrote:Excellent!
In sci.math Scott Hoge <nospam@nospam.com> wrote:I own a copy of Gödel's /On Formally Undecidable Propositions of
I learned what directed graphs were in high school.I strongly urge you to read and understand an actual proof of
It seems our views are somewhat in agreement, but my directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
Gödel's incompleteness theorem[*]. There are no looping or
endless directed graphs in these. Such notions result from misunderstandings by those lacking formal training in
mathematics.
Principia Mathematica and Related Systems/ and have read the
original proof.
You're correct that the proof does not refer to directed graphs.In the graph you drew, (still in the quoted text above), each node is
What I want to argue, rather, is that such graphs can be used to
/visualize the meaning/ of the Gödel sentence. That meaning
exists for the first unencoded sentence, which (as Gödel showed)
is true. But for what I'm calling the "formally abstracted
sentence" -- that is, the concept of being any sentence
represented by some node in the graph -- perhaps there is no such
meaning.
-- Scott Hoge--
[ Followup-To: set ]
In comp.theory olcott <polcott333@gmail.com> wrote:
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
In sci.math Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, olcott <polcott333@gmail.com> wrote:
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G
has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will
never get this. If you always knew what directed graphs
of evaluation sequences that contain cycles are then
you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of Gödel's
incompleteness theorem[*]. There are no looping or endless directed
graphs in these. Such notions result from misunderstandings by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, Escher, Bach, >>> an Eternal Golden Braid" by Douglas Hofstadter, published around 1978 or >>> 1979. A proof of the incompleteness theorem is a central theme of the
book, which is witty and entertaining and well worth reading.
Peter Olcott has never read and understood such a proof. Although not
particularly difficult, it is beyond his understanding.
After all these years where I have repeatedly proven ....
You have spent years demonstrating you don't understand the concept of a mathematical proof. You haven't proven anything.
.... that Gödel himself says that his proof does have pathological self
reference you repeatedly deny this because you and everyone else here
only cares about denigration rather than truth.
I care deeply about the truth. Gödel's theorem is part of the truth.
Prolog detects [and rejects] pathological self reference in the Gödel
sentence
This suggests Prolog is not up to the job. Or more likely, the
programmer of that piece of Prolog isn't up to the job.
BEGIN:(Gödel 1931:39-41)...there is also a close
...We are therefore confronted with a proposition which asserts its own
unprovability. 15
[ Spam snipped ]
Yes. You have not read and understood this proof. You have merely
extracted and misunderstood an off the cuff motivational remark from it.
And please note, this theorem is _TRUE_. It has been proven rigorously
and verified by millions of students and academics over a very long time >>> period.
Yet never once examined within the alternative foundation of
proof theoretic semantics utterly replacing foundation of model
theoretic semantics.
Whatever proof theoretic semantics is. It would appear it is
insufficiently powerful to do maths with -
that it is insufficiently
powerful to express anything it cannot prove.
But what do I know? I've
only got your probably garbled accounts of it to go on.
Peter Olcott doesn't like it any more than he doesn't understand it, so
he pours scorn on the distinguished mathematicians of the past, falsely
claiming it to be false. I would urge you to be sceptical of _any_ so
called "result" emanating from him.
[ .... ]
-- Scott Hoge
--
Copyright 2026 Olcott
On 4/28/2026 5:22 AM, Alan Mackenzie wrote:[ .... ]
In comp.theory olcott <polcott333@gmail.com> wrote:
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
Please stop lying about what I wrote.So you are trying to get away with saying ....You have spent years demonstrating you don't understand the concept of a mathematical proof. You haven't proven anything.Peter Olcott has never read and understood such a proof. Although not >>> particularly difficult, it is beyond his understanding.After all these years where I have repeatedly proven ....
.... that Gödel himself says that his proof does have pathological self >> reference you repeatedly deny this because you and everyone else hereI care deeply about the truth. Gödel's theorem is part of the truth.
only cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in the GödelThis suggests Prolog is not up to the job. Or more likely, the
sentence
programmer of that piece of Prolog isn't up to the job.
BEGIN:(Gödel 1931:39-41)...there is also a close[ Spam snipped ]
...We are therefore confronted with a proposition which asserts its own
unprovability. 15
Yes. You have not read and understood this proof. You have merely extracted and misunderstood an off the cuff motivational remark from it.
that Gödel did not say: ...We are therefore confronted with aYes, Gödel wrote that.
proposition which asserts its own unprovability. 15
I don't see how that is not dishonest.What is dishonest (or more likely ignorant) is your trying to construe
The theorem is true.Within the wrong kind of semantics.And please note, this theorem is _TRUE_. It has been proven
rigorously and verified by millions of students and academics over
a very long time period.
I am an educated person. You are the wilfully ignorant outsider tryingYou are a mere sheep that follows the herd.Yet never once examined within the alternative foundation ofWhatever proof theoretic semantics is. It would appear it is insufficiently powerful to do maths with - that it is insufficiently powerful to express anything it cannot prove.
proof theoretic semantics utterly replacing foundation of model
theoretic semantics.
It is not about math, it is about meaning. unprovable essentiallyYou are objectively wrong. Unprovable and untrue are two different
means untrue. Going outside of PA in a separate model of PA has always
been cheating.
You are mistaking your own ignorance of proof theoreticI have no interest in "proof theoretic semantics". It has no relevance, whatever it might be. You are, as you admit, ignorant about Gödel's
semantics for my ignorance of Gödel.
----
Copyright 2026 Olcott
[ Followup-To: set ]
In comp.theory olcott <polcott333@gmail.com> wrote:
On 4/28/2026 5:22 AM, Alan Mackenzie wrote:
In comp.theory olcott <polcott333@gmail.com> wrote:
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ .... ]
Peter Olcott has never read and understood such a proof. Although not >>>>> particularly difficult, it is beyond his understanding.
After all these years where I have repeatedly proven ....
You have spent years demonstrating you don't understand the concept of a >>> mathematical proof. You haven't proven anything.
.... that Gödel himself says that his proof does have pathological self >>>> reference you repeatedly deny this because you and everyone else here
only cares about denigration rather than truth.
I care deeply about the truth. Gödel's theorem is part of the truth.
Prolog detects [and rejects] pathological self reference in the Gödel >>>> sentence
This suggests Prolog is not up to the job. Or more likely, the
programmer of that piece of Prolog isn't up to the job.
BEGIN:(Gödel 1931:39-41)...there is also a close
...We are therefore confronted with a proposition which asserts its own >>>> unprovability. 15
[ Spam snipped ]
Yes. You have not read and understood this proof. You have merely
extracted and misunderstood an off the cuff motivational remark from it.
So you are trying to get away with saying ....
Please stop lying about what I wrote.
that Gödel did not say: ...We are therefore confronted with a
proposition which asserts its own unprovability. 15
Yes, Gödel wrote that.
I don't see how that is not dishonest.
What is dishonest (or more likely ignorant) is your trying to construe
that sentence as being the same as the liar paradox. It's not the same,
as you have been told countless times.
[ .... ]
And please note, this theorem is _TRUE_. It has been proven
rigorously and verified by millions of students and academics over
a very long time period.
Within the wrong kind of semantics.
The theorem is true.
Yet never once examined within the alternative foundation of
proof theoretic semantics utterly replacing foundation of model
theoretic semantics.
Whatever proof theoretic semantics is. It would appear it is
insufficiently powerful to do maths with - that it is insufficiently
powerful to express anything it cannot prove.
You are a mere sheep that follows the herd.
I am an educated person. You are the wilfully ignorant outsider trying
to spread falsehood.
It is not about math, it is about meaning. unprovable essentially
means untrue. Going outside of PA in a separate model of PA has always
been cheating.
You are objectively wrong. Unprovable and untrue are two different
things, again, as has been pointed out to you countless times.
You are mistaking your own ignorance of proof theoretic
semantics for my ignorance of Gödel.
I have no interest in "proof theoretic semantics". It has no relevance, whatever it might be. You are, as you admit, ignorant about Gödel's theorem.
[ .... ]
--
Copyright 2026 Olcott
On 28/04/2026 01:22, olcott wrote:
On 4/27/2026 5:01 PM, Scott Hoge wrote:
On 2026-04-27, Alan Mackenzie <acm@muc.de> wrote:
In sci.math Scott Hoge <nospam@nospam.com> wrote:
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of
Gödel's incompleteness theorem[*]. There are no looping or
endless directed graphs in these. Such notions result from
misunderstandings by those lacking formal training in
mathematics.
I own a copy of Gödel's /On Formally Undecidable Propositions of
Principia Mathematica and Related Systems/ and have read the
original proof.
You're correct that the proof does not refer to directed graphs.
What I want to argue, rather, is that such graphs can be used to
/visualize the meaning/ of the Gödel sentence. That meaning
exists for the first unencoded sentence, which (as Gödel showed)
is true. But for what I'm calling the "formally abstracted
sentence" -- that is, the concept of being any sentence
represented by some node in the graph -- perhaps there is no such
meaning.
Olcott's Minimal Type Theory
G ↔ ¬Prov_PA(⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov_PA 04
04 Gödel_Number_of 01 // cycle
There is no cycle in any Gödel number. Gödel numbers are natural numbers and there are not any cycles in any natural number.
On 4/28/2026 3:10 AM, Mikko wrote:
On 28/04/2026 01:22, olcott wrote:
On 4/27/2026 5:01 PM, Scott Hoge wrote:
On 2026-04-27, Alan Mackenzie <acm@muc.de> wrote:
In sci.math Scott Hoge <nospam@nospam.com> wrote:
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of
Gödel's incompleteness theorem[*]. There are no looping or
endless directed graphs in these. Such notions result from
misunderstandings by those lacking formal training in
mathematics.
I own a copy of Gödel's /On Formally Undecidable Propositions of
Principia Mathematica and Related Systems/ and have read the
original proof.
You're correct that the proof does not refer to directed graphs.
What I want to argue, rather, is that such graphs can be used to
/visualize the meaning/ of the Gödel sentence. That meaning
exists for the first unencoded sentence, which (as Gödel showed)
is true. But for what I'm calling the "formally abstracted
sentence" -- that is, the concept of being any sentence
represented by some node in the graph -- perhaps there is no such
meaning.
Olcott's Minimal Type Theory
G ↔ ¬Prov_PA(⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov_PA 04
04 Gödel_Number_of 01 // cycle
There is no cycle in any Gödel number. Gödel numbers are natural numbers >> and there are not any cycles in any natural number.
There is a cycle in the directed graph of the evaluation
sequence of G. Step 4 even allows the complete computation
of G and this does not remove the cycle.
In comp.theory Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, Alan Mackenzie <acm@muc.de> wrote:
In sci.math Scott Hoge <nospam@nospam.com> wrote:
[...]
It seems our views are somewhat in agreement, but my
directed graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
[...]
I own a copy of Gödel's /On Formally Undecidable Propositions
of Principia Mathematica and Related Systems/ and have read
the original proof.
Excellent!
[...]
[Meaning] exists for the first unencoded sentence, which (as
Gödel showed) is true. But for what I'm calling the "formally
abstracted sentence" -- that is, the concept of being any
sentence represented by some node in the graph -- perhaps
there is no such meaning.
In the graph you drew, (still in the quoted text above), each
node is identical to the others. So anything proven about the
first node automatically applies to the rest of the nodes.
[...]
On 5/1/2026 3:24 AM, Mikko wrote:
On 30/04/2026 15:01, olcott wrote:
On 4/30/2026 2:55 AM, Mikko wrote:
On 29/04/2026 17:17, olcott wrote:
On 4/29/2026 1:37 AM, Mikko wrote:
On 28/04/2026 15:18, olcott wrote:
On 4/28/2026 2:34 AM, Mikko wrote:
On 28/04/2026 00:57, olcott wrote:
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ Followup-To: set ]
In sci.math Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, olcott <polcott333@gmail.com> wrote:
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This sentence >>>>>>>>>>>>>>> is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G
has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will
never get this. If you always knew what directed graphs >>>>>>>>>>>> of evaluation sequences that contain cycles are then
you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed >>>>>>>>>>> graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of >>>>>>>>>> Gödel's
incompleteness theorem[*]. There are no looping or endless >>>>>>>>>> directed
graphs in these. Such notions result from misunderstandings >>>>>>>>>> by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, >>>>>>>>>> Escher, Bach,
an Eternal Golden Braid" by Douglas Hofstadter, published
around 1978 or
1979. A proof of the incompleteness theorem is a central
theme of the
book, which is witty and entertaining and well worth reading. >>>>>>>>>>
Peter Olcott has never read and understood such a proof.
Although not
particularly difficult, it is beyond his understanding.
After all these years where I have repeatedly proven that Gödel >>>>>>>>> himself says that his proof does have pathological self reference >>>>>>>>> you repeatedly deny this because you and everyone else here only >>>>>>>>> cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in the >>>>>>>>> Gödel sentence
Prolog alone does not detect pathological self reference.
Counter-factual. unify_with_occurs_check() <is> Prolog.
The predicate unify_with_occurs_check is not the same as Prolog.
It is
just a small part of the standard language. It is one of those
library
predicates that can be used as I said below.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
You can check it every which way and find that it fails
because LP does not have a finite set of inference steps
thus would be rejected by proof theoretic semantics as
semantically ungrounded.
You can check it ever whixh way and find that it says nothing
more than "false".
If you don't give a rat's ass for this truth I am done
talking to you.
We already know you don't care about this truth any more than
other truths.
I just emphasized that because of the lack of truth
life on Earth will not survive and you said this was
off topic.
It is.
Yu >>>>> Though it does not say why unify_with_occurs_check fails. The
result
is the same for unify_with_occurs_check(5, not(true(LP))).
It has certain standard predicates
including unify_with_occurs_check
that makes such detection simpler than in typical programming
languages(like Fortran) but the same detection is possible in >>>>>> >> those, too.
Gödel's sentence is a sentence in the first order Peano arithmetic. >>>>>>>> In that language there is no way to express a reference and in >>>>>>>> particular a self-reference. For the undecidability proof there is >>>>>>>> no need to interprete the theorem at all. In the proof of an Peano- >>>>>>>> unprovable arithmetic truth the usual arithmetic interpretation is >>>>>>>> relevant.
In PTS if directly in PA there are no inference steps
that derive G directly in PA then G is ungrounded in
PA thus essentially meaningless in PA.
Meaning is not relevant.
Not being able to prove meaningless gibberish has
never been any actual limitation. The meaningless
gibberish should have always been rejected as bad input.
Not to be able to give meaning to an arithmetic statement has
never been more than a personal limitation. Every natural number
is a natural number number and Gödel numbers are no exception.
Colorless green ideas sleep furiously was composed by
Noam Chomsky in his 1957 book Syntactic Structures as
an example of a sentence that is grammatically well-formed,
but semantically nonsensical.
And not desiderable when discussing arithmetic.
The most important thing about arithmetic is to get the
correct answer. When a gibberish nonsense expression of
PA is construed as meaningful just because its syntax is
correct this is a woefully stupid mistake. Because you are
a mindless robot utterly bereft of a living soul you will
never get this.
Therefore the formal
languages for logic and arithemtic are desigend so that that kind of
nonsense is not expressible.
On 05/01/2026 07:54 AM, olcott wrote:
On 5/1/2026 3:24 AM, Mikko wrote:
On 30/04/2026 15:01, olcott wrote:
On 4/30/2026 2:55 AM, Mikko wrote:
On 29/04/2026 17:17, olcott wrote:
On 4/29/2026 1:37 AM, Mikko wrote:
On 28/04/2026 15:18, olcott wrote:
On 4/28/2026 2:34 AM, Mikko wrote:
On 28/04/2026 00:57, olcott wrote:
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ Followup-To: set ]
In sci.math Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, olcott <polcott333@gmail.com> wrote:
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This >>>>>>>>>>>>>>>> sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G
has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will >>>>>>>>>>>>> never get this. If you always knew what directed graphs >>>>>>>>>>>>> of evaluation sequences that contain cycles are then >>>>>>>>>>>>> you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed >>>>>>>>>>>> graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of >>>>>>>>>>> Gödel's
incompleteness theorem[*]. There are no looping or endless >>>>>>>>>>> directed
graphs in these. Such notions result from misunderstandings >>>>>>>>>>> by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, >>>>>>>>>>> Escher, Bach,
an Eternal Golden Braid" by Douglas Hofstadter, published >>>>>>>>>>> around 1978 or
1979. A proof of the incompleteness theorem is a central >>>>>>>>>>> theme of the
book, which is witty and entertaining and well worth reading. >>>>>>>>>>>
Peter Olcott has never read and understood such a proof. >>>>>>>>>>> Although not
particularly difficult, it is beyond his understanding.
After all these years where I have repeatedly proven that Gödel >>>>>>>>>> himself says that his proof does have pathological self reference >>>>>>>>>> you repeatedly deny this because you and everyone else here only >>>>>>>>>> cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in the >>>>>>>>>> Gödel sentence
Prolog alone does not detect pathological self reference.
Counter-factual. unify_with_occurs_check() <is> Prolog.
The predicate unify_with_occurs_check is not the same as Prolog. >>>>>>> It is
just a small part of the standard language. It is one of those
library
predicates that can be used as I said below.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
You can check it every which way and find that it fails
because LP does not have a finite set of inference steps
thus would be rejected by proof theoretic semantics as
semantically ungrounded.
You can check it ever whixh way and find that it says nothing
more than "false".
If you don't give a rat's ass for this truth I am done
talking to you.
We already know you don't care about this truth any more than
other truths.
I just emphasized that because of the lack of truth
life on Earth will not survive and you said this was
off topic.
It is.
Yu >>>>> Though it does not say why unify_with_occurs_check fails. The
result
is the same for unify_with_occurs_check(5, not(true(LP))).
It has certain standard predicates
including unify_with_occurs_check
that makes such detection simpler than in typical programming >>>>>>> >> languages(like Fortran) but the same detection is possible in >>>>>>> >> those, too.
Gödel's sentence is a sentence in the first order Peano
arithmetic.
In that language there is no way to express a reference and in >>>>>>>>> particular a self-reference. For the undecidability proof there is >>>>>>>>> no need to interprete the theorem at all. In the proof of an >>>>>>>>> Peano-
unprovable arithmetic truth the usual arithmetic interpretation is >>>>>>>>> relevant.
In PTS if directly in PA there are no inference steps
that derive G directly in PA then G is ungrounded in
PA thus essentially meaningless in PA.
Meaning is not relevant.
Not being able to prove meaningless gibberish has
never been any actual limitation. The meaningless
gibberish should have always been rejected as bad input.
Not to be able to give meaning to an arithmetic statement has
never been more than a personal limitation. Every natural number
is a natural number number and Gödel numbers are no exception.
Colorless green ideas sleep furiously was composed by
Noam Chomsky in his 1957 book Syntactic Structures as
an example of a sentence that is grammatically well-formed,
but semantically nonsensical.
And not desiderable when discussing arithmetic.
The most important thing about arithmetic is to get the
correct answer. When a gibberish nonsense expression of
PA is construed as meaningful just because its syntax is
correct this is a woefully stupid mistake. Because you are
a mindless robot utterly bereft of a living soul you will
never get this.
Therefore the formal
languages for logic and arithemtic are desigend so that that kind of
nonsense is not expressible.
In my theory of light and color I actually make an account where
there's "green-shift" and there really is "colorless green" or
as about "mono-green-shift", since something like Ogden Rood's
"Modern Chromatics".
One imagines "colorless green" and "sleep furiously" came out
of an early generative program and since multi-pass parsers
greatly modify the considerations of usual formal methods and
right linear automatons perhaps equipped with look-ahead.
Multi-pass parsers are an entirely different model of computation,
and natural languages here have Tesniere grammars.
So, maybe he just didn't get it, it's "grue" and "bleen",
about Nelson Goodman's "Riddle of Induction". Absent a
modal temporal relevance logic that's quite weak.
Anyways "sleep furiously" simply reflects on that the brain
works rather continuously on background problems, the digestion
and the internalization, for usual accounts of problems best
worked by taking a nap.
Chomsky lost a lot of cachet since the whole
hedonism/corruption/blackmail bit. Anyways
also the account of one-pass small-stack grammar's
is not according to the usual account of natural
language the parsing.
So, natural language grammars in their complexity
and the flow in the accidence and adjectival force
are much more about Tesniere and dependency-clause
grammars as students in English learned to diagram
sentences about the same time as mathematical "proof"
was introduced.
The formally abstracted sentence is closer in concept to "ThisThe rendition "I am not provable" is informal, the very
sentence is unprovable."
On 27/04/2026 21:15, Scott Hoge wrote:
The formally abstracted sentence is closer in concept to "ThisThe rendition "I am not provable" is informal, the very
sentence is unprovable."
self-reference is informal (so your diagrams). OTOH, its
arithmetization cannot be circular (or even divergent) or
it's not arithmetic.
Try and read the whole parer: Gödel does give a semantics
(an interpretation), based on relations, and that semantics
is essential to reaching the conclusion he reaches, and
without circularity.
Have fun,
Julio
On 05/01/2026 07:54 AM, olcott wrote:
On 5/1/2026 3:24 AM, Mikko wrote:
On 30/04/2026 15:01, olcott wrote:
On 4/30/2026 2:55 AM, Mikko wrote:
On 29/04/2026 17:17, olcott wrote:
On 4/29/2026 1:37 AM, Mikko wrote:
On 28/04/2026 15:18, olcott wrote:
On 4/28/2026 2:34 AM, Mikko wrote:
On 28/04/2026 00:57, olcott wrote:
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ Followup-To: set ]
In sci.math Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, olcott <polcott333@gmail.com> wrote:
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This >>>>>>>>>>>>>>>> sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G
has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will >>>>>>>>>>>>> never get this. If you always knew what directed graphs >>>>>>>>>>>>> of evaluation sequences that contain cycles are then >>>>>>>>>>>>> you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed >>>>>>>>>>>> graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of >>>>>>>>>>> Gödel's
incompleteness theorem[*]. There are no looping or endless >>>>>>>>>>> directed
graphs in these. Such notions result from misunderstandings >>>>>>>>>>> by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, >>>>>>>>>>> Escher, Bach,
an Eternal Golden Braid" by Douglas Hofstadter, published >>>>>>>>>>> around 1978 or
1979. A proof of the incompleteness theorem is a central >>>>>>>>>>> theme of the
book, which is witty and entertaining and well worth reading. >>>>>>>>>>>
Peter Olcott has never read and understood such a proof. >>>>>>>>>>> Although not
particularly difficult, it is beyond his understanding.
After all these years where I have repeatedly proven that Gödel >>>>>>>>>> himself says that his proof does have pathological self reference >>>>>>>>>> you repeatedly deny this because you and everyone else here only >>>>>>>>>> cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in the >>>>>>>>>> Gödel sentence
Prolog alone does not detect pathological self reference.
Counter-factual. unify_with_occurs_check() <is> Prolog.
The predicate unify_with_occurs_check is not the same as Prolog. >>>>>>> It is
just a small part of the standard language. It is one of those
library
predicates that can be used as I said below.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
You can check it every which way and find that it fails
because LP does not have a finite set of inference steps
thus would be rejected by proof theoretic semantics as
semantically ungrounded.
You can check it ever whixh way and find that it says nothing
more than "false".
If you don't give a rat's ass for this truth I am done
talking to you.
We already know you don't care about this truth any more than
other truths.
I just emphasized that because of the lack of truth
life on Earth will not survive and you said this was
off topic.
It is.
Yu >>>>> Though it does not say why unify_with_occurs_check fails. The
result
is the same for unify_with_occurs_check(5, not(true(LP))).
It has certain standard predicates
including unify_with_occurs_check
that makes such detection simpler than in typical programming >>>>>>> >> languages(like Fortran) but the same detection is possible in >>>>>>> >> those, too.
Gödel's sentence is a sentence in the first order Peano
arithmetic.
In that language there is no way to express a reference and in >>>>>>>>> particular a self-reference. For the undecidability proof there is >>>>>>>>> no need to interprete the theorem at all. In the proof of an >>>>>>>>> Peano-
unprovable arithmetic truth the usual arithmetic interpretation is >>>>>>>>> relevant.
In PTS if directly in PA there are no inference steps
that derive G directly in PA then G is ungrounded in
PA thus essentially meaningless in PA.
Meaning is not relevant.
Not being able to prove meaningless gibberish has
never been any actual limitation. The meaningless
gibberish should have always been rejected as bad input.
Not to be able to give meaning to an arithmetic statement has
never been more than a personal limitation. Every natural number
is a natural number number and Gödel numbers are no exception.
Colorless green ideas sleep furiously was composed by
Noam Chomsky in his 1957 book Syntactic Structures as
an example of a sentence that is grammatically well-formed,
but semantically nonsensical.
And not desiderable when discussing arithmetic.
The most important thing about arithmetic is to get the
correct answer. When a gibberish nonsense expression of
PA is construed as meaningful just because its syntax is
correct this is a woefully stupid mistake. Because you are
a mindless robot utterly bereft of a living soul you will
never get this.
Therefore the formal
languages for logic and arithemtic are desigend so that that kind of
nonsense is not expressible.
In my theory of light and color I actually make an account where
there's "green-shift" and there really is "colorless green" or
as about "mono-green-shift", since something like Ogden Rood's
"Modern Chromatics".
One imagines "colorless green" and "sleep furiously" came out
of an early generative program and since multi-pass parsers
greatly modify the considerations of usual formal methods and
right linear automatons perhaps equipped with look-ahead.
Multi-pass parsers are an entirely different model of computation,
and natural languages here have Tesniere grammars.
So, maybe he just didn't get it, it's "grue" and "bleen",
about Nelson Goodman's "Riddle of Induction". Absent a
modal temporal relevance logic that's quite weak.
Anyways "sleep furiously" simply reflects on that the brain
works rather continuously on background problems, the digestion
and the internalization, for usual accounts of problems best
worked by taking a nap.
Chomsky lost a lot of cachet since the whole
hedonism/corruption/blackmail bit. Anyways
also the account of one-pass small-stack grammar's
is not according to the usual account of natural
language the parsing.
So, natural language grammars in their complexity
and the flow in the accidence and adjectival force
are much more about Tesniere and dependency-clause
grammars as students in English learned to diagram
sentences about the same time as mathematical "proof"
was introduced.
On 27/04/2026 21:15, Scott Hoge wrote:
The formally abstracted sentence is closer in concept to "ThisThe rendition "I am not provable" is informal, the very
sentence is unprovable."
self-reference is informal (so your diagrams). OTOH, its
arithmetization cannot be circular (or even divergent) or
it's not arithmetic.
Try and read the whole parer: Gödel does give a semantics
(an interpretation), based on relations, and that semantics
is essential to reaching the conclusion he reaches, and
without circularity.
Have fun,
Julio
On 5/1/2026 12:47 PM, Ross Finlayson wrote:
On 05/01/2026 07:54 AM, olcott wrote:
On 5/1/2026 3:24 AM, Mikko wrote:
On 30/04/2026 15:01, olcott wrote:
On 4/30/2026 2:55 AM, Mikko wrote:
On 29/04/2026 17:17, olcott wrote:
On 4/29/2026 1:37 AM, Mikko wrote:
On 28/04/2026 15:18, olcott wrote:
On 4/28/2026 2:34 AM, Mikko wrote:
On 28/04/2026 00:57, olcott wrote:
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ Followup-To: set ]After all these years where I have repeatedly proven that Gödel >>>>>>>>>>> himself says that his proof does have pathological self
In sci.math Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, olcott <polcott333@gmail.com> wrote:
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This >>>>>>>>>>>>>>>>> sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G >>>>>>>>>>>>>> has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will >>>>>>>>>>>>>> never get this. If you always knew what directed graphs >>>>>>>>>>>>>> of evaluation sequences that contain cycles are then >>>>>>>>>>>>>> you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed >>>>>>>>>>>>> graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of >>>>>>>>>>>> Gödel's
incompleteness theorem[*]. There are no looping or endless >>>>>>>>>>>> directed
graphs in these. Such notions result from misunderstandings >>>>>>>>>>>> by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, >>>>>>>>>>>> Escher, Bach,
an Eternal Golden Braid" by Douglas Hofstadter, published >>>>>>>>>>>> around 1978 or
1979. A proof of the incompleteness theorem is a central >>>>>>>>>>>> theme of the
book, which is witty and entertaining and well worth reading. >>>>>>>>>>>>
Peter Olcott has never read and understood such a proof. >>>>>>>>>>>> Although not
particularly difficult, it is beyond his understanding. >>>>>>>>>>>
reference
you repeatedly deny this because you and everyone else here only >>>>>>>>>>> cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in the >>>>>>>>>>> Gödel sentence
Prolog alone does not detect pathological self reference.
Counter-factual. unify_with_occurs_check() <is> Prolog.
The predicate unify_with_occurs_check is not the same as Prolog. >>>>>>>> It is
just a small part of the standard language. It is one of those >>>>>>>> library
predicates that can be used as I said below.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
You can check it every which way and find that it fails
because LP does not have a finite set of inference steps
thus would be rejected by proof theoretic semantics as
semantically ungrounded.
You can check it ever whixh way and find that it says nothing
more than "false".
If you don't give a rat's ass for this truth I am done
talking to you.
We already know you don't care about this truth any more than
other truths.
I just emphasized that because of the lack of truth
life on Earth will not survive and you said this was
off topic.
It is.
Yu >>>>> Though it does not say why unify_with_occurs_check fails. The
result
is the same for unify_with_occurs_check(5, not(true(LP))).
It has certain standard predicates
including unify_with_occurs_check
that makes such detection simpler than in typical programming >>>>>>>> >> languages(like Fortran) but the same detection is possible in >>>>>>>> >> those, too.
Gödel's sentence is a sentence in the first order Peano
arithmetic.
In that language there is no way to express a reference and in >>>>>>>>>> particular a self-reference. For the undecidability proof
there is
no need to interprete the theorem at all. In the proof of an >>>>>>>>>> Peano-
unprovable arithmetic truth the usual arithmetic
interpretation is
relevant.
In PTS if directly in PA there are no inference steps
that derive G directly in PA then G is ungrounded in
PA thus essentially meaningless in PA.
Meaning is not relevant.
Not being able to prove meaningless gibberish has
never been any actual limitation. The meaningless
gibberish should have always been rejected as bad input.
Not to be able to give meaning to an arithmetic statement has
never been more than a personal limitation. Every natural number
is a natural number number and Gödel numbers are no exception.
Colorless green ideas sleep furiously was composed by
Noam Chomsky in his 1957 book Syntactic Structures as
an example of a sentence that is grammatically well-formed,
but semantically nonsensical.
And not desiderable when discussing arithmetic.
The most important thing about arithmetic is to get the
correct answer. When a gibberish nonsense expression of
PA is construed as meaningful just because its syntax is
correct this is a woefully stupid mistake. Because you are
a mindless robot utterly bereft of a living soul you will
never get this.
Therefore the formal
languages for logic and arithemtic are desigend so that that kind of
nonsense is not expressible.
In my theory of light and color I actually make an account where
there's "green-shift" and there really is "colorless green" or
as about "mono-green-shift", since something like Ogden Rood's
"Modern Chromatics".
One imagines "colorless green" and "sleep furiously" came out
of an early generative program and since multi-pass parsers
greatly modify the considerations of usual formal methods and
right linear automatons perhaps equipped with look-ahead.
Multi-pass parsers are an entirely different model of computation,
and natural languages here have Tesniere grammars.
So, maybe he just didn't get it, it's "grue" and "bleen",
about Nelson Goodman's "Riddle of Induction". Absent a
modal temporal relevance logic that's quite weak.
Anyways "sleep furiously" simply reflects on that the brain
works rather continuously on background problems, the digestion
and the internalization, for usual accounts of problems best
worked by taking a nap.
Chomsky lost a lot of cachet since the whole
hedonism/corruption/blackmail bit. Anyways
also the account of one-pass small-stack grammar's
is not according to the usual account of natural
language the parsing.
So, natural language grammars in their complexity
and the flow in the accidence and adjectival force
are much more about Tesniere and dependency-clause
grammars as students in English learned to diagram
sentences about the same time as mathematical "proof"
was introduced.
It seems that you are trying to get away with pretending
that you fail to understand the notion of a type mismatch
error.
Kurt Gödel in his 1944 Russell's mathematical logic gave the following definition of the "theory of simple types" in a footnote:
By the theory of simple types I mean the doctrine which says that the
objects of thought (or, in another interpretation, the symbolic
expressions) are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such
relations, etc. (with a similar hierarchy for extensions), and that
sentences of the form: " a has the property φ ", " b bears the relation
R to c ", etc. are meaningless, if a, b, c, R, φ are not of types
fitting together.
https://en.wikipedia.org/wiki/History_of_type_theory#G%C3%B6del_1944
On 05/01/2026 12:35 PM, olcott wrote:
On 5/1/2026 12:47 PM, Ross Finlayson wrote:
On 05/01/2026 07:54 AM, olcott wrote:
On 5/1/2026 3:24 AM, Mikko wrote:
On 30/04/2026 15:01, olcott wrote:
On 4/30/2026 2:55 AM, Mikko wrote:
On 29/04/2026 17:17, olcott wrote:
On 4/29/2026 1:37 AM, Mikko wrote:
On 28/04/2026 15:18, olcott wrote:
On 4/28/2026 2:34 AM, Mikko wrote:
On 28/04/2026 00:57, olcott wrote:Counter-factual. unify_with_occurs_check() <is> Prolog.
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ Followup-To: set ]After all these years where I have repeatedly proven that Gödel >>>>>>>>>>>> himself says that his proof does have pathological self >>>>>>>>>>>> reference
In sci.math Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This >>>>>>>>>>>>>>>>>> sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G >>>>>>>>>>>>>>> has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will >>>>>>>>>>>>>>> never get this. If you always knew what directed graphs >>>>>>>>>>>>>>> of evaluation sequences that contain cycles are then >>>>>>>>>>>>>>> you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school. >>>>>>>>>>>>>
It seems our views are somewhat in agreement, but my directed >>>>>>>>>>>>>> graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of >>>>>>>>>>>>> Gödel's
incompleteness theorem[*]. There are no looping or endless >>>>>>>>>>>>> directed
graphs in these. Such notions result from misunderstandings >>>>>>>>>>>>> by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, >>>>>>>>>>>>> Escher, Bach,
an Eternal Golden Braid" by Douglas Hofstadter, published >>>>>>>>>>>>> around 1978 or
1979. A proof of the incompleteness theorem is a central >>>>>>>>>>>>> theme of the
book, which is witty and entertaining and well worth reading. >>>>>>>>>>>>>
Peter Olcott has never read and understood such a proof. >>>>>>>>>>>>> Although not
particularly difficult, it is beyond his understanding. >>>>>>>>>>>>
you repeatedly deny this because you and everyone else here >>>>>>>>>>>> only
cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in the >>>>>>>>>>>> Gödel sentence
Prolog alone does not detect pathological self reference. >>>>>>>>>>
The predicate unify_with_occurs_check is not the same as Prolog. >>>>>>>>> It is
just a small part of the standard language. It is one of those >>>>>>>>> library
predicates that can be used as I said below.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
You can check it every which way and find that it fails
because LP does not have a finite set of inference steps
thus would be rejected by proof theoretic semantics as
semantically ungrounded.
You can check it ever whixh way and find that it says nothing
more than "false".
If you don't give a rat's ass for this truth I am done
talking to you.
We already know you don't care about this truth any more than
other truths.
I just emphasized that because of the lack of truth
life on Earth will not survive and you said this was
off topic.
It is.
Yu >>>>> Though it does not say why unify_with_occurs_check fails. The >>>> result
is the same for unify_with_occurs_check(5, not(true(LP))).
It has certain standard predicates
including unify_with_occurs_check
that makes such detection simpler than in typical programming >>>>>>>>> >> languages(like Fortran) but the same detection is possible in >>>>>>>>> >> those, too.
Gödel's sentence is a sentence in the first order Peano >>>>>>>>>>> arithmetic.
In that language there is no way to express a reference and in >>>>>>>>>>> particular a self-reference. For the undecidability proof >>>>>>>>>>> there is
no need to interprete the theorem at all. In the proof of an >>>>>>>>>>> Peano-
unprovable arithmetic truth the usual arithmetic
interpretation is
relevant.
In PTS if directly in PA there are no inference steps
that derive G directly in PA then G is ungrounded in
PA thus essentially meaningless in PA.
Meaning is not relevant.
Not being able to prove meaningless gibberish has
never been any actual limitation. The meaningless
gibberish should have always been rejected as bad input.
Not to be able to give meaning to an arithmetic statement has
never been more than a personal limitation. Every natural number >>>>>>> is a natural number number and Gödel numbers are no exception.
Colorless green ideas sleep furiously was composed by
Noam Chomsky in his 1957 book Syntactic Structures as
an example of a sentence that is grammatically well-formed,
but semantically nonsensical.
And not desiderable when discussing arithmetic.
The most important thing about arithmetic is to get the
correct answer. When a gibberish nonsense expression of
PA is construed as meaningful just because its syntax is
correct this is a woefully stupid mistake. Because you are
a mindless robot utterly bereft of a living soul you will
never get this.
Therefore the formal
languages for logic and arithemtic are desigend so that that kind of >>>>> nonsense is not expressible.
In my theory of light and color I actually make an account where
there's "green-shift" and there really is "colorless green" or
as about "mono-green-shift", since something like Ogden Rood's
"Modern Chromatics".
One imagines "colorless green" and "sleep furiously" came out
of an early generative program and since multi-pass parsers
greatly modify the considerations of usual formal methods and
right linear automatons perhaps equipped with look-ahead.
Multi-pass parsers are an entirely different model of computation,
and natural languages here have Tesniere grammars.
So, maybe he just didn't get it, it's "grue" and "bleen",
about Nelson Goodman's "Riddle of Induction". Absent a
modal temporal relevance logic that's quite weak.
Anyways "sleep furiously" simply reflects on that the brain
works rather continuously on background problems, the digestion
and the internalization, for usual accounts of problems best
worked by taking a nap.
Chomsky lost a lot of cachet since the whole
hedonism/corruption/blackmail bit. Anyways
also the account of one-pass small-stack grammar's
is not according to the usual account of natural
language the parsing.
So, natural language grammars in their complexity
and the flow in the accidence and adjectival force
are much more about Tesniere and dependency-clause
grammars as students in English learned to diagram
sentences about the same time as mathematical "proof"
was introduced.
It seems that you are trying to get away with pretending
that you fail to understand the notion of a type mismatch
error.
Kurt Gödel in his 1944 Russell's mathematical logic gave the following
definition of the "theory of simple types" in a footnote:
By the theory of simple types I mean the doctrine which says that the
objects of thought (or, in another interpretation, the symbolic
expressions) are divided into types, namely: individuals, properties of
individuals, relations between individuals, properties of such
relations, etc. (with a similar hierarchy for extensions), and that
sentences of the form: " a has the property φ ", " b bears the relation
R to c ", etc. are meaningless, if a, b, c, R, φ are not of types
fitting together.
https://en.wikipedia.org/wiki/History_of_type_theory#G%C3%B6del_1944
No, I'm just not ignorant of the lack of class/set distinction.
About the transfer principle, and about accounts where
something that is so for each apiece is so for all together,
there's one where there's a non-standard countable model of
integer with a point at infinity naturally simply since
quantification also makes it so, like Russell's paradox,
that Goedel's first object outside the theory would be.
Then, usually "Peirce" or "Pierce" are better sources for type theory,
though Russell whipped up ramified and stratified types in set theory.
https://iep.utm.edu/peir-log/
https://www.cis.upenn.edu/~bcpierce/tapl/
Russell comes across as an erudite logician and schooled philosopher,
yet though plenty of his accounts see him as a self-aggrandizing
free-loader.
Not that there's anything necessarily wrong with that, ....
https://ncatlab.org/nlab/show/set+theory https://en.wikipedia.org/wiki/Class_(set_theory)
Anyways Goedel's world of theorems of his arithmetization is
the same before and after second arithmetization, maybe you'd be
happier instead arguing against his completeness results.
On 05/01/2026 12:35 PM, olcott wrote:
On 5/1/2026 12:47 PM, Ross Finlayson wrote:
On 05/01/2026 07:54 AM, olcott wrote:
On 5/1/2026 3:24 AM, Mikko wrote:
On 30/04/2026 15:01, olcott wrote:
On 4/30/2026 2:55 AM, Mikko wrote:
On 29/04/2026 17:17, olcott wrote:
On 4/29/2026 1:37 AM, Mikko wrote:
On 28/04/2026 15:18, olcott wrote:
On 4/28/2026 2:34 AM, Mikko wrote:
On 28/04/2026 00:57, olcott wrote:Counter-factual. unify_with_occurs_check() <is> Prolog.
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ Followup-To: set ]After all these years where I have repeatedly proven that Gödel >>>>>>>>>>>> himself says that his proof does have pathological self >>>>>>>>>>>> reference
In sci.math Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This >>>>>>>>>>>>>>>>>> sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G >>>>>>>>>>>>>>> has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will >>>>>>>>>>>>>>> never get this. If you always knew what directed graphs >>>>>>>>>>>>>>> of evaluation sequences that contain cycles are then >>>>>>>>>>>>>>> you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school. >>>>>>>>>>>>>
It seems our views are somewhat in agreement, but my directed >>>>>>>>>>>>>> graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of >>>>>>>>>>>>> Gödel's
incompleteness theorem[*]. There are no looping or endless >>>>>>>>>>>>> directed
graphs in these. Such notions result from misunderstandings >>>>>>>>>>>>> by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, >>>>>>>>>>>>> Escher, Bach,
an Eternal Golden Braid" by Douglas Hofstadter, published >>>>>>>>>>>>> around 1978 or
1979. A proof of the incompleteness theorem is a central >>>>>>>>>>>>> theme of the
book, which is witty and entertaining and well worth reading. >>>>>>>>>>>>>
Peter Olcott has never read and understood such a proof. >>>>>>>>>>>>> Although not
particularly difficult, it is beyond his understanding. >>>>>>>>>>>>
you repeatedly deny this because you and everyone else here >>>>>>>>>>>> only
cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in the >>>>>>>>>>>> Gödel sentence
Prolog alone does not detect pathological self reference. >>>>>>>>>>
The predicate unify_with_occurs_check is not the same as Prolog. >>>>>>>>> It is
just a small part of the standard language. It is one of those >>>>>>>>> library
predicates that can be used as I said below.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
You can check it every which way and find that it fails
because LP does not have a finite set of inference steps
thus would be rejected by proof theoretic semantics as
semantically ungrounded.
You can check it ever whixh way and find that it says nothing
more than "false".
If you don't give a rat's ass for this truth I am done
talking to you.
We already know you don't care about this truth any more than
other truths.
I just emphasized that because of the lack of truth
life on Earth will not survive and you said this was
off topic.
It is.
Yu >>>>> Though it does not say why unify_with_occurs_check fails. The >>>> result
is the same for unify_with_occurs_check(5, not(true(LP))).
It has certain standard predicates
including unify_with_occurs_check
that makes such detection simpler than in typical programming >>>>>>>>> >> languages(like Fortran) but the same detection is possible in >>>>>>>>> >> those, too.
Gödel's sentence is a sentence in the first order Peano >>>>>>>>>>> arithmetic.
In that language there is no way to express a reference and in >>>>>>>>>>> particular a self-reference. For the undecidability proof >>>>>>>>>>> there is
no need to interprete the theorem at all. In the proof of an >>>>>>>>>>> Peano-
unprovable arithmetic truth the usual arithmetic
interpretation is
relevant.
In PTS if directly in PA there are no inference steps
that derive G directly in PA then G is ungrounded in
PA thus essentially meaningless in PA.
Meaning is not relevant.
Not being able to prove meaningless gibberish has
never been any actual limitation. The meaningless
gibberish should have always been rejected as bad input.
Not to be able to give meaning to an arithmetic statement has
never been more than a personal limitation. Every natural number >>>>>>> is a natural number number and Gödel numbers are no exception.
Colorless green ideas sleep furiously was composed by
Noam Chomsky in his 1957 book Syntactic Structures as
an example of a sentence that is grammatically well-formed,
but semantically nonsensical.
And not desiderable when discussing arithmetic.
The most important thing about arithmetic is to get the
correct answer. When a gibberish nonsense expression of
PA is construed as meaningful just because its syntax is
correct this is a woefully stupid mistake. Because you are
a mindless robot utterly bereft of a living soul you will
never get this.
Therefore the formal
languages for logic and arithemtic are desigend so that that kind of >>>>> nonsense is not expressible.
In my theory of light and color I actually make an account where
there's "green-shift" and there really is "colorless green" or
as about "mono-green-shift", since something like Ogden Rood's
"Modern Chromatics".
One imagines "colorless green" and "sleep furiously" came out
of an early generative program and since multi-pass parsers
greatly modify the considerations of usual formal methods and
right linear automatons perhaps equipped with look-ahead.
Multi-pass parsers are an entirely different model of computation,
and natural languages here have Tesniere grammars.
So, maybe he just didn't get it, it's "grue" and "bleen",
about Nelson Goodman's "Riddle of Induction". Absent a
modal temporal relevance logic that's quite weak.
Anyways "sleep furiously" simply reflects on that the brain
works rather continuously on background problems, the digestion
and the internalization, for usual accounts of problems best
worked by taking a nap.
Chomsky lost a lot of cachet since the whole
hedonism/corruption/blackmail bit. Anyways
also the account of one-pass small-stack grammar's
is not according to the usual account of natural
language the parsing.
So, natural language grammars in their complexity
and the flow in the accidence and adjectival force
are much more about Tesniere and dependency-clause
grammars as students in English learned to diagram
sentences about the same time as mathematical "proof"
was introduced.
It seems that you are trying to get away with pretending
that you fail to understand the notion of a type mismatch
error.
Kurt Gödel in his 1944 Russell's mathematical logic gave the following
definition of the "theory of simple types" in a footnote:
By the theory of simple types I mean the doctrine which says that the
objects of thought (or, in another interpretation, the symbolic
expressions) are divided into types, namely: individuals, properties of
individuals, relations between individuals, properties of such
relations, etc. (with a similar hierarchy for extensions), and that
sentences of the form: " a has the property φ ", " b bears the relation
R to c ", etc. are meaningless, if a, b, c, R, φ are not of types
fitting together.
https://en.wikipedia.org/wiki/History_of_type_theory#G%C3%B6del_1944
No, I'm just not ignorant of the lack of class/set distinction.
About the transfer principle, and about accounts where
something that is so for each apiece is so for all together,
there's one where there's a non-standard countable model of
integer with a point at infinity naturally simply since
quantification also makes it so, like Russell's paradox,
that Goedel's first object outside the theory would be.
Then, usually "Peirce" or "Pierce" are better sources for type theory,
though Russell whipped up ramified and stratified types in set theory.
https://iep.utm.edu/peir-log/
https://www.cis.upenn.edu/~bcpierce/tapl/
Russell comes across as an erudite logician and schooled philosopher,
yet though plenty of his accounts see him as a self-aggrandizing
free-loader.
Not that there's anything necessarily wrong with that, ....
https://ncatlab.org/nlab/show/set+theory https://en.wikipedia.org/wiki/Class_(set_theory)
Anyways Goedel's world of theorems of his arithmetization is
the same before and after second arithmetization, maybe you'd be
happier instead arguing against his completeness results.
On 27/04/2026 21:15, Scott Hoge wrote:
The formally abstracted sentence is closer in concept to "This
sentence is unprovable."
The rendition "I am not provable" is informal, the very
self-reference is informal (so your diagrams). OTOH, its
arithmetization cannot be circular (or even divergent) or it's
not arithmetic.
Try and read the whole [paper]: Gödel does give a semantics (an interpretation), based on relations, and that semantics is
essential to reaching the conclusion he reaches, and without
circularity.
On 5/1/2026 2:54 PM, Ross Finlayson wrote:
On 05/01/2026 12:35 PM, olcott wrote:
On 5/1/2026 12:47 PM, Ross Finlayson wrote:
On 05/01/2026 07:54 AM, olcott wrote:
On 5/1/2026 3:24 AM, Mikko wrote:
On 30/04/2026 15:01, olcott wrote:
On 4/30/2026 2:55 AM, Mikko wrote:
On 29/04/2026 17:17, olcott wrote:
On 4/29/2026 1:37 AM, Mikko wrote:
On 28/04/2026 15:18, olcott wrote:
On 4/28/2026 2:34 AM, Mikko wrote:
On 28/04/2026 00:57, olcott wrote:Counter-factual. unify_with_occurs_check() <is> Prolog.
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ Followup-To: set ]After all these years where I have repeatedly proven that >>>>>>>>>>>>> Gödel
In sci.math Scott Hoge <nospam@nospam.com> wrote: >>>>>>>>>>>>>>> On 2026-04-27, olcott <polcott333@gmail.com> wrote: >>>>>>>>>>>>>>
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This >>>>>>>>>>>>>>>>>>> sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G >>>>>>>>>>>>>>>> has a cycle preventing its evaluation from ever >>>>>>>>>>>>>>>> terminating.
If you have no idea what directed graphs are you will >>>>>>>>>>>>>>>> never get this. If you always knew what directed graphs >>>>>>>>>>>>>>>> of evaluation sequences that contain cycles are then >>>>>>>>>>>>>>>> you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school. >>>>>>>>>>>>>>
It seems our views are somewhat in agreement, but my >>>>>>>>>>>>>>> directed
graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of >>>>>>>>>>>>>> Gödel's
incompleteness theorem[*]. There are no looping or endless >>>>>>>>>>>>>> directed
graphs in these. Such notions result from misunderstandings >>>>>>>>>>>>>> by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, >>>>>>>>>>>>>> Escher, Bach,
an Eternal Golden Braid" by Douglas Hofstadter, published >>>>>>>>>>>>>> around 1978 or
1979. A proof of the incompleteness theorem is a central >>>>>>>>>>>>>> theme of the
book, which is witty and entertaining and well worth reading. >>>>>>>>>>>>>>
Peter Olcott has never read and understood such a proof. >>>>>>>>>>>>>> Although not
particularly difficult, it is beyond his understanding. >>>>>>>>>>>>>
himself says that his proof does have pathological self >>>>>>>>>>>>> reference
you repeatedly deny this because you and everyone else here >>>>>>>>>>>>> only
cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in >>>>>>>>>>>>> the
Gödel sentence
Prolog alone does not detect pathological self reference. >>>>>>>>>>>
The predicate unify_with_occurs_check is not the same as Prolog. >>>>>>>>>> It is
just a small part of the standard language. It is one of those >>>>>>>>>> library
predicates that can be used as I said below.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
You can check it every which way and find that it fails
because LP does not have a finite set of inference steps
thus would be rejected by proof theoretic semantics as
semantically ungrounded.
You can check it ever whixh way and find that it says nothing
more than "false".
If you don't give a rat's ass for this truth I am done
talking to you.
We already know you don't care about this truth any more than
other truths.
I just emphasized that because of the lack of truth
life on Earth will not survive and you said this was
off topic.
It is.
Yu >>>>> Though it does not say why unify_with_occurs_check fails. The >>>>> result
Colorless green ideas sleep furiously was composed byis the same for unify_with_occurs_check(5, not(true(LP))). >>>>>>>>>>
It has certain standard predicates
including unify_with_occurs_check
possible inthat makes such detection simpler than in typical programming >>>>>>>>>> >> languages(like Fortran) but the same detection is
those, too.
Gödel's sentence is a sentence in the first order Peano >>>>>>>>>>>> arithmetic.
In that language there is no way to express a reference and in >>>>>>>>>>>> particular a self-reference. For the undecidability proof >>>>>>>>>>>> there is
no need to interprete the theorem at all. In the proof of an >>>>>>>>>>>> Peano-
unprovable arithmetic truth the usual arithmetic
interpretation is
relevant.
In PTS if directly in PA there are no inference steps
that derive G directly in PA then G is ungrounded in
PA thus essentially meaningless in PA.
Meaning is not relevant.
Not being able to prove meaningless gibberish has
never been any actual limitation. The meaningless
gibberish should have always been rejected as bad input.
Not to be able to give meaning to an arithmetic statement has
never been more than a personal limitation. Every natural number >>>>>>>> is a natural number number and Gödel numbers are no exception. >>>>>>>
Noam Chomsky in his 1957 book Syntactic Structures as
an example of a sentence that is grammatically well-formed,
but semantically nonsensical.
And not desiderable when discussing arithmetic.
The most important thing about arithmetic is to get the
correct answer. When a gibberish nonsense expression of
PA is construed as meaningful just because its syntax is
correct this is a woefully stupid mistake. Because you are
a mindless robot utterly bereft of a living soul you will
never get this.
Therefore the formal
languages for logic and arithemtic are desigend so that that kind of >>>>>> nonsense is not expressible.
In my theory of light and color I actually make an account where
there's "green-shift" and there really is "colorless green" or
as about "mono-green-shift", since something like Ogden Rood's
"Modern Chromatics".
One imagines "colorless green" and "sleep furiously" came out
of an early generative program and since multi-pass parsers
greatly modify the considerations of usual formal methods and
right linear automatons perhaps equipped with look-ahead.
Multi-pass parsers are an entirely different model of computation,
and natural languages here have Tesniere grammars.
So, maybe he just didn't get it, it's "grue" and "bleen",
about Nelson Goodman's "Riddle of Induction". Absent a
modal temporal relevance logic that's quite weak.
Anyways "sleep furiously" simply reflects on that the brain
works rather continuously on background problems, the digestion
and the internalization, for usual accounts of problems best
worked by taking a nap.
Chomsky lost a lot of cachet since the whole
hedonism/corruption/blackmail bit. Anyways
also the account of one-pass small-stack grammar's
is not according to the usual account of natural
language the parsing.
So, natural language grammars in their complexity
and the flow in the accidence and adjectival force
are much more about Tesniere and dependency-clause
grammars as students in English learned to diagram
sentences about the same time as mathematical "proof"
was introduced.
It seems that you are trying to get away with pretending
that you fail to understand the notion of a type mismatch
error.
Kurt Gödel in his 1944 Russell's mathematical logic gave the following
definition of the "theory of simple types" in a footnote:
By the theory of simple types I mean the doctrine which says that the
objects of thought (or, in another interpretation, the symbolic
expressions) are divided into types, namely: individuals, properties of
individuals, relations between individuals, properties of such
relations, etc. (with a similar hierarchy for extensions), and that
sentences of the form: " a has the property φ ", " b bears the relation >>> R to c ", etc. are meaningless, if a, b, c, R, φ are not of types
fitting together.
https://en.wikipedia.org/wiki/History_of_type_theory#G%C3%B6del_1944
No, I'm just not ignorant of the lack of class/set distinction.
About the transfer principle, and about accounts where
something that is so for each apiece is so for all together,
there's one where there's a non-standard countable model of
integer with a point at infinity naturally simply since
quantification also makes it so, like Russell's paradox,
that Goedel's first object outside the theory would be.
Then, usually "Peirce" or "Pierce" are better sources for type theory,
though Russell whipped up ramified and stratified types in set theory.
https://iep.utm.edu/peir-log/
https://www.cis.upenn.edu/~bcpierce/tapl/
Russell comes across as an erudite logician and schooled philosopher,
yet though plenty of his accounts see him as a self-aggrandizing
free-loader.
Ridiculously stupid ad hominem basis.
I always took you for much smarter than that.
Not that there's anything necessarily wrong with that, ....
https://ncatlab.org/nlab/show/set+theory
https://en.wikipedia.org/wiki/Class_(set_theory)
Anyways Goedel's world of theorems of his arithmetization is
the same before and after second arithmetization, maybe you'd be
happier instead arguing against his completeness results.
On 01/05/2026 17:54, olcott wrote:
On 5/1/2026 3:24 AM, Mikko wrote:
On 30/04/2026 15:01, olcott wrote:
On 4/30/2026 2:55 AM, Mikko wrote:
On 29/04/2026 17:17, olcott wrote:
On 4/29/2026 1:37 AM, Mikko wrote:
On 28/04/2026 15:18, olcott wrote:
On 4/28/2026 2:34 AM, Mikko wrote:
On 28/04/2026 00:57, olcott wrote:
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ Followup-To: set ]
In sci.math Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, olcott <polcott333@gmail.com> wrote:
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This >>>>>>>>>>>>>>>> sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G
has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will >>>>>>>>>>>>> never get this. If you always knew what directed graphs >>>>>>>>>>>>> of evaluation sequences that contain cycles are then >>>>>>>>>>>>> you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed >>>>>>>>>>>> graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof of >>>>>>>>>>> Gödel's
incompleteness theorem[*]. There are no looping or endless >>>>>>>>>>> directed
graphs in these. Such notions result from misunderstandings >>>>>>>>>>> by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, >>>>>>>>>>> Escher, Bach,
an Eternal Golden Braid" by Douglas Hofstadter, published >>>>>>>>>>> around 1978 or
1979. A proof of the incompleteness theorem is a central >>>>>>>>>>> theme of the
book, which is witty and entertaining and well worth reading. >>>>>>>>>>>
Peter Olcott has never read and understood such a proof. >>>>>>>>>>> Although not
particularly difficult, it is beyond his understanding.
After all these years where I have repeatedly proven that Gödel >>>>>>>>>> himself says that his proof does have pathological self reference >>>>>>>>>> you repeatedly deny this because you and everyone else here only >>>>>>>>>> cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in >>>>>>>>>> the Gödel sentence
Prolog alone does not detect pathological self reference.
Counter-factual. unify_with_occurs_check() <is> Prolog.
The predicate unify_with_occurs_check is not the same as Prolog. >>>>>>> It is
just a small part of the standard language. It is one of those
library
predicates that can be used as I said below.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
You can check it every which way and find that it fails
because LP does not have a finite set of inference steps
thus would be rejected by proof theoretic semantics as
semantically ungrounded.
You can check it ever whixh way and find that it says nothing
more than "false".
If you don't give a rat's ass for this truth I am done
talking to you.
We already know you don't care about this truth any more than
other truths.
I just emphasized that because of the lack of truth
life on Earth will not survive and you said this was
off topic.
It is.
Yu >>>>> Though it does not say why unify_with_occurs_check fails. The
result
is the same for unify_with_occurs_check(5, not(true(LP))).
It has certain standard predicates
including unify_with_occurs_check
that makes such detection simpler than in typical programming >>>>>>> >> languages(like Fortran) but the same detection is possible in >>>>>>> >> those, too.
Gödel's sentence is a sentence in the first order Peano
arithmetic.
In that language there is no way to express a reference and in >>>>>>>>> particular a self-reference. For the undecidability proof there is >>>>>>>>> no need to interprete the theorem at all. In the proof of an >>>>>>>>> Peano-
unprovable arithmetic truth the usual arithmetic interpretation is >>>>>>>>> relevant.
In PTS if directly in PA there are no inference steps
that derive G directly in PA then G is ungrounded in
PA thus essentially meaningless in PA.
Meaning is not relevant.
Not being able to prove meaningless gibberish has
never been any actual limitation. The meaningless
gibberish should have always been rejected as bad input.
Not to be able to give meaning to an arithmetic statement has
never been more than a personal limitation. Every natural number
is a natural number number and Gödel numbers are no exception.
Colorless green ideas sleep furiously was composed by
Noam Chomsky in his 1957 book Syntactic Structures as
an example of a sentence that is grammatically well-formed,
but semantically nonsensical.
And not desiderable when discussing arithmetic.
The most important thing about arithmetic is to get the
correct answer.
Only when something is asked. Another important thing is to
determine whether the given answer is correct when a question
is asked and answered. Yet another important thing is to
check whether a statement about numbers is true or false.
The formal lanugage of arithemtic can only express statements
that can be interpreted as statements abut numbers. Questions
cannot be expressed in the formal language but informal
questions about a formal expression can be asked.
Gödel's sentence is
a formal sentence that can be interpreted
as a claim about natural numbers. Whether the claim is true
is a reasonable question about the claim.
When a gibberish nonsense expression of
PA is construed as meaningful just because its syntax is
correct this is a woefully stupid mistake.
A sentence about numbers and addition, multiplication, equality
and ordering is not gibberish just because you don't understand
it.
Therefore the formal languages for logic and arithemtic are
desigend so that that kind of nonsense is not expressible.
Which means that all your talk about arithmetic gibberish is
just empty claims about nothing.
Yet nothing prevents us from /expanding/ the semantics given by<snip>
Gödel. What I call the /formally abstracted Gödel sentence/ is
not the same sentence that he proved undecidable.
On 02/05/2026 00:10, Scott Hoge wrote:
Yet nothing prevents us from /expanding/ the semantics given by<snip>
Gödel. What I call the /formally abstracted Gödel sentence/ is
not the same sentence that he proved undecidable.
Everything prevents us from doing that.
Besides that
interesting would a minimal such semantics, you should
rather consider what GIT is actually about: it is not a
logical investigation into some kind of extra-ordinary
statements, it is a mathematical investigation into the
limits of recursively axiomatised systems of arithmetic
(the systems we can run on a concrete computer, or those
that are needed in foundations), up to proving the
incompleteness of any such systems if they are consistent.
Indeed, Gödel's argument rather generalises as a form of
diagonalisation.
That said, I do find interesting that the argument has a
semantic component to it (contra widespread belief that
it is "purely syntactic"), and what that entails, e.g. as
to the validity(?) of any models in which the G-sentence
is false... Still, as said, you'd have to keep in mind
what the argument is actually about.
Julio
On 02/05/2026 00:10, Scott Hoge wrote:
Yet nothing prevents us from /expanding/ the semantics given
by Gödel. What I call the /formally abstracted Gödel sentence/
is not the same sentence that he proved undecidable.
[...]
Everything prevents us from doing that. Besides that
interesting would a minimal such semantics, you should
rather consider what GIT is actually about: it is not a
logical investigation into some kind of extra-ordinary
statements [...]
Indeed, Gödel's argument rather generalises as a form of
diagonalisation.
[...]
On 2026-05-02, Julio Di Egidio <julio@diegidio.name> wrote:
On 02/05/2026 00:10, Scott Hoge wrote:
Yet nothing prevents us from /expanding/ the semantics given
by Gödel. What I call the /formally abstracted Gödel sentence/
is not the same sentence that he proved undecidable.
[...]
Everything prevents us from doing that. Besides that
interesting would a minimal such semantics, you should
rather consider what GIT is actually about: it is not a
logical investigation into some kind of extra-ordinary
statements [...]
Theoretical physicist Roger Penrose has speculated that Gödel's Incompleteness Theorem relates to both quantum mechanics and
consciousness. Based on the premise that consciousness depends on
grasping undecidable and uncomputable truths, his theory is
called Orchestrated Objective Reduction, or Orch-OR.
Orch-OR proposes that consciousness arises from wave function--
collapse, and that it does so through attributes of the brain and
of its biological constitution. These attributes allow the brain
to transcend the limits of what a computer can do, which is where
Gödel's incompleteness enters into the theory.
Indeed, Gödel's argument rather generalises as a form of
diagonalisation.
[...]
My view is that consciousness may require some kind of subjective indeterminism, whether in the form of "freedom," "choice," or
"uncertainty," that permits the following characteristics:
1. Presence in the here-and-now.
2. Synthesis of a manifold of perception.
3. Undecidability of certain problems on the basis of "antinomy."
4. Thought regarding what /possibly/ may happen.
By "synthesis of a manifold," I mean the binding and
putting-together of multiple items of consciousness. I may see a
desk, a chair, a computer, and some flash drives all drawn
together in my field of vision. These presentations, or items of consciousness, carry signification insofar as it is logically
possible for me to apprehend any one of them selectively. I may
nudge the chair, insert one of the flash drives, or turn on the
computer; freedom or uncertainty therefore seems tied to
manifoldness of presentation.
By "antinomy," I mean unsolvable questions about what happens
beyond the limits of sensibility, such as at the infinite.
In Cantor's theorem, we do not actually construct a diagonal.
Rather, we presuppose that we can enumerate a set, and then,
/purely on the grounds of possibility/, conceive a diagonalized
non-element. This links diagonalization to criterion (4) of
consciousness.
On the foregoing basis, we may conjecture that Penrose was in
some sense right about Orch-OR. Gödel's theorem provides us with
knowledge about the unknowability of what happens "at infinity"
in the nested sequence of Gödel sentences.
How this relates to what happens in the brain is another question
that Penrose attempted to answer on the basis of microtubules.
On the other hand, I think that /any/ physical phenomenon
resulting from amplification from the microscopic world via
self-reinforcing feedback loops may provide the link between
Gödel sentences and human consciousness.
-- Scott Hoge
On 02/05/2026 00:10, Scott Hoge wrote:
Yet nothing prevents us from /expanding/ the semantics given by<snip>
Gödel. What I call the /formally abstracted Gödel sentence/ is
not the same sentence that he proved undecidable.
Everything prevents us from doing that. Besides that
interesting would a minimal such semantics, you should
rather consider what GIT is actually about: it is not a
logical investigation into some kind of extra-ordinary
statements, it is a mathematical investigation into the
limits of recursively axiomatised systems of arithmetic
(the systems we can run on a concrete computer, or those
that are needed in foundations), up to proving the
incompleteness of any such systems if they are consistent.
Indeed, Gödel's argument rather generalises as a form of
diagonalisation.
That said, I do find interesting that the argument has a
semantic component to it (contra widespread belief that
it is "purely syntactic"), and what that entails, e.g. as
to the validity(?) of any models in which the G-sentence
is false... Still, as said, you'd have to keep in mind
what the argument is actually about.
Julio
On 5/2/2026 3:04 AM, Mikko wrote:
On 01/05/2026 17:54, olcott wrote:
On 5/1/2026 3:24 AM, Mikko wrote:
On 30/04/2026 15:01, olcott wrote:
On 4/30/2026 2:55 AM, Mikko wrote:
On 29/04/2026 17:17, olcott wrote:
On 4/29/2026 1:37 AM, Mikko wrote:
On 28/04/2026 15:18, olcott wrote:
On 4/28/2026 2:34 AM, Mikko wrote:
On 28/04/2026 00:57, olcott wrote:
On 4/27/2026 4:03 PM, Alan Mackenzie wrote:
[ Followup-To: set ]After all these years where I have repeatedly proven that Gödel >>>>>>>>>>> himself says that his proof does have pathological self >>>>>>>>>>> reference
In sci.math Scott Hoge <nospam@nospam.com> wrote:
On 2026-04-27, olcott <polcott333@gmail.com> wrote:
[...]
On 4/26/2026 3:01 PM, Scott Hoge wrote:
[...]
The correct interpretation was, I argued, not "This >>>>>>>>>>>>>>>>> sentence
is unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
The directed graph of the evaluation sequence of G >>>>>>>>>>>>>> has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will >>>>>>>>>>>>>> never get this. If you always knew what directed graphs >>>>>>>>>>>>>> of evaluation sequences that contain cycles are then >>>>>>>>>>>>>> you rebuttal has always been pure dishonesty.
I learned what directed graphs were in high school.
It seems our views are somewhat in agreement, but my directed >>>>>>>>>>>>> graph looks like this:
(D1)
· ─→ · ─→ · ─→ · ─→ ...
I strongly urge you to read and understand an actual proof >>>>>>>>>>>> of Gödel's
incompleteness theorem[*]. There are no looping or endless >>>>>>>>>>>> directed
graphs in these. Such notions result from misunderstandings >>>>>>>>>>>> by those
lacking formal training in mathematics.
[*] I would suggest finding a second hand copy of "Gödel, >>>>>>>>>>>> Escher, Bach,
an Eternal Golden Braid" by Douglas Hofstadter, published >>>>>>>>>>>> around 1978 or
1979. A proof of the incompleteness theorem is a central >>>>>>>>>>>> theme of the
book, which is witty and entertaining and well worth reading. >>>>>>>>>>>>
Peter Olcott has never read and understood such a proof. >>>>>>>>>>>> Although not
particularly difficult, it is beyond his understanding. >>>>>>>>>>>
you repeatedly deny this because you and everyone else here only >>>>>>>>>>> cares about denigration rather than truth.
Prolog detects [and rejects] pathological self reference in >>>>>>>>>>> the Gödel sentence
Prolog alone does not detect pathological self reference.
Counter-factual. unify_with_occurs_check() <is> Prolog.
The predicate unify_with_occurs_check is not the same as Prolog. >>>>>>>> It is
just a small part of the standard language. It is one of those >>>>>>>> library
predicates that can be used as I said below.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
You can check it every which way and find that it fails
because LP does not have a finite set of inference steps
thus would be rejected by proof theoretic semantics as
semantically ungrounded.
You can check it ever whixh way and find that it says nothing
more than "false".
If you don't give a rat's ass for this truth I am done
talking to you.
We already know you don't care about this truth any more than
other truths.
I just emphasized that because of the lack of truth
life on Earth will not survive and you said this was
off topic.
It is.
Yu >>>>> Though it does not say why unify_with_occurs_check fails.
The result
is the same for unify_with_occurs_check(5, not(true(LP))).
It has certain standard predicates
including unify_with_occurs_check
that makes such detection simpler than in typical programming >>>>>>>> >> languages(like Fortran) but the same detection is possible in >>>>>>>> >> those, too.
Gödel's sentence is a sentence in the first order Peano
arithmetic.
In that language there is no way to express a reference and in >>>>>>>>>> particular a self-reference. For the undecidability proof >>>>>>>>>> there is
no need to interprete the theorem at all. In the proof of an >>>>>>>>>> Peano-
unprovable arithmetic truth the usual arithmetic
interpretation is
relevant.
In PTS if directly in PA there are no inference steps
that derive G directly in PA then G is ungrounded in
PA thus essentially meaningless in PA.
Meaning is not relevant.
Not being able to prove meaningless gibberish has
never been any actual limitation. The meaningless
gibberish should have always been rejected as bad input.
Not to be able to give meaning to an arithmetic statement has
never been more than a personal limitation. Every natural number
is a natural number number and Gödel numbers are no exception.
Colorless green ideas sleep furiously was composed by
Noam Chomsky in his 1957 book Syntactic Structures as
an example of a sentence that is grammatically well-formed,
but semantically nonsensical.
And not desiderable when discussing arithmetic.
The most important thing about arithmetic is to get the
correct answer.
Only when something is asked. Another important thing is to
determine whether the given answer is correct when a question
is asked and answered. Yet another important thing is to
check whether a statement about numbers is true or false.
The formal lanugage of arithemtic can only express statements
that can be interpreted as statements abut numbers. Questions
cannot be expressed in the formal language but informal
questions about a formal expression can be asked.
Gödel's sentence is
semantically meaningless in arithmetic when examined
within the correct foundation of proof theoretic semantics.
In Cantor's theorem, we do not actually construct a diagonal.
Rather, we presuppose that we can enumerate a set, and then,
/purely on the grounds of possibility/, conceive a diagonalized
non-element.
This links diagonalization to criterion (4) of consciousness.
On 02/05/2026 20:47, Scott Hoge wrote:
In Cantor's theorem, we do not actually construct a diagonal.
Rather, we presuppose that we can enumerate a set, and then,
/purely on the grounds of possibility/, conceive a diagonalized
non-element.
Nope, as explained and re-explained ad nauseam around here:
just the resident trolls won't get it.
Cantor's diagonal argument, the one with the binary sequences,
is indeed constructive: a definition of anti-diagonal of *any*
(infinite) list is provided, and the proof that the anti-diagonal
cannot be in the list is quite constructive.
(Namely, we don't need to say "assume ab abdsurdo that
an enumeration is given", we can just say "for *any* list,
we *construct* an element not in the list".)
Just look it up. Here is my own rendition in Rocq: <https://gist.github.com/jp-diegidio/eb05f6265c38b35c85853514ed46ab47>
This links diagonalization to criterion (4) of consciousness.
Rather, and to sum up, it links diagonalisation to the limits
of physicalism...
HTH,
Julio
Julio Di Egidio wrote:
On 02/05/2026 20:47, Scott Hoge wrote:
In Cantor's theorem, we do not actually construct a diagonal.
Rather, we presuppose that we can enumerate a set, and then,
/purely on the grounds of possibility/, conceive a diagonalized
non-element.
Nope, as explained and re-explained ad nauseam around here:
just the resident trolls won't get it.
Cantor's diagonal argument, the one with the binary sequences,
is indeed constructive: a definition of anti-diagonal of *any*
(infinite) list is provided, and the proof that the anti-diagonal
cannot be in the list is quite constructive.
(Namely, we don't need to say "assume ab abdsurdo that
an enumeration is given", we can just say "for *any* list,
we *construct* an element not in the list".)
Just look it up. Here is my own rendition in Rocq:
<https://gist.github.com/jp-diegidio/eb05f6265c38b35c85853514ed46ab47>
This links diagonalization to criterion (4) of consciousness.
Rather, and to sum up, it links diagonalisation to the limits
of physicalism...
HTH,
Julio
I guess my question is this: If the diagonal sequence is inadequate,
just what exactly is Cantor attempting to represent with the diagonal sequence at all?
On 02/05/2026 20:47, Scott Hoge wrote:
In Cantor's theorem, we do not actually construct a diagonal.
Rather, we presuppose that we can enumerate a set, and then,
/purely on the grounds of possibility/, conceive a
diagonalized non-element.
Nope, as explained and re-explained ad nauseam around here:
just the resident trolls won't get it.
Cantor's diagonal argument, the one with the binary sequences,
is indeed constructive: a definition of anti-diagonal of *any*
(infinite) list is provided, and the proof that the
anti-diagonal cannot be in the list is quite constructive.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,116 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 85:27:55 |
| Calls: | 14,305 |
| Files: | 186,338 |
| D/L today: |
650 files (185M bytes) |
| Messages: | 2,525,478 |