We call a set of formulas $\Sigma$ of a language $L$ consistent if there is no $\varphi$ in $L$ such that $\Sigma \vdash \varphi$ and $\Sigma \vdash \lnot \varphi$.

Apparently, an equivalent formulation is the following:

A set $\Sigma$ of formulas of $L$ is consistent iff $\Sigma \not\vdash \varphi$ for some sentence $\varphi$ of $L$.

The $\implies$ direction is clear: if we can prove all sentences then we can prove both $\varphi$ and $\lnot \varphi$ so that $\Sigma$ is inconsistent.

But I don't immediately see how to prove $\Longleftarrow$. Can someone explain this to me? Thanks!

  • $\begingroup$ Hm ... seems to depend on the conclusion rules you are using, but I'd say something along the lines $\Sigma \vdash \varphi, \neg \varphi$ gives $\Sigma \vdash \varphi \land\neg\varphi$ and by $\Sigma \vdash(\varphi \land \neg\varphi \to \psi)$ (logical axiom) we have by MP $\Sigma \vdash \psi$. $\endgroup$ – martini Nov 19 '12 at 10:48

Assume that $\Sigma$ is consistent then it cannot prove $\varphi\land\lnot\varphi$. Therefore there exists a sentence which it does not prove.

Assume that $\Sigma$ is inconsistent then it proves everything (using the principle of explosion). Therefore there is no sentence it does not prove.

  • $\begingroup$ @Matt: I know you do. :-) I like writing long answers, though. ;-) $\endgroup$ – Asaf Karagila Nov 22 '12 at 15:23
  • $\begingroup$ I know you do. ${}$ $\endgroup$ – Rudy the Reindeer Nov 22 '12 at 15:25
  • $\begingroup$ Perhaps you could consider writing a set theoretic novel, set 42 B.C. -- 42 before Cantor? $\endgroup$ – Rudy the Reindeer Nov 22 '12 at 15:26
  • $\begingroup$ @Matt: Ha. I might take you on that. It will take me a "non-standard integer"-many days to write such novel, though. $\endgroup$ – Asaf Karagila Nov 22 '12 at 15:28

The characterizations are not equivalent in general. Take the most trivial case: suppose $L$ is a negation-free language. Then vacuously, the set $\Sigma$ of all $L$-formulae is consistent in the first sense, but not in the second sense.

However, in a language with negation and in the presence of ex contradictione quodlibet (the rule that from $\varphi$ and $\neg\varphi$ you can derive any $\psi$), the two characterizations become co-extensional.

  • 1
    $\begingroup$ I am fairly certain this is in the context of classical FOL. $\endgroup$ – Asaf Karagila Nov 19 '12 at 11:05
  • 1
    $\begingroup$ @AsafKaragila Sure thing, they come to the same in FOL. But it was important to Post, to whom we owe the second definition, that it applies more widely. So I thought it was worth emphasizing that, in a more general setting, the definitions peel apart. $\endgroup$ – Peter Smith Nov 19 '12 at 11:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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