section ‹Foundations of HOL›
theory Higher_Order_Logic
imports Pure
begin
text ‹
The following theory development demonstrates Higher-Order Logic itself,
represented directly within the Pure framework of Isabelle. The ``HOL''
logic given here is essentially that of Gordon @{cite "Gordon:1985:HOL"},
although we prefer to present basic concepts in a slightly more conventional
manner oriented towards plain Natural Deduction.
›
subsection ‹Pure Logic›
class type
default_sort type
typedecl o
instance o :: type ..
instance "fun" :: (type, type) type ..
subsubsection ‹Basic logical connectives›
judgment Trueprop :: "o ⇒ prop" ("_" 5)
axiomatization imp :: "o ⇒ o ⇒ o" (infixr "⟶" 25)
where impI [intro]: "(A ⟹ B) ⟹ A ⟶ B"
and impE [dest, trans]: "A ⟶ B ⟹ A ⟹ B"
axiomatization All :: "('a ⇒ o) ⇒ o" (binder "∀" 10)
where allI [intro]: "(⋀x. P x) ⟹ ∀x. P x"
and allE [dest]: "∀x. P x ⟹ P a"
subsubsection ‹Extensional equality›
axiomatization equal :: "'a ⇒ 'a ⇒ o" (infixl "=" 50)
where refl [intro]: "x = x"
and subst: "x = y ⟹ P x ⟹ P y"
abbreviation iff :: "o ⇒ o ⇒ o" (infixr "⟷" 25)
where "A ⟷ B ≡ A = B"
axiomatization
where ext [intro]: "(⋀x. f x = g x) ⟹ f = g"
and iff [intro]: "(A ⟹ B) ⟹ (B ⟹ A) ⟹ A ⟷ B"
theorem sym [sym]:
assumes "x = y"
shows "y = x"
using assms by (rule subst) (rule refl)
lemma [trans]: "x = y ⟹ P y ⟹ P x"
by (rule subst) (rule sym)
lemma [trans]: "P x ⟹ x = y ⟹ P y"
by (rule subst)
theorem trans [trans]: "x = y ⟹ y = z ⟹ x = z"
by (rule subst)
theorem iff1 [elim]: "A ⟷ B ⟹ A ⟹ B"
by (rule subst)
theorem iff2 [elim]: "A ⟷ B ⟹ B ⟹ A"
by (rule subst) (rule sym)
subsubsection ‹Derived connectives›
definition false :: o ("⊥") where "⊥ ≡ ∀A. A"
theorem falseE [elim]:
assumes "⊥"
shows A
proof -
from ‹⊥› have "∀A. A" unfolding false_def .
then show A ..
qed
definition true :: o ("⊤") where "⊤ ≡ ⊥ ⟶ ⊥"
theorem trueI [intro]: ⊤
unfolding true_def ..
definition not :: "o ⇒ o" ("¬ _" [40] 40)
where "not ≡ λA. A ⟶ ⊥"
abbreviation not_equal :: "'a ⇒ 'a ⇒ o" (infixl "≠" 50)
where "x ≠ y ≡ ¬ (x = y)"
theorem notI [intro]:
assumes "A ⟹ ⊥"
shows "¬ A"
using assms unfolding not_def ..
theorem notE [elim]:
assumes "¬ A" and A
shows B
proof -
from ‹¬ A› have "A ⟶ ⊥" unfolding not_def .
from this and ‹A› have "⊥" ..
then show B ..
qed
lemma notE': "A ⟹ ¬ A ⟹ B"
by (rule notE)
lemmas contradiction = notE notE' ― ‹proof by contradiction in any order›
definition conj :: "o ⇒ o ⇒ o" (infixr "∧" 35)
where "conj ≡ λA B. ∀C. (A ⟶ B ⟶ C) ⟶ C"
theorem conjI [intro]:
assumes A and B
shows "A ∧ B"
unfolding conj_def
proof
fix C
show "(A ⟶ B ⟶ C) ⟶ C"
proof
assume "A ⟶ B ⟶ C"
also note ‹A›
also note ‹B›
finally show C .
qed
qed
theorem conjE [elim]:
assumes "A ∧ B"
obtains A and B
proof
from ‹A ∧ B› have *: "(A ⟶ B ⟶ C) ⟶ C" for C
unfolding conj_def ..
show A
proof -
note * [of A]
also have "A ⟶ B ⟶ A"
proof
assume A
then show "B ⟶ A" ..
qed
finally show ?thesis .
qed
show B
proof -
note * [of B]
also have "A ⟶ B ⟶ B"
proof
show "B ⟶ B" ..
qed
finally show ?thesis .
qed
qed
definition disj :: "o ⇒ o ⇒ o" (infixr "∨" 30)
where "disj ≡ λA B. ∀C. (A ⟶ C) ⟶ (B ⟶ C) ⟶ C"
theorem disjI1 [intro]:
assumes A
shows "A ∨ B"
unfolding disj_def
proof
fix C
show "(A ⟶ C) ⟶ (B ⟶ C) ⟶ C"
proof
assume "A ⟶ C"
from this and ‹A› have C ..
then show "(B ⟶ C) ⟶ C" ..
qed
qed
theorem disjI2 [intro]:
assumes B
shows "A ∨ B"
unfolding disj_def
proof
fix C
show "(A ⟶ C) ⟶ (B ⟶ C) ⟶ C"
proof
show "(B ⟶ C) ⟶ C"
proof
assume "B ⟶ C"
from this and ‹B› show C ..
qed
qed
qed
theorem disjE [elim]:
assumes "A ∨ B"
obtains (a) A | (b) B
proof -
from ‹A ∨ B› have "(A ⟶ thesis) ⟶ (B ⟶ thesis) ⟶ thesis"
unfolding disj_def ..
also have "A ⟶ thesis"
proof
assume A
then show thesis by (rule a)
qed
also have "B ⟶ thesis"
proof
assume B
then show thesis by (rule b)
qed
finally show thesis .
qed
definition Ex :: "('a ⇒ o) ⇒ o" (binder "∃" 10)
where "∃x. P x ≡ ∀C. (∀x. P x ⟶ C) ⟶ C"
theorem exI [intro]: "P a ⟹ ∃x. P x"
unfolding Ex_def
proof
fix C
assume "P a"
show "(∀x. P x ⟶ C) ⟶ C"
proof
assume "∀x. P x ⟶ C"
then have "P a ⟶ C" ..
from this and ‹P a› show C ..
qed
qed
theorem exE [elim]:
assumes "∃x. P x"
obtains (that) x where "P x"
proof -
from ‹∃x. P x› have "(∀x. P x ⟶ thesis) ⟶ thesis"
unfolding Ex_def ..
also have "∀x. P x ⟶ thesis"
proof
fix x
show "P x ⟶ thesis"
proof
assume "P x"
then show thesis by (rule that)
qed
qed
finally show thesis .
qed
subsection ‹Cantor's Theorem›
text ‹
Cantor's Theorem states that there is no surjection from a set to its
powerset. The subsequent formulation uses elementary ‹λ›-calculus and
predicate logic, with standard introduction and elimination rules.
›
lemma iff_contradiction:
assumes *: "¬ A ⟷ A"
shows C
proof (rule notE)
show "¬ A"
proof
assume A
with * have "¬ A" ..
from this and ‹A› show ⊥ ..
qed
with * show A ..
qed
theorem Cantor: "¬ (∃f :: 'a ⇒ 'a ⇒ o. ∀A. ∃x. A = f x)"
proof
assume "∃f :: 'a ⇒ 'a ⇒ o. ∀A. ∃x. A = f x"
then obtain f :: "'a ⇒ 'a ⇒ o" where *: "∀A. ∃x. A = f x" ..
let ?D = "λx. ¬ f x x"
from * have "∃x. ?D = f x" ..
then obtain a where "?D = f a" ..
then have "?D a ⟷ f a a" using refl by (rule subst)
then have "¬ f a a ⟷ f a a" .
then show ⊥ by (rule iff_contradiction)
qed
subsection ‹Classical logic›
text ‹
The subsequent rules of classical reasoning are all equivalent.
›
locale classical =
assumes classical: "(¬ A ⟹ A) ⟹ A"
theorem (in classical) Peirce's_Law: "((A ⟶ B) ⟶ A) ⟶ A"
proof
assume a: "(A ⟶ B) ⟶ A"
show A
proof (rule classical)
assume "¬ A"
have "A ⟶ B"
proof
assume A
with ‹¬ A› show B by (rule contradiction)
qed
with a show A ..
qed
qed
theorem (in classical) double_negation:
assumes "¬ ¬ A"
shows A
proof (rule classical)
assume "¬ A"
with ‹¬ ¬ A› show ?thesis by (rule contradiction)
qed
theorem (in classical) tertium_non_datur: "A ∨ ¬ A"
proof (rule double_negation)
show "¬ ¬ (A ∨ ¬ A)"
proof
assume "¬ (A ∨ ¬ A)"
have "¬ A"
proof
assume A then have "A ∨ ¬ A" ..
with ‹¬ (A ∨ ¬ A)› show ⊥ by (rule contradiction)
qed
then have "A ∨ ¬ A" ..
with ‹¬ (A ∨ ¬ A)› show ⊥ by (rule contradiction)
qed
qed
theorem (in classical) classical_cases:
obtains A | "¬ A"
using tertium_non_datur
proof
assume A
then show thesis ..
next
assume "¬ A"
then show thesis ..
qed
lemma
assumes classical_cases: "⋀A C. (A ⟹ C) ⟹ (¬ A ⟹ C) ⟹ C"
shows "PROP classical"
proof
fix A
assume *: "¬ A ⟹ A"
show A
proof (rule classical_cases)
assume A
then show A .
next
assume "¬ A"
then show A by (rule *)
qed
qed
end