On 4/15/2026 2:11 AM, Mikko wrote:
On 14/04/2026 16:41, olcott wrote:
On 4/14/2026 1:04 AM, Mikko wrote:
On 13/04/2026 18:01, olcott wrote:
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
typedef int (*ptr)();
int HHH(ptr P);
int DD()
{
-a-a int Halt_Status = HHH(DD);
-a-a if (Halt_Status)
-a-a-a-a HERE: goto HERE;
-a-a return Halt_Status;
}
int main()
{
-a-a HHH(DD);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>>> tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic
Semantics as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know
everythihg that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve >>>>>> the halting problem.
Tarski Undefinability, G||del 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
Everything derived from axioms and postulates with truth preserving
inferences is true in every interpretation where the axioms are true.
G||del doesn't do that. His definition of true sneaks
off somewhere else into a meta-math model.
How is a definition of "true" relevant to G||del's incomleteness
theorem?
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F. https://plato.stanford.edu/entries/goedel-incompleteness/
On 4/15/2026 2:11 AM, Mikko wrote:
On 14/04/2026 16:41, olcott wrote:
On 4/14/2026 1:04 AM, Mikko wrote:
On 13/04/2026 18:01, olcott wrote:
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
typedef int (*ptr)();
int HHH(ptr P);
int DD()
{
-a-a int Halt_Status = HHH(DD);
-a-a if (Halt_Status)
-a-a-a-a HERE: goto HERE;
-a-a return Halt_Status;
}
int main()
{
-a-a HHH(DD);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>>> tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic
Semantics as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know
everythihg that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve >>>>>> the halting problem.
Tarski Undefinability, G||del 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
Everything derived from axioms and postulates with truth preserving
inferences is true in every interpretation where the axioms are true.
G||del doesn't do that. His definition of true sneaks
off somewhere else into a meta-math model.
How is a definition of "true" relevant to G||del's incomleteness
theorem?
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F. https://plato.stanford.edu/entries/goedel-incompleteness/
Olcott's Minimal Type Theory
G rao -4Prov[PA](riLGriY)
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
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 04
04 G||del_Number_of 01-a // cycle
Proof Theoretic Semantics prover rejects the above
expression because it has a cycle in the directed
graph of its evaluation sequence.
On 4/15/2026 2:11 AM, Mikko wrote:
On 14/04/2026 16:41, olcott wrote:
On 4/14/2026 1:04 AM, Mikko wrote:
On 13/04/2026 18:01, olcott wrote:
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
typedef int (*ptr)();
int HHH(ptr P);
int DD()
{
-a-a int Halt_Status = HHH(DD);
-a-a if (Halt_Status)
-a-a-a-a HERE: goto HERE;
-a-a return Halt_Status;
}
int main()
{
-a-a HHH(DD);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>>> tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic
Semantics as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know
everythihg that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve >>>>>> the halting problem.
Tarski Undefinability, G||del 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
Everything derived from axioms and postulates with truth preserving
inferences is true in every interpretation where the axioms are true.
G||del doesn't do that. His definition of true sneaks
off somewhere else into a meta-math model.
How is a definition of "true" relevant to G||del's incomleteness
theorem?
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F. https://plato.stanford.edu/entries/goedel-incompleteness/
Olcott's Minimal Type Theory
G rao -4Prov[PA](riLGriY) https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
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 04
04 G||del_Number_of 01-a // cycle
Proof Theoretic Semantics prover rejects the above
expression because it has a cycle in the directed
graph of its evaluation sequence.
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its definition
is irrelevant to the first incompletness theorem.
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its definition
is irrelevant to the first incompletness theorem.
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 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 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its definition >>> is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its
definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
A cycle is detected in the directed graphs of its
evaluation sequence proving that it does not represent
a well-founded justification tree.
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its
definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be meaningful
in the sempantics of natural number arithmetic.
A cycle is detected in the directed graphs of its
evaluation sequence proving that it does not represent
a well-founded justification tree.
From the syntax rules of the first order logic follows that there are
no cycles in any sentence in the language of the first order Peano arithmetic, which is the language of G||del's sentence. Therefore there
is no cycle in G||del's sentence.
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its
definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its
definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its
definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of provability?
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its
definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
By the rules of PA the sentence G re? -4G where G is G||del's sentence
is a theorem.
It is provable (and actually proven by G||del( in the metatheory
that neither G nor -4G is provable in Peano arithmetic. This follows
from the way G is constructed.
On 4/19/2026 4:33 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its >>>>>>>> definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be meaningful >>>> in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
By the rules of PA the sentence G re? -4G where G is G||del's sentence
is a theorem.
It is provable (and actually proven by G||del( in the metatheory
that neither G nor -4G is provable in Peano arithmetic. This follows
from the way G is constructed.
Yet switching to a meta-theory is cheating in PTS.
When G and ~G cannot be proven directly in PA then inRegardless what PTS says, as an arithmetic sentence G has an arithmetic meaning.
the standard conventional PTS G has no meaning in PA.
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its >>>>>>>> definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be meaningful >>>> in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of
provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
On 19/04/2026 20:22, olcott wrote:
On 4/19/2026 4:33 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its >>>>>>>>> definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be meaningful >>>>> in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
By the rules of PA the sentence G re? -4G where G is G||del's sentence
is a theorem.
It is provable (and actually proven by G||del( in the metatheory
that neither G nor -4G is provable in Peano arithmetic. This follows
from the way G is constructed.
Yet switching to a meta-theory is cheating in PTS.
As PTS is a metatheory, switching to PTS is cheating.
Use of metatheory is needed in order to answer qeusstions about a
theory, for example whether G is a theorem of Peano arithmetic, and questions about two or more theories, for example whether two theories
are equivalent.
When G and ~G cannot be proven directly in PA then inRegardless what PTS says, as an arithmetic sentence G has an arithmetic meaning.
the standard conventional PTS G has no meaning in PA.
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its >>>>>>>>> definition
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be meaningful >>>>> in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of
provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question
about the input is needed.
On 4/20/2026 4:00 AM, Mikko wrote:
On 19/04/2026 20:22, olcott wrote:
On 4/19/2026 4:33 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
That's right. You did no not use the word "true" above so its >>>>>>>>>> definition
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be
meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
By the rules of PA the sentence G re? -4G where G is G||del's sentence >>>> is a theorem.
It is provable (and actually proven by G||del( in the metatheory
that neither G nor -4G is provable in Peano arithmetic. This follows
from the way G is constructed.
Yet switching to a meta-theory is cheating in PTS.
As PTS is a metatheory, switching to PTS is cheating.
Use of metatheory is needed in order to answer qeusstions about a
theory, for example whether G is a theorem of Peano arithmetic, and
questions about two or more theories, for example whether two theories
are equivalent.
When G and ~G cannot be proven directly in PA then inRegardless what PTS says, as an arithmetic sentence G has an arithmetic
the standard conventional PTS G has no meaning in PA.
meaning.
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 4/20/2026 4:10 AM, Mikko wrote:
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
That's right. You did no not use the word "true" above so its >>>>>>>>>> definition
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be
meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of
provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question
about the input is needed.
OK then that would mean that your own inability
to answer this question makes you stupid:
"What time is it (yes or no)?"
On 20/04/2026 19:55, olcott wrote:
On 4/20/2026 4:00 AM, Mikko wrote:
On 19/04/2026 20:22, olcott wrote:
On 4/19/2026 4:33 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
That's right. You did no not use the word "true" above so its >>>>>>>>>>> definition
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>>
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be
meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
By the rules of PA the sentence G re? -4G where G is G||del's sentence >>>>> is a theorem.
It is provable (and actually proven by G||del( in the metatheory
that neither G nor -4G is provable in Peano arithmetic. This follows >>>>> from the way G is constructed.
Yet switching to a meta-theory is cheating in PTS.
As PTS is a metatheory, switching to PTS is cheating.
Use of metatheory is needed in order to answer qeusstions about a
theory, for example whether G is a theorem of Peano arithmetic, and
questions about two or more theories, for example whether two theories
are equivalent.
When G and ~G cannot be proven directly in PA then inRegardless what PTS says, as an arithmetic sentence G has an arithmetic
the standard conventional PTS G has no meaning in PA.
meaning.
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 arithmetic semantics assigns meanings to symbols like 0 or + as
well as tems and formulas. Does proof-theoretic semantics do that?
On 20/04/2026 20:22, olcott wrote:
On 4/20/2026 4:10 AM, Mikko wrote:
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
That's right. You did no not use the word "true" above so its >>>>>>>>>>> definition
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>>
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be
meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of
provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question
about the input is needed.
OK then that would mean that your own inability
to answer this question makes you stupid:
"What time is it (yes or no)?"
Answers or non-answers to questions don't make stupid. They may
reveal already existing stupidity, though that usually takes
more than one question. Whoever asks the above question is likely
to look stupid.
KnownTrue-a-a := +o ree PA(+o reu -a)
KnownFalse-a := +o ree PA(+o reu -4-a)
Unknown-a-a-a-a := KnownTrue(PA, -a) reo KnownFalse(PA, -a)
Some of Unknown is semantically incoherent
On 2026-04-21 07:43, olcott wrote:
KnownTrue-a-a := +o ree PA(+o reu -a)
KnownFalse-a := +o ree PA(+o reu -4-a)
Unknown-a-a-a-a := KnownTrue(PA, -a) reo KnownFalse(PA, -a)
Some of Unknown is semantically incoherent
You may think the above means something by it really doesn't.
Andr|-
On 4/21/2026 2:48 PM, Andr|- G. Isaak wrote:
On 2026-04-21 07:43, olcott wrote:
KnownTrue-a-a := +o ree PA(+o reu -a)
KnownFalse-a := +o ree PA(+o reu -4-a)
Unknown-a-a-a-a := KnownTrue(PA, -a) reo KnownFalse(PA, -a)
Some of Unknown is semantically incoherent
You may think the above means something by it really doesn't.
Andr|-
It had a severe typo on its last line.
That you do not know what it means is
no measure what-so-ever that it has no meaning.
KnownTrue := +orea ree PA(+o reu -a)
KnownFalse := rea+o ree PA(+o reu -4-a)
Unknown(PA, -a)-a := -4KnownTrue(PA, -a) reo -4KnownFalse(PA, -a)
On 2026-04-21 15:37, olcott wrote:
On 4/21/2026 2:48 PM, Andr|- G. Isaak wrote:
On 2026-04-21 07:43, olcott wrote:
KnownTrue-a-a := +o ree PA(+o reu -a)
KnownFalse-a := +o ree PA(+o reu -4-a)
Unknown-a-a-a-a := KnownTrue(PA, -a) reo KnownFalse(PA, -a)
Some of Unknown is semantically incoherent
You may think the above means something by it really doesn't.
Andr|-
It had a severe typo on its last line.
That you do not know what it means is
no measure what-so-ever that it has no meaning.
KnownTrue := +orea ree PA(+o reu -a)
That's not what you wrote above (you've added the quantifier rea), and it still doesn't mean anything coherent.
You're apparently defining some constant called "KnownTrue" to mean that 'there exists +o' is a proper subset of some undefined set called PA(+o reu -a)
"There exists +o" isn't the sort of thing that can be a proper subset of something else. It's q quantifier which expects a formula as an
argument, not an operators like ree.
You *might* be trying to say something along the lines of
KnownTrue(-a) := +orea PA(+o reu -a)
but that's not what you wrote. And you've left it up to the reader to determine what PA is supposed to refer to. I am assuming you might
intend PA(+o reu -a) to mean something along the lines of -a is provable from
+o in Peano Arithmetic, but you need to actually state that.
KnownFalse := rea+o ree PA(+o reu -4-a)
Same problem as with the previous
Unknown(PA, -a)-a := -4KnownTrue(PA, -a) reo -4KnownFalse(PA, -a)
Which isn't at all what you wrote originally.
Andr|-
On 4/21/2026 2:09 AM, Mikko wrote:
On 20/04/2026 20:22, olcott wrote:
On 4/20/2026 4:10 AM, Mikko wrote:
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
That's right. You did no not use the word "true" above so >>>>>>>>>>>> its definition
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>>>
is irrelevant to the first incompletness theorem.
Olcott's Minimal Type Theory
G rao -4Prov[PA](riLGriY)
Directed Graph of evaluation sequence
00 rao 01 02
01 G
02 -4 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be
meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of
provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question
about the input is needed.
OK then that would mean that your own inability
to answer this question makes you stupid:
"What time is it (yes or no)?"
Answers or non-answers to questions don't make stupid. They may
reveal already existing stupidity, though that usually takes
more than one question. Whoever asks the above question is likely
to look stupid.
The problem with "undecidability" is that it requires
correct answers to incorrect questions. When we toss
out the inputs whose inference steps within the semantics
of the inference language do not specify a well-founded
justification tree, then we reject this input as
not-well-formed.
On 2026-04-21 15:37, olcott wrote:
On 4/21/2026 2:48 PM, Andr|- G. Isaak wrote:
On 2026-04-21 07:43, olcott wrote:
KnownTrue-a-a := +o ree PA(+o reu -a)
KnownFalse-a := +o ree PA(+o reu -4-a)
Unknown-a-a-a-a := KnownTrue(PA, -a) reo KnownFalse(PA, -a)
Some of Unknown is semantically incoherent
You may think the above means something by it really doesn't.
Andr|-
It had a severe typo on its last line.
That you do not know what it means is
no measure what-so-ever that it has no meaning.
KnownTrue := +orea ree PA(+o reu -a)
That's not what you wrote above (you've added the quantifier rea), and it still doesn't mean anything coherent.
You're apparently defining some constant called "KnownTrue" to mean that 'there exists +o' is a proper subset of some undefined set called PA(+o reu -a)
"There exists +o" isn't the sort of thing that can be a proper subset of something else. It's q quantifier which expects a formula as an
argument, not an operators like ree.
You *might* be trying to say something along the lines of
KnownTrue(-a) := +orea PA(+o reu -a)
but that's not what you wrote. And you've left it up to the reader to determine what PA is supposed to refer to. I am assuming you might
intend PA(+o reu -a) to mean something along the lines of -a is provable from
+o in Peano Arithmetic, but you need to actually state that.
KnownFalse := rea+o ree PA(+o reu -4-a)
On 04/21/2026 06:47 AM, olcott wrote:
On 4/21/2026 2:09 AM, Mikko wrote:
On 20/04/2026 20:22, olcott wrote:
On 4/20/2026 4:10 AM, Mikko wrote:
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
That's right. You did no not use the word "true" above so >>>>>>>>>>>>> its definition
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>>>>
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be
meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of >>>>>>> provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question
about the input is needed.
OK then that would mean that your own inability
to answer this question makes you stupid:
"What time is it (yes or no)?"
Answers or non-answers to questions don't make stupid. They may
reveal already existing stupidity, though that usually takes
more than one question. Whoever asks the above question is likely
to look stupid.
The problem with "undecidability" is that it requires
correct answers to incorrect questions. When we toss
out the inputs whose inference steps within the semantics
of the inference language do not specify a well-founded
justification tree, then we reject this input as
not-well-formed.
What's a well-founded justification tree
On 4/21/2026 5:03 PM, Andr|- G. Isaak wrote:
On 2026-04-21 15:37, olcott wrote:
On 4/21/2026 2:48 PM, Andr|- G. Isaak wrote:
On 2026-04-21 07:43, olcott wrote:
KnownTrue-a-a := +o ree PA(+o reu -a)
KnownFalse-a := +o ree PA(+o reu -4-a)
Unknown-a-a-a-a := KnownTrue(PA, -a) reo KnownFalse(PA, -a)
Some of Unknown is semantically incoherent
You may think the above means something by it really doesn't.
Andr|-
It had a severe typo on its last line.
That you do not know what it means is
no measure what-so-ever that it has no meaning.
KnownTrue := +orea ree PA(+o reu -a)
That's not what you wrote above (you've added the quantifier rea), and
it still doesn't mean anything coherent.
You're apparently defining some constant called "KnownTrue" to mean
that 'there exists +o' is a proper subset of some undefined set called
PA(+o reu -a)
"There exists +o" isn't the sort of thing that can be a proper subset
of something else. It's q quantifier which expects a formula as an
argument, not an operators like ree.
You *might* be trying to say something along the lines of
KnownTrue(-a) := +orea PA(+o reu -a)
but that's not what you wrote. And you've left it up to the reader to
determine what PA is supposed to refer to. I am assuming you might
intend PA(+o reu -a) to mean something along the lines of -a is provable
from +o in Peano Arithmetic, but you need to actually state that.
KnownFalse := rea+o ree PA(+o reu -4-a)
KnownTrue(PA, -a) := rea+o ree PA(+o reu -a)
There exists a sequence of inference steps in PA
such that a back-chained sequence of these steps
reaches the axioms of PA.
On 2026-04-21 17:14, olcott wrote:
On 4/21/2026 5:03 PM, Andr|- G. Isaak wrote:
On 2026-04-21 15:37, olcott wrote:
On 4/21/2026 2:48 PM, Andr|- G. Isaak wrote:
On 2026-04-21 07:43, olcott wrote:
KnownTrue-a-a := +o ree PA(+o reu -a)
KnownFalse-a := +o ree PA(+o reu -4-a)
Unknown-a-a-a-a := KnownTrue(PA, -a) reo KnownFalse(PA, -a)
Some of Unknown is semantically incoherent
You may think the above means something by it really doesn't.
Andr|-
It had a severe typo on its last line.
That you do not know what it means is
no measure what-so-ever that it has no meaning.
KnownTrue := +orea ree PA(+o reu -a)
That's not what you wrote above (you've added the quantifier rea), and
it still doesn't mean anything coherent.
You're apparently defining some constant called "KnownTrue" to mean
that 'there exists +o' is a proper subset of some undefined set called
PA(+o reu -a)
"There exists +o" isn't the sort of thing that can be a proper subset
of something else. It's q quantifier which expects a formula as an
argument, not an operators like ree.
You *might* be trying to say something along the lines of
KnownTrue(-a) := +orea PA(+o reu -a)
but that's not what you wrote. And you've left it up to the reader to
determine what PA is supposed to refer to. I am assuming you might
intend PA(+o reu -a) to mean something along the lines of -a is provable >>> from +o in Peano Arithmetic, but you need to actually state that.
KnownFalse := rea+o ree PA(+o reu -4-a)
KnownTrue(PA, -a) := rea+o ree PA(+o reu -a)
There exists a sequence of inference steps in PA
such that a back-chained sequence of these steps
reaches the axioms of PA.
The point is that you always insist on writing things as formulae when
more often than not you mangle them into something unintelligible.
You simply don't know how to write formulae and you be better off to
simply stop doing so until you actually become competent at it. You're
much better off simply writing what you mean in clear English and
dispensing with all the formalism.
And what you have above still makes no sense. why is there a ree there?
You can't follow rea+o with a ree.
On reflection, I wonder if you might be trying to say:
KnownTrue(PA, -a) := rea+o reu -a((+o ree PA) reo (+o reu -a))
Just stick to English.
What you write usually requires more guesswork to
interpret than anyone should be required to do.
Andr|-
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:14, olcott wrote:
On 4/21/2026 5:03 PM, Andr|- G. Isaak wrote:
On 2026-04-21 15:37, olcott wrote:
On 4/21/2026 2:48 PM, Andr|- G. Isaak wrote:
On 2026-04-21 07:43, olcott wrote:
KnownTrue-a-a := +o ree PA(+o reu -a)
KnownFalse-a := +o ree PA(+o reu -4-a)
Unknown-a-a-a-a := KnownTrue(PA, -a) reo KnownFalse(PA, -a)
Some of Unknown is semantically incoherent
You may think the above means something by it really doesn't.
Andr|-
It had a severe typo on its last line.
That you do not know what it means is
no measure what-so-ever that it has no meaning.
KnownTrue := +orea ree PA(+o reu -a)
That's not what you wrote above (you've added the quantifier rea), and >>>> it still doesn't mean anything coherent.
You're apparently defining some constant called "KnownTrue" to mean
that 'there exists +o' is a proper subset of some undefined set
called PA(+o reu -a)
"There exists +o" isn't the sort of thing that can be a proper subset >>>> of something else. It's q quantifier which expects a formula as an
argument, not an operators like ree.
You *might* be trying to say something along the lines of
KnownTrue(-a) := +orea PA(+o reu -a)
but that's not what you wrote. And you've left it up to the reader
to determine what PA is supposed to refer to. I am assuming you
might intend PA(+o reu -a) to mean something along the lines of -a is >>>> provable from +o in Peano Arithmetic, but you need to actually state
that.
KnownFalse := rea+o ree PA(+o reu -4-a)
KnownTrue(PA, -a) := rea+o ree PA(+o reu -a)
There exists a sequence of inference steps in PA
such that a back-chained sequence of these steps
reaches the axioms of PA.
The point is that you always insist on writing things as formulae when
more often than not you mangle them into something unintelligible.
You simply don't know how to write formulae and you be better off to
simply stop doing so until you actually become competent at it. You're
much better off simply writing what you mean in clear English and
dispensing with all the formalism.
And what you have above still makes no sense. why is there a ree there?
You can't follow rea+o with a ree.
On reflection, I wonder if you might be trying to say:
KnownTrue(PA, -a) := rea+o reu -a((+o ree PA) reo (+o reu -a))
There exists a sequence of back-chained inference
steps +o in PA such that -a reaches the axioms of PA
Just stick to English.
I am writing for publication in academic journals.
On 2026-04-21 17:52, olcott wrote:
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:14, olcott wrote:
On 4/21/2026 5:03 PM, Andr|- G. Isaak wrote:
On 2026-04-21 15:37, olcott wrote:
On 4/21/2026 2:48 PM, Andr|- G. Isaak wrote:
On 2026-04-21 07:43, olcott wrote:
KnownTrue-a-a := +o ree PA(+o reu -a)
KnownFalse-a := +o ree PA(+o reu -4-a)
Unknown-a-a-a-a := KnownTrue(PA, -a) reo KnownFalse(PA, -a)
Some of Unknown is semantically incoherent
You may think the above means something by it really doesn't.
Andr|-
It had a severe typo on its last line.
That you do not know what it means is
no measure what-so-ever that it has no meaning.
KnownTrue := +orea ree PA(+o reu -a)
That's not what you wrote above (you've added the quantifier rea),
and it still doesn't mean anything coherent.
You're apparently defining some constant called "KnownTrue" to mean >>>>> that 'there exists +o' is a proper subset of some undefined set
called PA(+o reu -a)
"There exists +o" isn't the sort of thing that can be a proper
subset of something else. It's q quantifier which expects a formula >>>>> as an argument, not an operators like ree.
You *might* be trying to say something along the lines of
KnownTrue(-a) := +orea PA(+o reu -a)
but that's not what you wrote. And you've left it up to the reader
to determine what PA is supposed to refer to. I am assuming you
might intend PA(+o reu -a) to mean something along the lines of -a is >>>>> provable from +o in Peano Arithmetic, but you need to actually state >>>>> that.
KnownFalse := rea+o ree PA(+o reu -4-a)
KnownTrue(PA, -a) := rea+o ree PA(+o reu -a)
There exists a sequence of inference steps in PA
such that a back-chained sequence of these steps
reaches the axioms of PA.
The point is that you always insist on writing things as formulae
when more often than not you mangle them into something unintelligible.
You simply don't know how to write formulae and you be better off to
simply stop doing so until you actually become competent at it.
You're much better off simply writing what you mean in clear English
and dispensing with all the formalism.
And what you have above still makes no sense. why is there a ree there? >>> You can't follow rea+o with a ree.
On reflection, I wonder if you might be trying to say:
KnownTrue(PA, -a) := rea+o reu -a((+o ree PA) reo (+o reu -a))
The above is not a quote from me. Please do not attribute it to me. You
have edited what I actually wrote (and again turned it into something incoherent).
There exists a sequence of back-chained inference
steps +o in PA such that -a reaches the axioms of PA
Just stick to English.
I am writing for publication in academic journals.
Coherent English prose is going to have far more credibility than
malformed, incoherent formulae.
Andr|-
On 4/21/2026 7:01 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:52, olcott wrote:
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
Just stick to English.
I am writing for publication in academic journals.
Coherent English prose is going to have far more credibility than
malformed, incoherent formulae.
Andr|-
So there does not currently exist any current
and correct symbolic way to say that?
On 2026-04-21 19:36, olcott wrote:
On 4/21/2026 7:01 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:52, olcott wrote:
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
Just stick to English.
I am writing for publication in academic journals.
Coherent English prose is going to have far more credibility than
malformed, incoherent formulae.
Andr|-
So there does not currently exist any current
and correct symbolic way to say that?
I'm saying you should stop *worrying* about how to say it symbolically (since you always make a mess of it)
and focus instead on making a
coherent argument. If you ever manage to convince someone that your
argument has merit, *then* you can work on expressing it symbolically,
but since that's clearly not your forte, let it go for now. You're not currently writing for publication in academic journals; you're posting
on usenet.
Andr|-
On 4/21/2026 8:59 PM, Andr|- G. Isaak wrote:
On 2026-04-21 19:36, olcott wrote:
On 4/21/2026 7:01 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:52, olcott wrote:
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
Just stick to English.
I am writing for publication in academic journals.
Coherent English prose is going to have far more credibility than
malformed, incoherent formulae.
Andr|-
So there does not currently exist any current
and correct symbolic way to say that?
I'm saying you should stop *worrying* about how to say it symbolically
(since you always make a mess of it)
If I only say it with words math people will dismiss it as
simplistic. I must say it with complete mathematical rigor.
On 2026-04-21 20:11, olcott wrote:
On 4/21/2026 8:59 PM, Andr|- G. Isaak wrote:
On 2026-04-21 19:36, olcott wrote:
On 4/21/2026 7:01 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:52, olcott wrote:
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
Just stick to English.
I am writing for publication in academic journals.
Coherent English prose is going to have far more credibility than
malformed, incoherent formulae.
Andr|-
So there does not currently exist any current
and correct symbolic way to say that?
I'm saying you should stop *worrying* about how to say it
symbolically (since you always make a mess of it)
If I only say it with words math people will dismiss it as
simplistic. I must say it with complete mathematical rigor.
People aren't going to dismiss it for using words rather than formulae. They'll dismiss it for being incoherent.
So far you have not managed to
state anything in a way that remotely resembles mathematical rigor;
You've just perfected the art of writing syntactically ill-formed
"formulae" which are largely gibberish.
If you're really determined to write things in formulae, you should
first take a course or two in introductory logic where you might
actually learn how logical notation works.
Andr|-
On 2026-04-21 20:11, olcott wrote:
On 4/21/2026 8:59 PM, Andr|- G. Isaak wrote:
On 2026-04-21 19:36, olcott wrote:
On 4/21/2026 7:01 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:52, olcott wrote:
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
Just stick to English.
I am writing for publication in academic journals.
Coherent English prose is going to have far more credibility than
malformed, incoherent formulae.
Andr|-
So there does not currently exist any current
and correct symbolic way to say that?
I'm saying you should stop *worrying* about how to say it
symbolically (since you always make a mess of it)
If I only say it with words math people will dismiss it as
simplistic. I must say it with complete mathematical rigor.
People aren't going to dismiss it for using words rather than formulae. They'll dismiss it for being incoherent. So far you have not managed to
state anything in a way that remotely resembles mathematical rigor;
You've just perfected the art of writing syntactically ill-formed
"formulae" which are largely gibberish.
If you're really determined to write things in formulae, you should
first take a course or two in introductory logic where you might
actually learn how logical notation works.
Andr|-
On 4/21/2026 9:25 PM, Andr|- G. Isaak wrote:
On 2026-04-21 20:11, olcott wrote:
On 4/21/2026 8:59 PM, Andr|- G. Isaak wrote:
On 2026-04-21 19:36, olcott wrote:
On 4/21/2026 7:01 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:52, olcott wrote:
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
Just stick to English.
I am writing for publication in academic journals.
Coherent English prose is going to have far more credibility than
malformed, incoherent formulae.
Andr|-
So there does not currently exist any current
and correct symbolic way to say that?
I'm saying you should stop *worrying* about how to say it
symbolically (since you always make a mess of it)
If I only say it with words math people will dismiss it as
simplistic. I must say it with complete mathematical rigor.
People aren't going to dismiss it for using words rather than
formulae. They'll dismiss it for being incoherent.
Become an expert of Proof Theoretic Semantics before you
judge my work that way.
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
So far you have not managed to state anything in a way that remotely
resembles mathematical rigor; You've just perfected the art of writing
syntactically ill-formed "formulae" which are largely gibberish.
If you're really determined to write things in formulae, you should
first take a course or two in introductory logic where you might
actually learn how logical notation works.
Andr|-
On 04/21/2026 07:25 PM, Andr|- G. Isaak wrote:
On 2026-04-21 20:11, olcott wrote:
On 4/21/2026 8:59 PM, Andr|- G. Isaak wrote:
On 2026-04-21 19:36, olcott wrote:
On 4/21/2026 7:01 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:52, olcott wrote:
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
Just stick to English.
I am writing for publication in academic journals.
Coherent English prose is going to have far more credibility than
malformed, incoherent formulae.
Andr|-
So there does not currently exist any current
and correct symbolic way to say that?
I'm saying you should stop *worrying* about how to say it
symbolically (since you always make a mess of it)
If I only say it with words math people will dismiss it as
simplistic. I must say it with complete mathematical rigor.
People aren't going to dismiss it for using words rather than formulae.
They'll dismiss it for being incoherent. So far you have not managed to
state anything in a way that remotely resembles mathematical rigor;
You've just perfected the art of writing syntactically ill-formed
"formulae" which are largely gibberish.
If you're really determined to write things in formulae, you should
first take a course or two in introductory logic where you might
actually learn how logical notation works.
Andr|-
It's quite agreeable that anything that can be formalized in symbolic notation may be formalized in sufficiently un-ambiguous natural
language. One example account of this is the Herbrand semantics,
which basically intends to relay that any account of formalism has
any number of accounts in natural language. I'm a bit against the
Montague semantics, since it's more the flakier Berkeley school, so
it's often exploiting the empty set and the like with material
implication, so I'd generally rather see a description according to
the Herbrand semantics.
About issues of un-decide-ability beyond "in-sufficient information",
i.e., how people pass the SAT with the process of elimination and
the like or "logic", then there are "quantifier ambiguity" and then
the "impredicativity" to get sorted out, while "syncategorematical"
is quite a dense term here as about quantifier ambiguity and
impredicativity.
It might help to start with familiarization with the little language
of mathematical proof like "there exists" and "such that" and though
usually not to be getting right into "without loss of generality",
then about something like Proclus' account of Euclid for the "quod
erat demonstrandum" and "quod erat fasciendum". For most of 2000
years those would be expected to be known.
On 04/21/2026 07:59 PM, olcott wrote:
On 4/21/2026 9:25 PM, Andr|- G. Isaak wrote:
On 2026-04-21 20:11, olcott wrote:
On 4/21/2026 8:59 PM, Andr|- G. Isaak wrote:
On 2026-04-21 19:36, olcott wrote:
On 4/21/2026 7:01 PM, Andr|- G. Isaak wrote:
On 2026-04-21 17:52, olcott wrote:
On 4/21/2026 6:31 PM, Andr|- G. Isaak wrote:
Just stick to English.
I am writing for publication in academic journals.
Coherent English prose is going to have far more credibility than >>>>>>> malformed, incoherent formulae.
Andr|-
So there does not currently exist any current
and correct symbolic way to say that?
I'm saying you should stop *worrying* about how to say it
symbolically (since you always make a mess of it)
If I only say it with words math people will dismiss it as
simplistic. I must say it with complete mathematical rigor.
People aren't going to dismiss it for using words rather than
formulae. They'll dismiss it for being incoherent.
Become an expert of Proof Theoretic Semantics before you
judge my work that way.
-a-a Proof-theoretic semantics is inherently inferential, as
-a-a it is inferential activity which manifests itself in proofs.
-a-a ...inferences and the rules of inference establish the
-a-a meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
So far you have not managed to state anything in a way that remotely
resembles mathematical rigor; You've just perfected the art of writing
syntactically ill-formed "formulae" which are largely gibberish.
If you're really determined to write things in formulae, you should
first take a course or two in introductory logic where you might
actually learn how logical notation works.
Andr|-
Get off your high horse.-a ("... before you get thrown off" is the usual saying.)
On 4/21/2026 2:09 AM, Mikko wrote:
On 20/04/2026 20:22, olcott wrote:
On 4/20/2026 4:10 AM, Mikko wrote:
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
That's right. You did no not use the word "true" above so >>>>>>>>>>>> its definition
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>>>
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be
meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of
provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question
about the input is needed.
OK then that would mean that your own inability
to answer this question makes you stupid:
"What time is it (yes or no)?"
Answers or non-answers to questions don't make stupid. They may
reveal already existing stupidity, though that usually takes
more than one question. Whoever asks the above question is likely
to look stupid.
The problem with "undecidability" is that it requires
correct answers to incorrect questions.
When we toss out the inputs whose inference steps within thejustification tree, then we reject this input as not-well-formed.
semantics of the inference language do not specify a well-founded>
On 21/04/2026 16:47, olcott wrote:
On 4/21/2026 2:09 AM, Mikko wrote:
On 20/04/2026 20:22, olcott wrote:
On 4/20/2026 4:10 AM, Mikko wrote:
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
That's right. You did no not use the word "true" above so >>>>>>>>>>>>> its definition
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>>>>
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be >>>>>>>>> meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of >>>>>>> provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question
about the input is needed.
OK then that would mean that your own inability
to answer this question makes you stupid:
"What time is it (yes or no)?"
Answers or non-answers to questions don't make stupid. They may
reveal already existing stupidity, though that usually takes
more than one question. Whoever asks the above question is likely
to look stupid.
The problem with "undecidability" is that it requires
correct answers to incorrect questions.
No, it isn't. It does not require any answers to any questions.
It is merely a name of the phenomeon that in some systems there
are syntactically correct sentences that are neither theorems
nor negations of theorems.
When we toss out the inputs whose inference steps within thejustification tree, then we reject this input as not-well-formed.
semantics of the inference language do not specify a well-founded>
Whether something is a theorem does not depend on semantics.
Sometimes it is not known whether some syntactically correct sentence
is a theorem or the negation of a theorem or neither. If you can't
ask the question you will never find out.
On 4/22/2026 2:40 AM, Mikko wrote:
On 21/04/2026 16:47, olcott wrote:
On 4/21/2026 2:09 AM, Mikko wrote:
On 20/04/2026 20:22, olcott wrote:
On 4/20/2026 4:10 AM, Mikko wrote:
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
That's right. You did no not use the word "true" above so >>>>>>>>>>>>>> its definition
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out, >>>>>>>>>>>>>>> there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>>>>>
is irrelevant to the first incompletness theorem.
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be >>>>>>>>>> meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of >>>>>>>> provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question
about the input is needed.
OK then that would mean that your own inability
to answer this question makes you stupid:
"What time is it (yes or no)?"
Answers or non-answers to questions don't make stupid. They may
reveal already existing stupidity, though that usually takes
more than one question. Whoever asks the above question is likely
to look stupid.
The problem with "undecidability" is that it requires
correct answers to incorrect questions.
No, it isn't. It does not require any answers to any questions.
It is merely a name of the phenomeon that in some systems there
are syntactically correct sentences that are neither theorems
nor negations of theorems.
syntactically correct AND semantically incoherent
usually through self-contradiction.
When we toss out the inputs whose inference steps within thejustification tree, then we reject this input as not-well-formed.
semantics of the inference language do not specify a well-founded>
Whether something is a theorem does not depend on semantics.
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
Sometimes it is not known whether some syntactically correct sentence
is a theorem or the negation of a theorem or neither. If you can't
ask the question you will never find out.
Self-contradiction inserts cycles in the directed
graph of resolution sequences of expressions.
On 22/04/2026 10:58, olcott wrote:
On 4/22/2026 2:40 AM, Mikko wrote:
On 21/04/2026 16:47, olcott wrote:
On 4/21/2026 2:09 AM, Mikko wrote:
On 20/04/2026 20:22, olcott wrote:
On 4/20/2026 4:10 AM, Mikko wrote:
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:Olcott's Minimal Type Theory
That's right. You did no not use the word "true" above so >>>>>>>>>>>>>>> its definition
The first incompleteness theorem states that in >>>>>>>>>>>>>>>> any consistent formal system F within which a
certain amount of arithmetic can be carried out, >>>>>>>>>>>>>>>> there are statements of the language of F which >>>>>>>>>>>>>>>> can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>>>>>>
is irrelevant to the first incompletness theorem. >>>>>>>>>>>>>>
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be >>>>>>>>>>> meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of >>>>>>>>> provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question >>>>>>> about the input is needed.
OK then that would mean that your own inability
to answer this question makes you stupid:
"What time is it (yes or no)?"
Answers or non-answers to questions don't make stupid. They may
reveal already existing stupidity, though that usually takes
more than one question. Whoever asks the above question is likely
to look stupid.
The problem with "undecidability" is that it requires
correct answers to incorrect questions.
No, it isn't. It does not require any answers to any questions.
It is merely a name of the phenomeon that in some systems there
are syntactically correct sentences that are neither theorems
nor negations of theorems.
syntactically correct AND semantically incoherent
usually through self-contradiction.
If a syntactically corret sentence is semantically incorrect you
are using either wrong syntax or wrong semantics. You should
keep what serves your purposes and change what doesn't.
When we toss out the inputs whose inference steps within thejustification tree, then we reject this input as not-well-formed.
semantics of the inference language do not specify a well-founded>
Whether something is a theorem does not depend on semantics.
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
Nice to see you don't disagree.
Sometimes it is not known whether some syntactically correct sentence
is a theorem or the negation of a theorem or neither. If you can't
ask the question you will never find out.
Self-contradiction inserts cycles in the directed
graph of resolution sequences of expressions.
Which of A re? (-4A re? B), A reo (-4A re? B), and A reo (-4A reo B) has cycles in
its evaluation graph?
On 4/23/2026 2:01 AM, Mikko wrote:
On 22/04/2026 10:58, olcott wrote:
On 4/22/2026 2:40 AM, Mikko wrote:
On 21/04/2026 16:47, olcott wrote:
On 4/21/2026 2:09 AM, Mikko wrote:
On 20/04/2026 20:22, olcott wrote:
On 4/20/2026 4:10 AM, Mikko wrote:
On 19/04/2026 19:51, olcott wrote:
On 4/19/2026 4:36 AM, Mikko wrote:
On 18/04/2026 16:33, olcott wrote:
On 4/18/2026 4:48 AM, Mikko wrote:
On 17/04/2026 17:40, olcott wrote:
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:Olcott's Minimal Type Theory
That's right. You did no not use the word "true" above >>>>>>>>>>>>>>>> so its definition
The first incompleteness theorem states that in >>>>>>>>>>>>>>>>> any consistent formal system F within which a >>>>>>>>>>>>>>>>> certain amount of arithmetic can be carried out, >>>>>>>>>>>>>>>>> there are statements of the language of F which >>>>>>>>>>>>>>>>> can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/ >>>>>>>>>>>>>>>>
is irrelevant to the first incompletness theorem. >>>>>>>>>>>>>>>
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 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.
Nice to see that you don't disagree.
G||del's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
As a sentence of natural number arithmetic it only needs be >>>>>>>>>>>> meaningful
in the sempantics of natural number arithmetic.
Yes and Proof Theoretic Semantics defines its notion
of truth only within the finite inference steps of
the formal system. This means that anything that is
unprovable in PA is untrue in PA.
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
How is proof-theoretic semantics better than the usual concept of >>>>>>>>>> provability?
It has the fully developed complete basis for rejecting
semantically incoherent inputs.
Rejecting an input is not useful when an answwer to some question >>>>>>>> about the input is needed.
OK then that would mean that your own inability
to answer this question makes you stupid:
"What time is it (yes or no)?"
Answers or non-answers to questions don't make stupid. They may
reveal already existing stupidity, though that usually takes
more than one question. Whoever asks the above question is likely
to look stupid.
The problem with "undecidability" is that it requires
correct answers to incorrect questions.
No, it isn't. It does not require any answers to any questions.
It is merely a name of the phenomeon that in some systems there
are syntactically correct sentences that are neither theorems
nor negations of theorems.
syntactically correct AND semantically incoherent
usually through self-contradiction.
If a syntactically corret sentence is semantically incorrect you
are using either wrong syntax or wrong semantics. You should
keep what serves your purposes and change what doesn't.
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.
On 4/23/2026 2:01 AM, Mikko wrote:
On 22/04/2026 10:58, olcott wrote:
On 4/22/2026 2:40 AM, Mikko wrote:
Sometimes it is not known whether some syntactically correct sentence
is a theorem or the negation of a theorem or neither. If you can't
ask the question you will never find out.
Self-contradiction inserts cycles in the directed
graph of resolution sequences of expressions.
Which of A re? (-4A re? B), A reo (-4A re? B), and A reo (-4A reo B) has cycles in
its evaluation graph?
I don't see any cycles.
P re? Q Disjunction introduction is not allowed.
| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 65 |
| Nodes: | 6 (0 / 6) |
| Uptime: | 01:50:13 |
| Calls: | 862 |
| Files: | 1,311 |
| D/L today: |
10 files (20,373K bytes) |
| Messages: | 264,321 |