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

<ul>
<li><p>If your system is sound, and you can prove $\lnot \phi$, then you have a nonderivability result, of course.</p></li>
<li><p>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. </p></li>
<li><p>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$. </p></li>
<li><p>Sometimes you can get away with a translation into another logic, and show that derivability over here implies a known nonderivability result over there. </p></li>
<li><p>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.)</p></li>
<li><p>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.)</p></li>
</ul>

CC BY-SA 2.5
2010-10-26T19:56:01.873Z
Well, if I remember correctly, normalization for $F$ can be proven in $PA^2$, so no need for replacement.
Kaveh
CC BY-SA 2.5
2010-10-26T21:42:53.547Z
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.
Neel Krishnaswami
CC BY-SA 2.5
2010-10-27T01:10:32.850Z
Thanks, I now see what you meant by "things like normalization of System F". :)
Kaveh
CC BY-SA 2.5
2010-11-04T10:23:02.517Z
@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...
Charles Stewart
CC BY-SA 2.5
2010-11-04T11:10:22.840Z
@Charles: You are right, my carelessness, the relation is similar to the one between PA and Godel's T.
Kaveh
CC BY-SA 2.5
2010-11-04T11:56:14.407Z
@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.
Neel Krishnaswami
CC BY-SA 2.5
2010-10-26T14:41:16.540Z
2010-10-26T14:41:16.540Z
Neel Krishnaswami
<p>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.</p>

<p>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.</p>

<p>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?</p>

<p>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.</p>

CC BY-SA 2.5
2010-10-26T19:48:32.067Z
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?
Kaveh
CC BY-SA 2.5
2010-10-26T19:59:59.663Z
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".
Dave Clarke
CC BY-SA 2.5
2010-10-26T20:15:33.557Z
Thanks for the clarification, my mind goes to first-order logic by default when I read classical logic. :)
Kaveh
<lo.logic>
Techniques for showing non-derivability in logics and other formal proof systems
Dave Clarke
# Techniques for showing non-derivability in logics and other formal proof systems

(Asked by: username_0 on 2010-10-26)

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.

**Tags:** lo.logic

> **Comments:**
> **username_1**: 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?  
> **username_0**: 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".  
> **username_1**: Thanks for the clarification, my mind goes to first-order logic by default when I read classical logic. :)  

---

## 1 answers

### Answer by username_2 on 2010-10-26. Score: 15 | Accepted answer

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.)

> **Comments:**
> **username_1**: Well, if I remember correctly, normalization for $F$ can be proven in $PA^2$, so no need for replacement.  
> **username_2**: 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.  
> **username_1**: Thanks, I now see what you meant by "things like normalization of System F". :)  
> **username_3**: @username_1, @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...  
> **username_1**: @Charles: You are right, my carelessness, the relation is similar to the one between PA and Godel's T.  
> **username_2**: @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.  

---

