Axiom ax-6o 982

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 1027 in place of ax-4 977, ax-6o 982, and ax-7 966.

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

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 958	. . . . 5 wff ∀xφ
4	3	wn 2	. . . 4 wff ¬ ∀xφ
5	4, 2	wal 958	. . 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 983  a6e 994  hbnt 1006  ax46 1021  ax67 1024  ax467 1027  modal-b 1032  equid 1130

Copyright terms: Public domain