On 26/04/2026 23:54, olcott wrote:The directed graph of the evaluation sequence of GOn 4/26/2026 3:01 PM, Scott Hoge wrote:On 2026-04-20, olcott <polcott333@gmail.com> 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, φ)
Twenty years ago (under my sixth-grade-adopted nickname "Mike"),
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):
...
has a cycle preventing its evaluation from ever
terminating.
If you have no idea what directed graphs are you will
never get this. If you always knew what directed graphs
of evaluation sequences that contain cycles are then
you rebuttal has always been pure dishonesty.
In other words you did nor bother to page attention to whatOlcott's usual reaction is to say something unrelated to any asked>>
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
F ⊢ GF ↔ ¬ProvF(⌜GF⌝)
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.
question instead of answering. Perhaps he hopes to hide his ignorance
and incompetens. But it does not work.
Scott Hoge said.
--
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.