Axiom ax-6o 1014

Description: Axiom of Quantified Negation. This axiom is used to manipulate negated quantifiers. One of the 4 axioms of pure predicate calculus. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of the preprint). An alternate axiomatization could use ax467 1059 in place of ax-4 1009, ax-6o 1014, and ax-7 998.

This axiom is redundant, as shown by theorem ax6o 1013.

Assertion

Ref	Expression
ax-6o	⊢ (¬ ∀x ¬ ∀xφ → φ)

Detailed syntax breakdown of Axiom ax-6o

Step	Hyp	Ref	Expression
1		wph	. . . . . 6 wff φ
2		vx	. . . . . 6 set x
3	1, 2	wal 990	. . . . 5 wff ∀xφ
4	3	wn 2	. . . 4 wff ¬ ∀xφ
5	4, 2	wal 990	. . 3 wff ∀x ¬ ∀xφ
6	5	wn 2	. 2 wff ¬ ∀x ¬ ∀xφ
7	6, 1	wi 3	1 wff (¬ ∀x ¬ ∀xφ → φ)

This axiom is referenced by:  ax6 1015  a6e 1026  hbnt 1038  ax46 1053  ax67 1056  ax467 1059  modal-b 1064  equid 1162

Copyright terms: Public domain