[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-23 10:01, mechvel at scico.botik.ru wrote:
> On 2020-08-23 00:21, mechvel at scico.botik.ru wrote:
>> [..]
>> 
>> Do you mean that you doubt in that question of "will F terminate or 
>> not?"
>> is already solved somewhere?
>> Well, if we doubt in that the F machine can run infinitely, then very 
>> naturally
>> we doubt of that the above proof for the goal G is correct. Then the 
>> usage of EM
>> is not safe in this case.
>> 
>> If so, then the question of "What can be the third case" occurs 
>> senseless.
>> Because even the statement of the second case, "F never stops" occurs 
>> senseless.
> 
> 
> I think now in a different way about how can it look the third case
> (probably similar as Guillaume wrote):
> 
> the third case is that  time or space is exhausted before it becomes
> solved whether the machine F terminates.
> 


Still I doubt.
Probably this third case rather is:
"the machine F continues, and it is not known whether it stops".
So, without excluded third, the step of calling for F in the proof 
attempt for the goal
G needs to consider not two cases but the three cases: Yes, No, Unknown.
?

--
SM