[isabelle-dev] Isabelle/HOL axiom "iff" is redundant

[John R Harrison]

| If you look at "HOL done right" by John Harrison, he does not seem to
| comment on the redundancy either but sets the system up a bit
| differently: he includes "iff" (IMP_ANTISYM_RULE) as an axiom, but
| derives True_or_False (BOOL_CASES_AX) from the axiom for SOME. He
| comments he wants to delay the point at which the system becomes
| classical and introduces the SOME operator later. That must be the
| reason why he does not get rid of IMP_ANTISYM_RULE as well.

That paper is now mainly of historical interest, marking an
intermediate step in my thinking about how to rationalize the HOL
Light deductive system. For the current setup see, section 2 of my
TPHOLs paper.

  http://www.cl.cam.ac.uk/~jrh13/papers/hollight.pdf

Here implication is no longer in the core, and the analog of the
Isabelle rule "iff" is actually formulated using |- rather than
implication (see DEDUCT_ANTISYM_RULE). In that form it can't be
removed, because it's the only primitive rule that is able to reduce
the number of formulas on the left of a sequent. 

Also, in the HOL Light arrangement, the analog of True_or_False
(BOOL_CASES_AX) is not primitive anyway, but is derived from Choice
when I do eventually go classical. This was originally done using
Diaconescu's proof, but recently I switched to a simpler variant
shown to me by Mark Adams.

John.