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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL. Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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 +o ree PA(+o reu -a) 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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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 +o ree PA(+o reu -a) is
already in the usual metalanguage semantics.
KnownTrue-a := +o ree PA(+o reu -a)
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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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 +o ree PA(+o reu -a) 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-a := +o ree PA(+o reu -a)
It is a syntax error to use open variables -a 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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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 +o ree PA(+o reu -a) is >>
be a copy of the expression defining Probable.
already in the usual metalanguage semantics.
KnownTrue-a := +o ree PA(+o reu -a)
It is a syntax error to use open variables -a 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 +o in PA such that -a 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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a >>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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 +o ree PA(+o reu -a) 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-a := +o ree PA(+o reu -a)
It is a syntax error to use open variables -a 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 +o in PA such that -a reaches the axioms of PA
-a 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 -a 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 +o in PA such that -a 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 -a 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 +o in PA such that -a reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(-a) := ...
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 -a 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 +o in PA such that -a reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(-a) := ...
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 -a 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 +o in PA such that -a reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(-a) := ...
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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a >>>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL. >>>>>>> Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a >>>>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL. >>>>>>>> Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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 -a 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 +o in PA such that -a reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(-a) := ...
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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a >>>>>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL. >>>>>>>>> Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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 -a 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 +o in PA such that -a reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(-a) := ...
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 -a 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 +o in PA such that -a reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(-a) := ...
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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL. Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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)-(reR) belong the "formally abstracted sentence," and the concept under which all sentences (2)-(reR)
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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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):
-a The following is unprovable (2):
-a-a The following is unprovable (3):
-a-a-a ...
As regards semantics, I could call statement (1) the "unencoded
sentence," sentence (2) the "first encoded sentence," the concept
under which all sentences (1)-(reR) belong the "formally abstracted
sentence," and the concept under which all sentences (2)-(reR)
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 reo GF rao -4ProvF(riLGFriY) https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Olcott's Minimal Type Theory
G rao -4Prov_PA(riLGriY)
Directed Graph of evaluation sequence
00 rao-a-a-a-a-a-a-a-a-a-a-a-a-a-a 01 02
01 G
02 -4-a-a-a-a-a-a-a-a-a-a-a-a-a-a 03
03 Prov_PA-a-a-a-a-a-a-a-a 04
04 G||del_Number_of 01-a // 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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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):
-a The following is unprovable (2):
-a-a The following is unprovable (3):
-a-a-a ...
As regards semantics, I could call statement (1) the "unencoded
sentence," sentence (2) the "first encoded sentence," the concept
under which all sentences (1)-(reR) belong the "formally abstracted
sentence," and the concept under which all sentences (2)-(reR)
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 reo GF rao -4ProvF(riLGFriY) https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Olcott's Minimal Type Theory
G rao -4Prov_PA(riLGriY)
Directed Graph of evaluation sequence
00 rao-a-a-a-a-a-a-a-a-a-a-a-a-a-a 01 02
01 G
02 -4-a-a-a-a-a-a-a-a-a-a-a-a-a-a 03
03 Prov_PA-a-a-a-a-a-a-a-a 04
04 G||del_Number_of 01-a // 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, -a) := rea+o ree PA(+o reu -a)
There exists a finite set +o of inference steps of PA such that -a
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, -a) := Provable(PA, -a)
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):
-a The following is unprovable (2):
-a-a The following is unprovable (3):
-a-a-a ...
As regards semantics, I could call statement (1) the "unencoded
sentence," sentence (2) the "first encoded sentence," the concept
under which all sentences (1)-(reR) belong the "formally abstracted
sentence," and the concept under which all sentences (2)-(reR)
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 reo GF rao -4ProvF(riLGFriY)
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Olcott's Minimal Type Theory
G rao -4Prov_PA(riLGriY)
Directed Graph of evaluation sequence
00 rao-a-a-a-a-a-a-a-a-a-a-a-a-a-a 01 02
01 G
02 -4-a-a-a-a-a-a-a-a-a-a-a-a-a-a 03
03 Prov_PA-a-a-a-a-a-a-a-a 04
04 G||del_Number_of 01-a // 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):
-a The following is unprovable (2):
-a-a The following is unprovable (3):
-a-a-a ...
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)-(reR)
belong the "formally abstracted sentence," and the concept
under which all sentences (2)-(reR) 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):
-a The following is unprovable (2):
-a-a The following is unprovable (3):
-a-a-a ...
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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
Yours appears to look like this, where its semantic (?)
evaluation contains a cycle:
(D2)
-+ roCroE
raa rao
rooroC -+
(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)-(reR)
belong the "formally abstracted sentence," and the concept
under which all sentences (2)-(reR) 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):
-a The following is unprovable (2):
-a-a The following is unprovable (3):
-a-a-a ...
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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
-- 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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
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
[ 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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
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.
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.
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
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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
I strongly urge you to read and understand an actual proof of
G||del's incompleteness theorem[*].-a There are no looping or
endless directed graphs in these.-a 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 rao -4Prov_PA(riLGriY)
Directed Graph of evaluation sequence
00 rao-a-a-a-a-a-a-a-a-a-a-a-a-a-a 01 02
01 G
02 -4-a-a-a-a-a-a-a-a-a-a-a-a-a-a 03
03 Prov_PA-a-a-a-a-a-a-a-a 04
04 G||del_Number_of 01-a // 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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
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):
-a The following is unprovable (2):
-a-a The following is unprovable (3):
-a-a-a ...
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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
I strongly urge you to read and understand an actual proof of
G||del's incompleteness theorem[*].-a There are no looping or
endless directed graphs in these.-a 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 rao -4Prov_PA(riLGriY)
Directed Graph of evaluation sequence
00 rao-a-a-a-a-a-a-a-a-a-a-a-a-a-a 01 02
01 G
02 -4-a-a-a-a-a-a-a-a-a-a-a-a-a-a 03
03 Prov_PA-a-a-a-a-a-a-a-a 04
04 G||del_Number_of 01-a // 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.
[...] So anything proven about the first node
automatically applies to the rest of the nodes. There is no time
involved here - it does not take, say, one second to traverse an edge to
the next node, hence taking an infinite amount of time. Rather the "traversal", once proven, is instantaneous. [...]
On 28/04/2026 11:35, Alan Mackenzie wrote:
[...] So anything proven about the first node
automatically applies to the rest of the nodes. There is no time
involved here - it does not take, say, one second to traverse an edge to the next node, hence taking an infinite amount of time. Rather the "traversal", once proven, is instantaneous. [...]
While this is true, I don't see it as an essential part of
mathematics [as opposed to "of standard mathematics"]. Maths happens
to have evolved through Pythagoras/Euclid/Archimedes/Newton/Gauss/...,
and so very early on had to cope with problems of infinities and infinitesimals and links with geometry, physics and so on. So we
developed a standard model which is well understood by professional mathematicians but which is barely taught in our schools and is not understood at all by the general population, or even by professional scientists/engineers/.... It doesn't require too much imagination to contemplate what might have happened if computing [or combinatorial
game theory or ...] had been developed before a rigorous theory of the
real number system. Standard maths might well have been based around
a strictly constructivist theory and/or the surreal [or hyperreal]
numbers, and our current maths might have been an obscure offshoot
attracting mostly derision when cranks tried to espouse it and fell
into one of the many traps. Zeno's paradoxes, the theory of limits,
and so on could have been resolved in quite different ways.
How any of this applies to threads in this group is another
matter, which I don't propose to embark on here.
----
Andy Walker, Nottingham.
Andy's music pages: www.cuboid.me.uk/andy/Music
Composer of the day: www.cuboid.me.uk/andy/Music/Composers/Simpson
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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
I strongly urge you to read and understand an actual proof of
G||del's incompleteness theorem[*].-a There are no looping or
endless directed graphs in these.-a 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 rao -4Prov_PA(riLGriY)
Directed Graph of evaluation sequence
00 rao-a-a-a-a-a-a-a-a-a-a-a-a-a-a 01 02
01 G
02 -4-a-a-a-a-a-a-a-a-a-a-a-a-a-a 03
03 Prov_PA-a-a-a-a-a-a-a-a 04
04 G||del_Number_of 01-a // 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)
-+ roCraA -+ roCraA -+ roCraA -+ roCraA ...
[...]
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.
[...]
I think I disagree with your general argument here. I think you're suggestinig that the way maths has evolved was just one of many
possible, and that any of these ways could have become the dominant way.
I think that the emergence of rigour in mathematics was always going to
have developed to the result we now have, that it was somehow
inevitable.
I have no evidence to back that up, however.
On 28/04/2026 20:48, Alan Mackenzie wrote:All is simple,nothing mysterious or bizarre:
[... snippage ...]
I think I disagree with your general argument here.-a I think you're suggestinig that the way maths has evolved was just one of many
possible, and that any of these ways could have become the dominant way.
Broadly, that is indeed my suggestion, though "many" would be
too much to claim [unless we count every detail as a different possible
way].
I think that the emergence of rigour in mathematics was always going to have developed to the result we now have, that it was somehow
inevitable.
When irrational numbers were discovered, it was a major upset
to established maths.-a But irrational numbers were too useful to be discarded, so had to be incorporated.-a Infinitesimals were awkward to incorporate, so were discarded /by axiom/ [they were less useful in
the time before calculus];-a but there is no necessity for this, and
they sit quite happily in the surreals [and less happily, IMO, in the hyperreals], and the theory is perfectly rigorous.-a So ISTM that we
could easily have gone down at least three quite different routes had
things happened in a different order.-a None of this would have affected
what we might call engineering maths;-a bridges, railways and rockets
would still work in exactly the same way.-a But the theories of calculus
and limits would look [and be taught] quite different[ly].
Going somewhat the other way, if computers had been in use
earlier, we might have been worried by uncomputable numbers [which
after all are almost all of the reals], and ruled them out [again,
by axiom].-a Again, this doesn't affect engineering, or science more generally;-a all normal maths is computable apart from exotica such
as general Busy Beaver numbers.-a But it gets worse;-a almost all real numbers are [literally] indescribable.-a It's at least plausible that
a society might decide that "numbers" of which no example can be
given, still less calculated, don't deserve to be called "real"!-a The rigorous maths that would have developed in such a society would have
been the same as ours for all normal engineering and science, but
would have been quite different in its axioms and theorems;-a and
people who tried to argue that we should discuss [what we call] the
set of real numbers would be dismissed as misguided.
To step back a little to our previous articles, ISTM that
numbers defined by computable algorithms are intrinsically built
step by step and the idea that the steps can be carried out all at
the same time would seem absurd.-a Maths would have to cope with such algorithmic definitions.-a [As, in real life, it already does;-a it's
the rigorous theory that short-circuits the steps.]
I have no evidence to back that up, however.
I think I have given evidence to the contrary!-a YMMV.
| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 64 |
| Nodes: | 6 (0 / 6) |
| Uptime: | 492918:25:13 |
| Calls: | 842 |
| Files: | 1,304 |
| D/L today: |
8 files (14,225K bytes) |
| Messages: | 264,885 |