Re: The simple essence of Proof Theoretic Semantics

On 6/29/2026 9:49 PM, André G. Isaak wrote:
> On 2026-06-29 20:42, olcott wrote:
>> 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.
> 
> No, they are not. No author writing in the framework of proof-theoretic 
> semantics has ever offered those examples or comparable examples or made 
> any claims about 'rejecting expressions as proof theoretic semantically 
> incoherent'. And there's nothing incoherent about the statement 'no 
> number is equal to its successor' which is the example under discussion.
> 
> André
> 

None-the-less what I have said remains completely true.
What I have spent 28 years reverse-engineering from first
principles is exactly that. That no one applied PTS
exactly that way before does not mean that it is not
exactly correct PTS.

The biggest mistake that humanity makes that is killing
the whole planet is treating unbelievable as exactly
one-and-the-same-thing as untrue.

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