Re: The simple essence of Proof Theoretic Semantics

On 6/29/2026 9:31 PM, André G. Isaak wrote:
> On 2026-06-29 20:17, olcott wrote:
>> On 6/29/2026 8:54 PM, André G. Isaak wrote:
>>> On 2026-06-29 19:19, olcott wrote:
>>>> On 6/29/2026 8:01 PM, André G. Isaak wrote:
>>>>> On 2026-06-29 18:37, olcott wrote:
>>>>>> On 6/29/2026 6:45 PM, André G. Isaak wrote:
>>>>>>> On 2026-06-29 17:36, olcott wrote:
>>>>>
>>>>>>>> It does seem that they do agree that no proof
>>>>>>>> of G can possibly exist in PA does means that
>>>>>>>> G has no semantic meaning in PA.
>>>>>>>
>>>>>>> I've not seen anyone operating in PTS who says anything remotely 
>>>>>>> like that. They do not agree with this; rather, you are 
>>>>>>> projecting your own peculiar views onto their theory.
>>>>>>>
>>>>>>> André
>>>>>>>
>>>>>>
>>>>>> Because they beat around the bush about that using
>>>>>> terminology that varies across every author.
>>>>>
>>>>> It's not that they are beating around the bush; it's that they 
>>>>> aren't actually saying what you want them to say. Face it, you 
>>>>> really don't understand the PTS literature as it is above your head.
>>>>>
>>>>> André
>>>>>
>>>>
>>>> PTS is the way that meaning actually works.
>>>> We can make a simpler analogy in that English
>>>> words are meaningless until they are defined.
>>>>
>>>> The PTS connection of an expression in Q to
>>>> its axioms Q is analogous to the connection
>>>> of an English word to its definition.
>>>>
>>>> A proof merely looks to see if a definition
>>>> exists and if it does not then the English
>>>> Word / Expression of Q remains meaningless.
>>>
>>> That's not what PTS says; that's simply you.
>>>
>>> There is a difference between meaningless and wrong.
>>>
>> % 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.
> 
> That's completely nonresponsive. You're simply copying and pasting text 
> from previous posts without any explanation of how you think it relates 
> to the point I made (which you disingenuously snipped).
> 
> The Liar's Paradox isn't what I am discussing. I am discussing the fact 
> that 'no number is equal to its successor' can't be proven in Q. That 
> statement has absolutely no similarities to the Liar's Paradox.
> 
> André
> 

Those are specific concrete examples of how
Proof Theoretic Semantics rejects expressions
as Proof Theoretic Semantically incoherent.

-- 
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).