Propositional axioms are valid

Proof

1. 1
   Throughout, excluded middle licenses splitting on whether (or , ) holds, for whichever formulas is built from; each split is closed by unfolding the matching clause of D091.
2. 2
   A1: . If fails, the implies clause gives vacuously (a false antecedent). If it holds, then whatever 's own antecedent does, its consequent holds, so holds too, and again the outer implies clause is satisfied.
3. 3
   A2: . Suppose the antecedent holds and, for the consequent, suppose further and ; then (from the second supposition) and (from and the antecedent), so . Each implies clause is satisfied by this chain, so the whole formula holds; if any supposition along the way fails, the corresponding implies clause holds vacuously instead.
4. 4
   A3: . Suppose the antecedent holds and, for the consequent, suppose . If failed, the neg clause would give , so the antecedent would force , contradicting the supposition via the neg clause again. So holds, and the whole formula holds (vacuously if either supposition fails).
5. 5
   A4: . By the and clause, iff and . By the implies and neg clauses, holds iff it is not the case that implies , which is exactly and not , i.e. and - the same condition, so the iff clause holds.
6. 6
   A5: . By the or clause, iff or . By the implies and neg clauses, iff not implies , which (by F08, case on whether ) is exactly " or " - the same condition.
7. 7
   A6: . By the iff clause, iff . By the implies and neg clauses, the right side holds iff it is not the case that implies , which is exactly and , i.e. implies , and implies - by F08 on both, exactly , the same condition.
8. 8
   A7: . By the exists clause, iff there is with . By the forall and neg clauses, holds iff it is not the case that, for every , , i.e. not that, for every , not - which by F08 applied pointwise to each is exactly: there is some with - the same condition.

Used by