Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-nnf | Structured version Visualization version GIF version |
Description: 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 (Ⅎ'𝑥𝜑 & PHI_{1} & ... & PHI_{n} ⇒ PHI_{0}, DV) is provable in S, then so is the scheme (PHI_{1} & ... & PHI_{n} ⇒ PHI_{0}, DV ∪ {{𝑥, 𝜑}}). Proof: By bj-nnfv 34159, 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 (PHI_{1} & ... & PHI_{n} ⇒ PHI_{0}, DV) is provable in S, then so is the scheme (Ⅎ'𝑥𝜑 & PHI_{1} & ... & PHI_{n} ⇒ PHI_{0}, DV ∖ {{𝑥, 𝜑}}). More precisely, if S contains modal 45 and if the variables quantified over in PHI_{0}, ..., PHI_{n} are among 𝑥_{1}, ..., 𝑥_{m}, then the scheme (PHI_{1} & ... & PHI_{n} ⇒ (antecedent → PHI_{0}), 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 34133 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 34159, 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 34151, bj-nnfnt 34145, bj-nnfan 34153, bj-nnfor 34155, bj-nnfbit 34157, bj-nnfalt 34171, bj-nnfext 34172. 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 34151 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 34171 yields ((∀𝑦∀𝑥_{1} ...∀𝑥_{m} Ⅎ'𝑥𝜑 → Ⅎ'𝑥∀𝑦 PHI), {{𝑥, 𝑎} ∣ 𝑎 ∈ OC(∀𝑦 PHI) ∖ {𝜑}}) and similarly for antecedents which are conjunctions as in the statement of the lemma. Note bj-nnfalt 34171 and bj-nnfext 34172 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 34166). 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 34136 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 34138 or bj-nnfea 34140 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 1797, by bj-nnf-alrim 34160 and bj-nnfa1 34164 (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 1786, the present definition is stricter on positive propositional calculus (bj-nnfnfTEMP 34143) and equivalent on core FOL plus sp 2183 (bj-nfnnfTEMP 34163). While being stricter, it still holds for non-occurring variables (bj-nnfv 34159), 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.) |
Ref | Expression |
---|---|
df-bj-nnf | ⊢ (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | wnnf 34131 | . 2 wff Ⅎ'𝑥𝜑 |
4 | 1, 2 | wex 1781 | . . . 4 wff ∃𝑥𝜑 |
5 | 4, 1 | wi 4 | . . 3 wff (∃𝑥𝜑 → 𝜑) |
6 | 1, 2 | wal 1536 | . . . 4 wff ∀𝑥𝜑 |
7 | 1, 6 | wi 4 | . . 3 wff (𝜑 → ∀𝑥𝜑) |
8 | 5, 7 | wa 399 | . 2 wff ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑)) |
9 | 3, 8 | wb 209 | 1 wff (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑 → 𝜑) ∧ (𝜑 → ∀𝑥𝜑))) |
Colors of variables: wff setvar class |
This definition is referenced by: bj-nnfbi 34133 bj-nnfa 34136 bj-nnfe 34138 bj-dfnnf2 34142 bj-wnfnf 34144 bj-nnfnt 34145 bj-nnftht 34146 bj-nnfim 34151 bj-nnfan 34153 bj-nnfand 34154 bj-nnfor 34155 bj-nnford 34156 bj-nnfv 34159 bj-dfnnf3 34162 bj-nnfa1 34164 bj-nnfe1 34165 bj-nnfalt 34171 bj-nnfext 34172 |
Copyright terms: Public domain | W3C validator |