P. 172 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 17101-17133   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	wrals 17101	Extend wff definition to include "all some" applied to a class, which means ps is true whenever ph is true for x in A, and there is at least one x in A where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
wff A.E. x e. A ( ph -> ps )
Definition	df-als 17102	Define "all some" applied to a top-level implication, which means ps is true whenever ph is true and there is at least one x where ph is true. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( A.E. x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
Definition	df-rals 17103	Define "all some" applied to a class, which means ps is true whenever ph is true for x in A, and there is at least one x in A where ph is true. An older definition of the "all some" quantifier when scoped to a class, named df-alsc and now removed, instead applied a bare formula ph to the members of a class, asserting only ( A. x e. A ph /\ E. x x e. A ), that is, that the formula held throughout A and that A had at least one member. I've now decided that that was a mistake. Its older existence conjunct E. x x e. A did not require any member of A to satisfy the antecedent, so if the formula was itself an implication, that inner implication could still be vacuously true, which is precisely what the allsome quantifier exists to prevent. For example, the older definition meant that "among Martians, all tall ones are green" could be considered true if there are Martians, but no tall Martians. This version of the definition instead ensures that claims of the form "among Martians, all tall ones are green" can only be true if all tall Martians are green and that there is at least one tall Martian. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E. x e. A ph ) )
Theorem	dfrals2 17104	The bounded "all some" form is the general form with the class membership folded into the antecedent. (Contributed by David A. Wheeler, 22-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x e. A ( ph -> ps ) <-> A.E. x ( ( x e. A /\ ph ) -> ps ) )
Theorem	alsd 17105	Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17107 and als2d 17108 taken together, and is what lets an "all some" statement be proved rather than merely taken apart. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A. x ( ps -> ch ) )   &    |- ( ph -> E. x ps )   =>    |- ( ph -> A.E. x ( ps -> ch ) )
Theorem	ralsd 17106	Introduction rule for "all some" restricted to a class. This is the converse of rals1d 17109 and rals2d 17110 taken together. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A. x e. A ( ps -> ch ) )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> A.E. x e. A ( ps -> ch ) )
Theorem	als1d 17107	Deduction rule: Given "all some" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( ph -> A.E. x ( ps -> ch ) )   =>    |- ( ph -> A. x ( ps -> ch ) )
Theorem	als2d 17108	Deduction rule: Given "all some" applied to a top-level inference, you can extract the "exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
|- ( ph -> A.E. x ( ps -> ch ) )   =>    |- ( ph -> E. x ps )
Theorem	rals1d 17109	Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A.E. x e. A ( ps -> ch ) )   =>    |- ( ph -> A. x e. A ( ps -> ch ) )
Theorem	rals2d 17110	Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. Note that the witness must satisfy the antecedent ps, not merely be a member of A. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A.E. x e. A ( ps -> ch ) )   =>    |- ( ph -> E. x e. A ps )
Theorem	ralsn0d 17111*	Deduction rule: Given "all some" applied to a class, the class is not the empty set. (Contributed by David A. Wheeler, 23-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
|- ( ph -> A.E. x e. A ( ps -> ch ) )   =>    |- ( ph -> A =/= (/) )
Theorem	ralsmd 17112*	Deduction rule: Given "all some" applied to a class, the class is inhabited. This is stronger than ralsn0d 17111, which only concludes that the class is nonempty; see n0r 3535. (Contributed by David A. Wheeler, 20-Jul-2026.)
|- ( ph -> A.E. x e. A ( ps -> ch ) )   =>    |- ( ph -> E. x x e. A )
Theorem	alsex 17113	The consequent of an "all some" is witnessed: if ps holds of every x satisfying ph, and some x satisfies ph, then some x satisfies ps. This is the positive counterpart of als-no-surprise 17121, and it is the property that ordinary "for all" with implication lacks: from A. x ( ph -> ps ) alone nothing whatever follows about ps, since nothing need satisfy ph. It is the allsome quantifier says what a speaker of "all Martians are green" usually means. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x ( ph -> ps ) -> E. x ps )
Theorem	ralsex 17114	The consequent of an "all some" restricted to a class is witnessed: some member of A satisfying ph also satisfies ps. Restricted counterpart of alsex 17113. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x e. A ( ph -> ps ) -> E. x e. A ps )
Theorem	alsbii 17115	Congruence: equivalents may be substituted inside an "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( ph <-> ch )   &    |- ( ps <-> th )   =>    |- ( A.E. x ( ph -> ps ) <-> A.E. x ( ch -> th ) )
Theorem	ralsbii 17116	Congruence for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( ph <-> ch )   &    |- ( ps <-> th )   =>    |- ( A.E. x e. A ( ph -> ps ) <-> A.E. x e. A ( ch -> th ) )
Theorem	alsbid 17117	Deduction form of alsbii 17115. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- F/ x ph   &    |- ( ph -> ( ps <-> th ) )   &    |- ( ph -> ( ch <-> ta ) )   =>    |- ( ph -> ( A.E. x ( ps -> ch ) <-> A.E. x ( th -> ta ) ) )
Theorem	nfals 17118	Bound-variable hypothesis builder for "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x A.E. y ( ph -> ps )
Theorem	nfrals 17119*	Bound-variable hypothesis builder for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- F/_ x A   &    |- F/ x ph   &    |- F/ x ps   =>    |- F/ x A.E. y e. A ( ph -> ps )
Theorem	cbvals 17120*	Rule used to change bound variables, using implicit substitution. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( x = y -> ( ph <-> ch ) )   &    |- ( x = y -> ( ps <-> th ) )   =>    |- ( A.E. x ( ph -> ps ) <-> A.E. y ( ch -> th ) )
Theorem	als-no-surprise 17121	Demonstrate that there is never a "surprise" when using the allsome quantifier, that is, it is never possible for the consequent to be both always true and always false. This uses the definition of df-als 17102: the universal parts give A. x -. ph, which contradicts the witness that the allsome quantifier supplies. Ordinary "for all" with implication has no such property, since A. x ( ph -> ps ) and A. x ( ph -> -. ps ) can both hold when nothing satisfies ph. (Contributed by David A. Wheeler, 27-Oct-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- -. ( A.E. x ( ph -> ps ) /\ A.E. x ( ph -> -. ps ) )
Theorem	rals-no-surprise 17122	Demonstrate that there is never a "surprise" when using the allsome quantifier restricted to a class, that is, it is never possible for the consequent to be both always true and always false of the members of A that satisfy the antecedent. This is the restricted counterpart of als-no-surprise 17121, and follows from it by dfrals2 17104. Note that this holds without any assumption that A is inhabited; that is the point of allsome, since the corresponding claim for the ordinary restricted "for all" fails when nothing in A satisfies ph. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- -. ( A.E. x e. A ( ph -> ps ) /\ A.E. x e. A ( ph -> -. ps ) )
Theorem	ralrals 17123	If the universal part of a restricted "all some" statement holds, then the statement reduces to the existence of a member of A satisfying its antecedent. This is the restricted counterpart of ralals 17129. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
|- ( A. x e. A ( ph -> ps ) -> ( A.E. x e. A ( ph -> ps ) <-> E. x e. A ph ) )
Theorem	rexrals 17124	If a member of A satisfying the antecedent exists, then a restricted "all some" statement reduces to its universal part. This is the restricted counterpart of rexals 17130. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
|- ( E. x e. A ph -> ( A.E. x e. A ( ph -> ps ) <-> A. x e. A ( ph -> ps ) ) )
Theorem	alsanmo 17125	An "all some" statement conjoined with the claim that at most one x satisfies its antecedent is equivalent to the universal part conjoined with the claim that exactly one x satisfies the antecedent. The "all some" quantifier supplies the existence of such an x and E* x ph supplies the at-most-one part, so together they yield E! x ph. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
|- ( ( A.E. x ( ph -> ps ) /\ E* x ph ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
Theorem	ralsanmo 17126	An "all some" statement restricted to a class, conjoined with the claim that at most one x in A satisfies its antecedent, is equivalent to the universal part conjoined with the claim that exactly one x in A satisfies the antecedent. This is the restricted counterpart of alsanmo 17125. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
|- ( ( A.E. x e. A ( ph -> ps ) /\ E* x e. A ph ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
Theorem	alsralrex 17127*	The general "all some" quantifier with class membership as its antecedent holds if and only if ph holds for every x in A and some x in A satisfies ph. (Contributed by Peter Mazsa, 27-Nov-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( A.E. x ( x e. A -> ph ) <-> ( A. x e. A ph /\ E. x e. A ph ) )
Theorem	alsraln0m 17128*	The general "all some" quantifier with class membership as its antecedent holds if and only if ph holds for every x in A and A is inhabited. This is the intuitionistic form of what set.mm states using A =/= (/); see the section comment. (Contributed by Peter Mazsa, 28-Nov-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( A.E. x ( x e. A -> ph ) <-> ( A. x e. A ph /\ E. x x e. A ) )
Theorem	ralals 17129*	If ph holds for every x in A, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that some x in A satisfies ph. See ralrals 17123 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
|- ( A. x e. A ph -> ( A.E. x ( x e. A -> ph ) <-> E. x e. A ph ) )
Theorem	rexals 17130*	If some x in A satisfies ph, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that ph holds for every x in A. See rexrals 17124 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
|- ( E. x e. A ph -> ( A.E. x ( x e. A -> ph ) <-> A. x e. A ph ) )
Theorem	n0alsm 17131*	If A is inhabited, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that ph holds for every x in A. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( E. x x e. A -> ( A.E. x ( x e. A -> ph ) <-> A. x e. A ph ) )
Theorem	2alsraln0m 17132*	Nested general "all some" quantifiers with class membership as their antecedents: ph holds for every x in A and every y in B, and both A and B are inhabited. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( A.E. x ( x e. A -> A.E. y ( y e. B -> ph ) ) <-> ( A. x e. A A. y e. B ph /\ ( E. x x e. A /\ E. y y e. B ) ) )
Theorem	2alsraln0idm 17133*	Nested general "all some" quantifiers with class membership as their antecedents, for the same class A: ph holds for every x and every y in A, and A is inhabited. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 20-Jul-2026.)
|- ( A.E. x ( x e. A -> A.E. y ( y e. A -> ph ) ) <-> ( A. x e. A A. y e. A ph /\ E. x x e. A ) )

< Previous  Wrap >