Description: Definition of the nonfreeness quantifier. The formula F// x ph has the intended meaning that the variable x is semantically nonfree in the formula ph . 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 ( x , ph ) (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 |- F// x x = x , that is, x is semantically (but not syntactically) nonfree in the formula x = x ; for the second, note that x is syntactically nonfree in the formula A. x x = x 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 F// x ph is very close to the non-occurrence condition DV ( x , ph ) .
Let S be a Metamath system with the FOL-syntax of (i)set.mm, containing intuitionistic positive propositional calculus and ax-5 and ax5e .
Theorem 1. If the scheme
( F// x ph & PHI_1 & ... & PHI_n => PHI_0, DV)
is provable in S, then so is the scheme
(PHI_1 & ... & PHI_n => PHI_0, DV u. { { x , ph } } ) .
Proof: By bj-nnfv , we can prove ( F// x ph , { { x , ph } } ) , from which the theorem follows. QED
Theorem 2. Suppose that S also contains (the FOL version of) modal logic KB and commutation of quantifiers alcom and excom (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 , ax5e , ax5ea . If the scheme
(PHI_1 & ... & PHI_n => PHI_0, DV)
is provable in S, then so is the scheme
( F// x ph & PHI_1 & ... & PHI_n => PHI_0, DV \ { { x , ph } } ) .
More precisely, if S contains modal 45 and if the variables quantified over in PHI_0, ..., PHI_n are among x_1, ..., x_m, then the scheme
(PHI_1 & ... & PHI_n => (antecedent -> PHI_0), DV \ { { x , ph } } )
is provable in S, where the antecedent is a finite conjunction of formulas of the form A. x_i1 ... A. x_ip F// x ph where the x_ij's are among the x_i's.
Lemma: If x e/ OC(PHI), then S proves the scheme
( F// x ph => F// x PHI, { { x , a } | a e. OC(PHI) \ { ph } } ) .
More precisely, if the variables quantified over in PHI are among x_1, ..., x_m, then
((antecedent -> F// x PHI), { { x , a } | a e. OC(PHI) \ { ph } } )
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 we can assume that PHI contains only primitive (as opposed to defined) symbols. For the base case, atomic formulas are either ph , in which case the scheme to prove is an instance of id , or have variables all in OC(PHI) \ { ph } , so ( F// x PHI, { { x , a } | a e. OC(PHI) \ { ph } } ) by bj-nnfv , hence ( ( F// x ph -> F// x PHI), { { x , a } | a e. OC(PHI) \ { ph } } ) by a1i . 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 x does not occur. We use respectively bj-nnfim , bj-nnfnt , bj-nnfan , bj-nnfor , bj-nnfbit , bj-nnfalt , bj-nnfext . For instance, in the implication case, if we have by induction hypothesis
( ( A. x_1 ... A. x_m F// x ph -> F// x PHI), { { x , a } | a e. OC(PHI) \ { ph } } ) and ( ( A. y_1 ... A. y_n F// x ph -> F// x PSI), { { x , a } | a e. OC(PSI) \ { ph } } ) ,
then bj-nnfim yields
( ( ( A. x_1 ... A. x_m F// x ph /\ A. y_1 ... A. y_n F// x ph ) -> F// x (PHI -> PSI)), { { x , a } | a e. OC(PHI -> PSI) \ { ph } } )
and similarly for antecedents which are conjunctions as in the statement of the lemma.
In the universal quantification case, say quantification over y , if we have by induction hypothesis
( ( A. x_1 ... A. x_m F// x ph -> F// x PHI), { { x , a } | a e. OC(PHI) \ { ph } } ) ,
then bj-nnfalt yields
( ( A. y A. x_1 ... A. x_m F// x ph -> F// x A. y PHI), { { x , a } | a e. OC( A. y PHI) \ { ph } } )
and similarly for antecedents which are conjunctions as in the statement of the lemma.
Note bj-nnfalt and bj-nnfext are proved from positive propositional calculus with alcom and excom (possibly weakened by a DV condition on the quantifying variables), and modalB (via bj-19.12 ). QED
Proof of the theorem: Consider a proof of that scheme directly from the axioms. Consider a step where a DV condition involving ph is used. By hypothesis, that step is an instance of ax-5 or ax5e or ax5ea . It has the form (PSI -> A. x PSI) where PSI has the form of the lemma and the DV conditions of the proof contain { { x , a } | a e. OC(PSI) } . Therefore, one has
( ( A. x_1 ... A. x_m F// x ph -> F// x PSI), { { x , a } | a e. OC(PSI) \ { ph } } )
for appropriate x_i's, and by bj-nnfa we obtain
( ( A. x_1 ... A. x_m F// x ph -> (PSI -> A. x PSI)), { { x , a } | a e. OC(PSI) \ { ph } } )
and similarly for antecedents which are conjunctions as in the statement of the theorem. Similarly if the step is using ax5e or ax5ea , we would use bj-nnfe or bj-nnfea 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 , and when the step uses ax-gen , by bj-nnf-alrim and bj-nnfa1 (which requires modal 45). The condition DV ( x , ph ) 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 . QED
Compared with df-nf , the present definition is stricter on positive propositional calculus ( bj-nnfnfTEMP ) and equivalent on core FOL plus sp ( bj-nfnnfTEMP ). While being stricter, it still holds for non-occurring variables ( bj-nnfv ), 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 ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) /\ A. x ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) /\ A. x A. x ... 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 to work with), and also not to have redundant conjuncts when full metacomplete FOL= is developed.
(Contributed by BJ, 28-Jul-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-bj-nnf | ⊢ ( Ⅎ' 𝑥 𝜑 ↔ ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | wph | ⊢ 𝜑 | |
| 2 | 1 0 | wnnf | ⊢ Ⅎ' 𝑥 𝜑 |
| 3 | 1 0 | wex | ⊢ ∃ 𝑥 𝜑 |
| 4 | 3 1 | wi | ⊢ ( ∃ 𝑥 𝜑 → 𝜑 ) |
| 5 | 1 0 | wal | ⊢ ∀ 𝑥 𝜑 |
| 6 | 1 5 | wi | ⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) |
| 7 | 4 6 | wa | ⊢ ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) |
| 8 | 2 7 | wb | ⊢ ( Ⅎ' 𝑥 𝜑 ↔ ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜑 → ∀ 𝑥 𝜑 ) ) ) |