P. 348 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34701-34800   *Has distinct variable group(s)

Type	Label	Description
Statement
20.15.2  Modal logic In this section, we prove some theorems related to modal logic. For modal logic, we refer to https://en.wikipedia.org/wiki/Kripke_semantics, https://en.wikipedia.org/wiki/Modal_logic and https://plato.stanford.edu/entries/logic-modal/. Monadic first-order logic (i.e., with quantification over only one variable) is bi-interpretable with modal logic, by mapping ∀𝑥 to "necessity" (generally denoted by a box) and ∃𝑥 to "possibility" (generally denoted by a diamond). Therefore, we use these quantifiers so as not to introduce new symbols. (To be strictly within modal logic, we should add disjoint variable conditions between 𝑥 and any other metavariables appearing in the statements.) For instance, ax-gen 1799 corresponds to the necessitation rule of modal logic, and ax-4 1813 corresponds to the distributivity axiom (K) of modal logic, also called the Kripke scheme. Modal logics satisfying these rule and axiom are called "normal modal logics", of which the most important modal logics are. The minimal normal modal logic is also denoted by (K). Here are a few normal modal logics with their axiomatizations (on top of (K)): (K) axiomatized by no supplementary axioms; (T) axiomatized by the axiom T; (K4) axiomatized by the axiom 4; (S4) axiomatized by the axioms T,4; (S5) axiomatized by the axioms T,5 or D,B,4; (GL) axiomatized by the axiom GL. The last one, called Gödel–Löb logic or provability logic, is important because it describes exactly the properties of provability in Peano arithmetic, as proved by Robert Solovay. See for instance https://plato.stanford.edu/entries/logic-provability/ 1813. A basic result in this logic is bj-gl4 34704.
Theorem	bj-axdd2 34701	This implication, proved using only ax-gen 1799 and ax-4 1813 on top of propositional calculus (hence holding, up to the standard interpretation, in any normal modal logic), shows that the axiom scheme ⊢ ∃𝑥⊤ implies the axiom scheme ⊢ (∀𝑥𝜑 → ∃𝑥𝜑). These correspond to the modal axiom (D), and in predicate calculus, they assert that the universe of discourse is nonempty. For the converse, see bj-axd2d 34702. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜓))
Theorem	bj-axd2d 34702	This implication, proved using only ax-gen 1799 on top of propositional calculus (hence holding, up to the standard interpretation, in any modal logic), shows that the axiom scheme ⊢ (∀𝑥𝜑 → ∃𝑥𝜑) implies the axiom scheme ⊢ ∃𝑥⊤. These correspond to the modal axiom (D), and in predicate calculus, they assert that the universe of discourse is nonempty. For the converse, see bj-axdd2 34701. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥⊤ → ∃𝑥⊤) → ∃𝑥⊤)
Theorem	bj-axtd 34703	This implication, proved from propositional calculus only (hence holding, up to the standard interpretation, in any modal logic), shows that the axiom scheme ⊢ (∀𝑥𝜑 → 𝜑) (modal T) implies the axiom scheme ⊢ (∀𝑥𝜑 → ∃𝑥𝜑) (modal D). See also bj-axdd2 34701 and bj-axd2d 34702. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ 𝜑 → ¬ 𝜑) → ((∀𝑥𝜑 → 𝜑) → (∀𝑥𝜑 → ∃𝑥𝜑)))
Theorem	bj-gl4 34704	In a normal modal logic, the modal axiom GL implies the modal axiom (4). Translated to first-order logic, Axiom GL reads ⊢ (∀𝑥(∀𝑥𝜑 → 𝜑) → ∀𝑥𝜑). Note that the antecedent of bj-gl4 34704 is an instance of the axiom GL, with 𝜑 replaced by (∀𝑥𝜑 ∧ 𝜑), which is a modality sometimes called the "strong necessity" of 𝜑. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥(∀𝑥(∀𝑥𝜑 ∧ 𝜑) → (∀𝑥𝜑 ∧ 𝜑)) → ∀𝑥(∀𝑥𝜑 ∧ 𝜑)) → (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑))
Theorem	bj-axc4 34705	Over minimal calculus, the modal axiom (4) (hba1 2293) and the modal axiom (K) (ax-4 1813) together imply axc4 2319. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) → ((∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥∀𝑥𝜑 → ∀𝑥𝜓)) → (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))))
20.15.3  Provability logic In this section, we assume that, on top of propositional calculus, there is given a provability predicate Prv satisfying the three axioms ax-prv1 34707 and ax-prv2 34708 and ax-prv3 34709. Note the similarity with ax-gen 1799, ax-4 1813 and hba1 2293 respectively. These three properties of Prv are often called the Hilbert–Bernays–Löb derivability conditions, or the Hilbert–Bernays provability conditions. This corresponds to the modal logic (K4) (see previous section for modal logic). The interpretation of provability logic is the following: we are given a background first-order theory T, the wff Prv 𝜑 means "𝜑 is provable in T", and the turnstile ⊢ indicates provability in T. Beware that "provability logic" often means (K) augmented with the Gödel–Löb axiom GL, which we do not assume here (at least for the moment). See for instance https://plato.stanford.edu/entries/logic-provability/ 2293. Provability logic is worth studying because whenever T is a first-order theory containing Robinson arithmetic (a fragment of Peano arithmetic), one can prove (using Gödel numbering, and in the much weaker primitive recursive arithmetic) that there exists in T a provability predicate Prv satisfying the above three axioms. (We do not construct this predicate in this section; this is still a project.) The main theorems of this section are the "easy parts" of the proofs of Gödel's second incompleteness theorem (bj-babygodel 34712) and Löb's theorem (bj-babylob 34713). See the comments of these theorems for details.
Syntax	cprvb 34706	Syntax for the provability predicate.
wff Prv 𝜑
Axiom	ax-prv1 34707	First property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ 𝜑    ⇒   ⊢ Prv 𝜑
Axiom	ax-prv2 34708	Second property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (Prv (𝜑 → 𝜓) → (Prv 𝜑 → Prv 𝜓))
Axiom	ax-prv3 34709	Third property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (Prv 𝜑 → Prv Prv 𝜑)
Theorem	prvlem1 34710	An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (Prv 𝜑 → Prv 𝜓)
Theorem	prvlem2 34711	An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (Prv 𝜑 → (Prv 𝜓 → Prv 𝜒))
Theorem	bj-babygodel 34712	See the section header comments for the context. The first hypothesis reads "𝜑 is true if and only if it is not provable in T" (and having this first hypothesis means that we can prove this fact in T). The wff 𝜑 is a formal version of the sentence "This sentence is not provable". The hard part of the proof of Gödel's theorem is to construct such a 𝜑, called a "Gödel–Rosser sentence", for a first-order theory T which is effectively axiomatizable and contains Robinson arithmetic, through Gödel diagonalization (this can be done in primitive recursive arithmetic). The second hypothesis means that ⊥ is not provable in T, that is, that the theory T is consistent (and having this second hypothesis means that we can prove in T that the theory T is consistent). The conclusion is the falsity, so having the conclusion means that T can prove the falsity, that is, T is inconsistent. Therefore, taking the contrapositive, this theorem expresses that if a first-order theory is consistent (and one can prove in it that some formula is true if and only if it is not provable in it), then this theory does not prove its own consistency. This proof is due to George Boolos, Gödel's Second Incompleteness Theorem Explained in Words of One Syllable, Mind, New Series, Vol. 103, No. 409 (January 1994), pp. 1--3. (Contributed by BJ, 3-Apr-2019.)
⊢ (𝜑 ↔ ¬ Prv 𝜑)    &   ⊢ ¬ Prv ⊥    ⇒   ⊢ ⊥
Theorem	bj-babylob 34713	See the section header comments for the context, as well as the comments for bj-babygodel 34712. Löb's theorem when the Löb sentence is given as a hypothesis (the hard part of the proof of Löb's theorem is to construct this Löb sentence; this can be done, using Gödel diagonalization, for any first-order effectively axiomatizable theory containing Robinson arithmetic). More precisely, the present theorem states that if a first-order theory proves that the provability of a given sentence entails its truth (and if one can construct in this theory a provability predicate and a Löb sentence, given here as the first hypothesis), then the theory actually proves that sentence. See for instance, Eliezer Yudkowsky, The Cartoon Guide to Löb's Theorem (available at http://yudkowsky.net/rational/lobs-theorem/ 34712). (Contributed by BJ, 20-Apr-2019.)
⊢ (𝜓 ↔ (Prv 𝜓 → 𝜑))    &   ⊢ (Prv 𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	bj-godellob 34714	Proof of Gödel's theorem from Löb's theorem (see comments at bj-babygodel 34712 and bj-babylob 34713 for details). (Contributed by BJ, 20-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ↔ ¬ Prv 𝜑)    &   ⊢ ¬ Prv ⊥    ⇒   ⊢ ⊥
20.15.4  First-order logic Utility lemmas or strengthenings of theorems in the main part (biconditional or closed forms, or fewer disjoint variable conditions, or disjoint variable conditions replaced with nonfreeness hypotheses...). Sorted in the same order as in the main part.
20.15.4.1  Adding ax-gen
Theorem	bj-genr 34715	Generalization rule on the right conjunct. See 19.28 2224. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 ∧ ∀𝑥𝜓)
Theorem	bj-genl 34716	Generalization rule on the left conjunct. See 19.27 2223. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ∧ 𝜓)
Theorem	bj-genan 34717	Generalization rule on a conjunction. Forward inference associated with 19.26 1874. (Contributed by BJ, 7-Jul-2021.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ∧ ∀𝑥𝜓)
Theorem	bj-mpgs 34718	From a closed form theorem (the major premise) with an antecedent in the "strong necessity" modality (in the language of modal logic), deduce the inference ⊢ 𝜑 ⇒ ⊢ 𝜓. Strong necessity is stronger than necessity, and equivalent to it when sp 2178 (modal T) is available. Therefore, this theorem is stronger than mpg 1801 when sp 2178 is not available. (Contributed by BJ, 1-Nov-2023.)
⊢ 𝜑    &   ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓)    ⇒   ⊢ 𝜓
20.15.4.2  Adding ax-4
Theorem	bj-2alim 34719	Closed form of 2alimi 1816. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-2exim 34720	Closed form of 2eximi 1839. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓))
Theorem	bj-alanim 34721	Closed form of alanimi 1820. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥((𝜑 ∧ 𝜓) → 𝜒) → ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒))
Theorem	bj-2albi 34722	Closed form of 2albii 1824. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓))
Theorem	bj-notalbii 34723	Equivalence of universal quantification of negation of equivalent formulas. Shortens ab0 4305 (103>94), ballotlem2 32355 (2655>2648), bnj1143 32670 (522>519), hausdiag 22704 (2119>2104). (Contributed by BJ, 17-Jul-2021.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓)
Theorem	bj-2exbi 34724	Closed form of 2exbii 1852. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓))
Theorem	bj-3exbi 34725	Closed form of 3exbii 1853. (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓))
Theorem	bj-sylgt2 34726	Uncurried (imported) form of sylgt 1825. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜓 → 𝜒) ∧ (𝜑 → ∀𝑥𝜓)) → (𝜑 → ∀𝑥𝜒))
Theorem	bj-alrimg 34727	The general form of the *alrim* family of theorems: if 𝜑 is substituted for 𝜓, then the antecedent expresses a form of nonfreeness of 𝑥 in 𝜑, so the theorem means that under a nonfreeness condition in an antecedent, one can deduce from the universally quantified implication an implication where the consequent is universally quantified. Dual of bj-exlimg 34731. (Contributed by BJ, 9-Dec-2023.)
⊢ ((𝜑 → ∀𝑥𝜓) → (∀𝑥(𝜓 → 𝜒) → (𝜑 → ∀𝑥𝜒)))
Theorem	bj-alrimd 34728	A slightly more general alrimd 2211. A common usage will have 𝜑 substituted for 𝜓 and 𝜒 substituted for 𝜃, giving a form closer to alrimd 2211. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜃))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜏))
Theorem	bj-sylget 34729	Dual statement of sylgt 1825. Closed form of bj-sylge 34732. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜒 → 𝜑) → ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylget2 34730	Uncurried (imported) form of bj-sylget 34729. (Contributed by BJ, 2-May-2019.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ (∃𝑥𝜓 → 𝜒)) → (∃𝑥𝜑 → 𝜒))
Theorem	bj-exlimg 34731	The general form of the *exlim* family of theorems: if 𝜑 is substituted for 𝜓, then the antecedent expresses a form of nonfreeness of 𝑥 in 𝜑, so the theorem means that under a nonfreeness condition in a consequent, one can deduce from the universally quantified implication an implication where the antecedent is existentially quantified. Dual of bj-alrimg 34727. (Contributed by BJ, 9-Dec-2023.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → (∃𝑥𝜒 → 𝜓)))
Theorem	bj-sylge 34732	Dual statement of sylg 1826 (the final "e" in the label stands for "existential (version of sylg 1826)". Variant of exlimih 2289. (Contributed by BJ, 25-Dec-2023.)
⊢ (∃𝑥𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimd 34733	A slightly more general exlimd 2214. A common usage will have 𝜑 substituted for 𝜓 and 𝜃 substituted for 𝜏, giving a form closer to exlimd 2214. (Contributed by BJ, 25-Dec-2023.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (∃𝑥𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥𝜒 → 𝜏))
Theorem	bj-nfimexal 34734	A weak from of nonfreeness in either an antecedent or a consequent implies that a universally quantified implication is equivalent to the associated implication where the antecedent is existentially quantified and the consequent is universally quantified. The forward implication always holds (this is 19.38 1842) and the converse implication is the join of instances of bj-alrimg 34727 and bj-exlimg 34731 (see 19.38a 1843 and 19.38b 1844). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.)
⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-alexim 34735	Closed form of aleximi 1835. Note: this proof is shorter, so aleximi 1835 could be deduced from it (exim 1837 would have to be proved first, see bj-eximALT 34749 but its proof is shorter (currently almost a subproof of aleximi 1835)). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-nexdh 34736	Closed form of nexdh 1869 (actually, its general instance). (Contributed by BJ, 6-May-2019.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → ((𝜒 → ∀𝑥𝜑) → (𝜒 → ¬ ∃𝑥𝜓)))
Theorem	bj-nexdh2 34737	Uncurried (imported) form of bj-nexdh 34736. (Contributed by BJ, 6-May-2019.)
⊢ ((∀𝑥(𝜑 → ¬ 𝜓) ∧ (𝜒 → ∀𝑥𝜑)) → (𝜒 → ¬ ∃𝑥𝜓))
Theorem	bj-hbxfrbi 34738	Closed form of hbxfrbi 1828. Note: it is less important than nfbiit 1854. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht 34850) in order not to require sp 2178 (modal T). See bj-hbyfrbi 34739 for its version with existential quantifiers. (Contributed by BJ, 6-May-2019.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((𝜑 → ∀𝑥𝜑) ↔ (𝜓 → ∀𝑥𝜓)))
Theorem	bj-hbyfrbi 34739	Version of bj-hbxfrbi 34738 with existential quantifiers. (Contributed by BJ, 23-Aug-2023.)
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((∃𝑥𝜑 → 𝜑) ↔ (∃𝑥𝜓 → 𝜓)))
Theorem	bj-exalim 34740	Distribute quantifiers over a nested implication. This and the following theorems are the general instances of already proved theorems. They could be moved to the main part, before ax-5 1914. I propose to move to the main part: bj-exalim 34740, bj-exalimi 34741, bj-exalims 34742, bj-exalimsi 34743, bj-ax12i 34745, bj-ax12wlem 34752, bj-ax12w 34785. A new label is needed for bj-ax12i 34745 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1968 and spimfw 1970 (other spim* theorems use ∃𝑥 and very few theorems in set.mm use ¬ ∀𝑥¬). (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒)))
Theorem	bj-exalimi 34741	An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim 34740 (using mpg 1801) has fewer essential steps, but more steps in total (yielding a longer compressed proof). (Almost) the general statement that speimfw 1968 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒))
Theorem	bj-exalims 34742	Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1970 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒)))
Theorem	bj-exalimsi 34743	An inference for distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1970 proves. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒))    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-ax12ig 34744	A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i 34745. (Contributed by BJ, 19-Dec-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-ax12i 34745	A weakening of bj-ax12ig 34744 that is sufficient to prove a weak form of the axiom of substitution ax-12 2173. The general statement of which ax12i 1971 is an instance. (Contributed by BJ, 29-Sep-2019.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-nfimt 34746	Closed form of nfim 1900 and curried (exported) form of nfimt 1899. (Contributed by BJ, 20-Oct-2021.)
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓)))
Theorem	bj-cbvalimt 34747	A lemma in closed form used to prove bj-cbval 34757 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1881 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.)
⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓)))))
Theorem	bj-cbveximt 34748	A lemma in closed form used to prove bj-cbvex 34758 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1881 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.)
⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∀𝑥(𝜑 → ∀𝑦𝜑) → ((∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) → (∃𝑥𝜑 → ∃𝑦𝜓)))))
Theorem	bj-eximALT 34749	Alternate proof of exim 1837 directly from alim 1814 by using df-ex 1784 (using duality of ∀ and ∃. (Contributed by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	bj-aleximiALT 34750	Alternate proof of aleximi 1835 from exim 1837, which is sometimes used as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	bj-eximcom 34751	A commuted form of exim 1837 which is sometimes posited as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023.)
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
20.15.4.3  Adding ax-5
Theorem	bj-ax12wlem 34752*	A lemma used to prove a weak version of the axiom of substitution ax-12 2173. (Temporary comment: The general statement that ax12wlem 2130 proves.) (Contributed by BJ, 20-Mar-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-cbvalim 34753*	A lemma used to prove bj-cbval 34757 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-cbvexim 34754*	A lemma used to prove bj-cbvex 34758 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∃𝑥𝜑 → ∃𝑦𝜓)))
Theorem	bj-cbvalimi 34755*	An equality-free general instance of one half of a precise form of bj-cbval 34757. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ ∀𝑦∃𝑥𝜒    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	bj-cbveximi 34756*	An equality-free general instance of one half of a precise form of bj-cbvex 34758. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ ∀𝑥∃𝑦𝜒    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-cbval 34757*	Changing a bound variable (universal quantification case) in a weak axiomatization, assuming that all variables denote (which is valid in inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ ∀𝑦∃𝑥 𝑥 = 𝑦    &   ⊢ ∀𝑥∃𝑦 𝑦 = 𝑥    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	bj-cbvex 34758*	Changing a bound variable (existential quantification case) in a weak axiomatization, assuming that all variables denote (which is valid in inclusive free logic) and that equality is symmetric. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.)
⊢ ∀𝑦∃𝑥 𝑥 = 𝑦    &   ⊢ ∀𝑥∃𝑦 𝑦 = 𝑥    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Syntax	wmoo 34759	Syntax for BJ's version of the uniqueness quantifier.
wff ∃**𝑥𝜑
Definition	df-bj-mo 34760*	Definition of the uniqueness quantifier which is correct on the empty domain. Instead of the fresh variable 𝑧, one could save a dummy variable by using 𝑥 or 𝑦 at the cost of having nested quantifiers on the same variable. (Contributed by BJ, 12-Mar-2023.)
⊢ (∃**𝑥𝜑 ↔ ∀𝑧∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
20.15.4.4  Equality and substitution
Theorem	bj-ssbeq 34761*	Substitution in an equality, disjoint variables case. Uses only ax-1 6 through ax-6 1972. It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq 34761 first with a DV condition on 𝑥, 𝑡, and then in the general case. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ ([𝑡 / 𝑥]𝑦 = 𝑧 ↔ 𝑦 = 𝑧)
Theorem	bj-ssblem1 34762*	A lemma for the definiens of df-sb 2069. An instance of sp 2178 proved without it. Note: it has a common subproof with sbjust 2067. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ssblem2 34763*	An instance of ax-11 2156 proved without it. The converse may not be provable without ax-11 2156 (since using alcomiw 2047 would require a DV on 𝜑, 𝑥, which defeats the purpose). (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ax12v 34764*	A weaker form of ax-12 2173 and ax12v 2174, namely the generalization over 𝑥 of the latter. In this statement, all occurrences of 𝑥 are bound. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	bj-ax12 34765*	Remove a DV condition from bj-ax12v 34764 (using core axioms only). (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	bj-ax12ssb 34766*	Axiom bj-ax12 34765 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.)
⊢ [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑)
Theorem	bj-19.41al 34767	Special case of 19.41 2231 proved from core axioms, ax-10 2139 (modal5), and hba1 2293 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥(𝜑 ∧ ∀𝑥𝜓) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝜓))
Theorem	bj-equsexval 34768*	Special case of equsexv 2263 proved from core axioms, ax-10 2139 (modal5), and hba1 2293 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥𝜓)
Theorem	bj-subst 34769*	Proof of sbalex 2238 from core axioms, ax-10 2139 (modal5), and bj-ax12 34765. (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	bj-ssbid2 34770	A special case of sbequ2 2244. (Contributed by BJ, 22-Dec-2020.)
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑)
Theorem	bj-ssbid2ALT 34771	Alternate proof of bj-ssbid2 34770, not using sbequ2 2244. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑)
Theorem	bj-ssbid1 34772	A special case of sbequ1 2243. (Contributed by BJ, 22-Dec-2020.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜑)
Theorem	bj-ssbid1ALT 34773	Alternate proof of bj-ssbid1 34772, not using sbequ1 2243. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → [𝑥 / 𝑥]𝜑)
Theorem	bj-ax6elem1 34774*	Lemma for bj-ax6e 34776. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	bj-ax6elem2 34775*	Lemma for bj-ax6e 34776. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑦 = 𝑧 → ∃𝑥 𝑥 = 𝑦)
Theorem	bj-ax6e 34776	Proof of ax6e 2383 (hence ax6 2384) from Tarski's system, ax-c9 36831, ax-c16 36833. Remark: ax-6 1972 is used only via its principal (unbundled) instance ax6v 1973. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
20.15.4.5  Adding ax-6
Theorem	bj-spimvwt 34777*	Closed form of spimvw 2000. See also spimt 2386. (Contributed by BJ, 8-Nov-2021.)
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-spnfw 34778	Theorem close to a closed form of spnfw 1984. (Contributed by BJ, 12-May-2019.)
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-cbvexiw 34779*	Change bound variable. This is to cbvexvw 2041 what cbvaliw 2010 is to cbvalvw 2040. TODO: move after cbvalivw 2011. (Contributed by BJ, 17-Mar-2020.)
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-cbvexivw 34780*	Change bound variable. This is to cbvexvw 2041 what cbvalivw 2011 is to cbvalvw 2040. TODO: move after cbvalivw 2011. (Contributed by BJ, 17-Mar-2020.)
⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑦𝜓)
Theorem	bj-modald 34781	A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021.)
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	bj-denot 34782*	A weakening of ax-6 1972 and ax6v 1973. (Contributed by BJ, 4-Apr-2021.) (New usage is discouraged.)
⊢ (𝑥 = 𝑥 → ¬ ∀𝑦 ¬ 𝑦 = 𝑥)
Theorem	bj-eqs 34783*	A lemma for substitutions, proved from Tarski's FOL. The version without DV (𝑥, 𝑦) is true but requires ax-13 2372. The disjoint variable condition DV (𝑥, 𝜑) is necessary for both directions: consider substituting 𝑥 = 𝑧 for 𝜑. (Contributed by BJ, 25-May-2021.)
⊢ (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
20.15.4.6  Adding ax-7
Theorem	bj-cbvexw 34784*	Change bound variable. This is to cbvexvw 2041 what cbvalw 2039 is to cbvalvw 2040. (Contributed by BJ, 17-Mar-2020.)
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	bj-ax12w 34785*	The general statement that ax12w 2131 proves. (Contributed by BJ, 20-Mar-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥(𝜑 → 𝜓)))
20.15.4.7  Membership predicate, ax-8 and ax-9
Theorem	bj-ax89 34786	A theorem which could be used as sole axiom for the non-logical predicate instead of ax-8 2110 and ax-9 2118. Indeed, it is implied over propositional calculus by the conjunction of ax-8 2110 and ax-9 2118, as proved here. In the other direction, one can prove ax-8 2110 (respectively ax-9 2118) from bj-ax89 34786 by using mpan2 687 (respectively mpan 686) and equid 2016. TODO: move to main part. (Contributed by BJ, 3-Oct-2019.)
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡))
Theorem	bj-elequ12 34787	An identity law for the non-logical predicate, which combines elequ1 2115 and elequ2 2123. For the analogous theorems for class terms, see eleq1 2826, eleq2 2827 and eleq12 2828. TODO: move to main part. (Contributed by BJ, 29-Sep-2019.)
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑡))
Theorem	bj-cleljusti 34788*	One direction of cleljust 2117, requiring only ax-1 6-- ax-5 1914 and ax8v1 2112. (Contributed by BJ, 31-Dec-2020.) (Proof modification is discouraged.)
⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑦)
20.15.4.8  Adding ax-11
Theorem	bj-alcomexcom 34789	Commutation of universal quantifiers implies commutation of existential quantifiers. Can be placed in the ax-4 1813 section, soon after 2nexaln 1833, and used to prove excom 2164. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.)
⊢ ((∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑦∀𝑥 ¬ 𝜑) → (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑))
Theorem	bj-hbalt 34790	Closed form of hbal 2169. When in main part, prove hbal 2169 and hbald 2170 from it. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
20.15.4.9  Adding ax-12
Theorem	axc11n11 34791	Proof of axc11n 2426 from { ax-1 6-- ax-7 2012, axc11 2430 } . Almost identical to axc11nfromc11 36867. (Contributed by NM, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	axc11n11r 34792	Proof of axc11n 2426 from { ax-1 6-- ax-7 2012, axc9 2382, axc11r 2366 } (note that axc16 2256 is provable from { ax-1 6-- ax-7 2012, axc11r 2366 }). Note that axc11n 2426 proves (over minimal calculus) that axc11 2430 and axc11r 2366 are equivalent. Therefore, axc11n11 34791 and axc11n11r 34792 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2430 appears slightly stronger since axc11n11r 34792 requires axc9 2382 while axc11n11 34791 does not). (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	bj-axc16g16 34793*	Proof of axc16g 2255 from { ax-1 6-- ax-7 2012, axc16 2256 }. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	bj-ax12v3 34794*	A weak version of ax-12 2173 which is stronger than ax12v 2174. Note that if one assumes reflexivity of equality ⊢ 𝑥 = 𝑥 (equid 2016), then bj-ax12v3 34794 implies ax-5 1914 over modal logic K (substitute 𝑥 for 𝑦). See also bj-ax12v3ALT 34795. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-ax12v3ALT 34795*	Alternate proof of bj-ax12v3 34794. Uses axc11r 2366 and axc15 2422 instead of ax-12 2173. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-sb 34796*	A weak variant of sbid2 2512 not requiring ax-13 2372 nor ax-10 2139. On top of Tarski's FOL, one implication requires only ax12v 2174, and the other requires only sp 2178. (Contributed by BJ, 25-May-2021.)
⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	bj-modalbe 34797	The predicate-calculus version of the axiom (B) of modal logic. See also modal-b 2317. (Contributed by BJ, 20-Oct-2019.)
⊢ (𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	bj-spst 34798	Closed form of sps 2180. Once in main part, prove sps 2180 and spsd 2182 from it. (Contributed by BJ, 20-Oct-2019.)
⊢ ((𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-19.21bit 34799	Closed form of 19.21bi 2184. (Contributed by BJ, 20-Oct-2019.)
⊢ ((𝜑 → ∀𝑥𝜓) → (𝜑 → 𝜓))
Theorem	bj-19.23bit 34800	Closed form of 19.23bi 2186. (Contributed by BJ, 20-Oct-2019.)
⊢ ((∃𝑥𝜑 → 𝜓) → (𝜑 → 𝜓))