In Isabelle/HOL, the following axiomatizations can be found
axiomatization The :: "('a ⇒ bool) ⇒ 'a"
axiomatization undefined :: 'a
Is there a reason that one couldn't use
definition "undefined ≡ The (λx. False)"
or is this just a historic artifact? It seems that the current way leads to "different" notions of undefinedness. I stumbled upon this when I defined something along the lines of
definition "of_interest y ≡ (THE x. foobar x y)"
and wanted to prove the (in hindsight foolish) sanity-check
lemma "(∄x. foobar x y) ⟹ of_interest y = undefined"
which obviously doesn't work in the current state, but should go through with the above definition of undefined.
By using the axiomatization mechanism you clearly state that you cannot assume anything about undefined :: 'a but that it's an arbitrary but unknown value of type 'a. On the contrary, by using your definition, you now know a bit more about undefined, namely that it's the value to which The maps λx. False (the same applies for Eps (λx. True) and similar definitions). For example, with your definition you can prove that The (λx. False) = undefined, which you cannot prove using the axiomatization.