Definition df-nf 1514

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 1830). An example of where this is used is stdpc5 1637. See nf2 1720 for an alternate definition which does not involve nested quantifiers on the same variable.

Nonfreeness is a commonly used condition, 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 notion of nonfreeness 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 considers syntactic freedom). For example, 𝑥 is effectively not free in the expression 𝑥 = 𝑥 (even though 𝑥 is syntactically free in it, so would be considered "free" in the usual textbook definition) because the value of 𝑥 in the formula 𝑥 = 𝑥 does not affect the truth of that formula (and thus substitutions will not change the result), see nfequid 1754. (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 1513	. 2 wff Ⅎ𝑥𝜑
4	1, 2	wal 1400	. . . 4 wff ∀𝑥𝜑
5	1, 4	wi 4	. . 3 wff (𝜑 → ∀𝑥𝜑)
6	5, 2	wal 1400	. 2 wff ∀𝑥(𝜑 → ∀𝑥𝜑)
7	3, 6	wb 105	1 wff (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))

This definition is referenced by:  nfi  1515  nfbii  1526  nfr  1571  nfd  1576  nfbidf  1592  nfnf1  1597  nford  1620  nfand  1621  nfal  1629  nfnf  1630  nfalt  1631  19.21t  1635  nfimd  1638  19.9t  1695  nfnt  1708  nf2  1720  drnf1  1786  drnf2  1787  nfexd  1814  dveeq2or  1869  nfsb2or  1890  nfdv  1930  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  sbnf2  2041  dvelimALT  2070  dvelimfv  2071  nfsb4t  2074  dvelimor  2078  oprabidlem  6109  bj-nfalt  16709