20
$\begingroup$

In proof systems for classical propositional logic if one want to show that a certain formula $\psi$ is not derivable one simply shows that $\neg\psi$ can be derived (although other techniques certainly are possible). Non-derivability follows essentially from the soundness and completeness of the proof system.

Unfortunately for non-classical logics and more exotic proof systems (such as the rules underlying operational semantics) no such direct technique exists. This could be because the non-derivability of $\psi$ does not imply that $\neg\psi$ is derivable, as is the case with intuitionistic logics, or simply that no notion of negation exists.

My question is given a proof system $(\mathcal{L},\vdash)$, where $\vdash\;\subseteq\mathcal{L}^*\times\mathcal{L}$, (and presumably its semantics), what techniques exist to show non-derivability?

The proof systems of interest could include operational semantics of programming languages, Hoare logics, type systems, a non-classical logic, or inference rules for what-have-you.

Improve this question
$\endgroup$
3
  • $\begingroup$ Dave, I think there is a typo in the question, to show that $\varphi$ is not derivable we don't show that $\lnot \varphi$ is derivable, we just show that it is consistent, and this is only based on consistency of classical logic. If the logic is first-order classical logic, then there are sentences that we can neither prove nor refute (unless we are talking about a complete theory). Or am I misreading your question? $\endgroup$
    – Kaveh
    Commented Oct 26, 2010 at 19:48
  • $\begingroup$ I changed it to classical propositional logic. The question asks for any technique apart from proving the negation, as many formal system (collections of axioms and inference rules) do not have negation, or in fact may not even look like "logic". $\endgroup$
    – Dave Clarke
    Commented Oct 26, 2010 at 19:59
  • $\begingroup$ Thanks for the clarification, my mind goes to first-order logic by default when I read classical logic. :) $\endgroup$
    – Kaveh
    Commented Oct 26, 2010 at 20:15

1 Answer 1

Reset to default
15
$\begingroup$

IME, the following list is easiest to hardest (of course, it's also least to most powerful):

  • If your system is sound, and you can prove $\lnot \phi$, then you have a nonderivability result, of course.

  • If you have a lattice-theoretic semantics for your logic, relative to which all your proof rules are valid, then if the meaning of a proposition is not the topmost element of the lattice, then it is not a derivable proposition.

  • If you know that your logic is complete with respect to a class of models, check to see if there is a particular model in that class which invalidates $\phi$.

  • Sometimes you can get away with a translation into another logic, and show that derivability over here implies a known nonderivability result over there.

  • If you have a natural deduction or sequent calculus, check to see if there is a cut-elimination result known, or if you can prove one. If there is, then you can often exploit the subformula property to give simple inductive arguments about nonderivability. (Eg., consistency via cut-elimination is just the statement that there are no cut-free proofs of false, and so if all cuts can be eliminated then there are no inconsistencies.)

  • If nothing else works, then you can often show consistency/nonderivability results via a logical relations argument. This is the big gun, which works when nothing else does -- in set-theoretic terms, it boils down to a use of the axiom of Replacement, which lets you show huge sets are well-ordered. (This is why you can use it to prove things like normalization of System F.)

Improve this answer
$\endgroup$
6
  • $\begingroup$ Well, if I remember correctly, normalization for $F$ can be proven in $PA^2$, so no need for replacement. $\endgroup$
    – Kaveh
    Commented Oct 26, 2010 at 19:56
  • 3
    $\begingroup$ If you just assume second-order Peano arithmetic, you can prove F, but not stronger systems (eg, $F^2$), but logical relations proofs continue to scale up to these systems. When you do a proof via logical relations, you are secretly building a little sheaf model, which viewed as a topos can interpret a fairly strong set theory (IIRC, bounded ZF) including replacement. $\endgroup$
    – Neel Krishnaswami
    Commented Oct 26, 2010 at 21:42
  • $\begingroup$ Thanks, I now see what you meant by "things like normalization of System F". :) $\endgroup$
    – Kaveh
    Commented Oct 27, 2010 at 1:10
  • 1
    $\begingroup$ @Kaveh, @Neel: Strong normalisation of system F is not a theorem of PA2, instead it is equivalent over PA to the consistency of PA2. Rather, strong normalisation for all terms of rank n (rank being the measure of the maxiumum depth of nsted type quantifiers) can be proven using ACA-n. I like talk of building sheaf models in secret... $\endgroup$
    – Charles Stewart
    Commented Nov 4, 2010 at 10:23
  • 1
    $\begingroup$ @Charles: I learned about this idea from some papers of Jean Gallier, which are surprisingly under-cited. Somewhat perversely, this fancy view helped me understand Mitchell & Scedrov's simpler account. $\endgroup$
    – Neel Krishnaswami
    Commented Nov 4, 2010 at 11:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.