| Description: A version of aev 2057
with two universal quantifiers in the consequent.
One can prove similar statements with arbitrary numbers of universal
quantifiers in the consequent (the series begins with aeveq 2056, aev 2057,
aev2 2058).
Using aev 2057 and alrimiv 1927, one can actually prove (with no more axioms)
any scheme of the form (∀𝑥𝑥 = 𝑦 → PHI) , DV (𝑥, 𝑦) where
PHI involves only setvar variables and the connectors →, ↔,
∧, ∨, ⊤, =, ∀, ∃, ∃*, ∃!,
Ⅎ. An example is given by aevdemo 30479. This list cannot be
extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is
consistent with ax-mp 5, ax-gen 1795, ax-1 6--
ax-13 2377 (as the
one-element universe shows), so for instance (∀𝑥𝑥 = 𝑦 → ⊥),
DV (𝑥, 𝑦) is not provable from these axioms
alone (indeed, dtru 5441
uses non-logical axioms as well). (Contributed by BJ,
23-Mar-2021.) |