Home | Intuitionistic Logic Explorer Theorem List (p. 132 of 133) | < Previous Next > |
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 | bdssexi 13101 | Bounded version of ssexi 4066. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 & ⊢ 𝐵 ∈ V & ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | bdssexg 13102 | Bounded version of ssexg 4067. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) | ||
Theorem | bdssexd 13103 | Bounded version of ssexd 4068. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ BOUNDED 𝐴 ⇒ ⊢ (𝜑 → 𝐴 ∈ V) | ||
Theorem | bdrabexg 13104* | Bounded version of rabexg 4071. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝜑 & ⊢ BOUNDED 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | ||
Theorem | bj-inex 13105 | The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V) | ||
Theorem | bj-intexr 13106 | intexr 4075 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅) | ||
Theorem | bj-intnexr 13107 | intnexr 4076 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∩ 𝐴 = V → ¬ ∩ 𝐴 ∈ V) | ||
Theorem | bj-zfpair2 13108 | Proof of zfpair2 4132 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | bj-prexg 13109 | Proof of prexg 4133 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) | ||
Theorem | bj-snexg 13110 | snexg 4108 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) | ||
Theorem | bj-snex 13111 | snex 4109 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ∈ V | ||
Theorem | bj-sels 13112* | If a class is a set, then it is a member of a set. (Copied from set.mm.) (Contributed by BJ, 3-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥) | ||
Theorem | bj-axun2 13113* | axun2 4357 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) | ||
Theorem | bj-uniex2 13114* | uniex2 4358 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.) |
⊢ ∃𝑦 𝑦 = ∪ 𝑥 | ||
Theorem | bj-uniex 13115 | uniex 4359 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∪ 𝐴 ∈ V | ||
Theorem | bj-uniexg 13116 | uniexg 4361 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | ||
Theorem | bj-unex 13117 | unex 4362 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ V | ||
Theorem | bdunexb 13118 | Bounded version of unexb 4363. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 & ⊢ BOUNDED 𝐵 ⇒ ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | bj-unexg 13119 | unexg 4364 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | bj-sucexg 13120 | sucexg 4414 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V) | ||
Theorem | bj-sucex 13121 | sucex 4415 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ suc 𝐴 ∈ V | ||
Axiom | ax-bj-d0cl 13122 | Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ DECID 𝜑 | ||
Theorem | bj-d0clsepcl 13123 | Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.) |
⊢ DECID 𝜑 | ||
Syntax | wind 13124 | Syntax for inductive classes. |
wff Ind 𝐴 | ||
Definition | df-bj-ind 13125* | Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.) |
⊢ (Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | ||
Theorem | bj-indsuc 13126 | A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.) |
⊢ (Ind 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴)) | ||
Theorem | bj-indeq 13127 | Equality property for Ind. (Contributed by BJ, 30-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (Ind 𝐴 ↔ Ind 𝐵)) | ||
Theorem | bj-bdind 13128 | Boundedness of the formula "the setvar 𝑥 is an inductive class". (Contributed by BJ, 30-Nov-2019.) |
⊢ BOUNDED Ind 𝑥 | ||
Theorem | bj-indint 13129* | The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.) |
⊢ Ind ∩ {𝑥 ∈ 𝐴 ∣ Ind 𝑥} | ||
Theorem | bj-indind 13130* | If 𝐴 is inductive and 𝐵 is "inductive in 𝐴", then (𝐴 ∩ 𝐵) is inductive. (Contributed by BJ, 25-Oct-2020.) |
⊢ ((Ind 𝐴 ∧ (∅ ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → suc 𝑥 ∈ 𝐵))) → Ind (𝐴 ∩ 𝐵)) | ||
Theorem | bj-dfom 13131 | Alternate definition of ω, as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.) |
⊢ ω = ∩ {𝑥 ∣ Ind 𝑥} | ||
Theorem | bj-omind 13132 | ω is an inductive class. (Contributed by BJ, 30-Nov-2019.) |
⊢ Ind ω | ||
Theorem | bj-omssind 13133 | ω is included in all the inductive sets (but for the moment, we cannot prove that it is included in all the inductive classes). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (Ind 𝐴 → ω ⊆ 𝐴)) | ||
Theorem | bj-ssom 13134* | A characterization of subclasses of ω. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(Ind 𝑥 → 𝐴 ⊆ 𝑥) ↔ 𝐴 ⊆ ω) | ||
Theorem | bj-om 13135* | A set is equal to ω if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = ω ↔ (Ind 𝐴 ∧ ∀𝑥(Ind 𝑥 → 𝐴 ⊆ 𝑥)))) | ||
Theorem | bj-2inf 13136* | Two formulations of the axiom of infinity (see ax-infvn 13139 and bj-omex 13140) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
⊢ (ω ∈ V ↔ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦))) | ||
The first three Peano postulates follow from constructive set theory (actually, from its core axioms). The proofs peano1 4508 and peano3 4510 already show this. In this section, we prove bj-peano2 13137 to complete this program. We also prove a preliminary version of the fifth Peano postulate from the core axioms. | ||
Theorem | bj-peano2 13137 | Constructive proof of peano2 4509. Temporary note: another possibility is to simply replace sucexg 4414 with bj-sucexg 13120 in the proof of peano2 4509. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω) | ||
Theorem | peano5set 13138* | Version of peano5 4512 when ω ∩ 𝐴 is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ ((ω ∩ 𝐴) ∈ 𝑉 → ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴)) | ||
In the absence of full separation, the axiom of infinity has to be stated more precisely, as the existence of the smallest class containing the empty set and the successor of each of its elements. | ||
In this section, we introduce the axiom of infinity in a constructive setting (ax-infvn 13139) and deduce that the class ω of finite ordinals is a set (bj-omex 13140). | ||
Axiom | ax-infvn 13139* | Axiom of infinity in a constructive setting. This asserts the existence of the special set we want (the set of natural numbers), instead of the existence of a set with some properties (ax-iinf 4502) from which one then proves, using full separation, that the wanted set exists (omex 4507). "vn" is for "von Neumann". (Contributed by BJ, 14-Nov-2019.) |
⊢ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦 → 𝑥 ⊆ 𝑦)) | ||
Theorem | bj-omex 13140 | Proof of omex 4507 from ax-infvn 13139. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.) |
⊢ ω ∈ V | ||
In this section, we give constructive proofs of two versions of Peano's fifth postulate. | ||
Theorem | bdpeano5 13141* | Bounded version of peano5 4512. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) | ||
Theorem | speano5 13142* | Version of peano5 4512 when 𝐴 is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) | ||
In this section, we prove various versions of bounded induction from the basic axioms of CZF (in particular, without the axiom of set induction). We also prove Peano's fourth postulate. Together with the results from the previous sections, this proves from the core axioms of CZF (with infinity) that the set of finite ordinals satisfies the five Peano postulates and thus provides a model for the set of natural numbers. | ||
Theorem | findset 13143* | Bounded induction (principle of induction when 𝐴 is assumed to be a set) allowing a proof from basic constructive axioms. See find 4513 for a nonconstructive proof of the general case. See bdfind 13144 for a proof when 𝐴 is assumed to be bounded. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ((𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) → 𝐴 = ω)) | ||
Theorem | bdfind 13144* | Bounded induction (principle of induction when 𝐴 is assumed to be bounded), proved from basic constructive axioms. See find 4513 for a nonconstructive proof of the general case. See findset 13143 for a proof when 𝐴 is assumed to be a set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ ((𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) → 𝐴 = ω) | ||
Theorem | bj-bdfindis 13145* | Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See finds 4514 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4514, finds2 4515, finds1 4516. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑥𝜃 & ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) ⇒ ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ∀𝑥 ∈ ω 𝜑) | ||
Theorem | bj-bdfindisg 13146* | Version of bj-bdfindis 13145 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-bdfindis 13145 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑥𝜃 & ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜏 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜏)) ⇒ ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → (𝐴 ∈ ω → 𝜏)) | ||
Theorem | bj-bdfindes 13147 | Bounded induction (principle of induction for bounded formulas), using explicit substitutions. Constructive proof (from CZF). See the comment of bj-bdfindis 13145 for explanations. From this version, it is easy to prove the bounded version of findes 4517. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ (([∅ / 𝑥]𝜑 ∧ ∀𝑥 ∈ ω (𝜑 → [suc 𝑥 / 𝑥]𝜑)) → ∀𝑥 ∈ ω 𝜑) | ||
Theorem | bj-nn0suc0 13148* | Constructive proof of a variant of nn0suc 4518. For a constructive proof of nn0suc 4518, see bj-nn0suc 13162. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ 𝐴 𝐴 = suc 𝑥)) | ||
Theorem | bj-nntrans 13149 | A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | ||
Theorem | bj-nntrans2 13150 | A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω → Tr 𝐴) | ||
Theorem | bj-nnelirr 13151 | A natural number does not belong to itself. Version of elirr 4456 for natural numbers, which does not require ax-setind 4452. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω → ¬ 𝐴 ∈ 𝐴) | ||
Theorem | bj-nnen2lp 13152 |
A version of en2lp 4469 for natural numbers, which does not require
ax-setind 4452.
Note: using this theorem and bj-nnelirr 13151, one can remove dependency on ax-setind 4452 from nntri2 6390 and nndcel 6396; one can actually remove more dependencies from these. (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴)) | ||
Theorem | bj-peano4 13153 | Remove from peano4 4511 dependency on ax-setind 4452. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | bj-omtrans 13154 |
The set ω is transitive. A natural number is
included in
ω. Constructive proof of elnn 4519.
The idea is to use bounded induction with the formula 𝑥 ⊆ ω. This formula, in a logic with terms, is bounded. So in our logic without terms, we need to temporarily replace it with 𝑥 ⊆ 𝑎 and then deduce the original claim. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω → 𝐴 ⊆ ω) | ||
Theorem | bj-omtrans2 13155 | The set ω is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) |
⊢ Tr ω | ||
Theorem | bj-nnord 13156 | A natural number is an ordinal. Constructive proof of nnord 4525. Can also be proved from bj-nnelon 13157 if the latter is proved from bj-omssonALT 13161. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω → Ord 𝐴) | ||
Theorem | bj-nnelon 13157 | A natural number is an ordinal. Constructive proof of nnon 4523. Can also be proved from bj-omssonALT 13161. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) | ||
Theorem | bj-omord 13158 | The set ω is an ordinal. Constructive proof of ordom 4520. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) |
⊢ Ord ω | ||
Theorem | bj-omelon 13159 | The set ω is an ordinal. Constructive proof of omelon 4522. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) |
⊢ ω ∈ On | ||
Theorem | bj-omsson 13160 | Constructive proof of omsson 4526. See also bj-omssonALT 13161. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged. |
⊢ ω ⊆ On | ||
Theorem | bj-omssonALT 13161 | Alternate proof of bj-omsson 13160. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ω ⊆ On | ||
Theorem | bj-nn0suc 13162* | Proof of (biconditional form of) nn0suc 4518 from the core axioms of CZF. See also bj-nn0sucALT 13176. As a characterization of the elements of ω, this could be labeled "elom". (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) | ||
In this section, we add the axiom of set induction to the core axioms of CZF. | ||
In this section, we prove some variants of the axiom of set induction. | ||
Theorem | setindft 13163* | Axiom of set-induction with a disjoint variable condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥𝜑)) | ||
Theorem | setindf 13164* | Axiom of set-induction with a disjoint variable condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥𝜑) | ||
Theorem | setindis 13165* | Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 → 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜒 → 𝜑)) ⇒ ⊢ (∀𝑦(∀𝑧 ∈ 𝑦 𝜓 → 𝜒) → ∀𝑥𝜑) | ||
Axiom | ax-bdsetind 13166* | Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.) |
⊢ BOUNDED 𝜑 ⇒ ⊢ (∀𝑎(∀𝑦 ∈ 𝑎 [𝑦 / 𝑎]𝜑 → 𝜑) → ∀𝑎𝜑) | ||
Theorem | bdsetindis 13167* | Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑥 = 𝑧 → (𝜑 → 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜒 → 𝜑)) ⇒ ⊢ (∀𝑦(∀𝑧 ∈ 𝑦 𝜓 → 𝜒) → ∀𝑥𝜑) | ||
Theorem | bj-inf2vnlem1 13168* | Lemma for bj-inf2vn 13172. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → Ind 𝐴) | ||
Theorem | bj-inf2vnlem2 13169* | Lemma for bj-inf2vnlem3 13170 and bj-inf2vnlem4 13171. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → ∀𝑢(∀𝑡 ∈ 𝑢 (𝑡 ∈ 𝐴 → 𝑡 ∈ 𝑍) → (𝑢 ∈ 𝐴 → 𝑢 ∈ 𝑍)))) | ||
Theorem | bj-inf2vnlem3 13170* | Lemma for bj-inf2vn 13172. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 & ⊢ BOUNDED 𝑍 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → 𝐴 ⊆ 𝑍)) | ||
Theorem | bj-inf2vnlem4 13171* | Lemma for bj-inf2vn2 13173. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → 𝐴 ⊆ 𝑍)) | ||
Theorem | bj-inf2vn 13172* | A sufficient condition for ω to be a set. See bj-inf2vn2 13173 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
⊢ BOUNDED 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → 𝐴 = ω)) | ||
Theorem | bj-inf2vn2 13173* | A sufficient condition for ω to be a set; unbounded version of bj-inf2vn 13172. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → 𝐴 = ω)) | ||
Axiom | ax-inf2 13174* | Another axiom of infinity in a constructive setting (see ax-infvn 13139). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.) |
⊢ ∃𝑎∀𝑥(𝑥 ∈ 𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝑎 𝑥 = suc 𝑦)) | ||
Theorem | bj-omex2 13175 | Using bounded set induction and the strong axiom of infinity, ω is a set, that is, we recover ax-infvn 13139 (see bj-2inf 13136 for the equivalence of the latter with bj-omex 13140). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ω ∈ V | ||
Theorem | bj-nn0sucALT 13176* | Alternate proof of bj-nn0suc 13162, also constructive but from ax-inf2 13174, hence requiring ax-bdsetind 13166. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) | ||
In this section, using the axiom of set induction, we prove full induction on the set of natural numbers. | ||
Theorem | bj-findis 13177* | Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 13145 for a bounded version not requiring ax-setind 4452. See finds 4514 for a proof in IZF. From this version, it is easy to prove of finds 4514, finds2 4515, finds1 4516. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑥𝜃 & ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) ⇒ ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ∀𝑥 ∈ ω 𝜑) | ||
Theorem | bj-findisg 13178* | Version of bj-findis 13177 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 13177 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ Ⅎ𝑥𝜃 & ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) & ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜏 & ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜏)) ⇒ ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → (𝐴 ∈ ω → 𝜏)) | ||
Theorem | bj-findes 13179 | Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 13177 for explanations. From this version, it is easy to prove findes 4517. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
⊢ (([∅ / 𝑥]𝜑 ∧ ∀𝑥 ∈ ω (𝜑 → [suc 𝑥 / 𝑥]𝜑)) → ∀𝑥 ∈ ω 𝜑) | ||
In this section, we state the axiom scheme of strong collection, which is part of CZF set theory. | ||
Axiom | ax-strcoll 13180* | Axiom scheme of strong collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. (Contributed by BJ, 5-Oct-2019.) |
⊢ ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | strcoll2 13181* | Version of ax-strcoll 13180 with one disjoint variable condition removed and without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.) |
⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | strcollnft 13182* | Closed form of strcollnf 13183. Version of ax-strcoll 13180 with one disjoint variable condition removed, the other disjoint variable condition replaced with a non-freeness antecedent, and without initial universal quantifier. (Contributed by BJ, 21-Oct-2019.) |
⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑))) | ||
Theorem | strcollnf 13183* | Version of ax-strcoll 13180 with one disjoint variable condition removed, the other disjoint variable condition replaced with a non-freeness hypothesis, and without initial universal quantifier. (Contributed by BJ, 21-Oct-2019.) |
⊢ Ⅎ𝑏𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | strcollnfALT 13184* | Alternate proof of strcollnf 13183, not using strcollnft 13182. (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 13185* | Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. (Contributed by BJ, 5-Oct-2019.) |
⊢ ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Theorem | sscoll2 13186* | Version of ax-sscoll 13185 with two disjoint variable conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.) |
⊢ ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 ∀𝑦(𝑦 ∈ 𝑑 ↔ ∃𝑥 ∈ 𝑎 𝜑)) | ||
Axiom | ax-ddkcomp 13187 | 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 the axiom ax-ddkcomp 13187 should be used in place of construction specific results. In particular, axcaucvg 7708 should be proved from it. (Contributed by BJ, 24-Oct-2021.) |
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 < 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ ((𝐵 ∈ 𝑅 ∧ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝑥 ≤ 𝐵))) | ||
Theorem | el2oss1o 13188 | Being an element of ordinal two implies being a subset of ordinal one. The converse is equivalent to excluded middle by ss1oel2o 13189. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ (𝐴 ∈ 2o → 𝐴 ⊆ 1o) | ||
Theorem | ss1oel2o 13189 | Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4121 which more directly illustrates the contrast with el2oss1o 13188. (Contributed by Jim Kingdon, 8-Aug-2022.) |
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ 1o → 𝑥 ∈ 2o)) | ||
Theorem | pw1dom2 13190 | The power set of 1o dominates 2o. Also see pwpw0ss 3731 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.) |
⊢ 2o ≼ 𝒫 1o | ||
Theorem | nnti 13191 | Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.) |
⊢ (𝜑 → 𝐴 ∈ ω) ⇒ ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢 E 𝑣 ∧ ¬ 𝑣 E 𝑢))) | ||
Theorem | pwtrufal 13192 | A subset of the singleton {∅} cannot be anything other than ∅ or {∅}. Removing the double negation would change the meaning, as seen at exmid01 4121. If we view a subset of a singleton as a truth value (as seen in theorems like exmidexmid 4120), 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 13193* | 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.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝑁 ({𝑥} × 1o) ⇒ ⊢ ((𝑁 ∈ ω ∧ 𝐺:𝑇–1-1→𝒫 1o) → 𝑁 ⊆ 2o) | ||
Theorem | pwf1oexmid 13194* | 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.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝑁 ({𝑥} × 1o) ⇒ ⊢ ((𝑁 ∈ ω ∧ 𝐺:𝑇–1-1→𝒫 1o) → (ran 𝐺 = 𝒫 1o ↔ (𝑁 = 2o ∧ EXMID))) | ||
Theorem | exmid1stab 13195* | 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 13196* | 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→(𝑥 ⊔ 1o))) & ⊢ (𝜑 → ω ∈ Markov) ⇒ ⊢ (𝜑 → EXMID) | ||
Theorem | 0nninf 13197 | The zero element of ℕ∞ (the constant sequence equal to ∅). (Contributed by Jim Kingdon, 14-Jul-2022.) |
⊢ (ω × {∅}) ∈ ℕ∞ | ||
Theorem | nninff 13198 | An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.) |
⊢ (𝐴 ∈ ℕ∞ → 𝐴:ω⟶2o) | ||
Theorem | nnsf 13199* | Domain and range of 𝑆. Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.) |
⊢ 𝑆 = (𝑝 ∈ ℕ∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))) ⇒ ⊢ 𝑆:ℕ∞⟶ℕ∞ | ||
Theorem | peano4nninf 13200* | 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(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))) ⇒ ⊢ 𝑆:ℕ∞–1-1→ℕ∞ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |