Theorem ackm

Description: A remarkable equivalent to the Axiom of Choice that has only five quantifiers (when expanded to use only the primitive predicates = and e. and in prenex normal form), discovered and proved by Kurt Maes. This establishes a new record, reducing from 6 to 5 the largest number of quantified variables needed by any ZFC axiom. The ZF-equivalence to AC is shown by Theorem dfackm . Maes found this version of AC in April 2004 (replacing a longer version, also with five quantifiers, that he found in November 2003). See Kurt Maes, "A 5-quantifier ( e. , = )-expression ZF-equivalent to the Axiom of Choice", https://doi.org/10.48550/arXiv.0705.3162 .

The original FOM posts are: http://www.cs.nyu.edu/pipermail/fom/2003-November/007631.html http://www.cs.nyu.edu/pipermail/fom/2003-November/007641.html . (Contributed by NM, 29-Apr-2004) (Revised by Mario Carneiro, 17-May-2015) (Proof modification is discouraged.)

	Ref	Expression
Assertion	ackm	|- A. x E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axac3	|- CHOICE
2		dfackm	|- ( CHOICE <-> A. x E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) ) )
3	1 2	mpbi	|- A. x E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) )