On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not
make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is involved.
And G is not "out-of-scope": it is a perfectly well-formed sentence
of the language of T. What is out-of-scope, apparently, is merely
anything for which your proposed semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven. Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
...We are therefore confronted with a proposition which
asserts its own unprovability. … (Gödel 1931:40/43)
It would then be possible to reconstruct the
antinomy of the liar in the metalanguage, by
forming in the language itself a sentence x
such that the sentence of the metalanguage
which is correlated with x asserts that x is
not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not
make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is involved. >>>>
And G is not "out-of-scope": it is a perfectly well-formed sentence
of the language of T. What is out-of-scope, apparently, is merely
anything for which your proposed semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven.
Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does notWithin PTS any expression that is neither provable nor refutable
make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed sentence >>>>> of the language of T. What is out-of-scope, apparently, is merely
anything for which your proposed semantics fails to supply an answer. >>>>
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven.
Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not >>>>>> make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently,
is merely anything for which your proposed semantics fails to
supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven.
Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not >>>>>>> make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently, >>>>>>> is merely anything for which your proposed semantics fails to
supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven. >>>>> Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
meaningful in many theories and provable in some of them and
unporvable others.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where
its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently, >>>>>>>> is merely anything for which your proposed semantics fails to >>>>>>>> supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete >>>>>> method to find out whether a sentence or its negation can be proven. >>>>>> Consequently, it is not possible to construct a system that rejects >>>>>> all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It might be the case that its truth value is unknowable. I restricted
my system to "the body of general knowledge that can be expressed in language" to handle these edge cases.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where
its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
*This is the domain of my proposed system*
"the body of general knowledge that can be expressed in language"
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
Like the cycle in the directed graph of the evaluation sequence
of the Liar Paradox formalized in Prolog.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
I created the system of Minimal Type Theory for this exact same
purpose before I knew that Prolog could do this same thing.
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not
make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is involved. >>>>
And G is not "out-of-scope": it is a perfectly well-formed sentence
of the language of T. What is out-of-scope, apparently, is merely
anything for which your proposed semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven.
Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
This applies to
...We are therefore confronted with a proposition which
asserts its own unprovability. … (Gödel 1931:40/43)
It would then be possible to reconstruct the
antinomy of the liar in the metalanguage, by
forming in the language itself a sentence x
such that the sentence of the metalanguage
which is correlated with x asserts that x is
not a true sentence.
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not >>>>>> make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently,
is merely anything for which your proposed semantics fails to
supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven.
Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly.
They used back-chained inference.
In any case when a finite canonical proof is impossible then the
expression never gets semantically grounded.
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does notWithin PTS any expression that is neither provable nor refutable
make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed sentence >>>>> of the language of T. What is out-of-scope, apparently, is merely
anything for which your proposed semantics fails to supply an answer. >>>>
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven.
Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. Proofs are finite strings and strings don't contain
loops.
This applies to
...We are therefore confronted with a proposition which
asserts its own unprovability. … (Gödel 1931:40/43)
No, it does not. The quote is about a sentence and its interpretation,
not about any inference.
It would then be possible to reconstruct the
antinomy of the liar in the metalanguage, by
forming in the language itself a sentence x
such that the sentence of the metalanguage
which is correlated with x asserts that x is
not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Maybe, maybe mot. But whther it would be possible does not matter
as it was not done.
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently, >>>>>>>> is merely anything for which your proposed semantics fails to >>>>>>>> supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete >>>>>> method to find out whether a sentence or its negation can be proven. >>>>>> Consequently, it is not possible to construct a system that rejects >>>>>> all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It might be the case that its truth value is unknowable.
I restricted my system to "the body of general knowledge that can be
expressed in language" to handle these edge cases.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where
its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
*This is the domain of my proposed system*
"the body of general knowledge that can be expressed in language"
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
Like the cycle in the directed graph of the evaluation sequence
of the Liar Paradox formalized in Prolog.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
I created the system of Minimal Type Theory for this exact same
purpose before I knew that Prolog could do this same thing.
On 10/5/2026 3:19 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not >>>>>> make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently,
is merely anything for which your proposed semantics fails to
supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven.
Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. Proofs are finite strings and strings don't contain
loops.
Unprovable and irrefutable in PA entails that
G never acquires semantic meaning in PA.
Semantic meaning is only acquired by two types
of relations between finite strings.
(a) Stipulated relations provide the axiomatic basis.
(b) Semantic relations specified syntactically are
the only inference step that is allowed.
The above is the way that
"true on the basis of meaning expressed in language"
has always worked in actual reality.
This applies to
...We are therefore confronted with a proposition which
asserts its own unprovability. … (Gödel 1931:40/43)
No, it does not. The quote is about a sentence and its interpretation,
not about any inference.
It would then be possible to reconstruct the
antinomy of the liar in the metalanguage, by
forming in the language itself a sentence x
such that the sentence of the metalanguage
which is correlated with x asserts that x is
not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Maybe, maybe mot. But whther it would be possible does not matter... the diagonal lemma, with B(x) instantiated
as it was not done.
to ¬True(x), yields a counterexample to this
equivalence, by giving a "liar" formula S such
that S ⟺ ¬True(g(S)) holds in N.
https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem
He implements this as the basis of his whole proof.
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x https://liarparadox.org/Tarski_275_276.pdf
adapted to become this
x ∉ Pr if and only if p // line 1 of the proof
Here is the Tarski Undefinability Theorem proof
(1) x ∉ Provable if and only if p // assumption (see above)
(2) x ∈ True if and only if p // Tarski's convention T
(3) x ∉ Provable if and only if x ∈ True. // (1) and (2) combined
(4) either x ∉ True or x̄ ∉ True; // axiom: ~True(x) ∨ ~True(~x)
(5) if x ∈ Provable, then x ∈ True; // axiom: Provable(x) → True(x) (6) if x̄ ∈ Provable, then x̄ ∈ True; // axiom: Provable(~x) → True(~x)
(7) x ∈ True
(8) x ∉ Provable
(9) x̄ ∉ Provable
This is the final resolution to the Liar Paradox that
conclusively proves that it never had a truth value.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope,
apparently, is merely anything for which your proposed
semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete >>>>>>> method to find out whether a sentence or its negation can be proven. >>>>>>> Consequently, it is not possible to construct a system that rejects >>>>>>> all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It truth value will be known as soon as its proof has been chekcked and
found good. The proof can be algorithmically compressed as soon as it is found, even before the verification, though that is irrelevant to the knowledge of its truth. Thought it is possible that it will be found to
be unprovable. But none of that affects its meaning and meaningfulness.
What PTS says about its meaning is irrelevant.
It might be the case that its truth value is unknowable.
It even might be possible that we can't ever know whether its truth
value is unknowable.
I restricted my system to "the body of general knowledge that can be
expressed in language" to handle these edge cases.
Then your system needs be updated when something unknonw becames known.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication
https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
Being meaningful is not a limitation, nor is the ability to prove
that the commutativity law is false.
My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
A weaker system has a larger scope of applications, which is often
quite useful.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where
its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
*This is the domain of my proposed system*
"the body of general knowledge that can be expressed in language"
Irrelevant to your attempt to deceive with an ireelevancy.
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
Like the cycle in the directed graph of the evaluation sequence
of the Liar Paradox formalized in Prolog.
Quite unlike. Circular definitions don't define. A cyclic evaluation
graph
is valid and describes a possible evaluation.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
I created the system of Minimal Type Theory for this exact same
purpose before I knew that Prolog could do this same thing.
There are many nice things that are quite simple with Prolog if one
knows Prolog and thinks a little about how.
On 05/10/2026 16:28, olcott wrote:
On 10/5/2026 3:19 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not >>>>>>> make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently, >>>>>>> is merely anything for which your proposed semantics fails to
supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven. >>>>> Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. Proofs are finite strings and strings don't contain
loops.
Unprovable and irrefutable in PA entails that
G never acquires semantic meaning in PA.
PA is a formal theory that doesn't give any meaning to anything.
Meanings come from elsewhere. Peano already had the meanings
when he created his theory.
Semantic meaning is only acquired by two types
of relations between finite strings.
(a) Stipulated relations provide the axiomatic basis.
(b) Semantic relations specified syntactically are
the only inference step that is allowed.
That seems to permit invalid inferences, as those can be specified syntactically.
The above is the way that
"true on the basis of meaning expressed in language"
has always worked in actual reality.
No, "true on basis of meaning expressed in lanuage" has also required
that a meaning is expressed in a langugage.
... the diagonal lemma, with B(x) instantiatedThis applies to
...We are therefore confronted with a proposition which
asserts its own unprovability. … (Gödel 1931:40/43)
No, it does not. The quote is about a sentence and its interpretation,
not about any inference.
It would then be possible to reconstruct the;
antinomy of the liar in the metalanguage, by
forming in the language itself a sentence x
such that the sentence of the metalanguage
which is correlated with x asserts that x is
not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
Maybe, maybe mot. But whther it would be possible does not matter
as it was not done.
to ¬True(x), yields a counterexample to this
equivalence, by giving a "liar" formula S such
that S ⟺ ¬True(g(S)) holds in N.
https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem
He implements this as the basis of his whole proof.
Sort of. But the important point is not where the idea came from
but the result: a sound proof.
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
adapted to become this
x ∉ Pr if and only if p // line 1 of the proof
Here is the Tarski Undefinability Theorem proof
(1) x ∉ Provable if and only if p // assumption (see above)
(2) x ∈ True if and only if p // Tarski's convention T
(3) x ∉ Provable if and only if x ∈ True. // (1) and (2) combined
(4) either x ∉ True or x̄ ∉ True; // axiom: ~True(x) ∨ ~True(~x)
(5) if x ∈ Provable, then x ∈ True; // axiom: Provable(x) → True(x) >> (6) if x̄ ∈ Provable, then x̄ ∈ True; // axiom: Provable(~x) → True(~x)
(7) x ∈ True
(8) x ∉ Provable
(9) x̄ ∉ Provable
This is the final resolution to the Liar Paradox that
conclusively proves that it never had a truth value.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
About the liar paradox it ayss nothing that was not known 2000 years
ago. The new thing was a sound proof of undefinability of truth.
On 10/6/2026 2:59 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>> sentence of the language of T. What is out-of-scope,
apparently, is merely anything for which your proposed
semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete >>>>>>>> method to find out whether a sentence or its negation can be
proven.
Consequently, it is not possible to construct a system that rejects >>>>>>>> all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises >>>>>> to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It truth value will be known as soon as its proof has been chekcked and
found good. The proof can be algorithmically compressed as soon as it is
found, even before the verification, though that is irrelevant to the
knowledge of its truth. Thought it is possible that it will be found to
be unprovable. But none of that affects its meaning and meaningfulness.
What PTS says about its meaning is irrelevant.
A finite proof might not exist.
It may forever remain unknowable
thus outside of the domain of knowledge.
It might be the case that its truth value is unknowable.
It even might be possible that we can't ever know whether its truth
value is unknowable.
I restricted my system to "the body of general knowledge that can be
expressed in language" to handle these edge cases.
Then your system needs be updated when something unknonw becames known.
It is updated the same way that Pluto ceased to be a planet.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication
https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
Being meaningful is not a limitation, nor is the ability to prove
that the commutativity law is false.
Meaningless expressions are outside the body of knowledge.
counter-factual. "Weaker" is stipulated to mean a reduced scope.My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
A weaker system has a larger scope of applications, which is often
quite useful.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where
its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
*This is the domain of my proposed system*
"the body of general knowledge that can be expressed in language"
Irrelevant to your attempt to deceive with an ireelevancy.
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
Like the cycle in the directed graph of the evaluation sequence
of the Liar Paradox formalized in Prolog.
Quite unlike. Circular definitions don't define. A cyclic evaluation
graph
Never terminates thus never derives PTS semantic meaning.
is valid and describes a possible evaluation.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
I created the system of Minimal Type Theory for this exact same
purpose before I knew that Prolog could do this same thing.
There are many nice things that are quite simple with Prolog if one
knows Prolog and thinks a little about how.
So far as far as I know no one has derived that final
resolution of the Liar Paradox besides myself. We could
say that Kripke did this
On 06/10/2026 15:32, olcott wrote:
On 10/6/2026 2:59 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>>> sentence of the language of T. What is out-of-scope,
apparently, is merely anything for which your proposed
semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no
complete
method to find out whether a sentence or its negation can be >>>>>>>>> proven.
Consequently, it is not possible to construct a system that >>>>>>>>> rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises >>>>>>> to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It truth value will be known as soon as its proof has been chekcked and
found good. The proof can be algorithmically compressed as soon as it is >>> found, even before the verification, though that is irrelevant to the
knowledge of its truth. Thought it is possible that it will be found to
be unprovable. But none of that affects its meaning and meaningfulness.
What PTS says about its meaning is irrelevant.
A finite proof might not exist.
It may forever remain unknowable
thus outside of the domain of knowledge.
Maybe, maybe not. If it ever will be found it is in the domain
of knowledge and has always been.
It might be the case that its truth value is unknowable.
It even might be possible that we can't ever know whether its truth
value is unknowable.
I restricted my system to "the body of general knowledge that can be
expressed in language" to handle these edge cases.
Then your system needs be updated when something unknonw becames known.
It is updated the same way that Pluto ceased to be a planet.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication
https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
Being meaningful is not a limitation, nor is the ability to prove
that the commutativity law is false.
Meaningless expressions are outside the body of knowledge.
Some knowledge about meaningful expression, their properties, and
relations between them is in the bdoy of knowledge.
counter-factual. "Weaker" is stipulated to mean a reduced scope.My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
A weaker system has a larger scope of applications, which is often
quite useful.
No, it is not. When applied to theories it is stipulated to mean lesser provability.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where
its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
*This is the domain of my proposed system*
"the body of general knowledge that can be expressed in language"
Irrelevant to your attempt to deceive with an ireelevancy.
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
Like the cycle in the directed graph of the evaluation sequence
of the Liar Paradox formalized in Prolog.
Quite unlike. Circular definitions don't define. A cyclic evaluation
graph
Never terminates thus never derives PTS semantic meaning.
THe main similatity is that both evaluation graphs and PTS semantic
meanings are irrelevant to PA and provability.
is valid and describes a possible evaluation.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
I created the system of Minimal Type Theory for this exact same
purpose before I knew that Prolog could do this same thing.
There are many nice things that are quite simple with Prolog if one
knows Prolog and thinks a little about how.
So far as far as I know no one has derived that final
resolution of the Liar Paradox besides myself. We could
say that Kripke did this
No one, including you, has derived anything important about the liar
paradox during the last 2000 years. The only new results are attempts
to avoid the paradox in new systems, with variable success.
On 10/7/2026 3:49 AM, Mikko wrote:
On 06/10/2026 15:32, olcott wrote:
On 10/6/2026 2:59 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" >>>>>>>>>>>> does not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory >>>>>>>>>>>> is involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>>>> sentence of the language of T. What is out-of-scope,
apparently, is merely anything for which your proposed >>>>>>>>>>>> semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no >>>>>>>>>> complete
method to find out whether a sentence or its negation can be >>>>>>>>>> proven.
Consequently, it is not possible to construct a system that >>>>>>>>>> rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises >>>>>>>> to conclusion and an indirect proof is a similar chain from tne >>>>>>>> negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It truth value will be known as soon as its proof has been chekcked and >>>> found good. The proof can be algorithmically compressed as soon as
it is
found, even before the verification, though that is irrelevant to the
knowledge of its truth. Thought it is possible that it will be found to >>>> be unprovable. But none of that affects its meaning and meaningfulness. >>>> What PTS says about its meaning is irrelevant.
A finite proof might not exist.
It may forever remain unknowable
thus outside of the domain of knowledge.
Maybe, maybe not. If it ever will be found it is in the domain
of knowledge and has always been.
Unless at least one mind contains a truth such as
the ratio of the diameter to the circumference of
a circle back in caveman days I construe this as
outside of the domain of knowledge at the time.
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not >>>>>> make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently,
is merely anything for which your proposed semantics fails to
supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven.
Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently, >>>>>>>> is merely anything for which your proposed semantics fails to >>>>>>>> supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete >>>>>> method to find out whether a sentence or its negation can be proven. >>>>>> Consequently, it is not possible to construct a system that rejects >>>>>> all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It might be the case that its truth value is unknowable. I restricted
my system to "the body of general knowledge that can be expressed in language" to handle these edge cases.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not >>>>>>> make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently, >>>>>>> is merely anything for which your proposed semantics fails to
supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven. >>>>> Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
A sentence of natural number arithmetic has a well defined arithemtic meaning, whether grounded or not. Existence of a proof from some set
of axioms is irrelevant to the arithmetic meaning.
On 07/10/2026 16:10, polcott wrote:
On 10/7/2026 3:49 AM, Mikko wrote:
On 06/10/2026 15:32, olcott wrote:
On 10/6/2026 2:59 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:It truth value will be known as soon as its proof has been chekcked >>>>> and
On 02/10/2026 14:55, olcott wrote:The Goldbach conjecture is meaningful yet its truth value will be
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" >>>>>>>>>>>>> does not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory >>>>>>>>>>>>> is involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>>>>> sentence of the language of T. What is out-of-scope, >>>>>>>>>>>>> apparently, is merely anything for which your proposed >>>>>>>>>>>>> semantics fails to supply an answer.
Within PTS any expression that is neither provable nor >>>>>>>>>>>> refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no >>>>>>>>>>> complete
method to find out whether a sentence or its negation can be >>>>>>>>>>> proven.
Consequently, it is not possible to construct a system that >>>>>>>>>>> rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises >>>>>>>>> to conclusion and an indirect proof is a similar chain from tne >>>>>>>>> negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to >>>>>>
unknown unless and until it proof can be algorithmically compressed. >>>>>
found good. The proof can be algorithmically compressed as soon as
it is
found, even before the verification, though that is irrelevant to the >>>>> knowledge of its truth. Thought it is possible that it will be
found to
be unprovable. But none of that affects its meaning and
meaningfulness.
What PTS says about its meaning is irrelevant.
A finite proof might not exist.
It may forever remain unknowable
thus outside of the domain of knowledge.
Maybe, maybe not. If it ever will be found it is in the domain
of knowledge and has always been.
Unless at least one mind contains a truth such as
the ratio of the diameter to the circumference of
a circle back in caveman days I construe this as
outside of the domain of knowledge at the time.
An obvious attempt to decive (this time a change of subject) does not
work. In order to decive one needs to behave as a honest person would.
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope,
apparently, is merely anything for which your proposed
semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete >>>>>>> method to find out whether a sentence or its negation can be proven. >>>>>>> Consequently, it is not possible to construct a system that rejects >>>>>>> all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It might be the case that its truth value is unknowable. I restricted
my system to "the body of general knowledge that can be expressed in
language" to handle these edge cases.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication
https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
Does that include cases where X is Peano arithmetic and Y is a
proof that G is true about natural number?
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to object
to (Gödel, Tarski) make any claims about knowledge. Tarski is concerned with truth and Gödel with theoremhood.
André
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to object
to (Gödel, Tarski) make any claims about knowledge. Tarski is
concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
On 2026-10-09 10:03, olcott wrote:
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to
object to (Gödel, Tarski) make any claims about knowledge. Tarski is
concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The entire body of general knowledge is not a well-defined set. Sets are static entities defined by a binary membership operator, whereas 'the
entire body of general knowledge' is a loosely defined entity which
changes from day to day as new things
are learned and old things forgotten.Once in the system it is never forgotten.
It is also filled with contradictory propositions, so this isIt will have knowledge of these propositions and with my work
never going to be the basis for anything computable.
André
On 10/9/2026 6:40 PM, André G. Isaak wrote:
On 2026-10-09 10:03, olcott wrote:
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to
object to (Gödel, Tarski) make any claims about knowledge. Tarski is >>>> concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The entire body of general knowledge is not a well-defined set. Sets
are static entities defined by a binary membership operator, whereas
'the entire body of general knowledge' is a loosely defined entity
which changes from day to day as new things
It can be updated. Anything not known to be true
is outside the scope.
are learned and old things forgotten.Once in the system it is never forgotten.
It is also filled with contradictory propositions, so this isIt will have knowledge of these propositions and with my work
how to resolve some if not all of them.
never going to be the basis for anything computable.
On 2026-10-09 19:31, olcott wrote:
On 10/9/2026 6:40 PM, André G. Isaak wrote:
On 2026-10-09 10:03, olcott wrote:
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to
object to (Gödel, Tarski) make any claims about knowledge. Tarski
is concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The entire body of general knowledge is not a well-defined set. Sets
are static entities defined by a binary membership operator, whereas
'the entire body of general knowledge' is a loosely defined entity
which changes from day to day as new things
It can be updated. Anything not known to be true
is outside the scope.
are learned and old things forgotten.Once in the system it is never forgotten.
So for example, in the nineteenth century the existence of the
luminiferous ether was well known and widely accepted. Are you claiming
it is still part of 'the entire body of general knowledge'?
It is also filled with contradictory propositions, so this isIt will have knowledge of these propositions and with my work
how to resolve some if not all of them.
never going to be the basis for anything computable.
I don't follow what you mean by this. Are the basic tenets of General Relativity part of the body of general knowledge? Are the basic tenets
of Quantum Mechanics part of the body of general knowledge?
Both are widely accepted but we know both cannot be entirely correct
since they contradict one another.
André
On 2026-10-09 19:31, olcott wrote:
On 10/9/2026 6:40 PM, André G. Isaak wrote:
On 2026-10-09 10:03, olcott wrote:
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to
object to (Gödel, Tarski) make any claims about knowledge. Tarski
is concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The entire body of general knowledge is not a well-defined set. Sets
are static entities defined by a binary membership operator, whereas
'the entire body of general knowledge' is a loosely defined entity
which changes from day to day as new things
It can be updated. Anything not known to be true
is outside the scope.
are learned and old things forgotten.Once in the system it is never forgotten.
So for example, in the nineteenth century the existence of the
luminiferous ether was well known and widely accepted. Are you claiming
it is still part of 'the entire body of general knowledge'?
It is also filled with contradictory propositions, so this isIt will have knowledge of these propositions and with my work
how to resolve some if not all of them.
never going to be the basis for anything computable.
I don't follow what you mean by this. Are the basic tenets of General Relativity part of the body of general knowledge? Are the basic tenets
of Quantum Mechanics part of the body of general knowledge?
Both are widely accepted but we know both cannot be entirely correct
since they contradict one another.
André
On 10/09/2026 06:45 PM, André G. Isaak wrote:
On 2026-10-09 19:31, olcott wrote:
On 10/9/2026 6:40 PM, André G. Isaak wrote:
On 2026-10-09 10:03, olcott wrote:
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to
object to (Gödel, Tarski) make any claims about knowledge. Tarski >>>>>> is concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The entire body of general knowledge is not a well-defined set. Sets
are static entities defined by a binary membership operator, whereas
'the entire body of general knowledge' is a loosely defined entity
which changes from day to day as new things
It can be updated. Anything not known to be true
is outside the scope.
are learned and old things forgotten.Once in the system it is never forgotten.
So for example, in the nineteenth century the existence of the
luminiferous ether was well known and widely accepted. Are you claiming
it is still part of 'the entire body of general knowledge'?
It is also filled with contradictory propositions, so this isIt will have knowledge of these propositions and with my work
how to resolve some if not all of them.
never going to be the basis for anything computable.
I don't follow what you mean by this. Are the basic tenets of General
Relativity part of the body of general knowledge? Are the basic tenets
of Quantum Mechanics part of the body of general knowledge?
Both are widely accepted but we know both cannot be entirely correct
since they contradict one another.
André
Einstein has an aether in his theory, says it's obvious.
(Cf., "Sidelights in Relativity".)
Agreeably, there's that lies, hyperbole, exaggeration,
and other distortions of the truth make that "the body
of general knowledge" must include malice beyond ignorance,
then that besides, there's "science" involved that scientists
only say "not falsified".
Set-theory as you mentioned is nice and simple as a
theory-of-one-relation, there are others, first of all there are other set-theories,
then for example part-theory and class-theory, then for example various order-theory and ordering-theory, accounts of theories-of-one-relation.
Then, about all those being modeled by one of those, involves
"paradoxes" of, for examples:
induction
quantification
identity
infinity
continuity
and so on, then that there's a theory where it's part of the body
of knowledge that those are resolved for paradox-free reason.
GR and QM can be made compatible with real space-contraction and
real wave-collapse, providing "Lorentzians" and "Schroedingerians"
for "doubly-objective relativity theory" and "continuous quantum
mechanics".
It involves infinity and continuity in mathematics,
yet any account of motion and continuity already does.
On 10/9/2026 8:45 PM, André G. Isaak wrote:
On 2026-10-09 19:31, olcott wrote:
On 10/9/2026 6:40 PM, André G. Isaak wrote:
On 2026-10-09 10:03, olcott wrote:
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to
object to (Gödel, Tarski) make any claims about knowledge. Tarski >>>>>> is concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The entire body of general knowledge is not a well-defined set. Sets
are static entities defined by a binary membership operator, whereas
'the entire body of general knowledge' is a loosely defined entity
which changes from day to day as new things
It can be updated. Anything not known to be true
is outside the scope.
are learned and old things forgotten.Once in the system it is never forgotten.
So for example, in the nineteenth century the existence of the
luminiferous ether was well known and widely accepted. Are you
claiming it is still part of 'the entire body of general knowledge'?
You said forgotten. Try to use all of your words
as if they were a mathematical formalism.
It is also filled with contradictory propositions, so this isIt will have knowledge of these propositions and with my work
how to resolve some if not all of them.
never going to be the basis for anything computable.
I don't follow what you mean by this. Are the basic tenets of General
Relativity part of the body of general knowledge? Are the basic tenets
of Quantum Mechanics part of the body of general knowledge?
Both are widely accepted but we know both cannot be entirely correct
since they contradict one another.
André
All of the details about them are general knowledge.
Unresolved conflicts are outside the scope of knowledge.
On 2026-10-09 20:37, olcott wrote:
On 10/9/2026 8:45 PM, André G. Isaak wrote:
On 2026-10-09 19:31, olcott wrote:
On 10/9/2026 6:40 PM, André G. Isaak wrote:
On 2026-10-09 10:03, olcott wrote:
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to >>>>>>> object to (Gödel, Tarski) make any claims about knowledge. Tarski >>>>>>> is concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The entire body of general knowledge is not a well-defined set.
Sets are static entities defined by a binary membership operator,
whereas 'the entire body of general knowledge' is a loosely defined >>>>> entity which changes from day to day as new things
It can be updated. Anything not known to be true
is outside the scope.
are learned and old things forgotten.Once in the system it is never forgotten.
So for example, in the nineteenth century the existence of the
luminiferous ether was well known and widely accepted. Are you
claiming it is still part of 'the entire body of general knowledge'?
You said forgotten. Try to use all of your words
as if they were a mathematical formalism.
So is the luminiferous ether part of 'general knowledge' or not? It definetely was at one point and you claim that things are never forgotten.
It is also filled with contradictory propositions, so this isIt will have knowledge of these propositions and with my work
how to resolve some if not all of them.
never going to be the basis for anything computable.
I don't follow what you mean by this. Are the basic tenets of General
Relativity part of the body of general knowledge? Are the basic
tenets of Quantum Mechanics part of the body of general knowledge?
Both are widely accepted but we know both cannot be entirely correct
since they contradict one another.
André
All of the details about them are general knowledge.
Unresolved conflicts are outside the scope of knowledge.
Again, you don't answer the question. Are the basic tenets of relativity
and quantum mechanics part of general knowledge or not?
André
On 2026-10-09 20:37, olcott wrote:
On 10/9/2026 8:45 PM, André G. Isaak wrote:
On 2026-10-09 19:31, olcott wrote:
On 10/9/2026 6:40 PM, André G. Isaak wrote:
On 2026-10-09 10:03, olcott wrote:
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to >>>>>>> object to (Gödel, Tarski) make any claims about knowledge. Tarski >>>>>>> is concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The entire body of general knowledge is not a well-defined set.
Sets are static entities defined by a binary membership operator,
whereas 'the entire body of general knowledge' is a loosely defined >>>>> entity which changes from day to day as new things
It can be updated. Anything not known to be true
is outside the scope.
are learned and old things forgotten.Once in the system it is never forgotten.
So for example, in the nineteenth century the existence of the
luminiferous ether was well known and widely accepted. Are you
claiming it is still part of 'the entire body of general knowledge'?
You said forgotten. Try to use all of your words
as if they were a mathematical formalism.
So is the luminiferous ether part of 'general knowledge' or not? It definetely was at one point and you claim that things are never forgotten.
It is also filled with contradictory propositions, so this isIt will have knowledge of these propositions and with my work
how to resolve some if not all of them.
never going to be the basis for anything computable.
I don't follow what you mean by this. Are the basic tenets of General
Relativity part of the body of general knowledge? Are the basic
tenets of Quantum Mechanics part of the body of general knowledge?
Both are widely accepted but we know both cannot be entirely correct
since they contradict one another.
André
All of the details about them are general knowledge.
Unresolved conflicts are outside the scope of knowledge.
Again, you don't answer the question. Are the basic tenets of relativity
and quantum mechanics part of general knowledge or not?
On 10/6/2026 2:59 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>> sentence of the language of T. What is out-of-scope,
apparently, is merely anything for which your proposed
semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete >>>>>>>> method to find out whether a sentence or its negation can be
proven.
Consequently, it is not possible to construct a system that rejects >>>>>>>> all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises >>>>>> to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It truth value will be known as soon as its proof has been chekcked and
found good. The proof can be algorithmically compressed as soon as it is
found, even before the verification, though that is irrelevant to the
knowledge of its truth. Thought it is possible that it will be found to
be unprovable. But none of that affects its meaning and meaningfulness.
What PTS says about its meaning is irrelevant.
A finite proof might not exist.
It may forever remain unknowable
thus outside of the domain of knowledge.
It might be the case that its truth value is unknowable.
It even might be possible that we can't ever know whether its truth
value is unknowable.
I restricted my system to "the body of general knowledge that can be
expressed in language" to handle these edge cases.
Then your system needs be updated when something unknonw becames known.
It is updated the same way that Pluto ceased to be a planet.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication
https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
Being meaningful is not a limitation, nor is the ability to prove
that the commutativity law is false.
Meaningless expressions are outside the body of knowledge.
My focus has always been on "the body of general knowledge
that can be expressed in language".
I never really cared that system X is too weak to fully express Y.
A weaker system has a larger scope of applications, which is often
quite useful.
counter-factual. "Weaker" is stipulated to mean a reduced scope.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where
its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
*This is the domain of my proposed system*
"the body of general knowledge that can be expressed in language"
Irrelevant to your attempt to deceive with an ireelevancy.
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
Like the cycle in the directed graph of the evaluation sequence
of the Liar Paradox formalized in Prolog.
Quite unlike. Circular definitions don't define. A cyclic evaluation
graph
Never terminates thus never derives PTS semantic meaning.
is valid and describes a possible evaluation.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
I created the system of Minimal Type Theory for this exact same
purpose before I knew that Prolog could do this same thing.
There are many nice things that are quite simple with Prolog if one
knows Prolog and thinks a little about how.
So far as far as I know no one has derived that final
resolution of the Liar Paradox besides myself. We could
say that Kripke did this
On 2026-10-09 20:37, olcott wrote:
On 10/9/2026 8:45 PM, André G. Isaak wrote:
On 2026-10-09 19:31, olcott wrote:
On 10/9/2026 6:40 PM, André G. Isaak wrote:
On 2026-10-09 10:03, olcott wrote:
On 10/9/2026 10:25 AM, André G. Isaak wrote:
On 2026-10-09 09:02, olcott wrote:
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
The problem here is that none of the theorems which you seem to >>>>>>> object to (Gödel, Tarski) make any claims about knowledge. Tarski >>>>>>> is concerned with truth and Gödel with theoremhood.
André
There are several different aspects of my work
that has the final goal of:
Making "true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The entire body of general knowledge is not a well-defined set.
Sets are static entities defined by a binary membership operator,
whereas 'the entire body of general knowledge' is a loosely defined >>>>> entity which changes from day to day as new things
It can be updated. Anything not known to be true
is outside the scope.
are learned and old things forgotten.Once in the system it is never forgotten.
So for example, in the nineteenth century the existence of the
luminiferous ether was well known and widely accepted. Are you
claiming it is still part of 'the entire body of general knowledge'?
You said forgotten. Try to use all of your words
as if they were a mathematical formalism.
So is the luminiferous ether part of 'general knowledge' or not? It definetely was at one point and you claim that things are never forgotten.
It is also filled with contradictory propositions, so this isIt will have knowledge of these propositions and with my work
how to resolve some if not all of them.
never going to be the basis for anything computable.
I don't follow what you mean by this. Are the basic tenets of General
Relativity part of the body of general knowledge? Are the basic
tenets of Quantum Mechanics part of the body of general knowledge?
Both are widely accepted but we know both cannot be entirely correct
since they contradict one another.
André
All of the details about them are general knowledge.
Unresolved conflicts are outside the scope of knowledge.
Again, you don't answer the question. Are the basic tenets of relativity
and quantum mechanics part of general knowledge or not?
André
On 06/10/2026 15:32, olcott wrote:
On 10/6/2026 2:59 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>>> sentence of the language of T. What is out-of-scope,
apparently, is merely anything for which your proposed
semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no
complete
method to find out whether a sentence or its negation can be >>>>>>>>> proven.
Consequently, it is not possible to construct a system that >>>>>>>>> rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises >>>>>>> to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It truth value will be known as soon as its proof has been chekcked and
found good. The proof can be algorithmically compressed as soon as it is >>> found, even before the verification, though that is irrelevant to the
knowledge of its truth. Thought it is possible that it will be found to
be unprovable. But none of that affects its meaning and meaningfulness.
What PTS says about its meaning is irrelevant.
A finite proof might not exist.
It may forever remain unknowable
thus outside of the domain of knowledge.
That is one possibility, as already noted above. But it is also
possibe that a finite proof exists and is knowable but remains
forever unknown.
However, these possibilities are irrelevant to the meaning of the
of the conjecture, which we do know in spite or our ignorance of
its provability and truth value.
It might be the case that its truth value is unknowable.
It even might be possible that we can't ever know whether its truth
value is unknowable.
I restricted my system to "the body of general knowledge that can be
expressed in language" to handle these edge cases.
Then your system needs be updated when something unknonw becames known.
It is updated the same way that Pluto ceased to be a planet.
It is not updated unless somebody updates it. Also note that the process
that resulted to Pluto not being regarded as a planet was not simple and easy.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication
https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
Being meaningful is not a limitation, nor is the ability to prove
that the commutativity law is false.
Meaningless expressions are outside the body of knowledge.
The commutativity law is not meaningless, whther provable or not.
My focus has always been on "the body of general knowledge
that can be expressed in language".
That should include the meanings of the commutativity law and its
negation nad that in some cases both are unprovable but meaningful.
I never really cared that system X is too weak to fully express Y.
Then you should not post to this discussion as its topic is whether
PA is too weak to fully express the proof of G.
A weaker system has a larger scope of applications, which is often
quite useful.
counter-factual. "Weaker" is stipulated to mean a reduced scope.
No, "stronger" is stipualted to mean a reduced scope, i.e., greater
ability to exclude from the scope what is not wanted.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where
its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
*This is the domain of my proposed system*
"the body of general knowledge that can be expressed in language"
Irrelevant to your attempt to deceive with an ireelevancy.
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
Like the cycle in the directed graph of the evaluation sequence
of the Liar Paradox formalized in Prolog.
Quite unlike. Circular definitions don't define. A cyclic evaluation
graph
Never terminates thus never derives PTS semantic meaning.
Irrelevant. A cyclic evaluation graph is not meaningless. A circular definition does not present a meaning.
is valid and describes a possible evaluation.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
I created the system of Minimal Type Theory for this exact same
purpose before I knew that Prolog could do this same thing.
There are many nice things that are quite simple with Prolog if one
knows Prolog and thinks a little about how.
So far as far as I know no one has derived that final
resolution of the Liar Paradox besides myself. We could
say that Kripke did this
That you don't know what others have concluded does not matter.
On 10/7/2026 3:49 AM, Mikko wrote:
On 06/10/2026 15:32, olcott wrote:
On 10/6/2026 2:59 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" >>>>>>>>>>>> does not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory >>>>>>>>>>>> is involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>>>> sentence of the language of T. What is out-of-scope,
apparently, is merely anything for which your proposed >>>>>>>>>>>> semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no >>>>>>>>>> complete
method to find out whether a sentence or its negation can be >>>>>>>>>> proven.
Consequently, it is not possible to construct a system that >>>>>>>>>> rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises >>>>>>>> to conclusion and an indirect proof is a similar chain from tne >>>>>>>> negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It truth value will be known as soon as its proof has been chekcked and >>>> found good. The proof can be algorithmically compressed as soon as
it is
found, even before the verification, though that is irrelevant to the
knowledge of its truth. Thought it is possible that it will be found to >>>> be unprovable. But none of that affects its meaning and meaningfulness. >>>> What PTS says about its meaning is irrelevant.
A finite proof might not exist.
It may forever remain unknowable
thus outside of the domain of knowledge.
Maybe, maybe not. If it ever will be found it is in the domain
of knowledge and has always been.
Unless at least one mind contains a truth such as
the ratio of the diameter to the circumference of
a circle back in caveman days I construe this as
outside of the domain of knowledge at the time.
It might be the case that its truth value is unknowable.
It even might be possible that we can't ever know whether its truth
value is unknowable.
I restricted my system to "the body of general knowledge that can be
expressed in language" to handle these edge cases.
Then your system needs be updated when something unknonw becames known. >>>>
It is updated the same way that Pluto ceased to be a planet.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication
https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
Being meaningful is not a limitation, nor is the ability to prove
that the commutativity law is false.
Meaningless expressions are outside the body of knowledge.
Some knowledge about meaningful expression, their properties, and
relations between them is in the bdoy of knowledge.
Yes for example we already know that the Goldbach conjecture
is either true or false. Its actual truth value is currently
outside of the body of knowledge
counter-factual. "Weaker" is stipulated to mean a reduced scope.My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
A weaker system has a larger scope of applications, which is often
quite useful.
No, it is not. When applied to theories it is stipulated to mean lesser
provability.
The entire body of general knowledge expressed
in language can be fully encoded as two types
of relations between finite strings:
(a) Stipulated relations
(b) Semantic entailment specified syntactically.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where
its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
*This is the domain of my proposed system*
"the body of general knowledge that can be expressed in language"
Irrelevant to your attempt to deceive with an ireelevancy.
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
Like the cycle in the directed graph of the evaluation sequence
of the Liar Paradox formalized in Prolog.
Quite unlike. Circular definitions don't define. A cyclic evaluation
graph
Never terminates thus never derives PTS semantic meaning.
THe main similatity is that both evaluation graphs and PTS semantic
meanings are irrelevant to PA and provability.
Not at all.
The entire body of general knowledge expressed
in language can be fully encoded as two types
of relations between finite strings:
(a) Stipulated relations
(b) Semantic entailment specified syntactically.
It has always been the case that the above notion of
Proof Theoretic Semantics has always been the way that
"true on the basis of meaning expressed in language"
has always worked in actual reality.
is valid and describes a possible evaluation.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
I created the system of Minimal Type Theory for this exact same
purpose before I knew that Prolog could do this same thing.
There are many nice things that are quite simple with Prolog if one
knows Prolog and thinks a little about how.
So far as far as I know no one has derived that final
resolution of the Liar Paradox besides myself. We could
say that Kripke did this
No one, including you, has derived anything important about the liar
paradox during the last 2000 years. The only new results are attempts
to avoid the paradox in new systems, with variable success.
Kripke did define this same idea first with his: "The LP is ungrounded".
Outline of a Theory of Truth Saul Kripke (1975) https://files.commons.gc.cuny.edu/wp-content/blogs.dir/1358/ files/2019/04/Outline-of-a-Theory-of-Truth.pdf
All that I did is make this same idea maximally succinct.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false. // Copyright 2018 and 2026 PL Olcott
*Truth as an Epistemic Notion (2011) Dag Prawitz*
What is the appropriate notion of truth for sentences
whose meanings are understood in epistemic terms
such as proof or ground for an assertion? It seems
that the truth of such sentences has to be identified
with the existence of proofs or grounds https://link.springer.com/article/10.1007/s11245-011-9107-6
The above seems to be consistent with Wittgenstein
'True in Russell's system' means, as was said:
proved in Russell's system; and 'false in Russell's system'
means:the opposite has been proved in Russell's system. https://www.liarparadox.org/Wittgenstein.pdf
On 07/10/2026 16:10, polcott wrote:
On 10/7/2026 3:49 AM, Mikko wrote:
On 06/10/2026 15:32, olcott wrote:
On 10/6/2026 2:59 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:It truth value will be known as soon as its proof has been chekcked >>>>> and
On 02/10/2026 14:55, olcott wrote:The Goldbach conjecture is meaningful yet its truth value will be
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" >>>>>>>>>>>>> does not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory >>>>>>>>>>>>> is involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>>>>> sentence of the language of T. What is out-of-scope, >>>>>>>>>>>>> apparently, is merely anything for which your proposed >>>>>>>>>>>>> semantics fails to supply an answer.
Within PTS any expression that is neither provable nor >>>>>>>>>>>> refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no >>>>>>>>>>> complete
method to find out whether a sentence or its negation can be >>>>>>>>>>> proven.
Consequently, it is not possible to construct a system that >>>>>>>>>>> rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises >>>>>>>>> to conclusion and an indirect proof is a similar chain from tne >>>>>>>>> negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to >>>>>>
unknown unless and until it proof can be algorithmically compressed. >>>>>
found good. The proof can be algorithmically compressed as soon as
it is
found, even before the verification, though that is irrelevant to the >>>>> knowledge of its truth. Thought it is possible that it will be
found to
be unprovable. But none of that affects its meaning and
meaningfulness.
What PTS says about its meaning is irrelevant.
A finite proof might not exist.
It may forever remain unknowable
thus outside of the domain of knowledge.
Maybe, maybe not. If it ever will be found it is in the domain
of knowledge and has always been.
Unless at least one mind contains a truth such as
the ratio of the diameter to the circumference of
a circle back in caveman days I construe this as
outside of the domain of knowledge at the time.
Unless you explicitly define the expression in every opus where you use
it the expession means it means in Common Language, which usually is
vague.
It might be the case that its truth value is unknowable.
It even might be possible that we can't ever know whether its truth
value is unknowable.
I restricted my system to "the body of general knowledge that can be >>>>> > expressed in language" to handle these edge cases.
Then your system needs be updated when something unknonw becames
known.
It is updated the same way that Pluto ceased to be a planet.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is >>>>>>The Commutative Law For Multiplication
https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
Being meaningful is not a limitation, nor is the ability to prove
that the commutativity law is false.
Meaningless expressions are outside the body of knowledge.
Some knowledge about meaningful expression, their properties, and
relations between them is in the bdoy of knowledge.
Yes for example we already know that the Goldbach conjecture
is either true or false. Its actual truth value is currently
outside of the body of knowledge
And so is whether it will ever be found out.
counter-factual. "Weaker" is stipulated to mean a reduced scope.My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
A weaker system has a larger scope of applications, which is often
quite useful.
No, it is not. When applied to theories it is stipulated to mean lesser
provability.
The entire body of general knowledge expressed
in language can be fully encoded as two types
of relations between finite strings:
(a) Stipulated relations
(b) Semantic entailment specified syntactically.
Irrelevant.
For example, it is not provable in a group
(where its negation isn't, either) nor in the quaternions (where >>>>>>> its negation is provable) but it is meaningful in both.
For
"true on the basis of meaning expressed in language"
when an expression cannot possibly connect to the
expressions that give it meaning then it never gets
any meaning.
That is not the basis in the above examples.
*This is the domain of my proposed system*
"the body of general knowledge that can be expressed in language"
Irrelevant to your attempt to deceive with an ireelevancy.
If all words are defined in terms of other words and
there is a string of symbols that it never assigned
any relation to other strings then it remains meaningless.
They are also meaningless if there are diretly or indirectly
circular definitions.
Like the cycle in the directed graph of the evaluation sequence
of the Liar Paradox formalized in Prolog.
Quite unlike. Circular definitions don't define. A cyclic evaluation >>>>> graph
Never terminates thus never derives PTS semantic meaning.
THe main similatity is that both evaluation graphs and PTS semantic
meanings are irrelevant to PA and provability.
Not at all.
The entire body of general knowledge expressed
in language can be fully encoded as two types
of relations between finite strings:
(a) Stipulated relations
(b) Semantic entailment specified syntactically.
It has always been the case that the above notion of
Proof Theoretic Semantics has always been the way that
"true on the basis of meaning expressed in language"
has always worked in actual reality.
No, it is not. Whether "true on the basis of meaning expressed in
language" has ever worked at all in actual reality is not clear
(mainly because you have not defined it sufficiently well), let
alone how.
is valid and describes a possible evaluation.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
I created the system of Minimal Type Theory for this exact same
purpose before I knew that Prolog could do this same thing.
There are many nice things that are quite simple with Prolog if one
knows Prolog and thinks a little about how.
So far as far as I know no one has derived that final
resolution of the Liar Paradox besides myself. We could
say that Kripke did this
No one, including you, has derived anything important about the liar
paradox during the last 2000 years. The only new results are attempts
to avoid the paradox in new systems, with variable success.
Kripke did define this same idea first with his: "The LP is ungrounded".
Outline of a Theory of Truth Saul Kripke (1975)
https://files.commons.gc.cuny.edu/wp-content/blogs.dir/1358/
files/2019/04/Outline-of-a-Theory-of-Truth.pdf
Kripke simply specifies that some sentences of some languages are
neither true not false and consequently for some languages no truth
predicate is possible.
For those languages a partial truth predicate
is the best one can have.
In order to have a partial predicate one
must use a logic system that can be soundly interpreted to have more
than two truth values.
All that I did is make this same idea maximally succinct.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false. // Copyright 2018 and 2026 PL Olcott
You dind't do even that. Those Prolog queries above are irrelevant.
*Truth as an Epistemic Notion (2011) Dag Prawitz*
What is the appropriate notion of truth for sentences
whose meanings are understood in epistemic terms
such as proof or ground for an assertion? It seems
that the truth of such sentences has to be identified
with the existence of proofs or grounds
https://link.springer.com/article/10.1007/s11245-011-9107-6
Epistemic notions are outside of the scope of formal logic.
The above seems to be consistent with Wittgenstein
'True in Russell's system' means, as was said:
proved in Russell's system; and 'false in Russell's system'
means:the opposite has been proved in Russell's system.
https://www.liarparadox.org/Wittgenstein.pdf
That may be a reasonable interpretation of Russell's system but
it is not cosistent with what Wittgenstain would call "current
rules of the language game of logicians".
On 10/9/2026 3:50 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>> sentence of the language of T. What is out-of-scope,
apparently, is merely anything for which your proposed
semantics fails to supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete >>>>>>>> method to find out whether a sentence or its negation can be
proven.
Consequently, it is not possible to construct a system that rejects >>>>>>>> all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises >>>>>> to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to
The Goldbach conjecture is meaningful yet its truth value will be
unknown unless and until it proof can be algorithmically compressed.
It might be the case that its truth value is unknowable. I restricted
my system to "the body of general knowledge that can be expressed in
language" to handle these edge cases.
each other. For example, the sentence ∀x ∀y (x * y = y * x) is
The Commutative Law For Multiplication
https://en.wikiversity.org/wiki/Basic_Laws_of_Algebra
meaningful in many theories and provable in some of them and
unporvable others.
That is merely a limitation of the individual formal systems.
My focus has always been on "the body of general knowledge
that can be expressed in language". I never really cared that
system X is too weak to fully express Y.
Does that include cases where X is Peano arithmetic and Y is a
proof that G is true about natural number?
Now I have (with the help of Gemini) finally totally
anchored my claim that in PTS the meaning of an
expression is only derived by the existence of a
canonical proof of it.
On 10/9/2026 3:45 AM, Mikko wrote:
On 02/10/2026 14:55, olcott wrote:
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does >>>>>>>> not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is >>>>>>>> involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently, >>>>>>>> is merely anything for which your proposed semantics fails to >>>>>>>> supply an answer.
Within PTS any expression that is neither provable nor refutable >>>>>>> never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete >>>>>> method to find out whether a sentence or its negation can be proven. >>>>>> Consequently, it is not possible to construct a system that rejects >>>>>> all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from premises
to conclusion and an indirect proof is a similar chain from tne
negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
A sentence of natural number arithmetic has a well defined arithemtic
meaning, whether grounded or not. Existence of a proof from some set
of axioms is irrelevant to the arithmetic meaning.
**On the Relation Between Heyting’s**
**and Gentzen’s Approaches to Meaning**
"Gentzen’s idea could be summarized by saying that
the meaning of a sentence is determined by what
counts as a canonical proof of it..."
https://doi.org/10.1007/978-3-319-22686-6_2
On 10/9/2026 2:59 AM, Mikko wrote:
On 07/10/2026 16:10, polcott wrote:
On 10/7/2026 3:49 AM, Mikko wrote:
On 06/10/2026 15:32, olcott wrote:
On 10/6/2026 2:59 AM, Mikko wrote:
On 04/10/2026 16:22, olcott wrote:
On 10/4/2026 6:30 AM, Mikko wrote:It truth value will be known as soon as its proof has been
On 02/10/2026 14:55, olcott wrote:The Goldbach conjecture is meaningful yet its truth value will be >>>>>>> unknown unless and until it proof can be algorithmically compressed. >>>>>>
On 10/2/2026 4:37 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" >>>>>>>>>>>>>> does not make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means >>>>>>>>>>>>>>
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory >>>>>>>>>>>>>> is involved.
And G is not "out-of-scope": it is a perfectly well-formed >>>>>>>>>>>>>> sentence of the language of T. What is out-of-scope, >>>>>>>>>>>>>> apparently, is merely anything for which your proposed >>>>>>>>>>>>>> semantics fails to supply an answer.
Within PTS any expression that is neither provable nor >>>>>>>>>>>>> refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no >>>>>>>>>>>> complete
method to find out whether a sentence or its negation can be >>>>>>>>>>>> proven.
Consequently, it is not possible to construct a system that >>>>>>>>>>>> rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. A direct proof is either a forward chain from >>>>>>>>>> premises
to conclusion and an indirect proof is a similar chain from tne >>>>>>>>>> negation of the axioms and conclusion to a contradiction.
It turns out that automated proof systems expose
the correct details the most clearly. They used
back-chained inference. In any case when a finite
canonical proof is impossible then the expression
never gets semantically grounded.
Existence of a proof and existence of a meaning are irrelevant to >>>>>>>
chekcked and
found good. The proof can be algorithmically compressed as soon as >>>>>> it is
found, even before the verification, though that is irrelevant to the >>>>>> knowledge of its truth. Thought it is possible that it will be
found to
be unprovable. But none of that affects its meaning and
meaningfulness.
What PTS says about its meaning is irrelevant.
A finite proof might not exist.
It may forever remain unknowable
thus outside of the domain of knowledge.
Maybe, maybe not. If it ever will be found it is in the domain
of knowledge and has always been.
Unless at least one mind contains a truth such as
the ratio of the diameter to the circumference of
a circle back in caveman days I construe this as
outside of the domain of knowledge at the time.
An obvious attempt to decive (this time a change of subject) does not
work. In order to decive one needs to behave as a honest person would.
It seems incorrect to call anything "knowledge" that
no one has ever known. We can call it unknown truth.
On 10/5/2026 3:19 AM, Mikko wrote:
On 01/10/2026 17:47, olcott wrote:
On 10/1/2026 5:03 AM, Mikko wrote:
On 29/09/2026 19:31, olcott wrote:
On 9/29/2026 11:01 AM, Python wrote:
No, Pete. Calling an undecidable sentence "out-of-scope" does not >>>>>> make undecidability disappear.
For a formal theory T, "G is undecidable in T" simply means
T |-/- G and T |-/- ~G
That is a statement entirely about proofs. No model theory is
involved.
And G is not "out-of-scope": it is a perfectly well-formed
sentence of the language of T. What is out-of-scope, apparently,
is merely anything for which your proposed semantics fails to
supply an answer.
Within PTS any expression that is neither provable nor refutable
never acquires any semantic meaning.
There is one more thing one needs to consider: there is no complete
method to find out whether a sentence or its negation can be proven.
Consequently, it is not possible to construct a system that rejects
all undecidable sentences.
If back-chained inference from expression X to axioms
has a loop it is rejected.
Irrelevant. Proofs are finite strings and strings don't contain
loops.
Unprovable and irrefutable in PA entails that
G never acquires semantic meaning in PA.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,142 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 93:06:56 |
| Calls: | 14,704 |
| Calls today: | 2 |
| Files: | 186,497 |
| D/L today: |
2,344 files (777M bytes) |
| Messages: | 2,551,657 |