Re: The simple essence of Proof Theoretic Semantics

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 simply 
means it is unprovable in Q. And being ungrounded in the atomic base of 
Q means that it cannot achieve the PTS meaning of provable but rather 
remains unprovable. There's no way you can get from any of those things 
to 'random gibberish'.

André

-- 
To email remove 'invalid' & replace 'gm' with well known Google mail 
service.