Definition df-nf 1350

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 1660). An example of where this is used is stdpc5 1476. See nf2 1558 for an alternative 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 1349	. 2 wff Ⅎ𝑥𝜑
4	1, 2	wal 1241	. . . 4 wff ∀𝑥𝜑
5	1, 4	wi 4	. . 3 wff (𝜑 → ∀𝑥𝜑)
6	5, 2	wal 1241	. 2 wff ∀𝑥(𝜑 → ∀𝑥𝜑)
7	3, 6	wb 98	1 wff (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))

This definition is referenced by:  nfi  1351  nfbii  1362  nfr  1411  nfd  1416  nfbidf  1432  nfnf1  1436  nford  1459  nfand  1460  nfnf  1469  nfalt  1470  19.21t  1474  nfimd  1477  19.9t  1533  nfnt  1546  nf2  1558  drnf1  1621  drnf2  1622  nfexd  1644  dveeq2or  1697  nfsb2or  1718  nfdv  1757  nfsbxy  1818  nfsbxyt  1819  sbcomxyyz  1846  sbnf2  1857  dvelimALT  1886  dvelimfv  1887  nfsb4t  1890  dvelimor  1894  oprabidlem  5536  bj-nfalt  9904