Home | Intuitionistic Logic Explorer Theorem List (p. 137 of 137) | < Previous Wrap > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | strcollnft 13601* | Closed form of strcollnf 13602. (Contributed by BJ, 21-Oct-2019.) |
⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))) | ||
Theorem | strcollnf 13602* |
Version of ax-strcoll 13599 with one disjoint variable condition
removed,
the other disjoint variable condition replaced with a nonfreeness
hypothesis, and without initial universal quantifier. Version of
strcoll2 13600 with the disjoint variable condition on
𝑏, 𝜑 replaced
with a nonfreeness hypothesis.
This proof aims to demonstrate a standard technique, but strcoll2 13600 will generally suffice: since the theorem asserts the existence of a set 𝑏, supposing that that setvar does not occur in the already defined 𝜑 is not a big constraint. (Contributed by BJ, 21-Oct-2019.) |
⊢ Ⅎ𝑏𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | strcollnfALT 13603* | Alternate proof of strcollnf 13602, not using strcollnft 13601. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑏𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) | ||
In this section, we state the axiom scheme of subset collection, which is part of CZF set theory. | ||
Axiom | ax-sscoll 13604* | Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that 𝜑 represents a multivalued function from 𝑎 to 𝑏, or equivalently a collection of nonempty subsets of 𝑏 indexed by 𝑎, and the consequent asserts the existence of a subset of 𝑐 which "collects" at least one element in the image of each 𝑥 ∈ 𝑎 and which is made only of such elements. The axiom asserts the existence, for any sets 𝑎, 𝑏, of a set 𝑐 such that that implication holds for any value of the parameter 𝑧 of 𝜑. (Contributed by BJ, 5-Oct-2019.) |
⊢ ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | sscoll2 13605* | Version of ax-sscoll 13604 with two disjoint variable conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.) |
⊢ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑)) | ||
Axiom | ax-ddkcomp 13606 | Axiom of Dedekind completeness for Dedekind real numbers: every inhabited upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then Axiom ax-ddkcomp 13606 should be used in place of construction specific results. In particular, axcaucvg 7821 should be proved from it. (Contributed by BJ, 24-Oct-2021.) |
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵))) | ||
Theorem | ss1oel2o 13607 | Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4160 which more directly illustrates the contrast with el2oss1o 6391. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ 1_{o} → 𝑥 ∈ 2_{o})) | ||
Theorem | nnti 13608 | Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.) |
⊢ (𝜑 → 𝐴 ∈ ω) ⇒ ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢 E 𝑣 ∧ ¬ 𝑣 E 𝑢))) | ||
Theorem | 012of 13609 | Mapping zero and one between ℕ_{0} and ω style integers. (Contributed by Jim Kingdon, 28-Jun-2024.) |
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ⇒ ⊢ (^{◡}𝐺 ↾ {0, 1}):{0, 1}⟶2_{o} | ||
Theorem | 2o01f 13610 | Mapping zero and one between ω and ℕ_{0} style integers. (Contributed by Jim Kingdon, 28-Jun-2024.) |
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ⇒ ⊢ (𝐺 ↾ 2_{o}):2_{o}⟶{0, 1} | ||
Theorem | pwtrufal 13611 | A subset of the singleton {∅} cannot be anything other than ∅ or {∅}. Removing the double negation would change the meaning, as seen at exmid01 4160. If we view a subset of a singleton as a truth value (as seen in theorems like exmidexmid 4158), then this theorem states there are no truth values other than true and false, as described in section 1.1 of [Bauer], p. 481. (Contributed by Mario Carneiro and Jim Kingdon, 11-Sep-2023.) |
⊢ (𝐴 ⊆ {∅} → ¬ ¬ (𝐴 = ∅ ∨ 𝐴 = {∅})) | ||
Theorem | pwle2 13612* | An exercise related to 𝑁 copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝑁 ({𝑥} × 1_{o}) ⇒ ⊢ ((𝑁 ∈ ω ∧ 𝐺:𝑇–1-1→𝒫 1_{o}) → 𝑁 ⊆ 2_{o}) | ||
Theorem | pwf1oexmid 13613* | An exercise related to 𝑁 copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝑁 ({𝑥} × 1_{o}) ⇒ ⊢ ((𝑁 ∈ ω ∧ 𝐺:𝑇–1-1→𝒫 1_{o}) → (ran 𝐺 = 𝒫 1_{o} ↔ (𝑁 = 2_{o} ∧ EXMID))) | ||
Theorem | exmid1stab 13614* | If any proposition is stable, excluded middle follows. We are thinking of 𝑥 as a proposition and 𝑥 = {∅} as "x is true". (Contributed by Jim Kingdon, 28-Nov-2023.) |
⊢ ((𝜑 ∧ 𝑥 ⊆ {∅}) → STAB 𝑥 = {∅}) ⇒ ⊢ (𝜑 → EXMID) | ||
Theorem | subctctexmid 13615* | If every subcountable set is countable and Markov's principle holds, excluded middle follows. Proposition 2.6 of [BauerSwan], p. 14:4. The proof is taken from that paper. (Contributed by Jim Kingdon, 29-Nov-2023.) |
⊢ (𝜑 → ∀𝑥(∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝑥) → ∃𝑔 𝑔:ω–onto→(𝑥 ⊔ 1_{o}))) & ⊢ (𝜑 → ω ∈ Markov) ⇒ ⊢ (𝜑 → EXMID) | ||
Theorem | sssneq 13616* | Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.) |
⊢ (𝐴 ⊆ {𝐵} → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 𝑦 = 𝑧) | ||
Theorem | pw1nct 13617* | A condition which ensures that the powerset of a singleton is not countable. The antecedent here can be referred to as the uniformity principle. Based on Mastodon posts by Andrej Bauer and Rahul Chhabra. (Contributed by Jim Kingdon, 29-May-2024.) |
⊢ (∀𝑟(𝑟 ⊆ (𝒫 1_{o} × ω) → (∀𝑝 ∈ 𝒫 1_{o}∃𝑛 ∈ ω 𝑝𝑟𝑛 → ∃𝑚 ∈ ω ∀𝑞 ∈ 𝒫 1_{o}𝑞𝑟𝑚)) → ¬ ∃𝑓 𝑓:ω–onto→(𝒫 1_{o} ⊔ 1_{o})) | ||
Theorem | 0nninf 13618 | The zero element of ℕ_{∞} (the constant sequence equal to ∅). (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (ω × {∅}) ∈ ℕ_{∞} | ||
Theorem | nnsf 13619* | Domain and range of 𝑆. Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.) |
⊢ 𝑆 = (𝑝 ∈ ℕ_{∞} ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_{o}, (𝑝‘∪ 𝑖)))) ⇒ ⊢ 𝑆:ℕ_{∞}⟶ℕ_{∞} | ||
Theorem | peano4nninf 13620* | The successor function on ℕ_{∞} is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.) |
⊢ 𝑆 = (𝑝 ∈ ℕ_{∞} ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_{o}, (𝑝‘∪ 𝑖)))) ⇒ ⊢ 𝑆:ℕ_{∞}–1-1→ℕ_{∞} | ||
Theorem | peano3nninf 13621* | The successor function on ℕ_{∞} is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
⊢ 𝑆 = (𝑝 ∈ ℕ_{∞} ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_{o}, (𝑝‘∪ 𝑖)))) ⇒ ⊢ (𝐴 ∈ ℕ_{∞} → (𝑆‘𝐴) ≠ (𝑥 ∈ ω ↦ ∅)) | ||
Theorem | nninfalllem1 13622* | Lemma for nninfall 13623. (Contributed by Jim Kingdon, 1-Aug-2022.) |
⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝑥 ∈ ω ↦ 1_{o})) = 1_{o}) & ⊢ (𝜑 → ∀𝑛 ∈ ω (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{o}, ∅))) = 1_{o}) & ⊢ (𝜑 → 𝑃 ∈ ℕ_{∞}) & ⊢ (𝜑 → (𝑄‘𝑃) = ∅) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ ω (𝑃‘𝑛) = 1_{o}) | ||
Theorem | nninfall 13623* | 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 1_{o} (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.) |
⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝑥 ∈ ω ↦ 1_{o})) = 1_{o}) & ⊢ (𝜑 → ∀𝑛 ∈ ω (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{o}, ∅))) = 1_{o}) ⇒ ⊢ (𝜑 → ∀𝑝 ∈ ℕ_{∞} (𝑄‘𝑝) = 1_{o}) | ||
Theorem | nninfsellemdc 13624* | Lemma for nninfself 13627. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ ((𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ∧ 𝑁 ∈ ω) → DECID ∀𝑘 ∈ suc 𝑁(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}) | ||
Theorem | nninfsellemcl 13625* | Lemma for nninfself 13627. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ ((𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ∧ 𝑁 ∈ ω) → if(∀𝑘 ∈ suc 𝑁(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅) ∈ 2_{o}) | ||
Theorem | nninfsellemsuc 13626* | Lemma for nninfself 13627. (Contributed by Jim Kingdon, 6-Aug-2022.) |
⊢ ((𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ∧ 𝐽 ∈ ω) → if(∀𝑘 ∈ suc suc 𝐽(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅) ⊆ if(∀𝑘 ∈ suc 𝐽(𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅)) | ||
Theorem | nninfself 13627* | Domain and range of the selection function for ℕ_{∞}. (Contributed by Jim Kingdon, 6-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) ⇒ ⊢ 𝐸:(2_{o} ↑_{𝑚} ℕ_{∞})⟶ℕ_{∞} | ||
Theorem | nninfsellemeq 13628* | Lemma for nninfsel 13631. (Contributed by Jim Kingdon, 9-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) & ⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1_{o}) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∀𝑘 ∈ 𝑁 (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}) & ⊢ (𝜑 → (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1_{o}, ∅))) = ∅) ⇒ ⊢ (𝜑 → (𝐸‘𝑄) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1_{o}, ∅))) | ||
Theorem | nninfsellemqall 13629* | Lemma for nninfsel 13631. (Contributed by Jim Kingdon, 9-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) & ⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1_{o}) & ⊢ (𝜑 → 𝑁 ∈ ω) ⇒ ⊢ (𝜑 → (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1_{o}, ∅))) = 1_{o}) | ||
Theorem | nninfsellemeqinf 13630* | Lemma for nninfsel 13631. (Contributed by Jim Kingdon, 9-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) & ⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1_{o}) ⇒ ⊢ (𝜑 → (𝐸‘𝑄) = (𝑖 ∈ ω ↦ 1_{o})) | ||
Theorem | nninfsel 13631* | 𝐸 is a selection function for ℕ_{∞}. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) & ⊢ (𝜑 → 𝑄 ∈ (2_{o} ↑_{𝑚} ℕ_{∞})) & ⊢ (𝜑 → (𝑄‘(𝐸‘𝑄)) = 1_{o}) ⇒ ⊢ (𝜑 → ∀𝑝 ∈ ℕ_{∞} (𝑄‘𝑝) = 1_{o}) | ||
Theorem | nninfomnilem 13632* | Lemma for nninfomni 13633. (Contributed by Jim Kingdon, 10-Aug-2022.) |
⊢ 𝐸 = (𝑞 ∈ (2_{o} ↑_{𝑚} ℕ_{∞}) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1_{o}, ∅))) = 1_{o}, 1_{o}, ∅))) ⇒ ⊢ ℕ_{∞} ∈ Omni | ||
Theorem | nninfomni 13633 | ℕ_{∞} is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.) |
⊢ ℕ_{∞} ∈ Omni | ||
Theorem | nninffeq 13634* | 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, ⊢ (𝜑 → ∀𝑛 ∈ suc ω...). (Contributed by Jim Kingdon, 4-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ_{∞}⟶ℕ_{0}) & ⊢ (𝜑 → 𝐺:ℕ_{∞}⟶ℕ_{0}) & ⊢ (𝜑 → (𝐹‘(𝑥 ∈ ω ↦ 1_{o})) = (𝐺‘(𝑥 ∈ ω ↦ 1_{o}))) & ⊢ (𝜑 → ∀𝑛 ∈ ω (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{o}, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1_{o}, ∅)))) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | exmidsbthrlem 13635* | Lemma for exmidsbthr 13636. (Contributed by Jim Kingdon, 11-Aug-2022.) |
⊢ 𝑆 = (𝑝 ∈ ℕ_{∞} ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1_{o}, (𝑝‘∪ 𝑖)))) ⇒ ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID) | ||
Theorem | exmidsbthr 13636* | The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.) |
⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID) | ||
Theorem | exmidsbth 13637* |
The Schroeder-Bernstein Theorem is equivalent to excluded middle. This
is Metamath 100 proof #25. The forward direction (isbth 6912) 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 6912.
The reverse direction (exmidsbthr 13636) 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 13638 | Lemma for sbthom 13639. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.) |
⊢ (𝜑 → ω ∈ Omni) & ⊢ (𝜑 → 𝑌 ⊆ {∅}) & ⊢ (𝜑 → 𝐹:ω–1-1-onto→(𝑌 ⊔ ω)) ⇒ ⊢ (𝜑 → (𝑌 = ∅ ∨ 𝑌 = {∅})) | ||
Theorem | sbthom 13639 | Schroeder-Bernstein is not possible even for ω. We know by exmidsbth 13637 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) | ||
Theorem | qdencn 13640* | 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 11106 (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‘(𝑥 − 𝐴)) < 𝐵) | ||
Theorem | refeq 13641* | 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)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | triap 13642 | Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) ↔ DECID 𝐴 # 𝐵)) | ||
Theorem | isomninnlem 13643* | Lemma for isomninn 13644. 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))) | ||
Theorem | isomninn 13644* | Omniscience stated in terms of natural numbers. Similar to isomnimap 7081 but it will sometimes be more convenient to use 0 and 1 rather than ∅ and 1_{o}. (Contributed by Jim Kingdon, 30-Aug-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑_{𝑚} 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))) | ||
Theorem | cvgcmp2nlemabs 13645* | Lemma for cvgcmp2n 13646. 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 / 𝑀)) | ||
Theorem | cvgcmp2n 13646* | A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (1 / (2↑𝑘))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ ) | ||
Theorem | iooref1o 13647 | 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) | ||
Theorem | iooreen 13648 | An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.) |
⊢ (0(,)1) ≈ ℝ | ||
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 7086), (1) the Limited Principle of Omniscience (LPO) is ω ∈ Omni (see df-omni 7079), (2) the Weak Limited Principle of Omniscience (WLPO) is ω ∈ WOmni (see df-womni 7108), (3) Markov's Principle (MP) is ω ∈ Markov (see df-markov 7096), (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 13656), (2) Analytic WLPO is decidability of real number equality, ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝDECID 𝑥 = 𝑦 (see redcwlpo 13668), (3) Analytic MP is ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥 ≠ 𝑦 → 𝑥 # 𝑦) (see neapmkv 13680), (4) Analytic LLPO is real number dichotomy, ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥) (most relevant current theorem is maxclpr 11126). | ||
Theorem | trilpolemclim 13649* | Lemma for trilpo 13656. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛))) ⇒ ⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ ) | ||
Theorem | trilpolemcl 13650* | Lemma for trilpo 13656. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | trilpolemisumle 13651* | Lemma for trilpo 13656. 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↑𝑖))) | ||
Theorem | trilpolemgt1 13652* | Lemma for trilpo 13656. The 1 < 𝐴 case. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ⇒ ⊢ (𝜑 → ¬ 1 < 𝐴) | ||
Theorem | trilpolemeq1 13653* | Lemma for trilpo 13656. 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) | ||
Theorem | trilpolemlt1 13654* | Lemma for trilpo 13656. 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 7084 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) | ||
Theorem | trilpolemres 13655* | Lemma for trilpo 13656. The result. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) & ⊢ (𝜑 → (𝐴 < 1 ∨ 𝐴 = 1 ∨ 1 < 𝐴)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0 ∨ ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)) | ||
Theorem | trilpo 13656* |
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 13654 (which means the sequence contains a zero), trilpolemeq1 13653 (which means the sequence is all ones), and trilpolemgt1 13652 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 13642) or that the real numbers are a discrete field (see trirec0 13657). 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 10146 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.) |
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ω ∈ Omni) | ||
Theorem | trirec0 13657* |
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 13656). (Contributed by Jim Kingdon, 10-Jun-2024.) |
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑥 ∈ ℝ (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0)) | ||
Theorem | trirec0xor 13658* |
Version of trirec0 13657 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)) | ||
Theorem | apdifflemf 13659 | Lemma for apdiff 13661. 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‘(𝐴 − 𝑅))) | ||
Theorem | apdifflemr 13660 | Lemma for apdiff 13661. (Contributed by Jim Kingdon, 19-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑆 ∈ ℚ) & ⊢ (𝜑 → (abs‘(𝐴 − -1)) # (abs‘(𝐴 − 1))) & ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑆)))) ⇒ ⊢ (𝜑 → 𝐴 # 𝑆) | ||
Theorem | apdiff 13661* | 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‘(𝐴 − 𝑟))))) | ||
Theorem | iswomninnlem 13662* | Lemma for iswomnimap 7110. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.) |
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑_{𝑚} 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) | ||
Theorem | iswomninn 13663* | Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7110 but it will sometimes be more convenient to use 0 and 1 rather than ∅ and 1_{o}. (Contributed by Jim Kingdon, 20-Jun-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑_{𝑚} 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)) | ||
Theorem | iswomni0 13664* | Weak omniscience stated in terms of equality with 0. Like iswomninn 13663 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑_{𝑚} 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)) | ||
Theorem | ismkvnnlem 13665* | Lemma for ismkvnn 13666. 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))) | ||
Theorem | ismkvnn 13666* | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑_{𝑚} 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))) | ||
Theorem | redcwlpolemeq1 13667* | Lemma for redcwlpo 13668. A biconditionalized version of trilpolemeq1 13653. (Contributed by Jim Kingdon, 21-Jun-2024.) |
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ⇒ ⊢ (𝜑 → (𝐴 = 1 ↔ ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)) | ||
Theorem | redcwlpo 13668* |
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 13667). 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 10150 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.) |
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦 → ω ∈ WOmni) | ||
Theorem | tridceq 13669* | Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 13656 and redcwlpo 13668). Thus, this is an analytic analogue to lpowlpo 7112. (Contributed by Jim Kingdon, 24-Jul-2024.) |
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦) | ||
Theorem | redc0 13670* | Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.) |
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦 ↔ ∀𝑧 ∈ ℝ DECID 𝑧 = 0) | ||
Theorem | reap0 13671* | Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.) |
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑧 ∈ ℝ DECID 𝑧 # 0) | ||
Theorem | dceqnconst 13672* | 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 13668 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)) | ||
Theorem | dcapnconst 13673* |
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 13656 for more
discussion of decidability of real number apartness.
This is a weaker form of dceqnconst 13672 and in fact this theorem can be proved using dceqnconst 13672 as shown at dcapnconstALT 13674. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) |
⊢ (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ^{+} (𝑓‘𝑥) ≠ 0)) | ||
Theorem | dcapnconstALT 13674* | Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 13673 by means of dceqnconst 13672. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ^{+} (𝑓‘𝑥) ≠ 0)) | ||
Theorem | nconstwlpolem0 13675* | Lemma for nconstwlpo 13678. 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) | ||
Theorem | nconstwlpolemgt0 13676* | Lemma for nconstwlpo 13678. 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 < 𝐴) | ||
Theorem | nconstwlpolem 13677* | Lemma for nconstwlpo 13678. (Contributed by Jim Kingdon, 23-Jul-2024.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℤ) & ⊢ (𝜑 → (𝐹‘0) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ^{+}) → (𝐹‘𝑥) ≠ 0) & ⊢ (𝜑 → 𝐺:ℕ⟶{0, 1}) & ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖)) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ ℕ (𝐺‘𝑦) = 0 ∨ ¬ ∀𝑦 ∈ ℕ (𝐺‘𝑦) = 0)) | ||
Theorem | nconstwlpo 13678* | 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) | ||
Theorem | neapmkvlem 13679* | Lemma for neapmkv 13680. 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)) | ||
Theorem | neapmkv 13680* | 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 | supfz 13681 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁) | ||
Theorem | inffz 13682 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
⊢ (𝑁 ∈ (ℤ_{≥}‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀) | ||
Theorem | taupi 13683 | 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 · π) | ||
Theorem | ax1hfs 13684 | Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.) |
⊢ (𝜑 → (𝜑 ∧ 𝜑)) | ||
Theorem | dftest 13685 |
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 ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑)) | ||
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. | ||
Syntax | walsi 13686 | 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 ∀!𝑥(𝜑 → 𝜓) | ||
Syntax | walsc 13687 | 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 ∀!𝑥 ∈ 𝐴𝜑 | ||
Definition | df-alsi 13688 | 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-alsc 13689 | 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.) |
⊢ (∀!𝑥 ∈ 𝐴𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | alsconv 13690 | There is an equivalence between the two "all some" forms. (Contributed by David A. Wheeler, 22-Oct-2018.) |
⊢ (∀!𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀!𝑥 ∈ 𝐴𝜑) | ||
Theorem | alsi1d 13691 | 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.) |
⊢ (𝜑 → ∀!𝑥(𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒)) | ||
Theorem | alsi2d 13692 | 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.) |
⊢ (𝜑 → ∀!𝑥(𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | alsc1d 13693 | Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
⊢ (𝜑 → ∀!𝑥 ∈ 𝐴𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | alsc2d 13694 | Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.) |
⊢ (𝜑 → ∀!𝑥 ∈ 𝐴𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
< Previous Wrap > |
Copyright terms: Public domain | < Previous Wrap > |