Definition df-nf 1390

Description: Define the not-free predicate for wffs. This is read "𝑥 is not free in 𝜑". Not-free means that the value of 𝑥 cannot affect the value of 𝜑, e.g., any occurrence of 𝑥 in 𝜑 is effectively bound by a "for all" or something that expands to one (such as "there exists"). In particular, substitution for a variable not free in a wff does not affect its value (sbf 1700). An example of where this is used is stdpc5 1516. See nf2 1598 for an alternate definition which does not involve nested quantifiers on the same variable.

Not-free is a commonly used constraint, so it is useful to have a notation for it. Surprisingly, there is no common formal notation for it, so here we devise one. Our definition lets us work with the not-free notion within the logic itself rather than as a metalogical side condition.

To be precise, our definition really means "effectively not free," because it is slightly less restrictive than the usual textbook definition for not-free (which only considers syntactic freedom). For example, 𝑥 is effectively not free in the bare expression 𝑥 = 𝑥, even though 𝑥 would be considered free in the usual textbook definition, because the value of 𝑥 in the expression 𝑥 = 𝑥 cannot affect the truth of the expression (and thus substitution will not change the result). (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
df-nf	⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))

Detailed syntax breakdown of Definition df-nf

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wnf 1389	. 2 wff Ⅎ𝑥𝜑
4	1, 2	wal 1282	. . . 4 wff ∀𝑥𝜑
5	1, 4	wi 4	. . 3 wff (𝜑 → ∀𝑥𝜑)
6	5, 2	wal 1282	. 2 wff ∀𝑥(𝜑 → ∀𝑥𝜑)
7	3, 6	wb 103	1 wff (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))

This definition is referenced by:  nfi  1391  nfbii  1402  nfr  1451  nfd  1456  nfbidf  1472  nfnf1  1476  nford  1499  nfand  1500  nfnf  1509  nfalt  1510  19.21t  1514  nfimd  1517  19.9t  1573  nfnt  1586  nf2  1598  drnf1  1661  drnf2  1662  nfexd  1684  dveeq2or  1737  nfsb2or  1758  nfdv  1798  nfsbxy  1859  nfsbxyt  1860  sbcomxyyz  1887  sbnf2  1898  dvelimALT  1927  dvelimfv  1928  nfsb4t  1931  dvelimor  1935  oprabidlem  5556  bj-nfalt  10575