On 2026-04-20, olcott <polcott333@gmail.com> wrote:F ⊢ GF ↔ ¬ProvF(⌜GF⌝)Proof-theoretic semantics is inherently inferential, asTwenty years ago (under my sixth-grade-adopted nickname "Mike"),
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, φ)
I posted in sci.math that Gödel's G was meaningless due to the
infinite regression toward infinity on the basis of which its
meaning was supposedly obtained.
The correct interpretation was, I argued, not "This sentence is
unprovable," but rather:
The following is unprovable (1):
The following is unprovable (2):
The following is unprovable (3):
...
As regards semantics, I could call statement (1) the "unencoded
sentence," sentence (2) the "first encoded sentence," the concept
under which all sentences (1)-(∞) belong the "formally abstracted
sentence," and the concept under which all sentences (2)-(∞)
belong the "encoding-abstracted sentence."
Then, I could argue that:
1. The /unencoded sentence/ is /true and meaningful/. It's a
statement about numbers.
2. The /formally abstracted/ and /encoding-abstracted/ sentences
are both /meaningless/.
Does this seem in agreement with your view? If so, how would you
describe my concepts in your own terms?
--Scott Hoge
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Olcott's Minimal Type Theory
G ↔ ¬Prov_PA(⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov_PA 04
04 Gödel_Number_of 01 // cycle
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first incompleteness theorem sentence
has a cycle in the directed graph of its
evaluation sequence making it semantically
incoherent.
This kind of semantically incoherence is
foundational in proof theoretic semantics.
--
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.