Definition df-nfree-D6.1 682

Description: Definition of Effective Non-Freeness (ENF), 'Ⅎ'. Read as "is not (effectively) free in".

When we say that '𝑥' is not (effectively) free in '𝜑', we are saying (in semantic terms) that the truth value of '𝜑' does not depend on '𝑥'. It is easy to understand this definition if we interpret the WFF '𝜑' as a function with a binary output. Then clearly '𝜑' does not depend on '𝑥' if and only if one of the following holds...

1. '𝜑' is true for all '𝑥' (holding all other variables constant).

2. '𝜑 is false for all '𝑥' (holding all other variables constant).

This definition states exactly this. Unlike the regular textbook definition of non-freeness, it does *not* state that '𝑥' cannot occur free in '𝜑'. If we set '𝜑 ≔ 𝑥 = 𝑥' then '𝑥' is still *effectively* free in '𝜑' since '𝑥 = 𝑥' is a tautology in our system. Effective non-freeness is thus slightly more general than the standard textbook definition, which we will call grammatical non-freeness (GNF). We could also call effective non-freeness *logical* non-freenness because, unlike grammatical non-freeness, it is bound to logical equivalence (see nfrleq-P6 687).

Assertion

Ref	Expression
df-nfree-D6.1	⊢ (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑))

Detailed syntax breakdown of Definition df-nfree-D6.1

Step	Hyp	Ref	Expression
1		wff-ph	. . 3 wff 𝜑
2		objvar-x	. . 3 objvar 𝑥
3	1, 2	wff-nfree 681	. 2 wff Ⅎ𝑥𝜑
4	1, 2	wff-forall 8	. . 3 wff ∀𝑥𝜑
5	1	wff-neg 9	. . . 4 wff ¬ 𝜑
6	5, 2	wff-forall 8	. . 3 wff ∀𝑥 ¬ 𝜑
7	4, 6	wff-or 144	. 2 wff (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑)
8	3, 7	wff-bi 104	1 wff (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑))

This definition is referenced by:  dfnfreealt-P6  683  nfrleq-P6  687  nfrneg-P6  688