BoolClass Module
This module derives further predicate logic theorems and inference rules. Unlike all preceding derivations, these all use the Axiom of Choice (i.e. 'select_ax'), and thus could be considered as classical logic. However, note that some of these (such as 'exists_rule') are actually derivable in intuitionistic logic if an alternative definition of existential quantification is used (as in HOL Light).
Functions and values
| Function or value | Description |
|
|- !p. (p <=> true) \/ (p <=> false)
|
|
|
|
This is the classical contradiction rule. It takes a boolean term and a theorem with falsity as its conclusion. It returns a theorem with the supplied term as its conclusion, and with the same assumptions as the supplied theorem but with the logical negation of the supplied term removed. Note that the logical negation of the supplied term does not have to be in the supplied theorem's assumptions for the rule to succeed. `p` A |- false ---------------- A\{~p} |- p See also: contr_rule, deduct_contrapos_rule.
|
|
|- !t1 t2. (if false then t1 else t2) = t2
|
|
|- !p t. (if p then t else t) = t
|
|
|- !p t1 t2. (if ~ p then t1 else t2) = (if p then t2 else t1)
|
|
|- !t1 t2. (if true then t1 else t2) = t1
|
|
|- !p. p \/ ~p
|
|
|- !P Q. (?x. P x \/ Q x) <=> (?x. P x) \/ (?x. Q x)
|
|
|- !t. (?x. t) <=> t
|
|
|- !P a. (?x. x = a /\ P x) <=> P a
|
|
This is the existential introduction rule. It takes an existential term, a witness term and a theorem, where the theorem's conclusion is the body of the existential term but with the witness term replacing occurrences of its binding variable. It returns a theorem stating that the supplied existential term holds, under the same assumptions as the supplied theorem. `?x. p` `t` A |- p[t/x] --------------------------- A |- ?x. p See also: choose_rule, select_rule, mk_exists_rule.
|
|
|- !p q. (p ==> q) <=> (~ p \/ q)
|
Force module evaluation
|
|
|
|- !p q. ~ (p /\ q) <=> ~ p \/ ~ q
|
|
|- !P. ~ (?x. P x) <=> (!x. ~ P x)
|
|
|- !P. ~ (!x. P x) <=> (?x. ~ P x)
|
|
|- !p. ~ ~ p <=> p
|
|
|- !(a:'a). (@x. x = a) = a
|
|
This is the existential selection rule. It strips off the existential quantifier from the supplied theorem, and replaces each occurrence of the binding variable in the body with the selection operator applied to the original body (with the same binding variable). A |- ?x. p ---------------- A |- p[(@x.p)/x] See also: exists_rule.
|
|
|- !P. (!x. ?y. P x y) <=> (?f. !x. P x (f x))
|
|
|- !P a. (?!x. x = a /\ P x) <=> P a
|
|
|- !P. (?!x. P x) <=> (?x. P x /\ (!y. P y ==> y = x))
|
|
|- !P. (?!x. P x) <=> (?x. !y. P y <=> x = y)
|
|
|- !P. (?!x. P x) <=> (?x. P x) /\ (!x x'. P x /\ P x' ==> x = x')
|
|
|- !P. (!x. ?!y. P x y) <=> (?f. !x y. P x y <=> f x = y)
|