ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-nf Unicode version

Definition df-nf 1422
Description: Define the not-free predicate for wffs. This is read " x is not free in  ph". Not-free means that the value of  x cannot affect the value of  ph, e.g., any occurrence of  x in  ph 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 1735). An example of where this is used is stdpc5 1548. See nf2 1631 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,  x is effectively not free in the bare expression  x  =  x, even though  x would be considered free in the usual textbook definition, because the value of  x in the expression  x  =  x 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  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )

Detailed syntax breakdown of Definition df-nf
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
31, 2wnf 1421 . 2  wff  F/ x ph
41, 2wal 1314 . . . 4  wff  A. x ph
51, 4wi 4 . . 3  wff  ( ph  ->  A. x ph )
65, 2wal 1314 . 2  wff  A. x
( ph  ->  A. x ph )
73, 6wb 104 1  wff  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
Colors of variables: wff set class
This definition is referenced by:  nfi  1423  nfbii  1434  nfr  1483  nfd  1488  nfbidf  1504  nfnf1  1508  nford  1531  nfand  1532  nfnf  1541  nfalt  1542  19.21t  1546  nfimd  1549  19.9t  1606  nfnt  1619  nf2  1631  drnf1  1696  drnf2  1697  nfexd  1719  dveeq2or  1772  nfsb2or  1793  nfdv  1833  nfsbxy  1895  nfsbxyt  1896  sbcomxyyz  1923  sbnf2  1934  dvelimALT  1963  dvelimfv  1964  nfsb4t  1967  dvelimor  1971  oprabidlem  5770  bj-nfalt  12867
  Copyright terms: Public domain W3C validator