Re: The simple essence of Proof Theoretic Semantics

On 7/1/2026 2:20 PM, 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.
> 

In other words, (∀x, S(x) ≠ x) is not provable in Q.

So once again, you're saying the same thing as everyone else but using 
different words.