for all substitutions f (i.e., functions from atoms to formulas) and for all formulas φ: if φ is N-valid then f(φ) is N-valid.For example, the formula p→¬¬p is N-valid, but if we plug in q∧q for p we get (q∧q)→¬¬(q∧q), which turns out to be N-invalid. Although N does not validate uniform substitution in its full generality, N is closed under some classes of substitutions:
- renamings of atoms
- double negating atoms
- substituting N-validities for atoms,
- Is N′ consistent? (We can vary the notion of consistency here, thereby precisifying the question.)
- Does N′ have a suitably straightforward dialogical characterization?