P. 174 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 17301-17359   *Has distinct variable group(s)

Type	Label	Description
Statement
14.4.9  Supremum and infimum
Theorem	supfz 17301	The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
|- ( N e. ( ZZ>= ` M ) -> sup ( ( M ... N ) , ZZ , < ) = N )
Theorem	inffz 17302	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
|- ( N e. ( ZZ>= ` M ) -> inf ( ( M ... N ) , ZZ , < ) = M )
14.4.10  Circle constant
Theorem	taupi 17303	Relationship between tau and pi. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.)
|- tau = ( 2 x. pi )
14.5  Mathbox for Mykola Mostovenko
Theorem	ax1hfs 17304	Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)
|- ( ph -> ( ph /\ ph ) )
14.6  Mathbox for David A. Wheeler
14.6.1  Testable propositions
Theorem	dftest 17305	A proposition is testable iff its negative or double-negative is true. See Chapter 2 [Moschovakis] p. 2. We do not formally define testability with a new token, but instead use DECID -. before the formula in question. For example, DECID -. x = y corresponds to " x = y is testable". (Contributed by David A. Wheeler, 13-Aug-2018.) For statements about testable propositions, search for the keyword "testable" in the comments of statements, for instance using the Metamath command "MM> SEARCH * "testable" / COMMENTS". (New usage is discouraged.)
|- (DECID -. ph <-> ( -. ph \/ -. -. ph ) )
14.6.2  Allsome quantifier These are definitions and proofs involving the "allsome" quantifier (aka "all some"). In informal language, statements like "All Martians are green" imply that there is at least one Martian. But it's easy to mistranslate informal language into formal notations because similar statements like A. x ph -> ps do not imply that ph is ever true, leading to vacuous truths. Some systems include a mechanism to counter this, e.g., PVS allows types to be appended with "+" to declare that they are nonempty. This section presents a different solution to the same problem. The "allsome" quantifier expressly includes the notion of both "all" and "there exists at least one" (aka some), and is defined to make it easier to more directly express both notions. The hope is that if a quantifier more directly expresses this concept, it will be used instead and reduce the risk of creating formal expressions that look okay but in fact are mistranslations. The term "allsome" was chosen because it's short, easy to say, and clearly hints at the two concepts it combines. I do not expect this to be used much in Metamath, because in Metamath there's a general policy of avoiding the use of new definitions unless there are very strong reasons to do so. Instead, my goal is to rigorously define this quantifier and demonstrate a few basic properties of it. The syntax allows two forms that look like they would be problematic, but they are fine. When applied to a top-level implication we allow A.E. x ( ph -> ps ), and when restricted (applied to a class) we allow A.E. x e. A ( ph -> ps ). The first symbol after the setvar variable must always be e. if it is the form applied to a class, and since e. cannot begin a wff, it is unambiguous. The -> looks like it would be a problem because ph or ps might include implications, but any implication arrow -> within any wff must be surrounded by parentheses, so only the implication arrow of A.E. can follow the wff. The implication syntax would work fine without the parentheses, but I added the parentheses because it makes things clearer inside larger complex expressions, and it's also more consistent with the rest of the syntax. Naming: "als" is allsome. The form restricted to a class is prefixed with "r", following the way set.mm names the restricted quantifiers it is built from: A. gives df-ral 2533 and E. gives df-rex 2534, so df-als 17308 (the general form) gives df-rals 17309 (the restricted form). Earlier versions of this material differed, so old references may not match. They wrote the quantifier as an "inverted A" followed by an exclamation point, and they named the general form df-alsi and the restricted form df-alsc. The symbol is now an "inverted A" followed by a "backwards E", which more readers can correctly guess without being taught it. The restricted definition also changed, and the older one was a mistake; see df-rals 17309 for what was wrong with it. This database is intuitionistic, so some of this material differs from its counterpart in set.mm. In particular, a class A being inhabited ( E. x x e. A) is a stronger claim here than its being nonempty ( A =/= (/)); see n0r 3535. The allsome quantifier asserts that a witness exists, which is the stronger notion, so where set.mm states a result using A =/= (/) the corresponding result here uses inhabitedness instead. Such results are named with a trailing "m", following the convention of r19.2m 3614 and abn0m 3547. Results of set.mm that rely on recovering a witness from A =/= (/) are omitted, since that step is not available here. For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html 3547 I hope that others will eventually agree that allsome is awesome.
Syntax	wals 17306	Extend wff definition to include "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.) (Revised by David A. Wheeler, 12-Jul-2026.)
wff A.E. x ( ph -> ps )
Syntax	wrals 17307	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 17308	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 17309	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 17310	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 17311	Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17313 and als2d 17314 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 17312	Introduction rule for "all some" restricted to a class. This is the converse of rals1d 17315 and rals2d 17316 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 17313	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 17314	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 17315	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 17316	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 17317*	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 17318*	Deduction rule: Given "all some" applied to a class, the class is inhabited. This is stronger than ralsn0d 17317, 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 17319	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 17327, 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 17320	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 17319. (Contributed by David A. Wheeler, 12-Jul-2026.)
|- ( A.E. x e. A ( ph -> ps ) -> E. x e. A ps )
Theorem	alsbii 17321	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 17322	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 17323	Deduction form of alsbii 17321. (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 17324	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 17325*	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 17326*	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 17327	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 17308: 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 17328	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 17327, and follows from it by dfrals2 17310. 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 17329	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 17335. (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 17330	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 17336. (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 17331	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 17332	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 17331. (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 17333*	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 17334*	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 17335*	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 17329 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 17336*	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 17330 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 17337*	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 17338*	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 17339*	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 ) )
14.6.3  Allsome one quantifier These are definitions and proofs involving the "allsome one" quantifier, which extends the "allsome" quantifier of the previous section in the same way that E! (df-eu 2089) extends E.. Some systems extend "there exists" by appending a character to it. If a system provides such an extension, it should provide it for allsome as well: append the same character, let it modify allsome's existence conjunct, and change nothing else. Appending "!" gives "allsome one", so A.E! x ( ph -> ps ) means that ps is true whenever ph is true and that exactly one x satisfies ph. This is what the English word "the" usually does. "The king is hungry" claims that a king exists, that there is only one, and that he is hungry, and the form A.E! x ( ph -> ps ) claims exactly that kind of statement (specifically when ph means x is a king and ps means x is hungry). English says all of that in a single phrase, and the first two have a dedicated word ("the") for the construct. Many other languages have their own dedicated way of saying this. Languages reserve that kind of compression for what their speakers need constantly, which is a good reason for a formal notation to be able to say it just as directly, rather than spelling it out afresh as a conjunction of two quantified formulas every time it comes up. Russell analyzed such definite descriptions with this apparatus in "On Denoting", where his example of a phrase that appears to refer to someone but in fact denotes no one at all is "the present King of France", item (1) of [Russell1905] p. 479, France being a republic that has no king. Write "the king is hungry" as A. x ( ph -> ps ) instead and only the last of those three claims survives. The existence claim is silently gone, since that formula is vacuously true when there is no king, and the uniqueness claim is silently gone as well, since that formula holds just the same when there are five kings. Russell reached the opposite verdict for the same example, remarking that every proposition of the form "the present King of France ..." is false, [Russell1905] p. 482. The reason to care is the reason that motivates allsome, only more so. Note that this is not merely a way of writing E! x ( ph /\ ps ). Reading ph as "is a king" and ps as "is hungry", E! x ( ph /\ ps ) says that there is exactly one hungry king, whereas A.E! x ( ph -> ps ) says that there is exactly one king and that he is hungry. The first is true in a region with five kings exactly one of whom is hungry; the second is false there. Uniqueness attaches to the antecedent, not to the conjunction. See dfalseu2 17357 for the exact relationship between the two and alseueu 17358 for the one direction that does hold. Naming: "alseu" is allsome ("als", as in df-als 17308) extended with "exactly one" ("eu", as in df-eu 2089). The form restricted to a class is prefixed with "r", following df-rals 17309 and df-reu 2535, giving df-ralseu 17343. This database is intuitionistic, but nothing in this section depends on excluded middle, so every statement here has the same form as its counterpart in set.mm. That is unlike the allsome section above, where results that recover a witness from A =/= (/) are omitted or restated in terms of inhabitedness. Soundness: df-alseu 17342 and df-ralseu 17343 are eliminable and conservative directly, so neither needs a justification theorem. Definitions are required to be eliminable and conservative; see the section comment for df-bi 117. Each is a biconditional whose left side is a new syntax construct (walseu 17340 or wralseu 17341) applied to distinct metavariables, and whose right side uses only constructs introduced earlier ( A., E!, /\, ->, and the restricted quantifiers df-ral 2533 and df-reu 2535), so any occurrence of the new construct can be replaced by the right side, which is eliminability. Conservativity follows, since a proof of a statement not mentioning A.E! can have every use of the definition replaced in this way. Every variable occurring on the right side already occurs on the left side, so no dummy variable is introduced, and introducing a dummy variable whose choice must be shown not to matter is the only circumstance here that would call for a justification theorem. For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html 2535
Syntax	walseu 17340	Extend wff definition to include "all some one" applied to a top-level implication, which means ps is true whenever ph is true, and exactly one x satisfies ph. (Contributed by David A. Wheeler, 22-Jul-2026.)
wff A.E! x ( ph -> ps )
Syntax	wralseu 17341	Extend wff definition to include "all some one" applied to a class, which means ps is true whenever ph is true for x in A, and exactly one x in A satisfies ph. (Contributed by David A. Wheeler, 22-Jul-2026.)
wff A.E! x e. A ( ph -> ps )
Definition	df-alseu 17342	Define "all some one" applied to a top-level implication, which means ps is true whenever ph is true and exactly one x satisfies ph. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
Definition	df-ralseu 17343	Define "all some one" applied to a class, which means ps is true whenever ph is true for x in A, and exactly one x in A satisfies ph. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
Theorem	dfralseu2 17344	The bounded "all some one" form is the general form with the class membership folded into the antecedent. This is the "all some one" counterpart of dfrals2 17310. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x e. A ( ph -> ps ) <-> A.E! x ( ( x e. A /\ ph ) -> ps ) )
Theorem	alseuals 17345	"All some one" implies "all some": requiring exactly one witness is stronger than requiring at least one. Any consequence of an allsome statement is therefore a consequence of the corresponding "all some one" statement, which is how alseu-no-surprise 17359 is proved. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x ( ph -> ps ) -> A.E. x ( ph -> ps ) )
Theorem	ralseurals 17346	"All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals 17345. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x e. A ( ph -> ps ) -> A.E. x e. A ( ph -> ps ) )
Theorem	alseud 17347	Introduction rule: "all some one" holds if the "for all" part holds and the antecedent has exactly one witness. This is the converse of alseu1d 17349 and alseu2d 17350 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A. x ( ps -> ch ) )   &    |- ( ph -> E! x ps )   =>    |- ( ph -> A.E! x ( ps -> ch ) )
Theorem	ralseud 17348	Introduction rule for "all some one" restricted to a class. This is the converse of ralseu1d 17351 and ralseu2d 17352 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A. x e. A ( ps -> ch ) )   &    |- ( ph -> E! x e. A ps )   =>    |- ( ph -> A.E! x e. A ( ps -> ch ) )
Theorem	alseu1d 17349	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A.E! x ( ps -> ch ) )   =>    |- ( ph -> A. x ( ps -> ch ) )
Theorem	alseu2d 17350	Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "exactly one" part. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A.E! x ( ps -> ch ) )   =>    |- ( ph -> E! x ps )
Theorem	ralseu1d 17351	Deduction rule: Given "all some one" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A.E! x e. A ( ps -> ch ) )   =>    |- ( ph -> A. x e. A ( ps -> ch ) )
Theorem	ralseu2d 17352	Deduction rule: Given "all some one" applied to a class, you can extract the "exactly one" part. Note that the witness must satisfy the antecedent ps, not merely be a member of A. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph -> A.E! x e. A ( ps -> ch ) )   =>    |- ( ph -> E! x e. A ps )
Theorem	alseubii 17353	Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii 17321. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph <-> ch )   &    |- ( ps <-> th )   =>    |- ( A.E! x ( ph -> ps ) <-> A.E! x ( ch -> th ) )
Theorem	ralseubii 17354	Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii 17322. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( ph <-> ch )   &    |- ( ps <-> th )   =>    |- ( A.E! x e. A ( ph -> ps ) <-> A.E! x e. A ( ch -> th ) )
Theorem	nfalseu 17355	Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals 17324. Unlike the set.mm version of this theorem, no disjoint variable condition is needed, because nfeu 2105 here does not require one. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x A.E! y ( ph -> ps )
Theorem	nfralseu 17356*	Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals 17325. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- F/_ x A   &    |- F/ x ph   &    |- F/ x ps   =>    |- F/ x A.E! y e. A ( ph -> ps )
Theorem	dfalseu2 17357	An "all some one" statement is equivalent to its universal part conjoined with the claim that exactly one x satisfies both ph and ps. In other words, given A. x ( ph -> ps ), requiring exactly one x to satisfy ph, which is what df-alseu 17342 requires, and requiring exactly one x to satisfy ( ph /\ ps ) come to the same thing. Read ph as "is a king" and ps as "is hungry": if every king is hungry, then "there is exactly one king" and "there is exactly one hungry king" say the same thing, so either of them, together with "every king is hungry", gives "the king is hungry". The universal conjunct is what makes that work, and it cannot be dropped. E! x ( ph /\ ps ) on its own is strictly weaker than A.E! x ( ph -> ps ), since it is satisfied when many things are ph and just one of those is ps, as in a region with five kings exactly one of whom is hungry; see alseueu 17358 for the one direction that does hold without it. Uniqueness attaches to the antecedent, not to the conjunction. Russell's analysis of a definite description is built the same way: its uniqueness clause constrains the description predicate alone, while the predication is a separate conjunct. See his worked example of "the father of Charles II was executed", [Russell1905] p. 482. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ( ph /\ ps ) ) )
Theorem	alseueu 17358	"The ph is ps " implies that exactly one thing is both ph and ps. This is the half of dfalseu2 17357 that drops the universal conjunct; it does not reverse, so E! x ( ph /\ ps ) cannot be used in place of an "all some one" statement. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- ( A.E! x ( ph -> ps ) -> E! x ( ph /\ ps ) )
Theorem	alseu-no-surprise 17359	Demonstrate that there is never a "surprise" when using the "all some one" quantifier, that is, it is never possible for the consequent to be both always true and always false. This follows from als-no-surprise 17327 by alseuals 17345. See als-no-surprise 17327 for why ordinary "for all" with implication has no such property. (Contributed by David A. Wheeler, 22-Jul-2026.)
|- -. ( A.E! x ( ph -> ps ) /\ A.E! x ( ph -> -. ps ) )

< Previous  Wrap >