Re: The simple essence of Proof Theoretic Semantics

On 7/1/2026 2:53 PM, olcott wrote:
> On 7/1/2026 1:34 PM, dbush wrote:
>> 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.
>>
> 
> In PTS that means the expression is undefined.
> It does not mean that Q has undecidable sentences in PTS.

In your own words, what do you think it means for an expression to be 
undefined, and what do you think it means for a formal system to have 
undecidable sentences?

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