Gergely Buday (May 08 2025 at 10:13): Gergely Buday (May 08 2025 at 10:13):Generative artificial intelligence spreads the gossip that Michael Gordon included Hilbert's epsilon operator for practical verification aims but could not give a reference for this. But checking Church's original paper I see that he already uses what he calls a selection operator i_beta(o beta), that is, in modern notation, (beta -> bool) -> beta. So my question is: why Gordon did find the axiom of choice particularly useful for practical verification tasks? If you answer, please give me a reference.
Fabian Huch (May 08 2025 at 10:39):That just sounds like the typical hallucinations that LLMs create. HOL is quite convenient but saying that Gordon found the axiom of choice particularly useful is quite the claim. If you want to understand the history of HOL, have a look at "From LCF to HOL: A Short History" by Gordon.
Last updated: May 18 2025 at 04:27 UTC