Definition df-bj-nnf

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 .

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

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	$$⊢Ⅎ\text{'}x\phi \leftrightarrow \left(\left(\exists x\phi \to \phi \right)\wedge \left(\phi \to \forall x\phi \right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2	1 0	wnnf	$$wffℲ\text{'}x\phi$$
3	1 0	wex	$$wff\exists x\phi$$
4	3 1	wi	$$wff\left(\exists x\phi \to \phi \right)$$
5	1 0	wal	$$wff\forall x\phi$$
6	1 5	wi	$$wff\left(\phi \to \forall x\phi \right)$$
7	4 6	wa	$$wff\left(\left(\exists x\phi \to \phi \right)\wedge \left(\phi \to \forall x\phi \right)\right)$$
8	2 7	wb	$$wff\left(Ⅎ\text{'}x\phi \leftrightarrow \left(\left(\exists x\phi \to \phi \right)\wedge \left(\phi \to \forall x\phi \right)\right)\right)$$