Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics" https://plato.stanford.edu/entries/proof-theoretic-semantics/ #InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL. Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but
whether it is for any purpose more useful than alternatives.
For example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is already in the usual metalanguage semantics.
Which expression becomes shorter or simpler if Has_Meaning_PTS is
used instead of Provable ?
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
For example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is
already in the usual metalanguage semantics.
KnownTrue := Γ ⊂ PA(Γ ⊣ φ)
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it.
For example, if a sentence is known to be undecidable then it can be
added to the postulates. Conversely, if a sentence is known to be
decidable it should not be added to the postulates as the set of the postulates would become either inconsistent or redundant.
For example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is
There should be an existential quantifier above expression that should
be a copy of the expression defining Probable.
already in the usual metalanguage semantics.
KnownTrue := Γ ⊂ PA(Γ ⊣ φ)
It is a syntax error to use open variables φ in a definition.Besides KnownTrue is a bad name for a symbol that does not refer to knowledge.
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ
is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it.
For example, if a sentence is known to be undecidable then it can be
Such as "What time is it (yes or no)?"
Now the right side is as in the definition of Provable but the variableadded to the postulates. Conversely, if a sentence is known to be
decidable it should not be added to the postulates as the set of the
postulates would become either inconsistent or redundant.
There should be an existential quantifier above expression that shouldFor example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is >>
be a copy of the expression defining Probable.
already in the usual metalanguage semantics.
KnownTrue := Γ ⊂ PA(Γ ⊣ φ)
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
On 22/04/2026 10:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ >>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL.
Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but >>>>> whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it.
For example, if a sentence is known to be undecidable then it can be
Such as "What time is it (yes or no)?"
A question is neither true nor false and there is no way to prove
a question. But usually "undecidability" refers to affirmative
sentences only, as they only are in the scope of logic.
Now the right side is as in the definition of Provable but the variableadded to the postulates. Conversely, if a sentence is known to be
decidable it should not be added to the postulates as the set of the
postulates would become either inconsistent or redundant.
For example, the above expressed interpretation of Γ ⊂ PA(Γ ⊣ φ) is
There should be an existential quantifier above expression that should
be a copy of the expression defining Probable.
already in the usual metalanguage semantics.
KnownTrue := Γ ⊂ PA(Γ ⊣ φ)
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
φ is still free on the right side making KnownTrue ill-defined.
There still is no connection to knowledge so KnownTrue is a bad name.
Note that the Common Language phrase "known true" is not a noun phrase
and therefore does not denote any being.
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-chained inference steps from that proposition to the axioms of Peano Arithmetic.
I'm not saying I agree with the above, but at least it is more clear
than your attempts at formalism.
André
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-chained inference steps from that proposition to the axioms of Peano Arithmetic.
I'm not saying I agree with the above, but at least it is more clear
than your attempts at formalism.
André
On 04/22/2026 04:06 PM, André G. Isaak wrote:
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge. >>>>
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the
formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-chained
inference steps from that proposition to the axioms of Peano Arithmetic.
I'm not saying I agree with the above, but at least it is more clear
than your attempts at formalism.
André
Perhaps something like the band "Faith No More" the song "Empire".
On 4/22/2026 3:19 AM, Mikko wrote:
On 22/04/2026 10:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ >>>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL. >>>>>>> Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is but >>>>>> whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it.
For example, if a sentence is known to be undecidable then it can be
Such as "What time is it (yes or no)?"
A question is neither true nor false and there is no way to prove
a question. But usually "undecidability" refers to affirmative
sentences only, as they only are in the scope of logic.
This sentence is not true. // It is semantically incoherent
On 22/04/2026 16:17, olcott wrote:
On 4/22/2026 3:19 AM, Mikko wrote:
On 22/04/2026 10:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs.
...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>> #InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ >>>>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL. >>>>>>>> Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics is >>>>>>> but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it. >>>>> For example, if a sentence is known to be undecidable then it can be
Such as "What time is it (yes or no)?"
A question is neither true nor false and there is no way to prove
a question. But usually "undecidability" refers to affirmative
sentences only, as they only are in the scope of logic.
This sentence is not true. // It is semantically incoherent
Can you think any reason why typical formal languages have no symbol analogous to "this" in that sentence ?
On 4/22/2026 6:06 PM, André G. Isaak wrote:
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides
KnownTrue is a bad name for a symbol that does not refer to knowledge. >>>>
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the
formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of
back-chained inference steps from that proposition to the axioms of
Peano Arithmetic.
That certainly is more clear.
On 4/23/2026 2:06 AM, Mikko wrote:
On 22/04/2026 16:17, olcott wrote:
On 4/22/2026 3:19 AM, Mikko wrote:
On 22/04/2026 10:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
On 21/04/2026 16:33, olcott wrote:Such as "What time is it (yes or no)?"
On 4/21/2026 1:41 AM, Mikko wrote:
On 20/04/2026 19:57, olcott wrote:
Proof-theoretic semantics is inherently inferential, as
it is inferential activity which manifests itself in proofs. >>>>>>>>> ...inferences and the rules of inference establish the
meaning of expressions.
Schroeder-Heister, Peter, 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>>> #InfeIntuAntiReal
Provable(PA, φ) := ∃Γ ⊂ PA(Γ ⊣ φ)
There exists a finite set Γ of inference steps of PA such that φ >>>>>>>>> is back-chained to PA can ALWAYS be resolved in directly in SOL. >>>>>>>>> Has_Meaning_PTS(PA, φ) := Provable(PA, φ)
The interesting question is not what proof-theoretic semantics >>>>>>>> is but
whether it is for any purpose more useful than alternatives.
It utterly eliminates the result of undecidability.
Often the undesidability itself is more useful than any result of it. >>>>>> For example, if a sentence is known to be undecidable then it can be >>>>>
A question is neither true nor false and there is no way to prove
a question. But usually "undecidability" refers to affirmative
sentences only, as they only are in the scope of logic.
This sentence is not true. // It is semantically incoherent
Can you think any reason why typical formal languages have no symbol
analogous to "this" in that sentence ?
To keep reasoning about these things
so convoluted that they can never be
resolved?
I invented one that does
LP := ~True(LP)
On 2026-04-22 19:21, olcott wrote:
On 4/22/2026 6:06 PM, André G. Isaak wrote:
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides >>>>> KnownTrue is a bad name for a symbol that does not refer to knowledge. >>>>>
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the
formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-
chained inference steps from that proposition to the axioms of Peano
Arithmetic.
That certainly is more clear.
The point I want to make is that clarity and formalism are two different things. You do not excel at formalism. But that doesn't mean that you
cannot be clear. Just worry about the English for the time being and
worry about the formalism later.
On 4/23/2026 11:19 PM, André G. Isaak wrote:
On 2026-04-22 19:21, olcott wrote:
On 4/22/2026 6:06 PM, André G. Isaak wrote:
On 2026-04-22 01:48, olcott wrote:
On 4/22/2026 2:19 AM, Mikko wrote:
It is a syntax error to use open variables φ in a definition.Besides >>>>>> KnownTrue is a bad name for a symbol that does not refer to
knowledge.
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
You could solve this by changing it to KnownTrue(φ) := ...
But I still think your better off dispensing with the formalism and
simply expressing your ideas in English since you always mangle the
formalism.
Why not simply say:
A proposition is known to be true if there is a sequence of back-
chained inference steps from that proposition to the axioms of Peano
Arithmetic.
That certainly is more clear.
The point I want to make is that clarity and formalism are two
different things. You do not excel at formalism. But that doesn't mean
that you cannot be clear. Just worry about the English for the time
being and worry about the formalism later.
Can he take your good advise? Humm...
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,114 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 492511:57:35 |
| Calls: | 14,267 |
| Calls today: | 3 |
| Files: | 186,320 |
| D/L today: |
26,223 files (8,497M bytes) |
| Messages: | 2,518,394 |