Re: The simple essence of Proof Theoretic Semantics

On 7/3/2026 10:05 PM, olcott wrote:
> On 7/3/2026 8:58 PM, dbush wrote:
>> On 7/3/2026 9:52 PM, olcott wrote:
>>> On 7/3/2026 5:51 PM, André G. Isaak wrote:
>>>> On 2026-07-03 16:37, olcott wrote:
>>>>> On 7/3/2026 1:47 PM, André G. Isaak wrote:
>>>>>> On 2026-07-03 12:36, olcott wrote:
>>>>>>> On 7/3/2026 1:18 PM, dbush wrote:
>>>>>>
>>>>>>>> If an algorithm takes an input and produces an output, that is 
>>>>>>>> by definition a mapping. 
>>>>>>> That only proves that the definition is incoherent.
>>>>>>> The coherent way that it actually works is that
>>>>>>> inputs are transformed into outputs by applying
>>>>>>> finite string transformation rules to inputs to
>>>>>>> derive outputs.
>>>>>>
>>>>>> Apparently you don't understand the difference between a mapping 
>>>>>> and an algorithm. They are two different things.
>>>>>>
>>>>>> André
>>>>>>
>>>>>
>>>>> A function that ignores its input and only returns 0
>>>>> is not any sort of halt function.
>>>>
>>>> He was defining 'mapping', not 'halt function'.
>>>>
>>>> André
>>>>
>>>
>>> A actual halt function must compute 
>> The mathematical halting function:
>>
> 
> When you actually implement this concretely 

We find that it is not possible, as Linz and others have proved.

> so that
> you cannot just "assume away" details then your notion
> requires a halt decider to report on the behavior of
> its caller having no idea who its caller is.
> 
>>
>> Given any algorithm (i.e. a fixed immutable sequence of instructions) 
>> X described as <X> with input Y:
>>
>> A solution to the halting problem is an algorithm H that computes the 
>> following mapping:
>>
>> (<X>,Y) maps to 1 if and only if X(Y) halts when executed directly
>> (<X>,Y) maps to 0 if and only if X(Y) does not halt when executed 
>> directly
>>
> 
>