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 | ⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axac3 | ⊢ CHOICE | |
2 | dfackm | ⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) ) | |
3 | 1 2 | mpbi | ⊢ ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) |