Thursday, October 21, 2010

Is uniform substitution consistent with N?

One of N's curious features is its failure to validate uniform substitution: it is not true that
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 qq for p we get (qq)→¬¬(qq), 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
We have proofs that N is closed under these kinds of substitutions. We suspect further that N is closed under
  • substituting N-validities for atoms,
but we lack a proof for this third case. Question: how to respond to N's failure to validate uniform substitution? There are a number of possibilities that are worth investigating, but I want to explore one approach here: is N consistent with uniform substitution? More precisely, the question can be put this way. Let N′ be the closure of N under uniform substitution (i.e., N′ is the smallest set of formulas extending N that is closed under uniform substitution). We then ask:
  1. Is N′ consistent? (We can vary the notion of consistency here, thereby precisifying the question.)
  2. Does N′ have a suitably straightforward dialogical characterization?
We might further ask: what is it about Felscher's rule E (“Opponent must respond to the immediately prior assertion by Proponent”) that ensures closure under uniform substitution? Recall that our logic N is characterized simply by dropping the rule E from a ruleset known to characterize classical logic, which of course is closed under uniform substitution. We thus know that “Rule E” is not the answer to question 2 above that we seek!


  1. We, or at least I, also think that replacing atoms with their negations is also validity-preserving.

  2. Yes, that does seem to be valid, but a proof escapes me at the moment. Unlike the proofs of the two cases where we do have positive answers (renaming and double negating atoms), the approach used there (working directly with the game tree) doesn't immediately seem to work in the case of simply negating atoms, because the stance of the two players switches in a way that, at the moment, I'm not sure how to handle. For example, when dealing with double negating atoms, one can work directly with the dialogue tree and argue that, since Opponent gave up an atom in one game tree, he will assert the double negation, which Proponent can then attack, and he (may) give up the atom again. But if Opponent now does not give up an atom p but only ¬p, Proponent is in a different situation.

    Still, yes, the data does seem to suggest that this is another class of substitutions under which N is closed. I'm just kvetching about not knowing how to prove that.

  3. I also think there is a generalization of the double-negation substitution; I think not only is replacing atoms with their double-negations validity-preserving, but I suspect that replacing any arbitrary subformula with its double-negation is validity-preserving, and that the proof would be similar for the case of double-negating atoms.