I make a fully executable solution to the halting problem and then you deduce onUnivalence wrote: ↑Wed May 15, 2019 10:51 pmYou are going to have to define all your terms.PeteOlcott wrote: ↑Wed May 15, 2019 10:51 pm Like I said you are like a guy being slapped in the face that does not believe in faces or slapping
A
A → B
-------
∴ B
I won't believe it until you write a Prolog interpreter that does higher order logic.
I am most interested in the semantics/implementation of →
I will settle for code in Coq, Agda or Idris.
the basis of the contradiction that 1=0 and the principle of explosion that computers
don't exist and use this as your new excuse to reject what I say.