Home | Metamath
Proof Explorer Theorem List (p. 339 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-looinvii 33801 | Inference associated with bj-looinvi 33800. (Contributed by BJ, 30-Mar-2020.) |
⊢ ((𝜑 → 𝜓) → 𝜓) & ⊢ (𝜓 → 𝜑) ⇒ ⊢ 𝜑 | ||
A few lemmas about disjunction. The fundamental theorems in this family are the dual statements pm4.71 558 and pm4.72 943. See also biort 929 and biorf 930. | ||
Theorem | bj-jaoi1 33802 | Shortens orfa2 35247 (58>53), pm1.2 897 (20>18), pm1.2 897 (20>18), pm2.4 900 (31>25), pm2.41 901 (31>25), pm2.42 936 (38>32), pm3.2ni 874 (43>39), pm4.44 990 (55>51). (Contributed by BJ, 30-Sep-2019.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜓) → 𝜓) | ||
Theorem | bj-jaoi2 33803 | Shortens consensus 1044 (110>106), elnn0z 11983 (336>329), pm1.2 897 (20>19), pm3.2ni 874 (43>39), pm4.44 990 (55>51). (Contributed by BJ, 30-Sep-2019.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜓 ∨ 𝜑) → 𝜓) | ||
A few other characterizations of the bicondional. The inter-definability of logical connectives offers many ways to express a given statement. Some useful theorems in this regard are df-or 842, df-an 397, pm4.64 843, imor 847, pm4.62 850 through pm4.67 399, and, for the De Morgan laws, ianor 975 through pm4.57 984. | ||
Theorem | bj-dfbi4 33804 | Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∨ ¬ (𝜑 ∨ 𝜓))) | ||
Theorem | bj-dfbi5 33805 | Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∧ 𝜓))) | ||
Theorem | bj-dfbi6 33806 | Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∧ 𝜓))) | ||
Theorem | bj-bijust0ALT 33807 | Alternate proof of bijust0 205; shorter but using additional intermediate results. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Revised by BJ, 19-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ((𝜑 → 𝜑) → ¬ (𝜑 → 𝜑)) | ||
Theorem | bj-bijust00 33808 | A self-implication does not imply the negation of a self-implication. Most general theorem of which bijust 206 is an instance (bijust0 205 and bj-bijust0ALT 33807 are therefore also instances of it). (Contributed by BJ, 7-Sep-2022.) |
⊢ ¬ ((𝜑 → 𝜑) → ¬ (𝜓 → 𝜓)) | ||
Theorem | bj-consensus 33809 | Version of consensus 1044 expressed using the conditional operator. (Remark: it may be better to express it as consensus 1044, using only binary connectives, and hinting at the fact that it is a Boolean algebra identity, like the absorption identities.) (Contributed by BJ, 30-Sep-2019.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | bj-consensusALT 33810 | Alternate proof of bj-consensus 33809. (Contributed by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | bj-df-ifc 33811* | Candidate definition for the conditional operator for classes. This is in line with the definition of a class as the extension of a predicate in df-clab 2800. We reprove the current df-if 4466 from it in bj-dfif 33812. (Contributed by BJ, 20-Sep-2019.) (Proof modification is discouraged.) |
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ if-(𝜑, 𝑥 ∈ 𝐴, 𝑥 ∈ 𝐵)} | ||
Theorem | bj-dfif 33812* | Alternate definition of the conditional operator for classes, which used to be the main definition. (Contributed by BJ, 26-Dec-2023.) (Proof modification is discouraged.) |
⊢ if(𝜑, 𝐴, 𝐵) = {𝑥 ∣ ((𝜑 ∧ 𝑥 ∈ 𝐴) ∨ (¬ 𝜑 ∧ 𝑥 ∈ 𝐵))} | ||
Theorem | bj-ififc 33813 | A biconditional connecting the conditional operator for propositions and the conditional operator for classes. Note that there is no sethood hypothesis on 𝑋: it is implied by either side. (Contributed by BJ, 24-Sep-2019.) Generalize statement from setvar 𝑥 to class 𝑋. (Revised by BJ, 26-Dec-2023.) |
⊢ (𝑋 ∈ if(𝜑, 𝐴, 𝐵) ↔ if-(𝜑, 𝑋 ∈ 𝐴, 𝑋 ∈ 𝐵)) | ||
Miscellaneous theorems of propositional calculus. | ||
Theorem | bj-imbi12 33814 | Uncurried (imported) form of imbi12 348. (Contributed by BJ, 6-May-2019.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))) | ||
Theorem | bj-biorfi 33815 | This should be labeled "biorfi" while the current biorfi 932 should be labeled "biorfri". The dual of biorf 930 is not biantr 802 but iba 528 (and ibar 529). So there should also be a "biorfr". (Note that these four statements can actually be strengthened to biconditionals.) (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓)) | ||
Theorem | bj-falor 33816 | Dual of truan 1539 (which has biconditional reversed). (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 ↔ (⊥ ∨ 𝜑)) | ||
Theorem | bj-falor2 33817 | Dual of truan 1539. (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.) |
⊢ ((⊥ ∨ 𝜑) ↔ 𝜑) | ||
Theorem | bj-bibibi 33818 | A property of the biconditional. (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 ↔ (𝜓 ↔ (𝜑 ↔ 𝜓))) | ||
Theorem | bj-imn3ani 33819 | Duplication of bnj1224 31973. Three-fold version of imnani 401. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by BJ, 22-Oct-2019.) (Proof modification is discouraged.) |
⊢ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒) | ||
Theorem | bj-andnotim 33820 | Two ways of expressing a certain ternary connective. Note the respective positions of the three formulas on each side of the biconditional. (Contributed by BJ, 6-Oct-2018.) |
⊢ (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) ∨ 𝜒)) | ||
Theorem | bj-bi3ant 33821 | This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013.) (Revised by BJ, 14-Jun-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (((𝜃 → 𝜏) → 𝜑) → (((𝜏 → 𝜃) → 𝜓) → ((𝜃 ↔ 𝜏) → 𝜒))) | ||
Theorem | bj-bisym 33822 | This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013.) (Revised by BJ, 14-Jun-2019.) |
⊢ (((𝜑 → 𝜓) → (𝜒 → 𝜃)) → (((𝜓 → 𝜑) → (𝜃 → 𝜒)) → ((𝜑 ↔ 𝜓) → (𝜒 ↔ 𝜃)))) | ||
Theorem | bj-bixor 33823 | Equivalence of two ternary operations. Note the identical order and parenthesizing of the three arguments in both expressions. (Contributed by BJ, 31-Dec-2023.) |
⊢ ((𝜑 ↔ (𝜓 ⊻ 𝜒)) ↔ (𝜑 ⊻ (𝜓 ↔ 𝜒))) | ||
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 1787 corresponds to the necessitation rule of modal logic, and ax-4 1801 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/ 1801. A basic result in this logic is bj-gl4 33827. | ||
Theorem | bj-axdd2 33824 | This implication, proved using only ax-gen 1787 and ax-4 1801 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 33825. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜓)) | ||
Theorem | bj-axd2d 33825 | This implication, proved using only ax-gen 1787 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 33824. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥⊤ → ∃𝑥⊤) → ∃𝑥⊤) | ||
Theorem | bj-axtd 33826 | 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 33824 and bj-axd2d 33825. (Contributed by BJ, 16-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥 ¬ 𝜑 → ¬ 𝜑) → ((∀𝑥𝜑 → 𝜑) → (∀𝑥𝜑 → ∃𝑥𝜑))) | ||
Theorem | bj-gl4 33827 | 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 33827 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 33828 | Over minimal calculus, the modal axiom (4) (hba1 2293) and the modal axiom (K) (ax-4 1801) together imply axc4 2332. (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 33830 and ax-prv2 33831 and ax-prv3 33832. Note the similarity with ax-gen 1787, ax-4 1801 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 33835) and Löb's theorem (bj-babylob 33836). See the comments of these theorems for details. | ||
Syntax | cprvb 33829 | Syntax for the provability predicate. |
wff Prv 𝜑 | ||
Axiom | ax-prv1 33830 | First property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ 𝜑 ⇒ ⊢ Prv 𝜑 | ||
Axiom | ax-prv2 33831 | Second property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ (Prv (𝜑 → 𝜓) → (Prv 𝜑 → Prv 𝜓)) | ||
Axiom | ax-prv3 33832 | Third property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ (Prv 𝜑 → Prv Prv 𝜑) | ||
Theorem | prvlem1 33833 | An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (Prv 𝜑 → Prv 𝜓) | ||
Theorem | prvlem2 33834 | An elementary property of the provability predicate. (Contributed by BJ, 3-Apr-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (Prv 𝜑 → (Prv 𝜓 → Prv 𝜒)) | ||
Theorem | bj-babygodel 33835 |
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 33836 |
See the section header comments for the context, as well as the comments
for bj-babygodel 33835.
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/ 33835). (Contributed by BJ, 20-Apr-2019.) |
⊢ (𝜓 ↔ (Prv 𝜓 → 𝜑)) & ⊢ (Prv 𝜑 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | bj-godellob 33837 | Proof of Gödel's theorem from Löb's theorem (see comments at bj-babygodel 33835 and bj-babylob 33836 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 33838 | Generalization rule on the right conjunct. See 19.28 2221. (Contributed by BJ, 7-Jul-2021.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 ∧ ∀𝑥𝜓) | ||
Theorem | bj-genl 33839 | Generalization rule on the left conjunct. See 19.27 2220. (Contributed by BJ, 7-Jul-2021.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (∀𝑥𝜑 ∧ 𝜓) | ||
Theorem | bj-genan 33840 | Generalization rule on a conjunction. Forward inference associated with 19.26 1862. (Contributed by BJ, 7-Jul-2021.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ (∀𝑥𝜑 ∧ ∀𝑥𝜓) | ||
Theorem | bj-mpgs 33841 | 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 1789 when sp 2172 is not available. (Contributed by BJ, 1-Nov-2023.) |
⊢ 𝜑 & ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | bj-2alim 33842 | Closed form of 2alimi 1804. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)) | ||
Theorem | bj-2exim 33843 | Closed form of 2eximi 1827. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)) | ||
Theorem | bj-alanim 33844 | Closed form of alanimi 1808. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥((𝜑 ∧ 𝜓) → 𝜒) → ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒)) | ||
Theorem | bj-2albi 33845 | Closed form of 2albii 1812. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)) | ||
Theorem | bj-notalbii 33846 | Equivalence of universal quantification of negation of equivalent formulas. Shortens ab0 4332 (103>94), ballotlem2 31646 (2655>2648), bnj1143 31962 (522>519), hausdiag 22183 (2119>2104). (Contributed by BJ, 17-Jul-2021.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑥 ¬ 𝜓) | ||
Theorem | bj-2exbi 33847 | Closed form of 2exbii 1840. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)) | ||
Theorem | bj-3exbi 33848 | Closed form of 3exbii 1841. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥∀𝑦∀𝑧(𝜑 ↔ 𝜓) → (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)) | ||
Theorem | bj-sylgt2 33849 | Uncurried (imported) form of sylgt 1813. (Contributed by BJ, 2-May-2019.) |
⊢ ((∀𝑥(𝜓 → 𝜒) ∧ (𝜑 → ∀𝑥𝜓)) → (𝜑 → ∀𝑥𝜒)) | ||
Theorem | bj-alrimg 33850 | 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 33854. (Contributed by BJ, 9-Dec-2023.) |
⊢ ((𝜑 → ∀𝑥𝜓) → (∀𝑥(𝜓 → 𝜒) → (𝜑 → ∀𝑥𝜒))) | ||
Theorem | bj-alrimd 33851 | A slightly more general alrimd 2206. A common usage will have 𝜑 substituted for 𝜓 and 𝜒 substituted for 𝜃, giving a form closer to alrimd 2206. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜃)) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜒 → ∀𝑥𝜏)) | ||
Theorem | bj-sylget 33852 | Dual statement of sylgt 1813. Closed form of bj-sylge 33855. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜒 → 𝜑) → ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜒 → 𝜓))) | ||
Theorem | bj-sylget2 33853 | Uncurried (imported) form of bj-sylget 33852. (Contributed by BJ, 2-May-2019.) |
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ (∃𝑥𝜓 → 𝜒)) → (∃𝑥𝜑 → 𝜒)) | ||
Theorem | bj-exlimg 33854 | 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 33850. (Contributed by BJ, 9-Dec-2023.) |
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥(𝜒 → 𝜑) → (∃𝑥𝜒 → 𝜓))) | ||
Theorem | bj-sylge 33855 | Dual statement of sylg 1814 (the final "e" in the label stands for "existential (version of sylg 1814)". Variant of exlimih 2289. (Contributed by BJ, 25-Dec-2023.) |
⊢ (∃𝑥𝜑 → 𝜓) & ⊢ (𝜒 → 𝜑) ⇒ ⊢ (∃𝑥𝜒 → 𝜓) | ||
Theorem | bj-exlimd 33856 | A slightly more general exlimd 2209. A common usage will have 𝜑 substituted for 𝜓 and 𝜃 substituted for 𝜏, giving a form closer to exlimd 2209. (Contributed by BJ, 25-Dec-2023.) |
⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜑 → (∃𝑥𝜃 → 𝜏)) & ⊢ (𝜓 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → (∃𝑥𝜒 → 𝜏)) | ||
Theorem | bj-nfimexal 33857 | 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 1830) and the converse implication is the join of instances of bj-alrimg 33850 and bj-exlimg 33854 (see 19.38a 1831 and 19.38b 1832). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.) |
⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-alexim 33858 | Closed form of aleximi 1823. Note: this proof is shorter, so aleximi 1823 could be deduced from it (exim 1825 would have to be proved first, see bj-eximALT 33872 but its proof is shorter (currently almost a subproof of aleximi 1823)). (Contributed by BJ, 8-Nov-2021.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))) | ||
Theorem | bj-nexdh 33859 | Closed form of nexdh 1857 (actually, its general instance). (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → ((𝜒 → ∀𝑥𝜑) → (𝜒 → ¬ ∃𝑥𝜓))) | ||
Theorem | bj-nexdh2 33860 | Uncurried (imported) form of bj-nexdh 33859. (Contributed by BJ, 6-May-2019.) |
⊢ ((∀𝑥(𝜑 → ¬ 𝜓) ∧ (𝜒 → ∀𝑥𝜑)) → (𝜒 → ¬ ∃𝑥𝜓)) | ||
Theorem | bj-hbxfrbi 33861 | Closed form of hbxfrbi 1816. Note: it is less important than nfbiit 1842. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht 33968) in order not to require sp 2172 (modal T). See bj-hbyfrbi 33862 for its version with existential quantifiers. (Contributed by BJ, 6-May-2019.) |
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((𝜑 → ∀𝑥𝜑) ↔ (𝜓 → ∀𝑥𝜓))) | ||
Theorem | bj-hbyfrbi 33862 | Version of bj-hbxfrbi 33861 with existential quantifiers. (Contributed by BJ, 23-Aug-2023.) |
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → ((∃𝑥𝜑 → 𝜑) ↔ (∃𝑥𝜓 → 𝜓))) | ||
Theorem | bj-exalim 33863 |
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 1902. I propose to move to the main part: bj-exalim 33863, bj-exalimi 33864, bj-exalims 33865, bj-exalimsi 33866, bj-ax12i 33868, bj-ax12wlem 33875, bj-ax12w 33908, and remove equs3OLD 1956. A new label is needed for bj-ax12i 33868 and label suggestions are welcome for the others. I also propose to change ¬ ∀𝑥¬ to ∃𝑥 in speimfw 1957 and spimfw 1959 (other spim* theorems use ∃𝑥 and very few theorems in set.mm use ¬ ∀𝑥¬). (Contributed by BJ, 8-Nov-2021.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒))) | ||
Theorem | bj-exalimi 33864 | An inference for distributing quantifiers over a nested implication. The canonical derivation from its closed form bj-exalim 33863 (using mpg 1789) has fewer essential steps, but more steps in total (yielding a longer compressed proof). (Almost) the general statement that speimfw 1957 proves. (Contributed by BJ, 29-Sep-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | bj-exalims 33865 | Distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1959 proves. (Contributed by BJ, 29-Sep-2019.) |
⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒)) ⇒ ⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒))) | ||
Theorem | bj-exalimsi 33866 | An inference for distributing quantifiers over a nested implication. (Almost) the general statement that spimfw 1959 proves. (Contributed by BJ, 29-Sep-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (∃𝑥𝜑 → (¬ 𝜒 → ∀𝑥 ¬ 𝜒)) ⇒ ⊢ (∃𝑥𝜑 → (∀𝑥𝜓 → 𝜒)) | ||
Theorem | bj-ax12ig 33867 | A lemma used to prove a weak form of the axiom of substitution. A generalization of bj-ax12i 33868. (Contributed by BJ, 19-Dec-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-ax12i 33868 | A weakening of bj-ax12ig 33867 that is sufficient to prove a weak form of the axiom of substitution ax-12 2167. The general statement of which ax12i 1960 is an instance. (Contributed by BJ, 29-Sep-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-nfimt 33869 | Closed form of nfim 1888 and curried (exported) form of nfimt 1887. (Contributed by BJ, 20-Oct-2021.) |
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-cbvalimt 33870 | A lemma in closed form used to prove bj-cbval 33880 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1869 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.) |
⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓))))) | ||
Theorem | bj-cbveximt 33871 | A lemma in closed form used to prove bj-cbvex 33881 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1869 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.) |
⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∀𝑥(𝜑 → ∀𝑦𝜑) → ((∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) → (∃𝑥𝜑 → ∃𝑦𝜓))))) | ||
Theorem | bj-eximALT 33872 | Alternate proof of exim 1825 directly from alim 1802 by using df-ex 1772 (using duality of ∀ and ∃. (Contributed by BJ, 9-Dec-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | bj-aleximiALT 33873 | Alternate proof of aleximi 1823 from exim 1825, 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 33874 | A commuted form of exim 1825 which is sometimes posited as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023.) |
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | bj-ax12wlem 33875* | A lemma used to prove a weak version of the axiom of substitution ax-12 2167. (Temporary comment: The general statement that ax12wlem 2127 proves.) (Contributed by BJ, 20-Mar-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-cbvalim 33876* | A lemma used to prove bj-cbval 33880 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → ∀𝑦𝜓))) | ||
Theorem | bj-cbvexim 33877* | A lemma used to prove bj-cbvex 33881 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥∃𝑦𝜒 → (∀𝑥∀𝑦(𝜒 → (𝜑 → 𝜓)) → (∃𝑥𝜑 → ∃𝑦𝜓))) | ||
Theorem | bj-cbvalimi 33878* | An equality-free general instance of one half of a precise form of bj-cbval 33880. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ ∀𝑦∃𝑥𝜒 ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | bj-cbveximi 33879* | An equality-free general instance of one half of a precise form of bj-cbvex 33881. (Contributed by BJ, 12-Mar-2023.) (Proof modification is discouraged.) |
⊢ (𝜒 → (𝜑 → 𝜓)) & ⊢ ∀𝑥∃𝑦𝜒 ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
Theorem | bj-cbval 33880* | 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 33881* | 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 33882 | Syntax for BJ's version of the uniqueness quantifier. |
wff ∃**𝑥𝜑 | ||
Definition | df-bj-mo 33883* | 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 33884* | Substitution in an equality, disjoint variables case. Uses only ax-1 6 through ax-6 1961. It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq 33884 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 33885* | 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 33886* | An instance of ax-11 2151 proved without it. The converse may not be provable without ax-11 2151 (since using alcomiw 2041 would require a DV on 𝜑, 𝑥, which defeats the purpose). (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑥∀𝑦(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑)) → ∀𝑦∀𝑥(𝑦 = 𝑡 → (𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-ax12v 33887* | 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 33888* | Remove a DV condition from bj-ax12v 33887 (using core axioms only). (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.) |
⊢ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))) | ||
Theorem | bj-ax12ssb 33889* | The axiom bj-ax12 33888 expressed using substitution. (Contributed by BJ, 26-Dec-2020.) (Proof modification is discouraged.) |
⊢ [𝑡 / 𝑥](𝜑 → [𝑡 / 𝑥]𝜑) | ||
Theorem | bj-19.41al 33890 | Special case of 19.41 2228 proved from Tarski, ax-10 2136 (modal5) and hba1 2293 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑥(𝜑 ∧ ∀𝑥𝜓) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | bj-equsexval 33891* | Special case of equsexv 2260 proved from Tarski, ax-10 2136 (modal5) and hba1 2293 (modal4). (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥𝜓) | ||
Theorem | bj-sb56 33892* | Proof of sb56 2269 from Tarski, ax-10 2136 (modal5) and bj-ax12 33888. (Contributed by BJ, 29-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-ssbid2 33893 | A special case of sbequ2 2241. (Contributed by BJ, 22-Dec-2020.) |
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑) | ||
Theorem | bj-ssbid2ALT 33894 | Alternate proof of bj-ssbid2 33893, not using sbequ2 2241. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑥 / 𝑥]𝜑 → 𝜑) | ||
Theorem | bj-ssbid1 33895 | A special case of sbequ1 2240. (Contributed by BJ, 22-Dec-2020.) |
⊢ (𝜑 → [𝑥 / 𝑥]𝜑) | ||
Theorem | bj-ssbid1ALT 33896 | Alternate proof of bj-ssbid1 33895, not using sbequ1 2240. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → [𝑥 / 𝑥]𝜑) | ||
Theorem | bj-ax6elem1 33897* | Lemma for bj-ax6e 33899. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | bj-ax6elem2 33898* | Lemma for bj-ax6e 33899. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑦 = 𝑧 → ∃𝑥 𝑥 = 𝑦) | ||
Theorem | bj-ax6e 33899 | Proof of ax6e 2394 (hence ax6 2395) from Tarski's system, ax-c9 35908, ax-c16 35910. Remark: ax-6 1961 is used only via its principal (unbundled) instance ax6v 1962. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | bj-spimvwt 33900* | Closed form of spimvw 1993. See also spimt 2397. (Contributed by BJ, 8-Nov-2021.) |
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |