On 4/23/2026 2:06 AM, Mikko wrote:Wrong. The purpose is to avoid complexity that is not necessary forOn 22/04/2026 16:17, olcott wrote:To keep reasoning about these thingsOn 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 ?
so convoluted that they can never be
resolved?
the purpose of the language.
I invented one that doesAnd then you need to solve an uninteresting problem that does not
LP := ~True(LP)
exist in usual formal languages.
--
Mikko
Les messages affichés proviennent d'usenet.