HomeHome Intuitionistic Logic Explorer
Theorem List (p. 144 of 145)
< Previous  Next >
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 - 14301-14400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorembj-axempty 14301* Axiom of the empty set from bounded separation. It is provable from bounded separation since the intuitionistic FOL used in iset.mm assumes a nonempty universe. See axnul 4125. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4126 instead. (New usage is discouraged.)
𝑥𝑦𝑥
 
Theorembj-axempty2 14302* Axiom of the empty set from bounded separation, alternate version to bj-axempty 14301. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4126 instead. (New usage is discouraged.)
𝑥𝑦 ¬ 𝑦𝑥
 
Theorembj-nalset 14303* nalset 4130 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ ∃𝑥𝑦 𝑦𝑥
 
Theorembj-vprc 14304 vprc 4132 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ V ∈ V
 
Theorembj-nvel 14305 nvel 4133 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ V ∈ 𝐴
 
Theorembj-vnex 14306 vnex 4131 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ ∃𝑥 𝑥 = V
 
Theorembdinex1 14307 Bounded version of inex1 4134. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝐵    &   𝐴 ∈ V       (𝐴𝐵) ∈ V
 
Theorembdinex2 14308 Bounded version of inex2 4135. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝐵    &   𝐴 ∈ V       (𝐵𝐴) ∈ V
 
Theorembdinex1g 14309 Bounded version of inex1g 4136. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝐵       (𝐴𝑉 → (𝐴𝐵) ∈ V)
 
Theorembdssex 14310 Bounded version of ssex 4137. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝐴    &   𝐵 ∈ V       (𝐴𝐵𝐴 ∈ V)
 
Theorembdssexi 14311 Bounded version of ssexi 4138. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝐴    &   𝐵 ∈ V    &   𝐴𝐵       𝐴 ∈ V
 
Theorembdssexg 14312 Bounded version of ssexg 4139. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝐴       ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
 
Theorembdssexd 14313 Bounded version of ssexd 4140. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
(𝜑𝐵𝐶)    &   (𝜑𝐴𝐵)    &   BOUNDED 𝐴       (𝜑𝐴 ∈ V)
 
Theorembdrabexg 14314* Bounded version of rabexg 4143. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝜑    &   BOUNDED 𝐴       (𝐴𝑉 → {𝑥𝐴𝜑} ∈ V)
 
Theorembj-inex 14315 The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
 
Theorembj-intexr 14316 intexr 4147 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
( 𝐴 ∈ V → 𝐴 ≠ ∅)
 
Theorembj-intnexr 14317 intnexr 4148 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
( 𝐴 = V → ¬ 𝐴 ∈ V)
 
Theorembj-zfpair2 14318 Proof of zfpair2 4207 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
{𝑥, 𝑦} ∈ V
 
Theorembj-prexg 14319 Proof of prexg 4208 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ V)
 
Theorembj-snexg 14320 snexg 4181 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
(𝐴𝑉 → {𝐴} ∈ V)
 
Theorembj-snex 14321 snex 4182 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
𝐴 ∈ V       {𝐴} ∈ V
 
Theorembj-sels 14322* If a class is a set, then it is a member of a set. (Copied from set.mm.) (Contributed by BJ, 3-Apr-2019.)
(𝐴𝑉 → ∃𝑥 𝐴𝑥)
 
Theorembj-axun2 14323* axun2 4432 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
𝑦𝑧(𝑧𝑦 ↔ ∃𝑤(𝑧𝑤𝑤𝑥))
 
Theorembj-uniex2 14324* uniex2 4433 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
𝑦 𝑦 = 𝑥
 
Theorembj-uniex 14325 uniex 4434 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
𝐴 ∈ V        𝐴 ∈ V
 
Theorembj-uniexg 14326 uniexg 4436 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
(𝐴𝑉 𝐴 ∈ V)
 
Theorembj-unex 14327 unex 4438 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
𝐴 ∈ V    &   𝐵 ∈ V       (𝐴𝐵) ∈ V
 
Theorembdunexb 14328 Bounded version of unexb 4439. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝐴    &   BOUNDED 𝐵       ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴𝐵) ∈ V)
 
Theorembj-unexg 14329 unexg 4440 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
 
Theorembj-sucexg 14330 sucexg 4494 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
(𝐴𝑉 → suc 𝐴 ∈ V)
 
Theorembj-sucex 14331 sucex 4495 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
𝐴 ∈ V       suc 𝐴 ∈ V
 
12.2.9.1  Delta_0-classical logic
 
Axiomax-bj-d0cl 14332 Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
BOUNDED 𝜑       DECID 𝜑
 
Theorembj-d0clsepcl 14333 Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
DECID 𝜑
 
12.2.9.2  Inductive classes and the class of natural number ordinals
 
Syntaxwind 14334 Syntax for inductive classes.
wff Ind 𝐴
 
Definitiondf-bj-ind 14335* Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)
(Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴))
 
Theorembj-indsuc 14336 A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.)
(Ind 𝐴 → (𝐵𝐴 → suc 𝐵𝐴))
 
Theorembj-indeq 14337 Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
(𝐴 = 𝐵 → (Ind 𝐴 ↔ Ind 𝐵))
 
Theorembj-bdind 14338 Boundedness of the formula "the setvar 𝑥 is an inductive class". (Contributed by BJ, 30-Nov-2019.)
BOUNDED Ind 𝑥
 
Theorembj-indint 14339* The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.)
Ind {𝑥𝐴 ∣ Ind 𝑥}
 
Theorembj-indind 14340* If 𝐴 is inductive and 𝐵 is "inductive in 𝐴", then (𝐴𝐵) is inductive. (Contributed by BJ, 25-Oct-2020.)
((Ind 𝐴 ∧ (∅ ∈ 𝐵 ∧ ∀𝑥𝐴 (𝑥𝐵 → suc 𝑥𝐵))) → Ind (𝐴𝐵))
 
Theorembj-dfom 14341 Alternate definition of ω, as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.)
ω = {𝑥 ∣ Ind 𝑥}
 
Theorembj-omind 14342 ω is an inductive class. (Contributed by BJ, 30-Nov-2019.)
Ind ω
 
Theorembj-omssind 14343 ω 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 𝐴 → ω ⊆ 𝐴))
 
Theorembj-ssom 14344* A characterization of subclasses of ω. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(∀𝑥(Ind 𝑥𝐴𝑥) ↔ 𝐴 ⊆ ω)
 
Theorembj-om 14345* 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 𝑥𝐴𝑥))))
 
Theorembj-2inf 14346* Two formulations of the axiom of infinity (see ax-infvn 14349 and bj-omex 14350) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(ω ∈ V ↔ ∃𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦𝑥𝑦)))
 
12.2.9.3  The first three Peano postulates

The first three Peano postulates follow from constructive set theory (actually, from its core axioms). The proofs peano1 4590 and peano3 4592 already show this. In this section, we prove bj-peano2 14347 to complete this program. We also prove a preliminary version of the fifth Peano postulate from the core axioms.

 
Theorembj-peano2 14347 Constructive proof of peano2 4591. Temporary note: another possibility is to simply replace sucexg 4494 with bj-sucexg 14330 in the proof of peano2 4591. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
(𝐴 ∈ ω → suc 𝐴 ∈ ω)
 
Theorempeano5set 14348* Version of peano5 4594 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 𝑥𝐴)) → ω ⊆ 𝐴))
 
12.2.10  CZF: Infinity

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.

 
12.2.10.1  The set of natural number ordinals

In this section, we introduce the axiom of infinity in a constructive setting (ax-infvn 14349) and deduce that the class ω of natural number ordinals is a set (bj-omex 14350).

 
Axiomax-infvn 14349* 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 4584) from which one then proves, using full separation, that the wanted set exists (omex 4589). "vn" is for "von Neumann". (Contributed by BJ, 14-Nov-2019.)
𝑥(Ind 𝑥 ∧ ∀𝑦(Ind 𝑦𝑥𝑦))
 
Theorembj-omex 14350 Proof of omex 4589 from ax-infvn 14349. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.)
ω ∈ V
 
12.2.10.2  Peano's fifth postulate

In this section, we give constructive proofs of two versions of Peano's fifth postulate.

 
Theorembdpeano5 14351* Bounded version of peano5 4594. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝐴       ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴)
 
Theoremspeano5 14352* Version of peano5 4594 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 𝑥𝐴)) → ω ⊆ 𝐴)
 
12.2.10.3  Bounded induction and Peano's fourth postulate

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 natural number ordinals satisfies the five Peano postulates and thus provides a model for the set of natural numbers.

 
Theoremfindset 14353* Bounded induction (principle of induction when 𝐴 is assumed to be a set) allowing a proof from basic constructive axioms. See find 4595 for a nonconstructive proof of the general case. See bdfind 14354 for a proof when 𝐴 is assumed to be bounded. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
(𝐴𝑉 → ((𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴) → 𝐴 = ω))
 
Theorembdfind 14354* Bounded induction (principle of induction when 𝐴 is assumed to be bounded), proved from basic constructive axioms. See find 4595 for a nonconstructive proof of the general case. See findset 14353 for a proof when 𝐴 is assumed to be a set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝐴       ((𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴) → 𝐴 = ω)
 
Theorembj-bdfindis 14355* 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 4596 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4596, finds2 4597, finds1 4598. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝜑    &   𝑥𝜓    &   𝑥𝜒    &   𝑥𝜃    &   (𝑥 = ∅ → (𝜓𝜑))    &   (𝑥 = 𝑦 → (𝜑𝜒))    &   (𝑥 = suc 𝑦 → (𝜃𝜑))       ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒𝜃)) → ∀𝑥 ∈ ω 𝜑)
 
Theorembj-bdfindisg 14356* Version of bj-bdfindis 14355 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-bdfindis 14355 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝜑    &   𝑥𝜓    &   𝑥𝜒    &   𝑥𝜃    &   (𝑥 = ∅ → (𝜓𝜑))    &   (𝑥 = 𝑦 → (𝜑𝜒))    &   (𝑥 = suc 𝑦 → (𝜃𝜑))    &   𝑥𝐴    &   𝑥𝜏    &   (𝑥 = 𝐴 → (𝜑𝜏))       ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒𝜃)) → (𝐴 ∈ ω → 𝜏))
 
Theorembj-bdfindes 14357 Bounded induction (principle of induction for bounded formulas), using explicit substitutions. Constructive proof (from CZF). See the comment of bj-bdfindis 14355 for explanations. From this version, it is easy to prove the bounded version of findes 4599. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝜑       (([∅ / 𝑥]𝜑 ∧ ∀𝑥 ∈ ω (𝜑[suc 𝑥 / 𝑥]𝜑)) → ∀𝑥 ∈ ω 𝜑)
 
Theorembj-nn0suc0 14358* Constructive proof of a variant of nn0suc 4600. For a constructive proof of nn0suc 4600, see bj-nn0suc 14372. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
(𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥𝐴 𝐴 = suc 𝑥))
 
Theorembj-nntrans 14359 A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
(𝐴 ∈ ω → (𝐵𝐴𝐵𝐴))
 
Theorembj-nntrans2 14360 A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
(𝐴 ∈ ω → Tr 𝐴)
 
Theorembj-nnelirr 14361 A natural number does not belong to itself. Version of elirr 4537 for natural numbers, which does not require ax-setind 4533. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
(𝐴 ∈ ω → ¬ 𝐴𝐴)
 
Theorembj-nnen2lp 14362 A version of en2lp 4550 for natural numbers, which does not require ax-setind 4533.

Note: using this theorem and bj-nnelirr 14361, one can remove dependency on ax-setind 4533 from nntri2 6489 and nndcel 6495; one can actually remove more dependencies from these. (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)

((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ¬ (𝐴𝐵𝐵𝐴))
 
Theorembj-peano4 14363 Remove from peano4 4593 dependency on ax-setind 4533. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)
((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 = suc 𝐵𝐴 = 𝐵))
 
Theorembj-omtrans 14364 The set ω is transitive. A natural number is included in ω. Constructive proof of elnn 4602.

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.)

(𝐴 ∈ ω → 𝐴 ⊆ ω)
 
Theorembj-omtrans2 14365 The set ω is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
Tr ω
 
Theorembj-nnord 14366 A natural number is an ordinal class. Constructive proof of nnord 4608. Can also be proved from bj-nnelon 14367 if the latter is proved from bj-omssonALT 14371. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.)
(𝐴 ∈ ω → Ord 𝐴)
 
Theorembj-nnelon 14367 A natural number is an ordinal. Constructive proof of nnon 4606. Can also be proved from bj-omssonALT 14371. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.)
(𝐴 ∈ ω → 𝐴 ∈ On)
 
Theorembj-omord 14368 The set ω is an ordinal class. Constructive proof of ordom 4603. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
Ord ω
 
Theorembj-omelon 14369 The set ω is an ordinal. Constructive proof of omelon 4605. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
ω ∈ On
 
Theorembj-omsson 14370 Constructive proof of omsson 4609. See also bj-omssonALT 14371. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.
ω ⊆ On
 
Theorembj-omssonALT 14371 Alternate proof of bj-omsson 14370. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
ω ⊆ On
 
Theorembj-nn0suc 14372* Proof of (biconditional form of) nn0suc 4600 from the core axioms of CZF. See also bj-nn0sucALT 14386. As a characterization of the elements of ω, this could be labeled "elom". (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
(𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))
 
12.2.11  CZF: Set induction

In this section, we add the axiom of set induction to the core axioms of CZF.

 
12.2.11.1  Set induction

In this section, we prove some variants of the axiom of set induction.

 
Theoremsetindft 14373* Axiom of set-induction with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 22-Nov-2019.)
(∀𝑥𝑦𝜑 → (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝜑𝜑) → ∀𝑥𝜑))
 
Theoremsetindf 14374* Axiom of set-induction with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 22-Nov-2019.)
𝑦𝜑       (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥]𝜑𝜑) → ∀𝑥𝜑)
 
Theoremsetindis 14375* Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.)
𝑥𝜓    &   𝑥𝜒    &   𝑦𝜑    &   𝑦𝜓    &   (𝑥 = 𝑧 → (𝜑𝜓))    &   (𝑥 = 𝑦 → (𝜒𝜑))       (∀𝑦(∀𝑧𝑦 𝜓𝜒) → ∀𝑥𝜑)
 
Axiomax-bdsetind 14376* Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.)
BOUNDED 𝜑       (∀𝑎(∀𝑦𝑎 [𝑦 / 𝑎]𝜑𝜑) → ∀𝑎𝜑)
 
Theorembdsetindis 14377* Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
BOUNDED 𝜑    &   𝑥𝜓    &   𝑥𝜒    &   𝑦𝜑    &   𝑦𝜓    &   (𝑥 = 𝑧 → (𝜑𝜓))    &   (𝑥 = 𝑦 → (𝜒𝜑))       (∀𝑦(∀𝑧𝑦 𝜓𝜒) → ∀𝑥𝜑)
 
Theorembj-inf2vnlem1 14378* Lemma for bj-inf2vn 14382. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(∀𝑥(𝑥𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦𝐴 𝑥 = suc 𝑦)) → Ind 𝐴)
 
Theorembj-inf2vnlem2 14379* Lemma for bj-inf2vnlem3 14380 and bj-inf2vnlem4 14381. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(∀𝑥𝐴 (𝑥 = ∅ ∨ ∃𝑦𝐴 𝑥 = suc 𝑦) → (Ind 𝑍 → ∀𝑢(∀𝑡𝑢 (𝑡𝐴𝑡𝑍) → (𝑢𝐴𝑢𝑍))))
 
Theorembj-inf2vnlem3 14380* Lemma for bj-inf2vn 14382. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
BOUNDED 𝐴    &   BOUNDED 𝑍       (∀𝑥𝐴 (𝑥 = ∅ ∨ ∃𝑦𝐴 𝑥 = suc 𝑦) → (Ind 𝑍𝐴𝑍))
 
Theorembj-inf2vnlem4 14381* Lemma for bj-inf2vn2 14383. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(∀𝑥𝐴 (𝑥 = ∅ ∨ ∃𝑦𝐴 𝑥 = suc 𝑦) → (Ind 𝑍𝐴𝑍))
 
Theorembj-inf2vn 14382* A sufficient condition for ω to be a set. See bj-inf2vn2 14383 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
BOUNDED 𝐴       (𝐴𝑉 → (∀𝑥(𝑥𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦𝐴 𝑥 = suc 𝑦)) → 𝐴 = ω))
 
Theorembj-inf2vn2 14383* A sufficient condition for ω to be a set; unbounded version of bj-inf2vn 14382. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(𝐴𝑉 → (∀𝑥(𝑥𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦𝐴 𝑥 = suc 𝑦)) → 𝐴 = ω))
 
Axiomax-inf2 14384* Another axiom of infinity in a constructive setting (see ax-infvn 14349). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)
𝑎𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
 
Theorembj-omex2 14385 Using bounded set induction and the strong axiom of infinity, ω is a set, that is, we recover ax-infvn 14349 (see bj-2inf 14346 for the equivalence of the latter with bj-omex 14350). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
ω ∈ V
 
Theorembj-nn0sucALT 14386* Alternate proof of bj-nn0suc 14372, also constructive but from ax-inf2 14384, hence requiring ax-bdsetind 14376. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))
 
12.2.11.2  Full induction

In this section, using the axiom of set induction, we prove full induction on the set of natural numbers.

 
Theorembj-findis 14387* 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 14355 for a bounded version not requiring ax-setind 4533. See finds 4596 for a proof in IZF. From this version, it is easy to prove of finds 4596, finds2 4597, finds1 4598. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
𝑥𝜓    &   𝑥𝜒    &   𝑥𝜃    &   (𝑥 = ∅ → (𝜓𝜑))    &   (𝑥 = 𝑦 → (𝜑𝜒))    &   (𝑥 = suc 𝑦 → (𝜃𝜑))       ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒𝜃)) → ∀𝑥 ∈ ω 𝜑)
 
Theorembj-findisg 14388* Version of bj-findis 14387 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 14387 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
𝑥𝜓    &   𝑥𝜒    &   𝑥𝜃    &   (𝑥 = ∅ → (𝜓𝜑))    &   (𝑥 = 𝑦 → (𝜑𝜒))    &   (𝑥 = suc 𝑦 → (𝜃𝜑))    &   𝑥𝐴    &   𝑥𝜏    &   (𝑥 = 𝐴 → (𝜑𝜏))       ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒𝜃)) → (𝐴 ∈ ω → 𝜏))
 
Theorembj-findes 14389 Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 14387 for explanations. From this version, it is easy to prove findes 4599. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
(([∅ / 𝑥]𝜑 ∧ ∀𝑥 ∈ ω (𝜑[suc 𝑥 / 𝑥]𝜑)) → ∀𝑥 ∈ ω 𝜑)
 
12.2.12  CZF: Strong collection

In this section, we state the axiom scheme of strong collection, which is part of CZF set theory.

 
Axiomax-strcoll 14390* Axiom scheme of strong 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 on 𝑎, or equivalently a collection of nonempty classes indexed by 𝑎, and the axiom asserts the existence of a set 𝑏 which "collects" at least one element in the image of each 𝑥𝑎 and which is made only of such elements. That second conjunct is what makes it "strong", compared to the axiom scheme of collection ax-coll 4115. (Contributed by BJ, 5-Oct-2019.)
𝑎(∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑))
 
Theoremstrcoll2 14391* Version of ax-strcoll 14390 with one disjoint variable condition removed and without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
(∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑))
 
Theoremstrcollnft 14392* Closed form of strcollnf 14393. (Contributed by BJ, 21-Oct-2019.)
(∀𝑥𝑦𝑏𝜑 → (∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑)))
 
Theoremstrcollnf 14393* Version of ax-strcoll 14390 with one disjoint variable condition removed, the other disjoint variable condition replaced with a nonfreeness hypothesis, and without initial universal quantifier. Version of strcoll2 14391 with the disjoint variable condition on 𝑏, 𝜑 replaced with a nonfreeness hypothesis.

This proof aims to demonstrate a standard technique, but strcoll2 14391 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.)

𝑏𝜑       (∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑))
 
TheoremstrcollnfALT 14394* Alternate proof of strcollnf 14393, not using strcollnft 14392. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
𝑏𝜑       (∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑))
 
12.2.13  CZF: Subset collection

In this section, we state the axiom scheme of subset collection, which is part of CZF set theory.

 
Axiomax-sscoll 14395* 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.)
𝑎𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐 (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑))
 
Theoremsscoll2 14396* Version of ax-sscoll 14395 with two disjoint variable conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.)
𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐 (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑))
 
12.2.14  Real numbers
 
Axiomax-ddkcomp 14397 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 14397 should be used in place of construction specific results. In particular, axcaucvg 7890 should be proved from it. (Contributed by BJ, 24-Oct-2021.)
(((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴) ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 𝑦𝑥 ∧ ((𝐵𝑅 ∧ ∀𝑦𝐴 𝑦𝐵) → 𝑥𝐵)))
 
12.3  Mathbox for Jim Kingdon
 
12.3.1  Propositional and predicate logic
 
Theoremnnnotnotr 14398 Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 850, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.)
¬ ¬ (¬ ¬ 𝜑𝜑)
 
12.3.2  Natural numbers
 
Theoremss1oel2o 14399 Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4195 which more directly illustrates the contrast with el2oss1o 6438. (Contributed by Jim Kingdon, 8-Aug-2022.)
(EXMID ↔ ∀𝑥(𝑥 ⊆ 1o𝑥 ∈ 2o))
 
Theoremnnti 14400 Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.)
(𝜑𝐴 ∈ ω)       ((𝜑 ∧ (𝑢𝐴𝑣𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢 E 𝑣 ∧ ¬ 𝑣 E 𝑢)))
    < 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-14485
  Copyright terms: Public domain < Previous  Next >