| Liste des Groupes | Revenir à c theory |
On 4/22/2026 2:19 AM, Mikko wrote:A question is neither true nor false and there is no way to proveOn 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
Now the right side is as in the definition of Provable but the variableadded to the postulates. Conversely, if a sentence is known to beKnownTrue :=
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.
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
Les messages affichés proviennent d'usenet.