![]() |
Metamath
Proof Explorer Theorem List (p. 364 of 486) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-axc4 36301 | Over minimal calculus, the modal axiom (4) (hba1 2283) and the modal axiom (K) (ax-4 1804) together imply axc4 2310. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) → ((∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥∀𝑥𝜑 → ∀𝑥𝜓)) → (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)))) | ||
In this section, we assume that, on top of propositional calculus, there is given a provability predicate Prv satisfying the three axioms ax-prv1 36303 and ax-prv2 36304 and ax-prv3 36305. Note the similarity with ax-gen 1790, ax-4 1804 and hba1 2283 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/ 2283. 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 36308) and Löb's theorem (bj-babylob 36309). See the comments of these theorems for details. | ||
Syntax | cprvb 36302 | Syntax for the provability predicate. |
wff Prv 𝜑 | ||
Axiom | ax-prv1 36303 | First property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ 𝜑 ⇒ ⊢ Prv 𝜑 | ||
Axiom | ax-prv2 36304 | Second property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ (Prv (𝜑 → 𝜓) → (Prv 𝜑 → Prv 𝜓)) | ||
Axiom | ax-prv3 36305 | Third property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ (Prv 𝜑 → Prv Prv 𝜑) | ||
Theorem | prvlem1 36306 | An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (Prv 𝜑 → Prv 𝜓) | ||
Theorem | prvlem2 36307 | An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (Prv 𝜑 → (Prv 𝜓 → Prv 𝜒)) | ||
Theorem | bj-babygodel 36308 |
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 36309 |
See the section header comments for the context, as well as the comments
for bj-babygodel 36308.
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/ 36308). (Contributed by BJ, 20-Apr-2019.) |
⊢ (𝜓 ↔ (Prv 𝜓 → 𝜑)) & ⊢ (Prv 𝜑 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | bj-godellob 36310 | Proof of Gödel's theorem from Löb's theorem (see comments at bj-babygodel 36308 and bj-babylob 36309 for details). (Contributed by BJ, 20-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ↔ ¬ Prv 𝜑) & ⊢ ¬ Prv ⊥ ⇒ ⊢ ⊥ | ||
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. | ||
Theorem | bj-genr 36311 | Generalization rule on the right conjunct. See 19.28 2217. (Contributed by BJ, 7-Jul-2021.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 ∧ ∀𝑥𝜓) | ||
Theorem | bj-genl 36312 | Generalization rule on the left conjunct. See 19.27 2216. (Contributed by BJ, 7-Jul-2021.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (∀𝑥𝜑 ∧ 𝜓) | ||
Theorem | bj-genan 36313 | Generalization rule on a conjunction. Forward inference associated with 19.26 1866. (Contributed by BJ, 7-Jul-2021.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (∀𝑥𝜑 ∧ ∀𝑥𝜓) | ||
Theorem | bj-mpgs 36314 | 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 2172 (modal T) is available. Therefore, this theorem is stronger than mpg 1792 when sp 2172 is not available. (Contributed by BJ, 1-Nov-2023.) |
⊢ 𝜑 & ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | bj-2alim 36315 | Closed form of 2alimi 1807. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)) | ||
Theorem | bj-2exim 36316 | Closed form of 2eximi 1831. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)) | ||
Theorem | bj-alanim 36317 | Closed form of alanimi 1811. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥((𝜑 ∧ 𝜓) → 𝜒) → ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒)) | ||
Theorem | bj-2albi 36318 | Closed form of 2albii 1815. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)) | ||
Theorem | bj-notalbii 36319 | Equivalence of universal quantification of negation of equivalent formulas. Shortens ab0 4379 (103>94), ballotlem2 34322 (2655>2648), bnj1143 34635 (522>519), hausdiag 23640 (2119>2104). (Contributed by BJ, 17-Jul-2021.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓) | ||
Theorem | bj-2exbi 36320 | Closed form of 2exbii 1844. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)) | ||
Theorem | bj-3exbi 36321 | Closed form of 3exbii 1845. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)) | ||
Theorem | bj-sylgt2 36322 | Uncurried (imported) form of sylgt 1817. (Contributed by BJ, 2-May-2019.) |
⊢ ((∀𝑥(𝜓 → 𝜒) ∧ (𝜑 → ∀𝑥𝜓)) → (𝜑 → ∀𝑥𝜒)) | ||
Theorem | bj-alrimg 36323 | 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 36327. (Contributed by BJ, 9-Dec-2023.) |
⊢ ((𝜑 → ∀𝑥𝜓) → (∀𝑥(𝜓 → 𝜒) → (𝜑 → ∀𝑥𝜒))) | ||
Theorem | bj-alrimd 36324 | A slightly more general alrimd 2204. A common usage will have 𝜑 substituted for 𝜓 and 𝜒 substituted for 𝜃, giving a form closer to alrimd 2204. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜃)) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜒 → ∀𝑥𝜏)) | ||
Theorem | bj-sylget 36325 | Dual statement of sylgt 1817. Closed form of bj-sylge 36328. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜒 → 𝜑) → ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜒 → 𝜓))) | ||
Theorem | bj-sylget2 36326 | Uncurried (imported) form of bj-sylget 36325. (Contributed by BJ, 2-May-2019.) |
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ (∃𝑥𝜓 → 𝜒)) → (∃𝑥𝜑 → 𝜒)) | ||
Theorem | bj-exlimg 36327 | 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 36323. (Contributed by BJ, 9-Dec-2023.) |
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → (∃𝑥𝜒 → 𝜓))) | ||
Theorem | bj-sylge 36328 | Dual statement of sylg 1818 (the final "e" in the label stands for "existential (version of sylg 1818)". Variant of exlimih 2279. (Contributed by BJ, 25-Dec-2023.) |
⊢ (∃𝑥𝜑 → 𝜓) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimd 36329 | A slightly more general exlimd 2207. A common usage will have 𝜑 substituted for 𝜓 and 𝜃 substituted for 𝜏, giving a form closer to exlimd 2207. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜑 → (∃𝑥𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → (∃𝑥𝜒 → 𝜏)) | ||
Theorem | bj-nfimexal 36330 | 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 1834) and the converse implication is the join of instances of bj-alrimg 36323 and bj-exlimg 36327 (see 19.38a 1835 and 19.38b 1836). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.) |
⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-alexim 36331 | Closed form of aleximi 1827. Note: this proof is shorter, so aleximi 1827 could be deduced from it (exim 1829 would have to be proved first, see bj-eximALT 36345 but its proof is shorter (currently almost a subproof of aleximi 1827)). (Contributed by BJ, 8-Nov-2021.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))) | ||
Theorem | bj-nexdh 36332 | Closed form of nexdh 1861 (actually, its general instance). (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → ((𝜒 → ∀𝑥𝜑) → (𝜒 → ¬ ∃𝑥𝜓))) | ||
Theorem | bj-nexdh2 36333 | Uncurried (imported) form of bj-nexdh 36332. (Contributed by BJ, 6-May-2019.) |
⊢ ((∀𝑥(𝜑 → ¬ 𝜓) ∧ (𝜒 → ∀𝑥𝜑)) → (𝜒 → ¬ ∃𝑥𝜓)) | ||
Theorem | bj-hbxfrbi 36334 | Closed form of hbxfrbi 1820. Note: it is less important than nfbiit 1846. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht 36446) in order not to require sp 2172 (modal T). See bj-hbyfrbi 36335 for its version with existential quantifiers. (Contributed by BJ, 6-May-2019.) |
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((𝜑 → ∀𝑥𝜑) ↔ (𝜓 → ∀𝑥𝜓))) | ||
Theorem | bj-hbyfrbi 36335 | Version of bj-hbxfrbi 36334 with existential quantifiers. (Contributed by BJ, 23-Aug-2023.) |
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((∃𝑥𝜑 → 𝜑) ↔ (∃𝑥𝜓 → 𝜓))) | ||
Theorem | bj-exalim 36336 |
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 1906. I propose to move to the main part: bj-exalim 36336, bj-exalimi 36337, bj-exalims 36338, bj-exalimsi 36339, bj-ax12i 36341, bj-ax12wlem 36348, bj-ax12w 36381. A new label is needed for bj-ax12i 36341 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1960 and spimfw 1962 (other spim* theorems use ∃𝑥 and very few theorems in set.mm use ¬ ∀𝑥¬). (Contributed by BJ, 8-Nov-2021.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒))) | ||
Theorem | bj-exalimi 36337 | An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim 36336 (using mpg 1792) has fewer essential steps, but more steps in total (yielding a longer compressed proof). (Almost) the general statement that speimfw 1960 proves. (Contributed by BJ, 29-Sep-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | bj-exalims 36338 | Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1962 proves. (Contributed by BJ, 29-Sep-2019.) |
⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒)) ⇒ ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒))) | ||
Theorem | bj-exalimsi 36339 | An inference for distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1962 proves. (Contributed by BJ, 29-Sep-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒)) ⇒ ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | bj-ax12ig 36340 | A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i 36341. (Contributed by BJ, 19-Dec-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-ax12i 36341 | A weakening of bj-ax12ig 36340 that is sufficient to prove a weak form of the axiom of substitution ax-12 2167. The general statement of which ax12i 1963 is an instance. (Contributed by BJ, 29-Sep-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-nfimt 36342 | Closed form of nfim 1892 and curried (exported) form of nfimt 1891. (Contributed by BJ, 20-Oct-2021.) |
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-cbvalimt 36343 | A lemma in closed form used to prove bj-cbval 36353 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1873 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.) |
⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓))))) | ||
Theorem | bj-cbveximt 36344 | A lemma in closed form used to prove bj-cbvex 36354 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1873 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.) |
⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∀𝑥(𝜑 → ∀𝑦𝜑) → ((∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) → (∃𝑥𝜑 → ∃𝑦𝜓))))) | ||
Theorem | bj-eximALT 36345 | Alternate proof of exim 1829 directly from alim 1805 by using df-ex 1775 (using duality of ∀ and ∃. (Contributed by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | bj-aleximiALT 36346 | Alternate proof of aleximi 1827 from exim 1829, 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 36347 | A commuted form of exim 1829 which is sometimes posited as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023.) |
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | bj-ax12wlem 36348* | A lemma used to prove a weak version of the axiom of substitution ax-12 2167. (Temporary comment: The general statement that ax12wlem 2121 proves.) (Contributed by BJ, 20-Mar-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-cbvalim 36349* | A lemma used to prove bj-cbval 36353 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-cbvexim 36350* | A lemma used to prove bj-cbvex 36354 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∃𝑥𝜑 → ∃𝑦𝜓))) | ||
Theorem | bj-cbvalimi 36351* | An equality-free general instance of one half of a precise form of bj-cbval 36353. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ ∀𝑦∃𝑥𝜒 ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | bj-cbveximi 36352* | An equality-free general instance of one half of a precise form of bj-cbvex 36354. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ ∀𝑥∃𝑦𝜒 ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
Theorem | bj-cbval 36353* | 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 36354* | 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 36355 | Syntax for BJ's version of the uniqueness quantifier. |
wff ∃**𝑥𝜑 | ||
Definition | df-bj-mo 36356* | 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.) |
⊢ (∃**𝑥𝜑 ↔ ∀𝑧∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | bj-ssbeq 36357* | Substitution in an equality, disjoint variables case. Uses only ax-1 6 through ax-6 1964. It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq 36357 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 36358* | A lemma for the definiens of df-sb 2061. An instance of sp 2172 proved without it. Note: it has a common subproof with sbjust 2059. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-ssblem2 36359* | An instance of ax-11 2147 proved without it. The converse may not be provable without ax-11 2147 (since using alcomiw 2039 would require a DV on 𝜑, 𝑥, which defeats the purpose). (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-ax12v 36360* | A weaker form of ax-12 2167 and ax12v 2168, 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 36361* | Remove a DV condition from bj-ax12v 36360 (using core axioms only). (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.) |
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | bj-ax12ssb 36362* | Axiom bj-ax12 36361 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.) |
⊢ [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑) | ||
Theorem | bj-19.41al 36363 | Special case of 19.41 2224 proved from core axioms, ax-10 2130 (modal5), and hba1 2283 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑥(𝜑 ∧ ∀𝑥𝜓) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | bj-equsexval 36364* | Special case of equsexv 2255 proved from core axioms, ax-10 2130 (modal5), and hba1 2283 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥𝜓) | ||
Theorem | bj-subst 36365* | Proof of sbalex 2231 from core axioms, ax-10 2130 (modal5), and bj-ax12 36361. (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-ssbid2 36366 | A special case of sbequ2 2237. (Contributed by BJ, 22-Dec-2020.) |
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑) | ||
Theorem | bj-ssbid2ALT 36367 | Alternate proof of bj-ssbid2 36366, not using sbequ2 2237. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑) | ||
Theorem | bj-ssbid1 36368 | A special case of sbequ1 2236. (Contributed by BJ, 22-Dec-2020.) |
⊢ (𝜑 → [𝑥 / 𝑥]𝜑) | ||
Theorem | bj-ssbid1ALT 36369 | Alternate proof of bj-ssbid1 36368, not using sbequ1 2236. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → [𝑥 / 𝑥]𝜑) | ||
Theorem | bj-ax6elem1 36370* | Lemma for bj-ax6e 36372. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | bj-ax6elem2 36371* | Lemma for bj-ax6e 36372. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑦 = 𝑧 → ∃𝑥 𝑥 = 𝑦) | ||
Theorem | bj-ax6e 36372 | Proof of ax6e 2377 (hence ax6 2378) from Tarski's system, ax-c9 38588, ax-c16 38590. Remark: ax-6 1964 is used only via its principal (unbundled) instance ax6v 1965. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | bj-spimvwt 36373* | Closed form of spimvw 1992. See also spimt 2380. (Contributed by BJ, 8-Nov-2021.) |
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-spnfw 36374 | Theorem close to a closed form of spnfw 1976. (Contributed by BJ, 12-May-2019.) |
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-cbvexiw 36375* | Change bound variable. This is to cbvexvw 2033 what cbvaliw 2002 is to cbvalvw 2032. TODO: move after cbvalivw 2003. (Contributed by BJ, 17-Mar-2020.) |
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
Theorem | bj-cbvexivw 36376* | Change bound variable. This is to cbvexvw 2033 what cbvalivw 2003 is to cbvalvw 2032. TODO: move after cbvalivw 2003. (Contributed by BJ, 17-Mar-2020.) |
⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
Theorem | bj-modald 36377 | A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021.) |
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑) | ||
Theorem | bj-denot 36378* | A weakening of ax-6 1964 and ax6v 1965. (Contributed by BJ, 4-Apr-2021.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑥 → ¬ ∀𝑦 ¬ 𝑦 = 𝑥) | ||
Theorem | bj-eqs 36379* | A lemma for substitutions, proved from Tarski's FOL. The version without DV (𝑥, 𝑦) is true but requires ax-13 2366. The disjoint variable condition DV (𝑥, 𝜑) is necessary for both directions: consider substituting 𝑥 = 𝑧 for 𝜑. (Contributed by BJ, 25-May-2021.) |
⊢ (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-cbvexw 36380* | Change bound variable. This is to cbvexvw 2033 what cbvalw 2031 is to cbvalvw 2032. (Contributed by BJ, 17-Mar-2020.) |
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | bj-ax12w 36381* | The general statement that ax12w 2122 proves. (Contributed by BJ, 20-Mar-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-ax89 36382 | A theorem which could be used as sole axiom for the non-logical predicate instead of ax-8 2101 and ax-9 2109. Indeed, it is implied over propositional calculus by the conjunction of ax-8 2101 and ax-9 2109, as proved here. In the other direction, one can prove ax-8 2101 (respectively ax-9 2109) from bj-ax89 36382 by using mpan2 689 (respectively mpan 688) and equid 2008. TODO: move to main part. (Contributed by BJ, 3-Oct-2019.) |
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡)) | ||
Theorem | bj-elequ12 36383 | An identity law for the non-logical predicate, which combines elequ1 2106 and elequ2 2114. For the analogous theorems for class terms, see eleq1 2814, eleq2 2815 and eleq12 2816. TODO: move to main part. (Contributed by BJ, 29-Sep-2019.) |
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑡)) | ||
Theorem | bj-cleljusti 36384* | One direction of cleljust 2108, requiring only ax-1 6-- ax-5 1906 and ax8v1 2103. (Contributed by BJ, 31-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑦) | ||
Theorem | bj-alcomexcom 36385 | Commutation of two existential quantifiers on a formula is equivalent to commutation of two universal quantifiers over the same variables on the negation of that formula. Can be placed in the ax-4 1804 section, soon after 2nexaln 1825, and used to prove excom 2152. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.) |
⊢ ((∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑦∀𝑥 ¬ 𝜑) ↔ (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑)) | ||
Theorem | bj-hbalt 36386 | Closed form of hbal 2157. When in main part, prove hbal 2157 and hbald 2158 from it. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) | ||
Theorem | axc11n11 36387 | Proof of axc11n 2420 from { ax-1 6-- ax-7 2004, axc11 2424 } . Almost identical to axc11nfromc11 38624. (Contributed by NM, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | axc11n11r 36388 |
Proof of axc11n 2420 from { ax-1 6--
ax-7 2004, axc9 2376, axc11r 2360 } (note
that axc16 2248 is provable from { ax-1 6--
ax-7 2004, axc11r 2360 }).
Note that axc11n 2420 proves (over minimal calculus) that axc11 2424 and axc11r 2360 are equivalent. Therefore, axc11n11 36387 and axc11n11r 36388 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2424 appears slightly stronger since axc11n11r 36388 requires axc9 2376 while axc11n11 36387 does not). (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | bj-axc16g16 36389* | Proof of axc16g 2247 from { ax-1 6-- ax-7 2004, axc16 2248 }. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | bj-ax12v3 36390* | A weak version of ax-12 2167 which is stronger than ax12v 2168. Note that if one assumes reflexivity of equality ⊢ 𝑥 = 𝑥 (equid 2008), then bj-ax12v3 36390 implies ax-5 1906 over modal logic K (substitute 𝑥 for 𝑦). See also bj-ax12v3ALT 36391. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-ax12v3ALT 36391* | Alternate proof of bj-ax12v3 36390. Uses axc11r 2360 and axc15 2416 instead of ax-12 2167. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-sb 36392* | A weak variant of sbid2 2502 not requiring ax-13 2366 nor ax-10 2130. On top of Tarski's FOL, one implication requires only ax12v 2168, and the other requires only sp 2172. (Contributed by BJ, 25-May-2021.) |
⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-modalbe 36393 | The predicate-calculus version of the axiom (B) of modal logic. See also modal-b 2308. (Contributed by BJ, 20-Oct-2019.) |
⊢ (𝜑 → ∀𝑥∃𝑥𝜑) | ||
Theorem | bj-spst 36394 | Closed form of sps 2174. Once in main part, prove sps 2174 and spsd 2176 from it. (Contributed by BJ, 20-Oct-2019.) |
⊢ ((𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-19.21bit 36395 | Closed form of 19.21bi 2178. (Contributed by BJ, 20-Oct-2019.) |
⊢ ((𝜑 → ∀𝑥𝜓) → (𝜑 → 𝜓)) | ||
Theorem | bj-19.23bit 36396 | Closed form of 19.23bi 2180. (Contributed by BJ, 20-Oct-2019.) |
⊢ ((∃𝑥𝜑 → 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | bj-nexrt 36397 | Closed form of nexr 2181. Contrapositive of 19.8a 2170. (Contributed by BJ, 20-Oct-2019.) |
⊢ (¬ ∃𝑥𝜑 → ¬ 𝜑) | ||
Theorem | bj-alrim 36398 | Closed form of alrimi 2202. (Contributed by BJ, 2-May-2019.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-alrim2 36399 | Uncurried (imported) form of bj-alrim 36398. (Contributed by BJ, 2-May-2019.) |
⊢ ((Ⅎ𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-nfdt0 36400 | A theorem close to a closed form of nf5d 2274 and nf5dh 2136. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → (∀𝑥𝜑 → Ⅎ𝑥𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |