Definition df-nf 1402

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 1714). An example of where this is used is stdpc5 1528. See nf2 1610 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 1401	. 2 wff Ⅎ𝑥𝜑
4	1, 2	wal 1294	. . . 4 wff ∀𝑥𝜑
5	1, 4	wi 4	. . 3 wff (𝜑 → ∀𝑥𝜑)
6	5, 2	wal 1294	. 2 wff ∀𝑥(𝜑 → ∀𝑥𝜑)
7	3, 6	wb 104	1 wff (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))

This definition is referenced by:  nfi  1403  nfbii  1414  nfr  1463  nfd  1468  nfbidf  1484  nfnf1  1488  nford  1511  nfand  1512  nfnf  1521  nfalt  1522  19.21t  1526  nfimd  1529  19.9t  1585  nfnt  1598  nf2  1610  drnf1  1675  drnf2  1676  nfexd  1698  dveeq2or  1751  nfsb2or  1772  nfdv  1812  nfsbxy  1873  nfsbxyt  1874  sbcomxyyz  1901  sbnf2  1912  dvelimALT  1941  dvelimfv  1942  nfsb4t  1945  dvelimor  1949  oprabidlem  5718  bj-nfalt  12377