Home Intuitionistic Logic ExplorerTheorem List (p. 135 of 135) < Previous  Wrap > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 13401-13470   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremnninfsellemcl 13401* Lemma for nninfself 13403. (Contributed by Jim Kingdon, 8-Aug-2022.)
((𝑄 ∈ (2o𝑚) ∧ 𝑁 ∈ ω) → if(∀𝑘 ∈ suc 𝑁(𝑄‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) ∈ 2o)

Theoremnninfsellemsuc 13402* Lemma for nninfself 13403. (Contributed by Jim Kingdon, 6-Aug-2022.)
((𝑄 ∈ (2o𝑚) ∧ 𝐽 ∈ ω) → if(∀𝑘 ∈ suc suc 𝐽(𝑄‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) ⊆ if(∀𝑘 ∈ suc 𝐽(𝑄‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))

Theoremnninfself 13403* Domain and range of the selection function for . (Contributed by Jim Kingdon, 6-Aug-2022.)
𝐸 = (𝑞 ∈ (2o𝑚) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)))       𝐸:(2o𝑚)⟶ℕ

Theoremnninfsellemeq 13404* Lemma for nninfsel 13407. (Contributed by Jim Kingdon, 9-Aug-2022.)
𝐸 = (𝑞 ∈ (2o𝑚) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)))    &   (𝜑𝑄 ∈ (2o𝑚))    &   (𝜑 → (𝑄‘(𝐸𝑄)) = 1o)    &   (𝜑𝑁 ∈ ω)    &   (𝜑 → ∀𝑘𝑁 (𝑄‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o)    &   (𝜑 → (𝑄‘(𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))) = ∅)       (𝜑 → (𝐸𝑄) = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)))

Theoremnninfsellemqall 13405* Lemma for nninfsel 13407. (Contributed by Jim Kingdon, 9-Aug-2022.)
𝐸 = (𝑞 ∈ (2o𝑚) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)))    &   (𝜑𝑄 ∈ (2o𝑚))    &   (𝜑 → (𝑄‘(𝐸𝑄)) = 1o)    &   (𝜑𝑁 ∈ ω)       (𝜑 → (𝑄‘(𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))) = 1o)

Theoremnninfsellemeqinf 13406* Lemma for nninfsel 13407. (Contributed by Jim Kingdon, 9-Aug-2022.)
𝐸 = (𝑞 ∈ (2o𝑚) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)))    &   (𝜑𝑄 ∈ (2o𝑚))    &   (𝜑 → (𝑄‘(𝐸𝑄)) = 1o)       (𝜑 → (𝐸𝑄) = (𝑖 ∈ ω ↦ 1o))

Theoremnninfsel 13407* 𝐸 is a selection function for . Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.)
𝐸 = (𝑞 ∈ (2o𝑚) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)))    &   (𝜑𝑄 ∈ (2o𝑚))    &   (𝜑 → (𝑄‘(𝐸𝑄)) = 1o)       (𝜑 → ∀𝑝 ∈ ℕ (𝑄𝑝) = 1o)

Theoremnninfomnilem 13408* Lemma for nninfomni 13409. (Contributed by Jim Kingdon, 10-Aug-2022.)
𝐸 = (𝑞 ∈ (2o𝑚) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)))        ∈ Omni

Theoremnninfomni 13409 is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.)
∈ Omni

Theoremnninffeq 13410* Equality of two functions on which agree at every integer and at the point at infinity. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 4-Aug-2023.)
(𝜑𝐹:ℕ⟶ℕ0)    &   (𝜑𝐺:ℕ⟶ℕ0)    &   (𝜑 → (𝐹‘(𝑥 ∈ ω ↦ 1o)) = (𝐺‘(𝑥 ∈ ω ↦ 1o)))    &   (𝜑 → ∀𝑛 ∈ ω (𝐹‘(𝑖 ∈ ω ↦ if(𝑖𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖𝑛, 1o, ∅))))       (𝜑𝐹 = 𝐺)

11.3.4  Schroeder-Bernstein Theorem

Theoremexmidsbthrlem 13411* Lemma for exmidsbthr 13412. (Contributed by Jim Kingdon, 11-Aug-2022.)
𝑆 = (𝑝 ∈ ℕ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))))       (∀𝑥𝑦((𝑥𝑦𝑦𝑥) → 𝑥𝑦) → EXMID)

Theoremexmidsbthr 13412* The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.)
(∀𝑥𝑦((𝑥𝑦𝑦𝑥) → 𝑥𝑦) → EXMID)

Theoremexmidsbth 13413* The Schroeder-Bernstein Theorem is equivalent to excluded middle. This is Metamath 100 proof #25. The forward direction (isbth 6865) 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-intuitionist proof at https://us.metamath.org/mpeuni/sbth.html 6865.

The reverse direction (exmidsbthr 13412) 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 ↔ ∀𝑥𝑦((𝑥𝑦𝑦𝑥) → 𝑥𝑦))

Theoremsbthomlem 13414 Lemma for sbthom 13415. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.)
(𝜑 → ω ∈ Omni)    &   (𝜑𝑌 ⊆ {∅})    &   (𝜑𝐹:ω–1-1-onto→(𝑌 ⊔ ω))       (𝜑 → (𝑌 = ∅ ∨ 𝑌 = {∅}))

Theoremsbthom 13415 Schroeder-Bernstein is not possible even for ω. We know by exmidsbth 13413 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)

11.3.5  Real and complex numbers

Theoremqdencn 13416* 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 11026 (and also would hold for ℝ × ℝ with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.)
𝑄 = {𝑧 ∈ ℂ ∣ ((ℜ‘𝑧) ∈ ℚ ∧ (ℑ‘𝑧) ∈ ℚ)}       ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+) → ∃𝑥𝑄 (abs‘(𝑥𝐴)) < 𝐵)

Theoremrefeq 13417* 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.)
(𝜑𝐹:ℝ⟶ℝ)    &   (𝜑𝐺:ℝ⟶ℝ)    &   (𝜑 → ∀𝑥 ∈ ℝ (𝑥 < 0 → (𝐹𝑥) = (𝐺𝑥)))    &   (𝜑 → ∀𝑥 ∈ ℝ (0 < 𝑥 → (𝐹𝑥) = (𝐺𝑥)))    &   (𝜑 → (𝐹‘0) = (𝐺‘0))       (𝜑𝐹 = 𝐺)

Theoremtriap 13418 Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵𝐴 = 𝐵𝐵 < 𝐴) ↔ DECID 𝐴 # 𝐵))

Theoremisomninnlem 13419* Lemma for isomninn 13420. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)       (𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)))

Theoremisomninn 13420* Omniscience stated in terms of natural numbers. Similar to isomnimap 7019 but it will sometimes be more convenient to use 0 and 1 rather than and 1o. (Contributed by Jim Kingdon, 30-Aug-2023.)
(𝐴𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥𝐴 (𝑓𝑥) = 0 ∨ ∀𝑥𝐴 (𝑓𝑥) = 1)))

Theoremcvgcmp2nlemabs 13421* Lemma for cvgcmp2n 13422. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting (seq1( + , 𝐺)‘𝑁) as the sum of (seq1( + , 𝐺)‘𝑀) and a term which gets smaller as 𝑀 gets large. (Contributed by Jim Kingdon, 25-Aug-2023.)
((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘 ∈ ℕ) → 0 ≤ (𝐺𝑘))    &   ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (1 / (2↑𝑘)))    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ (ℤ𝑀))       (𝜑 → (abs‘((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀))) < (2 / 𝑀))

Theoremcvgcmp2n 13422* A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.)
((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)    &   ((𝜑𝑘 ∈ ℕ) → 0 ≤ (𝐺𝑘))    &   ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (1 / (2↑𝑘)))       (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ )

Theoremiooref1o 13423 A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.)
𝐹 = (𝑥 ∈ ℝ ↦ (1 / (1 + (exp‘𝑥))))       𝐹:ℝ–1-1-onto→(0(,)1)

Theoremiooreen 13424 An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.)
(0(,)1) ≈ ℝ

11.3.6  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 7024), (1) the Limited Principle of Omniscience (LPO) is ω ∈ Omni (see df-omni 7016), (2) the Weak Limited Principle of Omniscience (WLPO) is ω ∈ WOmni (see df-womni 7048), (3) Markov's Principle (MP) is ω ∈ Markov (see df-markov 7036), (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 13432), (2) Analytic WLPO is decidability of real number equality, 𝑥 ∈ ℝ∀𝑦 ∈ ℝDECID 𝑥 = 𝑦 (see redcwlpo 13444), (3) Analytic MP is 𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥𝑦𝑥 # 𝑦) (see neapmkv 13456), (4) Analytic LLPO is real number dichotomy, 𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥𝑦𝑦𝑥) (most relevant current theorem is maxclpr 11046).

Theoremtrilpolemclim 13425* Lemma for trilpo 13432. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.)
(𝜑𝐹:ℕ⟶{0, 1})    &   𝐺 = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹𝑛)))       (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ )

Theoremtrilpolemcl 13426* Lemma for trilpo 13432. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.)
(𝜑𝐹:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹𝑖))       (𝜑𝐴 ∈ ℝ)

Theoremtrilpolemisumle 13427* Lemma for trilpo 13432. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.)
(𝜑𝐹:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹𝑖))    &   𝑍 = (ℤ𝑀)    &   (𝜑𝑀 ∈ ℕ)       (𝜑 → Σ𝑖𝑍 ((1 / (2↑𝑖)) · (𝐹𝑖)) ≤ Σ𝑖𝑍 (1 / (2↑𝑖)))

Theoremtrilpolemgt1 13428* Lemma for trilpo 13432. The 1 < 𝐴 case. (Contributed by Jim Kingdon, 23-Aug-2023.)
(𝜑𝐹:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹𝑖))       (𝜑 → ¬ 1 < 𝐴)

Theoremtrilpolemeq1 13429* Lemma for trilpo 13432. The 𝐴 = 1 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.)
(𝜑𝐹:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹𝑖))    &   (𝜑𝐴 = 1)       (𝜑 → ∀𝑥 ∈ ℕ (𝐹𝑥) = 1)

Theoremtrilpolemlt1 13430* Lemma for trilpo 13432. The 𝐴 < 1 case. We can use the distance between 𝐴 and one (that is, 1 − 𝐴) to find a position in the sequence 𝑛 where terms after that point will not add up to as much as 1 − 𝐴. By finomni 7022 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.)
(𝜑𝐹:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹𝑖))    &   (𝜑𝐴 < 1)       (𝜑 → ∃𝑥 ∈ ℕ (𝐹𝑥) = 0)

Theoremtrilpolemres 13431* Lemma for trilpo 13432. The result. (Contributed by Jim Kingdon, 23-Aug-2023.)
(𝜑𝐹:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹𝑖))    &   (𝜑 → (𝐴 < 1 ∨ 𝐴 = 1 ∨ 1 < 𝐴))       (𝜑 → (∃𝑥 ∈ ℕ (𝐹𝑥) = 0 ∨ ∀𝑥 ∈ ℕ (𝐹𝑥) = 1))

Theoremtrilpo 13432* 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 13430 (which means the sequence contains a zero), trilpolemeq1 13429 (which means the sequence is all ones), and trilpolemgt1 13428 (which is not possible).

Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 13418) or that the real numbers are a discrete field (see trirec0 13433).

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 10071 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.)

(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦𝑥 = 𝑦𝑦 < 𝑥) → ω ∈ Omni)

Theoremtrirec0 13433* 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 13432). (Contributed by Jim Kingdon, 10-Jun-2024.)

(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦𝑥 = 𝑦𝑦 < 𝑥) ↔ ∀𝑥 ∈ ℝ (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0))

Theoremtrirec0xor 13434* Version of trirec0 13433 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.)

(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦𝑥 = 𝑦𝑦 < 𝑥) ↔ ∀𝑥 ∈ ℝ (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ⊻ 𝑥 = 0))

Theoremapdifflemf 13435 Lemma for apdiff 13437. 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.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝑄 ∈ ℚ)    &   (𝜑𝑅 ∈ ℚ)    &   (𝜑𝑄 < 𝑅)    &   (𝜑 → ((𝑄 + 𝑅) / 2) # 𝐴)       (𝜑 → (abs‘(𝐴𝑄)) # (abs‘(𝐴𝑅)))

Theoremapdifflemr 13436 Lemma for apdiff 13437. (Contributed by Jim Kingdon, 19-May-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝑆 ∈ ℚ)    &   (𝜑 → (abs‘(𝐴 − -1)) # (abs‘(𝐴 − 1)))    &   ((𝜑𝑆 ≠ 0) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑆))))       (𝜑𝐴 # 𝑆)

Theoremapdiff 13437* 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.)
(𝐴 ∈ ℝ → (∀𝑞 ∈ ℚ 𝐴 # 𝑞 ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞𝑟 → (abs‘(𝐴𝑞)) # (abs‘(𝐴𝑟)))))

Theoremiswomninnlem 13438* Lemma for iswomnimap 7050. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)       (𝐴𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1))

Theoremiswomninn 13439* Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7050 but it will sometimes be more convenient to use 0 and 1 rather than and 1o. (Contributed by Jim Kingdon, 20-Jun-2024.)
(𝐴𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 1))

Theoremiswomni0 13440* Weak omniscience stated in terms of equality with 0. Like iswomninn 13439 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)
(𝐴𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID𝑥𝐴 (𝑓𝑥) = 0))

Theoremismkvnnlem 13441* Lemma for ismkvnn 13442. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)       (𝐴𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)))

Theoremismkvnn 13442* The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.)
(𝐴𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥𝐴 (𝑓𝑥) = 1 → ∃𝑥𝐴 (𝑓𝑥) = 0)))

Theoremredcwlpolemeq1 13443* Lemma for redcwlpo 13444. A biconditionalized version of trilpolemeq1 13429. (Contributed by Jim Kingdon, 21-Jun-2024.)
(𝜑𝐹:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹𝑖))       (𝜑 → (𝐴 = 1 ↔ ∀𝑥 ∈ ℕ (𝐹𝑥) = 1))

Theoremredcwlpo 13444* 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 13443). 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 10075 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.)

(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦 → ω ∈ WOmni)

Theoremtridceq 13445* Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 13432 and redcwlpo 13444). Thus, this is an analytic analogue to lpowlpo 7052. (Contributed by Jim Kingdon, 24-Jul-2024.)
(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦𝑥 = 𝑦𝑦 < 𝑥) → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦)

Theoremredc0 13446* Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.)
(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦 ↔ ∀𝑧 ∈ ℝ DECID 𝑧 = 0)

Theoremreap0 13447* Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.)
(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦𝑥 = 𝑦𝑦 < 𝑥) ↔ ∀𝑧 ∈ ℝ DECID 𝑧 # 0)

Theoremdceqnconst 13448* 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 13444 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 𝑥 = 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓𝑥) ≠ 0))

Theoremdcapnconst 13449* 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 13432 for more discussion of decidability of real number apartness.

This is a weaker form of dceqnconst 13448 and in fact this theorem can be proved using dceqnconst 13448 as shown at dcapnconstALT 13450. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.)

(∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓𝑥) ≠ 0))

TheoremdcapnconstALT 13450* Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 13449 by means of dceqnconst 13448. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
(∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓𝑥) ≠ 0))

Theoremnconstwlpolem0 13451* Lemma for nconstwlpo 13454. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
(𝜑𝐺:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺𝑖))    &   (𝜑 → ∀𝑥 ∈ ℕ (𝐺𝑥) = 0)       (𝜑𝐴 = 0)

Theoremnconstwlpolemgt0 13452* Lemma for nconstwlpo 13454. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
(𝜑𝐺:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺𝑖))    &   (𝜑 → ∃𝑥 ∈ ℕ (𝐺𝑥) = 1)       (𝜑 → 0 < 𝐴)

Theoremnconstwlpolem 13453* Lemma for nconstwlpo 13454. (Contributed by Jim Kingdon, 23-Jul-2024.)
(𝜑𝐹:ℝ⟶ℤ)    &   (𝜑 → (𝐹‘0) = 0)    &   ((𝜑𝑥 ∈ ℝ+) → (𝐹𝑥) ≠ 0)    &   (𝜑𝐺:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺𝑖))       (𝜑 → (∀𝑦 ∈ ℕ (𝐺𝑦) = 0 ∨ ¬ ∀𝑦 ∈ ℕ (𝐺𝑦) = 0))

Theoremnconstwlpo 13454* 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.)
(𝜑𝐹:ℝ⟶ℤ)    &   (𝜑 → (𝐹‘0) = 0)    &   ((𝜑𝑥 ∈ ℝ+) → (𝐹𝑥) ≠ 0)       (𝜑 → ω ∈ WOmni)

Theoremneapmkvlem 13455* Lemma for neapmkv 13456. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
(𝜑𝐹:ℕ⟶{0, 1})    &   𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹𝑖))    &   ((𝜑𝐴 ≠ 1) → 𝐴 # 1)       (𝜑 → (¬ ∀𝑥 ∈ ℕ (𝐹𝑥) = 1 → ∃𝑥 ∈ ℕ (𝐹𝑥) = 0))

Theoremneapmkv 13456* 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)

11.3.7  Supremum and infimum

Theoremsupfz 13457 The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
(𝑁 ∈ (ℤ𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁)

Theoreminffz 13458 The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
(𝑁 ∈ (ℤ𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀)

11.3.8  Circle constant

Theoremtaupi 13459 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.)
τ = (2 · π)

11.4  Mathbox for Mykola Mostovenko

Theoremax1hfs 13460 Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)
(𝜑 → (𝜑𝜑))

11.5  Mathbox for David A. Wheeler

11.5.1  Testable propositions

Theoremdftest 13461 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 ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))

11.5.2  Allsome quantifier

These are definitions and proofs involving an experimental "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.

For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html I hope that others will eventually agree that allsome is awesome.

Syntaxwalsi 13462 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 least one 𝑥 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.)
wff ∀!𝑥(𝜑𝜓)

Syntaxwalsc 13463 Extend wff definition to include "all some" applied to a class, which means 𝜑 is true for all 𝑥 in 𝐴, and there is at least one 𝑥 in 𝐴. (Contributed by David A. Wheeler, 20-Oct-2018.)
wff ∀!𝑥𝐴𝜑

Definitiondf-alsi 13464 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.)
(∀!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃𝑥𝜑))

Definitiondf-alsc 13465 Define "all some" applied to a class, which means 𝜑 is true for all 𝑥 in 𝐴 and there is at least one 𝑥 in 𝐴. (Contributed by David A. Wheeler, 20-Oct-2018.)
(∀!𝑥𝐴𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∃𝑥 𝑥𝐴))

Theoremalsconv 13466 There is an equivalence between the two "all some" forms. (Contributed by David A. Wheeler, 22-Oct-2018.)
(∀!𝑥(𝑥𝐴𝜑) ↔ ∀!𝑥𝐴𝜑)

Theoremalsi1d 13467 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.)
(𝜑 → ∀!𝑥(𝜓𝜒))       (𝜑 → ∀𝑥(𝜓𝜒))

Theoremalsi2d 13468 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.)
(𝜑 → ∀!𝑥(𝜓𝜒))       (𝜑 → ∃𝑥𝜓)

Theoremalsc1d 13469 Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
(𝜑 → ∀!𝑥𝐴𝜓)       (𝜑 → ∀𝑥𝐴 𝜓)

Theoremalsc2d 13470 Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
(𝜑 → ∀!𝑥𝐴𝜓)       (𝜑 → ∃𝑥 𝑥𝐴)

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-13470
 Copyright terms: Public domain < Previous  Wrap >