On 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 incoherentCan 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?
I invented one that does
LP := ~True(LP)
The directed graph of its
evaluation sequence has a cycle
00 ~ 01
01 True 00
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
unify_with_occurs_check() rejects all terms
that have a cycle in their evaluation sequence.
--
Copyright 2026 Olcott
My 28 year goal has been to make
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
The complete structure of this system is now defined.
This required establishing a new foundation
Les messages affichés proviennent d'usenet.