Re: The simple essence of Proof Theoretic Semantics

On 7/1/2026 3:11 PM, André G. Isaak wrote:
> On 2026-07-01 13:47, olcott wrote:
>> On 7/1/2026 2:23 PM, André G. Isaak wrote:
>>> On 2026-07-01 12:50, olcott wrote:
>>>> On 7/1/2026 1:40 PM, André G. Isaak wrote:
>>>>> On 2026-07-01 12:20, olcott wrote:
>>>>>> On 7/1/2026 1:10 PM, André G. Isaak wrote:
>>>>>>> On 2026-07-01 12:01, olcott wrote:
>>>>>>>> On 7/1/2026 12:33 PM, dbush wrote:
>>>>>>>>> On 7/1/2026 10:40 AM, olcott wrote:
>>>>>>>
>>>>>>>>>> The truth value of (∀ x, S(x) ≠ x) does not exist in Q.
>>>>>>>>>
>>>>>>>>> In your own words, what does it mean for the truth value of 
>>>>>>>>> statement to not exist in a formal system?
>>>>>>>>>
>>>>>>>>
>>>>>>>> The same thing as: "cats are animals" expressed in
>>>>>>>> English has no English meaning in Chinese.
>>>>>>>>
>>>>>>>> Until "cats are animals" is translated into Chinese
>>>>>>>> it is just random gibberish that has no meaning or
>>>>>>>> truth value in Chinese.
>>>>>>>
>>>>>>> But ∀ x, S(x) ≠ x *isn't* random gibberish in Q. It is a well- 
>>>>>>> formed expression of Q that has a well-defined meaning. It just 
>>>>>>> happens to be unprovable. If it were random gibberish no one 
>>>>>>> would have entertained the question of whether it could or could 
>>>>>>> not be proven in Q.
>>>>>>>
>>>>>>> André
>>>>>>>
>>>>>>
>>>>>> It has no finite sequence of inference steps between
>>>>>> the expression and the axioms of Q. This seems to
>>>>>> mean that (∀x, S(x) ≠ x) is ungrounded in the atomic
>>>>>> base of Q in many of the different ways that this
>>>>>> can be expressed by different PTS authors.
>>>>>
>>>>> Having no finite sequence of inference steps between the expression 
>>>>> and the axioms of Q is *not* the same thing as random gibberish. 
>>>>
>>>> It is closer to an English word such as "cat" that is
>>>> defined in English us undefined in Chinese.
>>>
>>> That's a completely spurious analogy. 'cat' isn't an expression of 
>>> the Chinese language. ∀ x, S(x) ≠ x *is* an expression of the 
>>> language of Q.
>>>
>>>>> It simply means it is unprovable in Q. 
>>>
>>> Then you're either using a completely idiosyncratic definition of 
>>> 'gibberish' or a completely idiosyncratic definition of 'provable'
>>> (or both). That's why people keep asking you to provide *your* 
>>> definitions, but you only respond with examples or analogies which 
>>> fail to clarify what you might mean.
>>>
>>>> Which means something entirely different in PTS than
>>>> it means in TCS.
>>>
>>> unprovable means the same thing in both.
>>>
>>
>> Wittgenstein (1937)
>> 'True in Russell's system' means, as was said:
>> proved in Russell's system; and 'false in Russell's
>> system' means: the opposite has been proved
>> in Russell's system
> 
> You keep quoting this particular bit despite the fact that its been 
> pointed out on numerous occasions that Wittgenstein wrote the above in 
> his private notes *before* he had actually read Gödel's paper, and he 

What matters is the it is the way that true on the
basis of meaning expressed in language has always
worked. Also what matters is that I came up with
this exact same thing years before I ever heard
of him.

> never went on to publish anything to this effect suggesting he didn't 
> subscribe to this position after he'd actually read Gödel.
> 
>> Does not mean that G is undecidable in PA.
> 
> It doesn't say anything at all about whether G is decidable in PA.
> 
> André
> 

Any expression X that is unprovable in any formal
system F is untrue in that formal system F

Any expression X that is irrefutable in any formal
system F is unfalse in that formal system F.


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