From Newsgroup: comp.theory

On 6/12/2026 2:48 PM, Tristan Wibberley wrote:

On 12/06/2026 17:00, polcott wrote:

Proof Theoretic Semantics it intended to override supersede
and utterly replace Truth Conditional Semantics (AKA model
theory) thus PA becomes only what its axioms actually specify.

I don't think so, isn't model theory part of modal logic which was
developed for PTS?

Proof-theoretic semantics is an alternative to truth-condition
semantics. (AKA model theory) https://plato.stanford.edu/entries/proof-theoretic-semantics/

Try asking any LLM:

Is Proof Theoretic Semantics intended to be an alternative
to Truth Conditional Semantics utterly discarding TCS and
completely replacing it with PTS?

ChatGPT:
"PTS aims to replace TCS as the basic theory of meaning"

Peter Schroeder-Heister coined the term: "Proof Theoretic Semantics"

"...inferences and the rules of inference establish the meaning of
expressions"

That's an idea found in Carnap's work long before Peter
Schroeder-Heister. I read that Mr. Schroeder-Heister coined the phrase
to provide a term for the existing idea at the time of his coining. I

Yes.

think Carnap is credited for the idea but I don't know the material thoroughly enough to be sure I understood that right. Possibly Goedel is credited with it, the material I've seen isn't really thorough so it's
not fully clear.

I have not seen any lineage from Carnap.

I understand my above quote to be accurately paraphrased
to say that when G is unprovable in Peano Arithmetic then
G never derives any semantic meaning in PA.

when both G and not-G are unprovable, perhaps.

Yes that is more precisely accurate.

PA doesn't have an object for provability relations. But you're already
well into that race.

A language one level above PA would have this.

I think you're misusing the term "semantic" a bit but it's true because semantic meaning isn't derived at all, it's postulated or even lingered
(the term "semantic" seems to me to have been coined by Carnap
especially for that purpose).

That is standard practice in PTS usage.
I directly reverse-engineered PTS from first principles
and happily found that others have done this same thing
just six months ago.

This was a huge breakthrough for PTS when it caught up meet
my own work at the time. https://link.springer.com/article/10.1007/s11245-011-9107-6

This seems to be the point where my work exceeded even
the current state of the art PTS.

True(L, X) ≡ ∃Γ ⊆ BaseFacts(L) (Γ ⊢ X) // copyright Olcott 2018

% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.

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 indicates no well-founded justification
tree exists.
--
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.

The entire body of knowledge expressed in language is
comprised of two types of relations between finite strings:
(a) *Axioms* Expressions of language that are stipulated to be true.

My system bridges the analytic/synthetic distinction by
expressly encoding all empirical "atomic facts" in a formal
language such as CycL of the Cyc project.

(b) *Inference Rules* Expressions of language that are semantically
entailed syntactically from (a) and/or (b).
--- Synchronet 3.22a-Linux NewsLink 1.2