# Theory Hilbert_Classical

theory Hilbert_Classical
imports Main
```(*  Title:      HOL/Proofs/ex/Hilbert_Classical.thy
Author:     Stefan Berghofer
Author:     Makarius Wenzel
*)

section ‹Hilbert's choice and classical logic›

theory Hilbert_Classical
imports Main
begin

text ‹
Derivation of the classical law of tertium-non-datur by means of
Hilbert's choice operator (due to M. J. Beeson and J. Harrison).
›

subsection ‹Proof text›

theorem tertium_non_datur: "A ∨ ¬ A"
proof -
let ?P = "λx. (A ∧ x) ∨ ¬ x"
let ?Q = "λx. (A ∧ ¬ x) ∨ x"

have a: "?P (Eps ?P)"
proof (rule someI)
have "¬ False" ..
then show "?P False" ..
qed
have b: "?Q (Eps ?Q)"
proof (rule someI)
have True ..
then show "?Q True" ..
qed

from a show ?thesis
proof
assume "A ∧ Eps ?P"
then have A ..
then show ?thesis ..
next
assume "¬ Eps ?P"
from b show ?thesis
proof
assume "A ∧ ¬ Eps ?Q"
then have A ..
then show ?thesis ..
next
assume "Eps ?Q"
have neq: "?P ≠ ?Q"
proof
assume "?P = ?Q"
then have "Eps ?P ⟷ Eps ?Q" by (rule arg_cong)
also note ‹Eps ?Q›
finally have "Eps ?P" .
with ‹¬ Eps ?P› show False by contradiction
qed
have "¬ A"
proof
assume A
have "?P = ?Q"
proof (rule ext)
show "?P x ⟷ ?Q x" for x
proof
assume "?P x"
then show "?Q x"
proof
assume "¬ x"
with ‹A› have "A ∧ ¬ x" ..
then show ?thesis ..
next
assume "A ∧ x"
then have x ..
then show ?thesis ..
qed
next
assume "?Q x"
then show "?P x"
proof
assume "A ∧ ¬ x"
then have "¬ x" ..
then show ?thesis ..
next
assume x
with ‹A› have "A ∧ x" ..
then show ?thesis ..
qed
qed
qed
with neq show False by contradiction
qed
then show ?thesis ..
qed
qed
qed

subsection ‹Old proof text›

theorem tertium_non_datur1: "A ∨ ¬ A"
proof -
let ?P = "λx. (x ⟷ False) ∨ (x ⟷ True) ∧ A"
let ?Q = "λx. (x ⟷ False) ∧ A ∨ (x ⟷ True)"

have a: "?P (Eps ?P)"
proof (rule someI)
show "?P False" using refl ..
qed
have b: "?Q (Eps ?Q)"
proof (rule someI)
show "?Q True" using refl ..
qed

from a show ?thesis
proof
assume "(Eps ?P ⟷ True) ∧ A"
then have A ..
then show ?thesis ..
next
assume P: "Eps ?P ⟷ False"
from b show ?thesis
proof
assume "(Eps ?Q ⟷ False) ∧ A"
then have A ..
then show ?thesis ..
next
assume Q: "Eps ?Q ⟷ True"
have neq: "?P ≠ ?Q"
proof
assume "?P = ?Q"
then have "Eps ?P ⟷ Eps ?Q" by (rule arg_cong)
also note P
also note Q
finally show False by (rule False_neq_True)
qed
have "¬ A"
proof
assume A
have "?P = ?Q"
proof (rule ext)
show "?P x ⟷ ?Q x" for x
proof
assume "?P x"
then show "?Q x"
proof
assume "x ⟷ False"
from this and ‹A› have "(x ⟷ False) ∧ A" ..
then show ?thesis ..
next
assume "(x ⟷ True) ∧ A"
then have "x ⟷ True" ..
then show ?thesis ..
qed
next
assume "?Q x"
then show "?P x"
proof
assume "(x ⟷ False) ∧ A"
then have "x ⟷ False" ..
then show ?thesis ..
next
assume "x ⟷ True"
from this and ‹A› have "(x ⟷ True) ∧ A" ..
then show ?thesis ..
qed
qed
qed
with neq show False by contradiction
qed
then show ?thesis ..
qed
qed
qed

subsection ‹Old proof script›

theorem tertium_non_datur2: "A ∨ ¬ A"
apply (subgoal_tac
"(((SOME x. x = False ∨ x = True ∧ A) = False) ∨
((SOME x. x = False ∨ x = True ∧ A) = True) ∧ A) ∧
(((SOME x. x = False ∧ A ∨ x = True) = False) ∧ A ∨
((SOME x. x = False ∧ A ∨ x = True) = True))")
prefer 2
apply (rule conjI)
apply (rule someI)
apply (rule disjI1)
apply (rule refl)
apply (rule someI)
apply (rule disjI2)
apply (rule refl)
apply (erule conjE)
apply (erule disjE)
apply (erule disjE)
apply (erule conjE)
apply (erule disjI1)
prefer 2
apply (erule conjE)
apply (erule disjI1)
apply (subgoal_tac
"(λx. (x = False) ∨ (x = True) ∧ A) ≠
(λx. (x = False) ∧ A ∨ (x = True))")
prefer 2
apply (rule notI)
apply (drule_tac f = "λy. SOME x. y x" in arg_cong)
apply (drule trans, assumption)
apply (drule sym)
apply (drule trans, assumption)
apply (erule False_neq_True)
apply (rule disjI2)
apply (rule notI)
apply (erule notE)
apply (rule ext)
apply (rule iffI)
apply (erule disjE)
apply (rule disjI1)
apply (erule conjI)
apply assumption
apply (erule conjE)
apply (erule disjI2)
apply (erule disjE)
apply (erule conjE)
apply (erule disjI1)
apply (rule disjI2)
apply (erule conjI)
apply assumption
done

subsection ‹Proof terms›

prf tertium_non_datur
prf tertium_non_datur1
prf tertium_non_datur2

end
```