| Metamath
Proof Explorer Theorem List (p. 367 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Axiom | ax-prv3 36601 | Third property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
| ⊢ (Prv 𝜑 → Prv Prv 𝜑) | ||
| Theorem | prvlem1 36602 | An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ (Prv 𝜑 → Prv 𝜓) | ||
| Theorem | prvlem2 36603 | An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (Prv 𝜑 → (Prv 𝜓 → Prv 𝜒)) | ||
| Theorem | bj-babygodel 36604 |
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 36605 |
See the section header comments for the context, as well as the comments
for bj-babygodel 36604.
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/ 36604). (Contributed by BJ, 20-Apr-2019.) |
| ⊢ (𝜓 ↔ (Prv 𝜓 → 𝜑)) & ⊢ (Prv 𝜑 → 𝜑) ⇒ ⊢ 𝜑 | ||
| Theorem | bj-godellob 36606 | Proof of Gödel's theorem from Löb's theorem (see comments at bj-babygodel 36604 and bj-babylob 36605 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 36607 | Generalization rule on the right conjunct. See 19.28 2228. (Contributed by BJ, 7-Jul-2021.) |
| ⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 ∧ ∀𝑥𝜓) | ||
| Theorem | bj-genl 36608 | Generalization rule on the left conjunct. See 19.27 2227. (Contributed by BJ, 7-Jul-2021.) |
| ⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (∀𝑥𝜑 ∧ 𝜓) | ||
| Theorem | bj-genan 36609 | Generalization rule on a conjunction. Forward inference associated with 19.26 1870. (Contributed by BJ, 7-Jul-2021.) |
| ⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (∀𝑥𝜑 ∧ ∀𝑥𝜓) | ||
| Theorem | bj-mpgs 36610 | 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 2183 (modal T) is available. Therefore, this theorem is stronger than mpg 1797 when sp 2183 is not available. (Contributed by BJ, 1-Nov-2023.) |
| ⊢ 𝜑 & ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓) ⇒ ⊢ 𝜓 | ||
| Theorem | bj-2alim 36611 | Closed form of 2alimi 1812. (Contributed by BJ, 6-May-2019.) |
| ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)) | ||
| Theorem | bj-2exim 36612 | Closed form of 2eximi 1836. (Contributed by BJ, 6-May-2019.) |
| ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)) | ||
| Theorem | bj-alanim 36613 | Closed form of alanimi 1816. (Contributed by BJ, 6-May-2019.) |
| ⊢ (∀𝑥((𝜑 ∧ 𝜓) → 𝜒) → ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒)) | ||
| Theorem | bj-2albi 36614 | Closed form of 2albii 1820. (Contributed by BJ, 6-May-2019.) |
| ⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)) | ||
| Theorem | bj-notalbii 36615 | Equivalence of universal quantification of negation of equivalent formulas. Shortens ab0 4380 (103>94), ballotlem2 34491 (2655>2648), bnj1143 34804 (522>519), hausdiag 23653 (2119>2104). (Contributed by BJ, 17-Jul-2021.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓) | ||
| Theorem | bj-2exbi 36616 | Closed form of 2exbii 1849. (Contributed by BJ, 6-May-2019.) |
| ⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)) | ||
| Theorem | bj-3exbi 36617 | Closed form of 3exbii 1850. (Contributed by BJ, 6-May-2019.) |
| ⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)) | ||
| Theorem | bj-sylggt 36618 | Stronger form of sylgt 1822, closer to ax-2 7. (Contributed by BJ, 30-Jul-2025.) |
| ⊢ ((𝜑 → ∀𝑥(𝜓 → 𝜒)) → ((𝜑 → ∀𝑥𝜓) → (𝜑 → ∀𝑥𝜒))) | ||
| Theorem | bj-sylgt2 36619 | Uncurried (imported) form of sylgt 1822. (Contributed by BJ, 2-May-2019.) |
| ⊢ ((∀𝑥(𝜓 → 𝜒) ∧ (𝜑 → ∀𝑥𝜓)) → (𝜑 → ∀𝑥𝜒)) | ||
| Theorem | bj-alrimg 36620 | 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 36624. (Contributed by BJ, 9-Dec-2023.) |
| ⊢ ((𝜑 → ∀𝑥𝜓) → (∀𝑥(𝜓 → 𝜒) → (𝜑 → ∀𝑥𝜒))) | ||
| Theorem | bj-alrimd 36621 | A slightly more general alrimd 2215. A common usage will have 𝜑 substituted for 𝜓 and 𝜒 substituted for 𝜃, giving a form closer to alrimd 2215. (Contributed by BJ, 25-Dec-2023.) |
| ⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜃)) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜒 → ∀𝑥𝜏)) | ||
| Theorem | bj-sylget 36622 | Dual statement of sylgt 1822. Closed form of bj-sylge 36625. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥(𝜒 → 𝜑) → ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜒 → 𝜓))) | ||
| Theorem | bj-sylget2 36623 | Uncurried (imported) form of bj-sylget 36622. (Contributed by BJ, 2-May-2019.) |
| ⊢ ((∀𝑥(𝜑 → 𝜓) ∧ (∃𝑥𝜓 → 𝜒)) → (∃𝑥𝜑 → 𝜒)) | ||
| Theorem | bj-exlimg 36624 | 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 36620. (Contributed by BJ, 9-Dec-2023.) |
| ⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → (∃𝑥𝜒 → 𝜓))) | ||
| Theorem | bj-sylge 36625 | Dual statement of sylg 1823 (the final "e" in the label stands for "existential (version of sylg 1823)". Variant of exlimih 2289. (Contributed by BJ, 25-Dec-2023.) |
| ⊢ (∃𝑥𝜑 → 𝜓) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
| Theorem | bj-exlimd 36626 | A slightly more general exlimd 2218. A common usage will have 𝜑 substituted for 𝜓 and 𝜃 substituted for 𝜏, giving a form closer to exlimd 2218. (Contributed by BJ, 25-Dec-2023.) |
| ⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜑 → (∃𝑥𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → (∃𝑥𝜒 → 𝜏)) | ||
| Theorem | bj-nfimexal 36627 | 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 1839) and the converse implication is the join of instances of bj-alrimg 36620 and bj-exlimg 36624 (see 19.38a 1840 and 19.38b 1841). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.) |
| ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) | ||
| Theorem | bj-alexim 36628 | Closed form of aleximi 1832. Note: this proof is shorter, so aleximi 1832 could be deduced from it (exim 1834 would have to be proved first, see bj-eximALT 36642 but its proof is shorter (currently almost a subproof of aleximi 1832)). (Contributed by BJ, 8-Nov-2021.) |
| ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))) | ||
| Theorem | bj-nexdh 36629 | Closed form of nexdh 1865 (actually, its general instance). (Contributed by BJ, 6-May-2019.) |
| ⊢ (∀𝑥(𝜑 → ¬ 𝜓) → ((𝜒 → ∀𝑥𝜑) → (𝜒 → ¬ ∃𝑥𝜓))) | ||
| Theorem | bj-nexdh2 36630 | Uncurried (imported) form of bj-nexdh 36629. (Contributed by BJ, 6-May-2019.) |
| ⊢ ((∀𝑥(𝜑 → ¬ 𝜓) ∧ (𝜒 → ∀𝑥𝜑)) → (𝜒 → ¬ ∃𝑥𝜓)) | ||
| Theorem | bj-hbxfrbi 36631 | Closed form of hbxfrbi 1825. Note: it is less important than nfbiit 1851. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht 36742) in order not to require sp 2183 (modal T). See bj-hbyfrbi 36632 for its version with existential quantifiers. (Contributed by BJ, 6-May-2019.) |
| ⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((𝜑 → ∀𝑥𝜑) ↔ (𝜓 → ∀𝑥𝜓))) | ||
| Theorem | bj-hbyfrbi 36632 | Version of bj-hbxfrbi 36631 with existential quantifiers. (Contributed by BJ, 23-Aug-2023.) |
| ⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((∃𝑥𝜑 → 𝜑) ↔ (∃𝑥𝜓 → 𝜓))) | ||
| Theorem | bj-exalim 36633 |
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 1910. I propose to move to the main part: bj-exalim 36633, bj-exalimi 36634, bj-exalims 36635, bj-exalimsi 36636, bj-ax12i 36638, bj-ax12wlem 36645, bj-ax12w 36678. A new label is needed for bj-ax12i 36638 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1963 and spimfw 1965 (other spim* theorems use ∃𝑥 and very few theorems in set.mm use ¬ ∀𝑥¬). (Contributed by BJ, 8-Nov-2021.) |
| ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒))) | ||
| Theorem | bj-exalimi 36634 | An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim 36633 (using mpg 1797) has fewer essential steps, but more steps in total (yielding a longer compressed proof). (Almost) the general statement that speimfw 1963 proves. (Contributed by BJ, 29-Sep-2019.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒)) | ||
| Theorem | bj-exalims 36635 | Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1965 proves. (Contributed by BJ, 29-Sep-2019.) |
| ⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒)) ⇒ ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒))) | ||
| Theorem | bj-exalimsi 36636 | An inference for distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1965 proves. (Contributed by BJ, 29-Sep-2019.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒)) ⇒ ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
| Theorem | bj-ax12ig 36637 | A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i 36638. (Contributed by BJ, 19-Dec-2020.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
| Theorem | bj-ax12i 36638 | A weakening of bj-ax12ig 36637 that is sufficient to prove a weak form of the axiom of substitution ax-12 2177. The general statement of which ax12i 1966 is an instance. (Contributed by BJ, 29-Sep-2019.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
| Theorem | bj-nfimt 36639 | Closed form of nfim 1896 and curried (exported) form of nfimt 1895. (Contributed by BJ, 20-Oct-2021.) |
| ⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓))) | ||
| Theorem | bj-cbvalimt 36640 | A lemma in closed form used to prove bj-cbval 36650 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1877 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.) |
| ⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓))))) | ||
| Theorem | bj-cbveximt 36641 | A lemma in closed form used to prove bj-cbvex 36651 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1877 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.) |
| ⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∀𝑥(𝜑 → ∀𝑦𝜑) → ((∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) → (∃𝑥𝜑 → ∃𝑦𝜓))))) | ||
| Theorem | bj-eximALT 36642 | Alternate proof of exim 1834 directly from alim 1810 by using df-ex 1780 (using duality of ∀ and ∃. (Contributed by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | ||
| Theorem | bj-aleximiALT 36643 | Alternate proof of aleximi 1832 from exim 1834, 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 36644 | A commuted form of exim 1834 which is sometimes posited as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023.) |
| ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓)) | ||
| Theorem | bj-ax12wlem 36645* | A lemma used to prove a weak version of the axiom of substitution ax-12 2177. (Temporary comment: The general statement that ax12wlem 2132 proves.) (Contributed by BJ, 20-Mar-2020.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
| Theorem | bj-cbvalim 36646* | A lemma used to prove bj-cbval 36650 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
| ⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
| Theorem | bj-cbvexim 36647* | A lemma used to prove bj-cbvex 36651 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∃𝑥𝜑 → ∃𝑦𝜓))) | ||
| Theorem | bj-cbvalimi 36648* | An equality-free general instance of one half of a precise form of bj-cbval 36650. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ ∀𝑦∃𝑥𝜒 ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
| Theorem | bj-cbveximi 36649* | An equality-free general instance of one half of a precise form of bj-cbvex 36651. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
| ⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ ∀𝑥∃𝑦𝜒 ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
| Theorem | bj-cbval 36650* | 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 36651* | 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 36652 | Syntax for BJ's version of the uniqueness quantifier. |
| wff ∃**𝑥𝜑 | ||
| Definition | df-bj-mo 36653* | 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 36654* | Substitution in an equality, disjoint variables case. Uses only ax-1 6 through ax-6 1967. It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq 36654 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 36655* | A lemma for the definiens of df-sb 2065. An instance of sp 2183 proved without it. Note: it has a common subproof with sbjust 2063. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
| Theorem | bj-ssblem2 36656* | An instance of ax-11 2157 proved without it. The converse may not be provable without ax-11 2157 (since using alcomimw 2042 would require a DV on 𝜑, 𝑥, which defeats the purpose). (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) | ||
| Theorem | bj-ax12v 36657* | A weaker form of ax-12 2177 and ax12v 2178, 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 36658* | Remove a DV condition from bj-ax12v 36657 (using core axioms only). (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
| Theorem | bj-ax12ssb 36659* | Axiom bj-ax12 36658 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑) | ||
| Theorem | bj-19.41al 36660 | Special case of 19.41 2235 proved from core axioms, ax-10 2141 (modal5), and hba1 2293 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ (∃𝑥(𝜑 ∧ ∀𝑥𝜓) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝜓)) | ||
| Theorem | bj-equsexval 36661* | Special case of equsexv 2268 proved from core axioms, ax-10 2141 (modal5), and hba1 2293 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥𝜓) | ||
| Theorem | bj-subst 36662* | Proof of sbalex 2242 from core axioms, ax-10 2141 (modal5), and bj-ax12 36658. (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
| Theorem | bj-ssbid2 36663 | A special case of sbequ2 2249. (Contributed by BJ, 22-Dec-2020.) |
| ⊢ ([𝑥 / 𝑥]𝜑 → 𝜑) | ||
| Theorem | bj-ssbid2ALT 36664 | Alternate proof of bj-ssbid2 36663, not using sbequ2 2249. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ([𝑥 / 𝑥]𝜑 → 𝜑) | ||
| Theorem | bj-ssbid1 36665 | A special case of sbequ1 2248. (Contributed by BJ, 22-Dec-2020.) |
| ⊢ (𝜑 → [𝑥 / 𝑥]𝜑) | ||
| Theorem | bj-ssbid1ALT 36666 | Alternate proof of bj-ssbid1 36665, not using sbequ1 2248. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → [𝑥 / 𝑥]𝜑) | ||
| Theorem | bj-ax6elem1 36667* | Lemma for bj-ax6e 36669. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
| Theorem | bj-ax6elem2 36668* | Lemma for bj-ax6e 36669. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥 𝑦 = 𝑧 → ∃𝑥 𝑥 = 𝑦) | ||
| Theorem | bj-ax6e 36669 | Proof of ax6e 2388 (hence ax6 2389) from Tarski's system, ax-c9 38891, ax-c16 38893. Remark: ax-6 1967 is used only via its principal (unbundled) instance ax6v 1968. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∃𝑥 𝑥 = 𝑦 | ||
| Theorem | bj-spimvwt 36670* | Closed form of spimvw 1995. See also spimt 2391. (Contributed by BJ, 8-Nov-2021.) |
| ⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → 𝜓)) | ||
| Theorem | bj-spnfw 36671 | Theorem close to a closed form of spnfw 1979. (Contributed by BJ, 12-May-2019.) |
| ⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
| Theorem | bj-cbvexiw 36672* | Change bound variable. This is to cbvexvw 2036 what cbvaliw 2005 is to cbvalvw 2035. TODO: move after cbvalivw 2006. (Contributed by BJ, 17-Mar-2020.) |
| ⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
| Theorem | bj-cbvexivw 36673* | Change bound variable. This is to cbvexvw 2036 what cbvalivw 2006 is to cbvalvw 2035. TODO: move after cbvalivw 2006. (Contributed by BJ, 17-Mar-2020.) |
| ⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
| Theorem | bj-modald 36674 | A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021.) |
| ⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑) | ||
| Theorem | bj-denot 36675* | A weakening of ax-6 1967 and ax6v 1968. (Contributed by BJ, 4-Apr-2021.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑥 → ¬ ∀𝑦 ¬ 𝑦 = 𝑥) | ||
| Theorem | bj-eqs 36676* | A lemma for substitutions, proved from Tarski's FOL. The version without DV (𝑥, 𝑦) is true but requires ax-13 2377. The disjoint variable condition DV (𝑥, 𝜑) is necessary for both directions: consider substituting 𝑥 = 𝑧 for 𝜑. (Contributed by BJ, 25-May-2021.) |
| ⊢ (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
| Theorem | bj-cbvexw 36677* | Change bound variable. This is to cbvexvw 2036 what cbvalw 2034 is to cbvalvw 2035. (Contributed by BJ, 17-Mar-2020.) |
| ⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
| Theorem | bj-ax12w 36678* | The general statement that ax12w 2133 proves. (Contributed by BJ, 20-Mar-2020.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
| Theorem | bj-ax89 36679 | 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 36679 by using mpan2 691 (respectively mpan 690) and equid 2011. TODO: move to main part. (Contributed by BJ, 3-Oct-2019.) |
| ⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡)) | ||
| Theorem | bj-cleljusti 36680* | One direction of cleljust 2117, requiring only ax-1 6-- ax-5 1910 and ax8v1 2112. (Contributed by BJ, 31-Dec-2020.) (Proof modification is discouraged.) |
| ⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑦) | ||
| Theorem | bj-alcomexcom 36681 | 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 1809 section, soon after 2nexaln 1830, and used to prove excom 2162. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.) |
| ⊢ ((∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑦∀𝑥 ¬ 𝜑) ↔ (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑)) | ||
| Theorem | bj-hbalt 36682 | Closed form of hbal 2167. When in main part, prove hbal 2167 and hbald 2168 from it. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) | ||
| Theorem | axc11n11 36683 | Proof of axc11n 2431 from { ax-1 6-- ax-7 2007, axc11 2435 } . Almost identical to axc11nfromc11 38927. (Contributed by NM, 6-Jul-2021.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
| Theorem | axc11n11r 36684 |
Proof of axc11n 2431 from { ax-1 6--
ax-7 2007, axc9 2387, axc11r 2371 } (note
that axc16 2261 is provable from { ax-1 6--
ax-7 2007, axc11r 2371 }).
Note that axc11n 2431 proves (over minimal calculus) that axc11 2435 and axc11r 2371 are equivalent. Therefore, axc11n11 36683 and axc11n11r 36684 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2435 appears slightly stronger since axc11n11r 36684 requires axc9 2387 while axc11n11 36683 does not). (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
| Theorem | bj-axc16g16 36685* | Proof of axc16g 2260 from { ax-1 6-- ax-7 2007, axc16 2261 }. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
| Theorem | bj-ax12v3 36686* | A weak version of ax-12 2177 which is stronger than ax12v 2178. Note that if one assumes reflexivity of equality ⊢ 𝑥 = 𝑥 (equid 2011), then bj-ax12v3 36686 implies ax-5 1910 over modal logic K (substitute 𝑥 for 𝑦). See also bj-ax12v3ALT 36687. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
| Theorem | bj-ax12v3ALT 36687* | Alternate proof of bj-ax12v3 36686. Uses axc11r 2371 and axc15 2427 instead of ax-12 2177. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
| Theorem | bj-sb 36688* | A weak variant of sbid2 2513 not requiring ax-13 2377 nor ax-10 2141. On top of Tarski's FOL, one implication requires only ax12v 2178, and the other requires only sp 2183. (Contributed by BJ, 25-May-2021.) |
| ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
| Theorem | bj-modalbe 36689 | The predicate-calculus version of the axiom (B) of modal logic. See also modal-b 2319. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (𝜑 → ∀𝑥∃𝑥𝜑) | ||
| Theorem | bj-spst 36690 | Closed form of sps 2185. Once in main part, prove sps 2185 and spsd 2187 from it. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ ((𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
| Theorem | bj-19.21bit 36691 | Closed form of 19.21bi 2189. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ ((𝜑 → ∀𝑥𝜓) → (𝜑 → 𝜓)) | ||
| Theorem | bj-19.23bit 36692 | Closed form of 19.23bi 2191. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ ((∃𝑥𝜑 → 𝜓) → (𝜑 → 𝜓)) | ||
| Theorem | bj-nexrt 36693 | Closed form of nexr 2192. Contrapositive of 19.8a 2181. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (¬ ∃𝑥𝜑 → ¬ 𝜑) | ||
| Theorem | bj-alrim 36694 | Closed form of alrimi 2213. (Contributed by BJ, 2-May-2019.) |
| ⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
| Theorem | bj-alrim2 36695 | Uncurried (imported) form of bj-alrim 36694. (Contributed by BJ, 2-May-2019.) |
| ⊢ ((Ⅎ𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (𝜑 → ∀𝑥𝜓)) | ||
| Theorem | bj-nfdt0 36696 | A theorem close to a closed form of nf5d 2284 and nf5dh 2147. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → (∀𝑥𝜑 → Ⅎ𝑥𝜓)) | ||
| Theorem | bj-nfdt 36697 | Closed form of nf5d 2284 and nf5dh 2147. (Contributed by BJ, 2-May-2019.) |
| ⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → ((𝜑 → ∀𝑥𝜑) → (𝜑 → Ⅎ𝑥𝜓))) | ||
| Theorem | bj-nexdt 36698 | Closed form of nexd 2221. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓))) | ||
| Theorem | bj-nexdvt 36699* | Closed form of nexdv 1936. (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓)) | ||
| Theorem | bj-alexbiex 36700 | Adding a second quantifier over the same variable is a transparent operation, (∀∃ case). (Contributed by BJ, 20-Oct-2019.) |
| ⊢ (∀𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |