Home | Metamath
Proof Explorer Theorem List (p. 341 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bj-ax6e 34001 | Proof of ax6e 2401 (hence ax6 2402) from Tarski's system, ax-c9 36041, ax-c16 36043. Remark: ax-6 1970 is used only via its principal (unbundled) instance ax6v 1971. (Contributed by BJ, 22-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | bj-spimvwt 34002* | Closed form of spimvw 2002. See also spimt 2404. (Contributed by BJ, 8-Nov-2021.) |
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-spnfw 34003 | Theorem close to a closed form of spnfw 1984. (Contributed by BJ, 12-May-2019.) |
⊢ ((∃𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-cbvexiw 34004* | Change bound variable. This is to cbvexvw 2044 what cbvaliw 2013 is to cbvalvw 2043. TODO: move after cbvalivw 2014. (Contributed by BJ, 17-Mar-2020.) |
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
Theorem | bj-cbvexivw 34005* | Change bound variable. This is to cbvexvw 2044 what cbvalivw 2014 is to cbvalvw 2043. TODO: move after cbvalivw 2014. (Contributed by BJ, 17-Mar-2020.) |
⊢ (𝑦 = 𝑥 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑦𝜓) | ||
Theorem | bj-modald 34006 | A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021.) |
⊢ (∀𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑) | ||
Theorem | bj-denot 34007* | A weakening of ax-6 1970 and ax6v 1971. (Contributed by BJ, 4-Apr-2021.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑥 → ¬ ∀𝑦 ¬ 𝑦 = 𝑥) | ||
Theorem | bj-eqs 34008* | A lemma for substitutions, proved from Tarski's FOL. The version without DV (𝑥, 𝑦) is true but requires ax-13 2390. The disjoint variable condition DV (𝑥, 𝜑) is necessary for both directions: consider substituting 𝑥 = 𝑧 for 𝜑. (Contributed by BJ, 25-May-2021.) |
⊢ (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | bj-cbvexw 34009* | Change bound variable. This is to cbvexvw 2044 what cbvalw 2042 is to cbvalvw 2043. (Contributed by BJ, 17-Mar-2020.) |
⊢ (∃𝑥∃𝑦𝜓 → ∃𝑦𝜓) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | bj-ax12w 34010* | The general statement that ax12w 2137 proves. (Contributed by BJ, 20-Mar-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 → (∀𝑦𝜓 → ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | bj-ax89 34011 | A theorem which could be used as sole axiom for the non-logical predicate instead of ax-8 2116 and ax-9 2124. Indeed, it is implied over propositional calculus by the conjunction of ax-8 2116 and ax-9 2124, as proved here. In the other direction, one can prove ax-8 2116 (respectively ax-9 2124) from bj-ax89 34011 by using mpan2 689 (respectively mpan 688) and equid 2019. TODO: move to main part. (Contributed by BJ, 3-Oct-2019.) |
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑡)) | ||
Theorem | bj-elequ12 34012 | An identity law for the non-logical predicate, which combines elequ1 2121 and elequ2 2129. For the analogous theorems for class terms, see eleq1 2900, eleq2 2901 and eleq12 2902. TODO: move to main part. (Contributed by BJ, 29-Sep-2019.) |
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑡) → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑡)) | ||
Theorem | bj-cleljusti 34013* | One direction of cleljust 2123, requiring only ax-1 6-- ax-5 1911 and ax8v1 2118. (Contributed by BJ, 31-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑦) | ||
Theorem | bj-alcomexcom 34014 | Commutation of universal quantifiers implies commutation of existential quantifiers. Can be placed in the ax-4 1810 section, soon after 2nexaln 1830, and used to prove excom 2169. (Contributed by BJ, 29-Nov-2020.) (Proof modification is discouraged.) |
⊢ ((∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑦∀𝑥 ¬ 𝜑) → (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑)) | ||
Theorem | bj-hbalt 34015 | Closed form of hbal 2174. When in main part, prove hbal 2174 and hbald 2175 from it. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)) | ||
Theorem | axc11n11 34016 | Proof of axc11n 2448 from { ax-1 6-- ax-7 2015, axc11 2452 } . Almost identical to axc11nfromc11 36077. (Contributed by NM, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | axc11n11r 34017 |
Proof of axc11n 2448 from { ax-1 6--
ax-7 2015, axc9 2400, axc11r 2386 } (note
that axc16 2262 is provable from { ax-1 6--
ax-7 2015, axc11r 2386 }).
Note that axc11n 2448 proves (over minimal calculus) that axc11 2452 and axc11r 2386 are equivalent. Therefore, axc11n11 34016 and axc11n11r 34017 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2452 appears slightly stronger since axc11n11r 34017 requires axc9 2400 while axc11n11 34016 does not). (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | bj-axc16g16 34018* | Proof of axc16g 2261 from { ax-1 6-- ax-7 2015, axc16 2262 }. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | bj-ax12v3 34019* | A weak version of ax-12 2177 which is stronger than ax12v 2178. Note that if one assumes reflexivity of equality ⊢ 𝑥 = 𝑥 (equid 2019), then bj-ax12v3 34019 implies ax-5 1911 over modal logic K (substitute 𝑥 for 𝑦). See also bj-ax12v3ALT 34020. (Contributed by BJ, 6-Jul-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-ax12v3ALT 34020* | Alternate proof of bj-ax12v3 34019. Uses axc11r 2386 and axc15 2444 instead of ax-12 2177. (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-sb 34021* | A weak variant of sbid2 2550 not requiring ax-13 2390 nor ax-10 2145. On top of Tarski's FOL, one implication requires only ax12v 2178, and the other requires only sp 2182. (Contributed by BJ, 25-May-2021.) |
⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | bj-modalbe 34022 | The predicate-calculus version of the axiom (B) of modal logic. See also modal-b 2338. (Contributed by BJ, 20-Oct-2019.) |
⊢ (𝜑 → ∀𝑥∃𝑥𝜑) | ||
Theorem | bj-spst 34023 | Closed form of sps 2184. Once in main part, prove sps 2184 and spsd 2186 from it. (Contributed by BJ, 20-Oct-2019.) |
⊢ ((𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | bj-19.21bit 34024 | Closed form of 19.21bi 2188. (Contributed by BJ, 20-Oct-2019.) |
⊢ ((𝜑 → ∀𝑥𝜓) → (𝜑 → 𝜓)) | ||
Theorem | bj-19.23bit 34025 | Closed form of 19.23bi 2190. (Contributed by BJ, 20-Oct-2019.) |
⊢ ((∃𝑥𝜑 → 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | bj-nexrt 34026 | Closed form of nexr 2191. Contrapositive of 19.8a 2180. (Contributed by BJ, 20-Oct-2019.) |
⊢ (¬ ∃𝑥𝜑 → ¬ 𝜑) | ||
Theorem | bj-alrim 34027 | Closed form of alrimi 2213. (Contributed by BJ, 2-May-2019.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-alrim2 34028 | Uncurried (imported) form of bj-alrim 34027. (Contributed by BJ, 2-May-2019.) |
⊢ ((Ⅎ𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-nfdt0 34029 | A theorem close to a closed form of nf5d 2292 and nf5dh 2151. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → (∀𝑥𝜑 → Ⅎ𝑥𝜓)) | ||
Theorem | bj-nfdt 34030 | Closed form of nf5d 2292 and nf5dh 2151. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜑 → (𝜓 → ∀𝑥𝜓)) → ((𝜑 → ∀𝑥𝜑) → (𝜑 → Ⅎ𝑥𝜓))) | ||
Theorem | bj-nexdt 34031 | Closed form of nexd 2223. (Contributed by BJ, 20-Oct-2019.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓))) | ||
Theorem | bj-nexdvt 34032* | Closed form of nexdv 1937. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) → (𝜑 → ¬ ∃𝑥𝜓)) | ||
Theorem | bj-alexbiex 34033 | Adding a second quantifier is a tranparent operation, (∀∃ case). (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | bj-exexbiex 34034 | Adding a second quantifier is a tranparent operation, (∃∃ case). (Contributed by BJ, 20-Oct-2019.) |
⊢ (∃𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | bj-alalbial 34035 | Adding a second quantifier is a tranparent operation, (∀∀ case). (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | bj-exalbial 34036 | Adding a second quantifier is a tranparent operation, (∃∀ case). (Contributed by BJ, 20-Oct-2019.) |
⊢ (∃𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | bj-19.9htbi 34037 | Strengthening 19.9ht 2339 by replacing its succedent with a biconditional (19.9t 2204 does have a biconditional succedent). This propagates. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 ↔ 𝜑)) | ||
Theorem | bj-hbntbi 34038 | Strengthening hbnt 2302 by replacing its succedent with a biconditional. See also hbntg 33050 and hbntal 40936. (Contributed by BJ, 20-Oct-2019.) Proved from bj-19.9htbi 34037. (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 ↔ ∀𝑥 ¬ 𝜑)) | ||
Theorem | bj-biexal1 34039 | A general FOL biconditional that generalizes 19.9ht 2339 among others. For this and the following theorems, see also 19.35 1878, 19.21 2207, 19.23 2211. When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-biexal2 34040 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(∃𝑥𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-biexal3 34041 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(∃𝑥𝜑 → 𝜓)) | ||
Theorem | bj-bialal 34042 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-biexex 34043 | When 𝜑 is substituted for 𝜓, both sides express a form of nonfreeness. (Contributed by BJ, 20-Oct-2019.) |
⊢ (∀𝑥(𝜑 → ∃𝑥𝜓) ↔ (∃𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | bj-hbext 34044 | Closed form of hbex 2344. (Contributed by BJ, 10-Oct-2019.) |
⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)) | ||
Theorem | bj-nfalt 34045 | Closed form of nfal 2342. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∀𝑥𝜑) | ||
Theorem | bj-nfext 34046 | Closed form of nfex 2343. (Contributed by BJ, 10-Oct-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∃𝑥𝜑) | ||
Theorem | bj-eeanvw 34047* | Version of exdistrv 1956 with a disjoint variable condition on 𝑥, 𝑦 not requiring ax-11 2161. (The same can be done with eeeanv 2371 and ee4anv 2372.) (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | bj-modal4 34048 | First-order logic form of the modal axiom (4). See hba1 2301. This is the standard proof of the implication in modal logic (B5 ⇒ 4). Its dual statement is bj-modal4e 34049. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | bj-modal4e 34049 | First-order logic form of the modal axiom (4) using existential quantifiers. Dual statement of bj-modal4 34048 (hba1 2301). (Contributed by BJ, 21-Dec-2020.) (Proof modification is discouraged.) |
⊢ (∃𝑥∃𝑥𝜑 → ∃𝑥𝜑) | ||
Theorem | bj-modalb 34050 | A short form of the axiom B of modal logic using only primitive symbols (→ , ¬ , ∀). (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) |
⊢ (¬ 𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | bj-wnf1 34051 | When 𝜑 is substituted for 𝜓, this is the first half of nonfreness (. → ∀) of the weak form of nonfreeness (∃ → ∀). (Contributed by BJ, 9-Dec-2023.) |
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∃𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-wnf2 34052 | When 𝜑 is substituted for 𝜓, this is the first half of nonfreness (. → ∀) of the weak form of nonfreeness (∃ → ∀). (Contributed by BJ, 9-Dec-2023.) |
⊢ (∃𝑥(∃𝑥𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-wnfanf 34053 | When 𝜑 is substituted for 𝜓, this statement expresses that weak nonfreeness implies the "forall" form of nonfreeness. (Contributed by BJ, 9-Dec-2023.) |
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → ∀𝑥𝜓)) | ||
Theorem | bj-wnfenf 34054 | When 𝜑 is substituted for 𝜓, this statement expresses that weak nonfreeness implies the "exists" form of nonfreeness. (Contributed by BJ, 9-Dec-2023.) |
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∃𝑥𝜑 → 𝜓)) | ||
Syntax | wnnf 34055 | Syntax for the nonfreeness quantifier. |
wff Ⅎ'𝑥𝜑 | ||
Definition | df-bj-nnf 34056 |
Definition of the nonfreeness quantifier. The formula Ⅎ'𝑥𝜑 has
the intended meaning that the variable 𝑥 is semantically nonfree in
the formula 𝜑. The motivation for this quantifier
is to have a
condition expressible in the logic which is as close as possible to the
non-occurrence condition DV (𝑥, 𝜑) (in Metamath files, "$d x ph
$."), which belongs to the metalogic.
The standard syntactic nonfreeness condition, also expressed in the metalogic, is intermediate between these two notions: semantic nonfreeness implies syntactic nonfreeness, which implies non-occurrence. Both implications are strict; for the first, note that ⊢ Ⅎ'𝑥𝑥 = 𝑥, that is, 𝑥 is semantically (but not syntactically) nonfree in the formula 𝑥 = 𝑥; for the second, note that 𝑥 is syntactically nonfree in the formula ∀𝑥𝑥 = 𝑥 although it occurs in it. We now prove two metatheorems which make precise the above fact that, as far as proving power is concerned, the nonfreeness condition Ⅎ'𝑥𝜑 is very close to the non-occurrence condition DV (𝑥, 𝜑). Let S be a Metamath system with the FOL-syntax of (i)set.mm, containing intuitionistic positive propositional calculus and ax-5 1911 and ax5e 1913. 1. If the scheme (Ⅎ'𝑥𝜑 & PHI1 & ... & PHIn ⇒ PHI0, DV) is provable in S, then so is the scheme (PHI1 & ... & PHIn ⇒ PHI0, DV ∪ {{𝑥, 𝜑}}). Proof: By bj-nnfv 34083, we can prove (Ⅎ'𝑥𝜑, {{𝑥, 𝜑}}), from which the theorem follows. QED 2. Suppose that S also contains (the FOL version of) modal logic KB and commutation of quantifiers alcom 2163 and excom 2169 (possibly weakened by a DV condition on the quantifying variables), and that S can be axiomatized such that the only axioms with a DV condition involving a formula variable are among ax-5 1911, ax5e 1913, ax5ea 1914. If the scheme (PHI1 & ... & PHIn ⇒ PHI0, DV) is provable in S, then so is the scheme (Ⅎ'𝑥𝜑 & PHI1 & ... & PHIn ⇒ PHI0, DV ∖ {{𝑥, 𝜑}}). More precisely, if S contains modal 45 and if the variables quantified over in PHI0, ..., PHIn are among 𝑥1, ..., 𝑥m, then the scheme (PHI1 & ... & PHIn ⇒ (antecedent → PHI0), DV ∖ {{𝑥, 𝜑}}) is provable in S, where the antecedent is a finite conjunction of formulas of the form ∀𝑥i1 ...∀𝑥ip Ⅎ'𝑥𝜑 where the 𝑥ij's are among the 𝑥i's. Lemma: If 𝑥 ∉ OC(PHI), then S proves the scheme (Ⅎ'𝑥𝜑 ⇒ Ⅎ'𝑥 PHI, {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}). More precisely, if the variables quantified over in PHI are among 𝑥1, ..., 𝑥m, then ((antecedent → Ⅎ'𝑥 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}) is provable in S, with the same form of antecedent as above. Proof: By induction on the height of PHI. We first note that by bj-nnfbi 34057 we can assume that PHI contains only primitive (as opposed to defined) symbols. For the base case, atomic formulas are either 𝜑, in which case the scheme to prove is an instance of id 22, or have variables all in OC(PHI) ∖ {𝜑}, so (Ⅎ'𝑥 PHI, {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}) by bj-nnfv 34083, hence ((Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}) by a1i 11. For the induction step, PHI is either an implication, a negation, a conjunction, a disjunction, a biconditional, a universal or an existential quantification of formulas where 𝑥 does not occur. We use respectively bj-nnfim 34075, bj-nnfnt 34069, bj-nnfan 34077, bj-nnfor 34079, bj-nnfbit 34081, bj-nnfalt 34095, bj-nnfext 34096. For instance, in the implication case, if we have by induction hypothesis ((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}) and ((∀𝑦1 ...∀𝑦n Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PSI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PSI) ∖ {𝜑}}), then bj-nnfim 34075 yields (((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 ∧ ∀𝑦1 ...∀𝑦n Ⅎ'𝑥𝜑) → Ⅎ'𝑥 (PHI → PSI)), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI → PSI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. In the universal quantification case, say quantification over 𝑦, if we have by induction hypothesis ((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PHI) ∖ {𝜑}}), then bj-nnfalt 34095 yields ((∀𝑦∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥∀𝑦 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(∀𝑦 PHI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. Note bj-nnfalt 34095 and bj-nnfext 34096 are proved from positive propositional calculus with alcom 2163 and excom 2169 (possibly weakened by a DV condition on the quantifying variables), and modalB (via bj-19.12 34090). QED Proof of the theorem: Consider a proof of that scheme directly from the axioms. Consider a step where a DV condition involving 𝜑 is used. By hypothesis, that step is an instance of ax-5 1911 or ax5e 1913 or ax5ea . It has the form (PSI → ∀𝑥 PSI) where PSI has the form of the lemma and the DV conditions of the proof contain {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PSI) }. Therefore, one has ((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → Ⅎ'𝑥 PSI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PSI) ∖ {𝜑}}) for appropriate 𝑥i's, and by bj-nnfa 34060 we obtain ((∀𝑥1 ...∀𝑥m Ⅎ'𝑥𝜑 → (PSI → ∀𝑥 PSI)), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(PSI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the theorem. Similarly if the step is using ax5e 1913 or ax5ea 1914, we would use bj-nnfe 34062 or bj-nnfea 34064 respectively. Therefore, taking as antecedent of the theorem to prove the conjunction of all the antecedents at each of these steps, we obtain a proof by "carrying the context over", which is possible, as in the deduction theorem when the step uses ax-mp 5, and when the step uses ax-gen 1796, by bj-nnf-alrim 34084 and bj-nnfa1 34088 (which requires modal 45). The condition DV (𝑥, 𝜑) is not required by the resulting proof. Finally, there may be in the global antecedent thus constructed some dummy variables, which can be removed by spvw 1985. QED Compared with df-nf 1785, the present definition is stricter on positive propositional calculus (bj-nnfnfTEMP 34067) and equivalent on core FOL plus sp 2182 (bj-nfnnfTEMP 34087). While being stricter, it still holds for non-occurring variables (bj-nnfv 34083), which is the basic requirement for this quantifier. In particular, it translates more closely the associated variable disjointness condition. Since the nonfreeness quantifier is a means to translate a variable disjointness condition from the metalogic to the logic, it seems preferable. Also, since nonfreeness is mainly used as a hypothesis, this definition would allow more theorems, notably the 19.xx theorems, to be proved from the core axioms, without needing a 19.xxv variant. One can devise infinitely many definitions increasingly close to the non-occurring condition, like ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ∧ ∀𝑥((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ∧ ∀𝑥∀𝑥... and each stronger definition would permit more theorems to be proved from the core axioms. A reasonable rule seems to be to stop before nested quantifiers appear (since they typically require ax-10 2145 to work with), and also not to have redundant conjuncts when full metacomplete FOL= is developed. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑))) | ||
Theorem | bj-nnfbi 34057 | If two formulas are equivalent for all 𝑥, then nonfreeness of 𝑥 in one of them is equivalent to nonfreeness in the other. Compare nfbiit 1851. From this and bj-nnfim 34075 and bj-nnfnt 34069, one can prove analogous nonfreeness conservation results for other propositional operators. The antecedent is in the "strong necessity" modality of modal logic (see also bj-nnftht 34070) in order not to require sp 2182 (modal T). (Contributed by BJ, 27-Aug-2023.) |
⊢ (((𝜑 ↔ 𝜓) ∧ ∀𝑥(𝜑 ↔ 𝜓)) → (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓)) | ||
Theorem | bj-nnfbd 34058* | If two formulas are equivalent for all 𝑥, then nonfreeness of 𝑥 in one of them is equivalent to nonfreeness in the other, deduction form. See bj-nnfbi 34057. (Contributed by BJ, 27-Aug-2023.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ'𝑥𝜓 ↔ Ⅎ'𝑥𝜒)) | ||
Theorem | bj-nnfbii 34059 | If two formulas are equivalent for all 𝑥, then nonfreeness of 𝑥 in one of them is equivalent to nonfreeness in the other, inference form. See bj-nnfbi 34057. (Contributed by BJ, 18-Nov-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥𝜓) | ||
Theorem | bj-nnfa 34060 | Nonfreeness implies the equivalent of ax-5 1911. See nf5r 2193, nf5ri 2195. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfad 34061 | Nonfreeness implies the equivalent of ax-5 1911, deduction form. See nf5rd 2196. (Contributed by BJ, 2-Dec-2024.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | bj-nnfe 34062 | Nonfreeness implies the equivalent of ax5e 1913. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → 𝜑)) | ||
Theorem | bj-nnfed 34063 | Nonfreeness implies the equivalent of ax5e 1913, deduction form. (Contributed by BJ, 2-Dec-2024.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓)) | ||
Theorem | bj-nnfea 34064 | Nonfreeness implies the equivalent of ax5ea 1914. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfead 34065 | Nonfreeness implies the equivalent of ax5ea 1914, deduction form. (Contributed by BJ, 2-Dec-2024.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) | ||
Theorem | bj-dfnnf2 34066 | Alternate definition of df-bj-nnf 34056 using only primitive symbols (→, ¬, ∀) in each conjunct. (Contributed by BJ, 20-Aug-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ ((𝜑 → ∀𝑥𝜑) ∧ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))) | ||
Theorem | bj-nnfnfTEMP 34067 | New nonfreeness implies old nonfreeness on implicational calculus (the proof indicates it uses ax-3 8 because of set.mm's definition of the biconditional, but the proof actually holds in minimal implicational calculus). (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1785 except via df-nf 1785 directly. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 → Ⅎ𝑥𝜑) | ||
Theorem | bj-wnfnf 34068 | When 𝜑 is substituted for 𝜓, this statement expresses nonfreeness in the weak form of nonfreeness (∃ → ∀). Note that this could also be proved from bj-nnfim 34075, bj-nnfe1 34089 and bj-nnfa1 34088. (Contributed by BJ, 9-Dec-2023.) |
⊢ Ⅎ'𝑥(∃𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | bj-nnfnt 34069 | A variable is nonfree in a formula if and only if it is nonfree in its negation. The foward implication is intuitionistically valid (and that direction is sufficient for the purpose of recursively proving that some formulas have a given variable not free in them, like bj-nnfim 34075). Intuitionistically, ⊢ (Ⅎ'𝑥¬ 𝜑 ↔ Ⅎ'𝑥¬ ¬ 𝜑). See nfnt 1856. (Contributed by BJ, 28-Jul-2023.) |
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ'𝑥 ¬ 𝜑) | ||
Theorem | bj-nnftht 34070 | A variable is nonfree in a theorem. The antecedent is in the "strong necessity" modality of modal logic in order not to require sp 2182 (modal T), as in bj-nnfbi 34057. (Contributed by BJ, 28-Jul-2023.) |
⊢ ((𝜑 ∧ ∀𝑥𝜑) → Ⅎ'𝑥𝜑) | ||
Theorem | bj-nnfth 34071 | A variable is nonfree in a theorem, inference form. (Contributed by BJ, 28-Jul-2023.) |
⊢ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnfnth 34072 | A variable is nonfree in the negation of a theorem, inference form. (Contributed by BJ, 27-Aug-2023.) |
⊢ ¬ 𝜑 ⇒ ⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnfim1 34073 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-nnfim2 34074 | A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜑 → 𝜓))) | ||
Theorem | bj-nnfim 34075 | Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 → 𝜓)) | ||
Theorem | bj-nnfimd 34076 | Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication, deduction form. (Contributed by BJ, 2-Dec-2023.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 → 𝜒)) | ||
Theorem | bj-nnfan 34077 | Nonfreeness in both conjuncts implies nonfreeness in the conjunction. (Contributed by BJ, 19-Nov-2023.) In classical logic, there is a proof using the definition of conjunction in terms of implication and negation, so using bj-nnfim 34075, bj-nnfnt 34069 and bj-nnfbi 34057, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | bj-nnfand 34078 | Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 34077, it has two more essential steps but fewer total steps (since there are fewer intermediate formulas to build) and is easier to follow and understand. This statement is of intermediate complexity: for simpler statements, closed-style proofs like that of bj-nnfan 34077 will generally be shorter than deduction-style proofs while still easy to follow, while for more complex statements, the opposite will be true (and deduction-style proofs like that of bj-nnfand 34078 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒)) | ||
Theorem | bj-nnfor 34079 | Nonfreeness in both disjuncts implies nonfreeness in the disjunction. (Contributed by BJ, 19-Nov-2023.) In classical logic, there is a proof using the definition of disjunction in terms of implication and negation, so using bj-nnfim 34075, bj-nnfnt 34069 and bj-nnfbi 34057, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | bj-nnford 34080 | Nonfreeness in both disjuncts implies nonfreeness in the disjunction, deduction form. See comments for bj-nnfor 34079 and bj-nnfand 34078. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∨ 𝜒)) | ||
Theorem | bj-nnfbit 34081 | Nonfreeness in both sides implies nonfreeness in the biconditional. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
⊢ ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑 ↔ 𝜓)) | ||
Theorem | bj-nnfbid 34082 | Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ'𝑥𝜓) & ⊢ (𝜑 → Ⅎ'𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ↔ 𝜒)) | ||
Theorem | bj-nnfv 34083* | A non-occurring variable is nonfree in a formula. (Contributed by BJ, 28-Jul-2023.) |
⊢ Ⅎ'𝑥𝜑 | ||
Theorem | bj-nnf-alrim 34084 | Proof of the closed form of alrimi 2213 from modalK (compare alrimiv 1928). See also bj-alrim 34027. Actually, most proofs between 19.3t 2201 and 2sbbid 2247 could be proved without ax-12 2177. (Contributed by BJ, 20-Aug-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-nnf-exlim 34085 | Proof of the closed form of exlimi 2217 from modalK (compare exlimiv 1931). See also bj-sylget2 33955. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))) | ||
Theorem | bj-dfnnf3 34086 | Alternate definition of nonfreeness when sp 2182 is available. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1785. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nfnnfTEMP 34087 | New nonfreeness is equivalent to old nonfreeness on core FOL axioms plus sp 2182. (Contributed by BJ, 28-Jul-2023.) The proof should not rely on df-nf 1785 except via df-nf 1785 directly. (Proof modification is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 ↔ Ⅎ𝑥𝜑) | ||
Theorem | bj-nnfa1 34088 | See nfa1 2155. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ Ⅎ'𝑥∀𝑥𝜑 | ||
Theorem | bj-nnfe1 34089 | See nfe1 2154. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ Ⅎ'𝑥∃𝑥𝜑 | ||
Theorem | bj-19.12 34090 | See 19.12 2346. Could be labeled "exalimalex" for "'there exists for all' implies 'for all there exists'". This proof is from excom 2169 and modal (B) on top of modalK logic. (Contributed by BJ, 12-Aug-2023.) The proof should not rely on df-nf 1785 or df-bj-nnf 34056, directly or indirectly. (Proof modification is discouraged.) |
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑) | ||
Theorem | bj-nnflemaa 34091 | One of four lemmas for nonfreeness: antecedent and consequent both expressed using universal quantifier. Note: this is bj-hbalt 34015. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)) | ||
Theorem | bj-nnflemee 34092 | One of four lemmas for nonfreeness: antecedent and consequent both expressed using existential quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥(∃𝑦𝜑 → 𝜑) → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)) | ||
Theorem | bj-nnflemae 34093 | One of four lemmas for nonfreeness: antecedent expressed with universal quantifier and consequent expressed with existential quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑)) | ||
Theorem | bj-nnflemea 34094 | One of four lemmas for nonfreeness: antecedent expressed with existential quantifier and consequent expressed with universal quantifier. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥(∃𝑦𝜑 → 𝜑) → (∃𝑦∀𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | bj-nnfalt 34095 | See nfal 2342 and bj-nfalt 34045. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∀𝑥𝜑) | ||
Theorem | bj-nnfext 34096 | See nfex 2343 and bj-nfext 34046. (Contributed by BJ, 12-Aug-2023.) (Proof modification is discouraged.) |
⊢ (∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑) | ||
Theorem | bj-stdpc5t 34097 | Alias of bj-nnf-alrim 34084 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2208 proved from modalK (obsoleting stdpc5v 1939). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 34084 instead. (New usaged is discouraged.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-19.21t 34098 | Statement 19.21t 2206 proved from modalK (obsoleting 19.21v 1940). (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))) | ||
Theorem | bj-19.23t 34099 | Statement 19.23t 2210 proved from modalK (obsoleting 19.23v 1943). (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) | ||
Theorem | bj-19.36im 34100 | One direction of 19.36 2232 from the same axioms as 19.36imv 1946. (Contributed by BJ, 2-Dec-2023.) |
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |