P. 173 of Theorem List - Intuitionistic Logic Explorer

Home	Intuitionistic Logic Explorer Theorem List (p. 173 of 174)	< Previous Next >
		Browser slow? Try the Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List

**Theorem List for Intuitionistic Logic Explorer -** 17201-17300 *Has distinct variable group(s)
Type	Label	Description
Statement

Theorem	pw1dceq 17201*	The powerset of having decidable equality is equivalent to excluded middle. (Contributed by Jim Kingdon, 12-Feb-2026.)
EXMID DECID

Theorem	exmidnotnotr 17202	Excluded middle is equivalent to double negation elimination. Read an element of as being a truth value and being that is true. For a similar theorem, but expressed in terms of formulas rather than subsets of , see dcfromnotnotr 1497. (Contributed by Jim Kingdon, 22-Apr-2026.)
EXMID

Theorem	exmidcon 17203*	Excluded middle is equivalent to the form of contraposition which removes negation. Read an element of as being a truth value and being that is true. For a similar theorem, but expressed in terms of formulas rather than subsets of , see dcfromcon 1498. (Contributed by Jim Kingdon, 22-Apr-2026.)
EXMID

Theorem	exmidpeirce 17204*	Excluded middle is equivalent to Peirce's law. Read an element of as being a truth value and being that is true. For a similar theorem, but expressed in terms of formulas rather than subsets of , see dcfrompeirce 1499. (Contributed by Jim Kingdon, 23-Apr-2026.)
EXMID

Theorem	stnot 17205*	A proposition is double negation stable if and only if it is equivalent to a negated proposition. Here by "proposition" we mean a subset of a singleton (which is a choice which allows us to quantify over them). Posed as an exercise online by Yannick Forster. (Contributed by Jim Kingdon, 24-Jul-2026.)


14.4.4 Weak excluded middle

Syntax	wwem 17206	Formula for an abbreviation of weak excluded middle.
WEXMID

Definition	df-wexmid 17207	Weak excluded middle is the principle that any negated proposition is decidable. (Contributed by Jim Kingdon, 30-Jul-2026.)
WEXMID $\/$

Theorem	wexmiddc 17208	Weak excluded middle expressed using WEXMID implies decidability of a negated proposition. (Contributed by Jim Kingdon, 30-Jul-2026.)
WEXMID DECID

Theorem	wexmiddiffilem 17209*	Lemma for wexmiddiffi 17210. The reverse direction, using different notation. (Contributed by Jim Kingdon, 29-Jul-2026.)
$\$ $\/$

Theorem	wexmiddiffi 17210*	Being able to subtract an arbitrary set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 29-Jul-2026.)
WEXMID $\$

Theorem	wexmiddifxylem 17211*	Lemma for wexmiddifxylem 17211. Showing weak excluded middle given a suitable finite set. (Contributed by Jim Kingdon, 1-Aug-2026.)
$\$ DECID

Theorem	wexmiddifxy 17212*	Being able to subtract an arbitrary finite set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 1-Aug-2026.)
WEXMID $/\$ $\$

14.4.5 Omniscience of NN+oo

Theorem	0nninf 17213	The zero element of ℕ_∞ (the constant sequence equal to ). (Contributed by Jim Kingdon, 14-Jul-2022.)
ℕ_∞

Theorem	nnsf 17214*	Domain and range of . Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.)
ℕ_∞ ℕ_∞ℕ_∞

Theorem	peano4nninf 17215*	The successor function on ℕ_∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.)
ℕ_∞ ℕ_∞ℕ_∞

Theorem	peano3nninf 17216*	The successor function on ℕ_∞ is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.)
ℕ_∞ ℕ_∞

Theorem	nninfalllem1 17217*	Lemma for nninfall 17218. (Contributed by Jim Kingdon, 1-Aug-2022.)
ℕ_∞ ℕ_∞

Theorem	nninfall 17218*	Given a decidable predicate on ℕ_∞, showing it holds for natural numbers and the point at infinity suffices to show it holds everywhere. The sense in which is a decidable predicate is that it assigns a value of either or (which can be thought of as false and true) to every element of ℕ_∞. Lemma 3.5 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.)
ℕ_∞ ℕ_∞

Theorem	nninfsellemdc 17219*	Lemma for nninfself 17222. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.)
ℕ_∞ $/\$ DECID

Theorem	nninfsellemcl 17220*	Lemma for nninfself 17222. (Contributed by Jim Kingdon, 8-Aug-2022.)
ℕ_∞ $/\$

Theorem	nninfsellemsuc 17221*	Lemma for nninfself 17222. (Contributed by Jim Kingdon, 6-Aug-2022.)
ℕ_∞ $/\$

Theorem	nninfself 17222*	Domain and range of the selection function for ℕ_∞. (Contributed by Jim Kingdon, 6-Aug-2022.)
ℕ_∞ ℕ_∞ℕ_∞

Theorem	nninfsellemeq 17223*	Lemma for nninfsel 17226. (Contributed by Jim Kingdon, 9-Aug-2022.)
ℕ_∞ ℕ_∞

Theorem	nninfsellemqall 17224*	Lemma for nninfsel 17226. (Contributed by Jim Kingdon, 9-Aug-2022.)
ℕ_∞ ℕ_∞

Theorem	nninfsellemeqinf 17225*	Lemma for nninfsel 17226. (Contributed by Jim Kingdon, 9-Aug-2022.)
ℕ_∞ ℕ_∞

Theorem	nninfsel 17226*	is a selection function for ℕ_∞. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.)
ℕ_∞ ℕ_∞ ℕ_∞

Theorem	nninfomnilem 17227*	Lemma for nninfomni 17228. (Contributed by Jim Kingdon, 10-Aug-2022.)
ℕ_∞ ℕ_∞ Omni

Theorem	nninfomni 17228	ℕ_∞ is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.)
ℕ_∞ Omni

Theorem	nninffeq 17229*	Equality of two functions on ℕ_∞ which agree at every integer and at the point at infinity. From an online post by Martin Escardo. Remark: the last two hypotheses can be grouped into one, . (Contributed by Jim Kingdon, 4-Aug-2023.)
ℕ_∞ ℕ_∞

Theorem	nnnninfen 17230	Equinumerosity of the natural numbers and ℕ_∞ is equivalent to the Limited Principle of Omniscience (LPO). Remark in Section 1.1 of [Pradic2025], p. 2. (Contributed by Jim Kingdon, 8-Jul-2025.)
ℕ_∞ Omni

Theorem	nnnninfex 17231*	If an element of ℕ_∞ has a value of zero somewhere, then it is the mapping of a natural number. (Contributed by Jim Kingdon, 4-Aug-2022.)
ℕ_∞

Theorem	nninfnfiinf 17232*	An element of ℕ_∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.)
ℕ_∞ $/\$

14.4.6 Schroeder-Bernstein Theorem

Theorem	exmidsbthrlem 17233*	Lemma for exmidsbthr 17234. (Contributed by Jim Kingdon, 11-Aug-2022.)
ℕ_∞ $/\$ EXMID

Theorem	exmidsbthr 17234*	The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.)
$/\$ EXMID

Theorem	exmidsbth 17235*	The Schroeder-Bernstein Theorem is equivalent to excluded middle. This is Metamath 100 proof #25. The forward direction (isbth 7284) is the proof of the Schroeder-Bernstein Theorem from the Metamath Proof Explorer database (in which excluded middle holds), but adapted to use EXMID as an antecedent rather than being unconditionally true, as in the non-intuitionistic proof at https://us.metamath.org/mpeuni/sbth.html 7284. The reverse direction (exmidsbthr 17234) is the one which establishes that Schroeder-Bernstein implies excluded middle. This resolves the question of whether we will be able to prove Schroeder-Bernstein from our axioms in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.)
EXMID $/\$

Theorem	sbthomlem 17236	Lemma for sbthom 17237. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.)
Omni ⊔ $\/$

Theorem	sbthom 17237	Schroeder-Bernstein is not possible even for . We know by exmidsbth 17235 that full Schroeder-Bernstein will not be provable but what about the case where one of the sets is ? That case plus the Limited Principle of Omniscience (LPO) implies excluded middle, so we will not be able to prove it. (Contributed by Mario Carneiro and Jim Kingdon, 10-Jul-2023.)
$/\$ $/\$ Omni EXMID

14.4.7 Real and complex numbers

Theorem	qdencn 17238*	The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 11985 (and also would hold for with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.)
$/\$ $/\$

Theorem	refeq 17239*	Equality of two real functions which agree at negative numbers, positive numbers, and zero. This holds even without real trichotomy. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 9-Jul-2023.)


Theorem	repiecelem 17240*	Lemma for repiecele0 17241, repiecege0 17242, and repiecef 17243. The function is defined everywhere. (Contributed by Jim Kingdon, 27-Apr-2026.)
inf $/\$ inf

Theorem	repiecele0 17241*	Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 17243 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
inf $/\$ $/\$

Theorem	repiecege0 17242*	Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 17243 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
inf $/\$ $/\$

Theorem	repiecef 17243*	Piecewise definition on the reals yields a function. The function agrees with and on their respective parts of the real line; see repiecele0 17241 and repiecege0 17242. From an online post by James E Hanson. The construction was published in Martín Hötzel Escardó, "Effective and sequential definition by cases on the reals via infinite signed-digit numerals", Electronic Notes in Theoretical Computer Science 10 (1998), page 2, https://martinescardo.github.io/papers/lexnew.pdf. 17242 (Contributed by Jim Kingdon, 27-Apr-2026.)
inf

Theorem	triap 17244	Two ways of stating real number trichotomy. See also cndcap 17276 which is similar but for complex number apartness. (Contributed by Jim Kingdon, 23-Aug-2023.)
$/\$ $\/$ $\/$ DECID #

Theorem	isomninnlem 17245*	Lemma for isomninn 17246. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.)
frec Omni $\/$

Theorem	isomninn 17246*	Omniscience stated in terms of natural numbers. Similar to isomnimap 7478 but it will sometimes be more convenient to use and rather than and . (Contributed by Jim Kingdon, 30-Aug-2023.)
Omni $\/$

Theorem	cvgcmp2nlemabs 17247*	Lemma for cvgcmp2n 17248. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting as the sum of and a term which gets smaller as gets large. (Contributed by Jim Kingdon, 25-Aug-2023.)
$/\$ $/\$ $/\$

Theorem	cvgcmp2n 17248*	A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.)
$/\$ $/\$ $/\$

Theorem	iooref1o 17249	A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.)


Theorem	iooreen 17250	An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.)


Theorem	rirrdisj 17251*	The rational and irrational numbers are disjoint. Here irrational means apart from any rational number. (Contributed by Jim Kingdon, 18-Sep-2026.)
#

14.4.8 Analytic omniscience principles Omniscience principles refer to several propositions, most of them weaker than full excluded middle, which do not follow from the axioms of IZF set theory. They are: (0) the Principle of Omniscience (PO), which is another name for excluded middle (see exmidomni 7483), (1) the Limited Principle of Omniscience (LPO) is Omni (see df-omni 7476), (2) the Weak Limited Principle of Omniscience (WLPO) is WOmni (see df-womni 7505), (3) Markov's Principle (MP) is Markov (see df-markov 7493), (4) the Lesser Limited Principle of Omniscience (LLPO) is not yet defined in iset.mm. They also have analytic counterparts each of which follows from the corresponding omniscience principle: (1) Analytic LPO is real number trichotomy, $\/$ $\/$ (see trilpo 17259), (2) Analytic WLPO is decidability of real number equality, DECID (see redcwlpo 17272), (3) Analytic MP is # (see neapmkv 17285), (4) Analytic LLPO is real number dichotomy, $\/$ (most relevant current theorem is maxclpr 12005).

Theorem	trilpolemclim 17252*	Lemma for trilpo 17259. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.)


Theorem	trilpolemcl 17253*	Lemma for trilpo 17259. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.)


Theorem	trilpolemisumle 17254*	Lemma for trilpo 17259. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.)


Theorem	trilpolemgt1 17255*	Lemma for trilpo 17259. The case. (Contributed by Jim Kingdon, 23-Aug-2023.)


Theorem	trilpolemeq1 17256*	Lemma for trilpo 17259. The case. This is proved by noting that if any is zero, then the infinite sum is less than one based on the term which is zero. We are using the fact that the sequence is decidable (in the sense that each element is either zero or one). (Contributed by Jim Kingdon, 23-Aug-2023.)


Theorem	trilpolemlt1 17257*	Lemma for trilpo 17259. The case. We can use the distance between and one (that is, ) to find a position in the sequence where terms after that point will not add up to as much as . By finomni 7481 we know the terms up to either contain a zero or are all one. But if they are all one that contradicts the way we constructed , so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.)


Theorem	trilpolemres 17258*	Lemma for trilpo 17259. The result. (Contributed by Jim Kingdon, 23-Aug-2023.)
$\/$ $\/$ $\/$

Theorem	trilpo 17259*	Real number trichotomy implies the Limited Principle of Omniscience (LPO). We expect that we'd need some form of countable choice to prove the converse. Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence contains a zero or it is all ones. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. Compare it with one using trichotomy. The three cases from trichotomy are trilpolemlt1 17257 (which means the sequence contains a zero), trilpolemeq1 17256 (which means the sequence is all ones), and trilpolemgt1 17255 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 17244) or that the real numbers are a discrete field (see trirec0 17260). LPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qtri3or 10686 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.)
$\/$ $\/$ Omni

Theorem	trirec0 17260*	Every real number having a reciprocal or equaling zero is equivalent to real number trichotomy. This is the key part of the definition of what is known as a discrete field, so "the real numbers are a discrete field" can be taken as an equivalent way to state real trichotomy (see further discussion at trilpo 17259). (Contributed by Jim Kingdon, 10-Jun-2024.)
$\/$ $\/$ $\/$

Theorem	trirec0xor 17261*	Version of trirec0 17260 with exclusive-or. The definition of a discrete field is sometimes stated in terms of exclusive-or but as proved here, this is equivalent to inclusive-or because the two disjuncts cannot be simultaneously true. (Contributed by Jim Kingdon, 10-Jun-2024.)
$\/$ $\/$ $\/_$

Theorem	apdifflemf 17262	Lemma for apdiff 17264. Being apart from the point halfway between and suffices for to be a different distance from and from . (Contributed by Jim Kingdon, 18-May-2024.)
# #

Theorem	apdifflemr 17263	Lemma for apdiff 17264. (Contributed by Jim Kingdon, 19-May-2024.)
# $/\$ # #

Theorem	apdiff 17264*	The irrationals (reals apart from any rational) are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 17-May-2024.)
# #

Theorem	qdiff 17265*	The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to apdiff 17264 but by stating the result positively we can completely sidestep the issue of not equal versus apart in the statement of the result. From an online post by Ingo Blechschmidt. (Contributed by Jim Kingdon, 24-Apr-2026.)
$/\$

Theorem	iswomninnlem 17266*	Lemma for iswomnimap 7507. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.)
frec WOmni DECID

Theorem	iswomninn 17267*	Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7507 but it will sometimes be more convenient to use and rather than and . (Contributed by Jim Kingdon, 20-Jun-2024.)
WOmni DECID

Theorem	iswomni0 17268*	Weak omniscience stated in terms of equality with . Like iswomninn 17267 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)
WOmni DECID

Theorem	ismkvnnlem 17269*	Lemma for ismkvnn 17270. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
frec Markov

Theorem	ismkvnn 17270*	The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.)
Markov

Theorem	redcwlpolemeq1 17271*	Lemma for redcwlpo 17272. A biconditionalized version of trilpolemeq1 17256. (Contributed by Jim Kingdon, 21-Jun-2024.)


Theorem	redcwlpo 17272*	Decidability of real number equality implies the Weak Limited Principle of Omniscience (WLPO). We expect that we'd need some form of countable choice to prove the converse. Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence is all ones or it is not. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. This real number will equal one if and only if the sequence is all ones (redcwlpolemeq1 17271). Therefore decidability of real number equality would imply decidability of whether the sequence is all ones. Because of this theorem, decidability of real number equality is sometimes called "analytic WLPO". WLPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qdceq 10690 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.)
DECID WOmni

Theorem	tridceq 17273*	Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 17259 and redcwlpo 17272). Thus, this is an analytic analogue to lpowlpo 7509. (Contributed by Jim Kingdon, 24-Jul-2024.)
$\/$ $\/$ DECID

Theorem	redc0 17274*	Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.)
DECID DECID

Theorem	reap0 17275*	Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.)
$\/$ $\/$ DECID #

Theorem	cndcap 17276*	Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.)
$\/$ $\/$ DECID #

Theorem	dceqnconst 17277*	Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 17272 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.)
DECID $/\$ $/\$

Theorem	dcapnconst 17278*	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See trilpo 17259 for more discussion of decidability of real number apartness. This is a weaker form of dceqnconst 17277 and in fact this theorem can be proved using dceqnconst 17277 as shown at dcapnconstALT 17279. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.)
DECID # $/\$ $/\$

Theorem	dcapnconstALT 17279*	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 17278 by means of dceqnconst 17277. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
DECID # $/\$ $/\$

Theorem	nconstwlpolem0 17280*	Lemma for nconstwlpo 17283. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.)


Theorem	nconstwlpolemgt0 17281*	Lemma for nconstwlpo 17283. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)


Theorem	nconstwlpolem 17282*	Lemma for nconstwlpo 17283. (Contributed by Jim Kingdon, 23-Jul-2024.)
$/\$ $\/$

Theorem	nconstwlpo 17283*	Existence of a certain non-constant function from reals to integers implies WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.)
$/\$ WOmni

Theorem	neapmkvlem 17284*	Lemma for neapmkv 17285. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
$/\$ #

Theorem	neapmkv 17285*	If negated equality for real numbers implies apartness, Markov's Principle follows. Exercise 11.10 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 24-Jun-2024.)
# Markov

Theorem	neap0mkv 17286*	The analytic Markov principle can be expressed either with two arbitrary real numbers, or one arbitrary number and zero. (Contributed by Jim Kingdon, 23-Feb-2025.)
# #

Theorem	ltlenmkv 17287*	If can be expressed as holding exactly when holds and the values are not equal, then the analytic Markov's Principle applies. (To get the regular Markov's Principle, combine with neapmkv 17285). (Contributed by Jim Kingdon, 23-Feb-2025.)
$/\$ #

14.4.9 Supremum and infimum

Theorem	supfz 17288	The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)


Theorem	inffz 17289	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
inf

14.4.10 Circle constant

Theorem	taupi 17290	Relationship between and . 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.)


14.5 Mathbox for Mykola Mostovenko

Theorem	ax1hfs 17291	Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)
$/\$

14.6 Mathbox for David A. Wheeler

14.6.1 Testable propositions

Theorem	dftest 17292	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 corresponds to " 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 $\/$

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 do not imply that 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 , and when restricted (applied to a class) we allow . The first symbol after the setvar variable must always be if it is the form applied to a class, and since cannot begin a wff, it is unambiguous. The looks like it would be a problem because or might include implications, but any implication arrow within any wff must be surrounded by parentheses, so only the implication arrow of 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: gives df-ral 2533 and gives df-rex 2534, so df-als 17295 (the general form) gives df-rals 17296 (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 17296 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 being inhabited ( ) is a stronger claim here than its being nonempty ( ); see n0r 3535. The allsome quantifier asserts that a witness exists, which is the stronger notion, so where set.mm states a result using 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 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 17293	Extend wff definition to include "all some" applied to a top-level implication, which means is true whenever is true, and there is at least one where is true. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)


Syntax	wrals 17294	Extend wff definition to include "all some" applied to a class, which means is true whenever is true for in , and there is at least one in where is true. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)


Definition	df-als 17295	Define "all some" applied to a top-level implication, which means is true whenever is true and there is at least one where is true. (Contributed by David A. Wheeler, 20-Oct-2018.)
$/\$

Definition	df-rals 17296	Define "all some" applied to a class, which means is true whenever is true for in , and there is at least one in where 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 to the members of a class, asserting only $/\$ , that is, that the formula held throughout and that had at least one member. I've now decided that that was a mistake. Its older existence conjunct did not require any member of 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.)
$/\$

Theorem	dfrals2 17297	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.)
$/\$

Theorem	alsd 17298	Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17300 and als2d 17301 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.)


Theorem	ralsd 17299	Introduction rule for "all some" restricted to a class. This is the converse of rals1d 17302 and rals2d 17303 taken together. (Contributed by David A. Wheeler, 12-Jul-2026.)


Theorem	als1d 17300	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.)

< Previous Next >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17346

< Previous Next >