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	⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axac3	⊢ CHOICE
2		dfackm	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) )
3	1 2	mpbi	⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )