Suppose I have a finite list of logical statements (would these be called axioms?) and for the sake of discussion say that there are 6 such statements. All statements are in the form of propositional logic.

From these statements I can prove other statements true. However, I wish to show that my list of logical statements is logically consistent. By logically consistent I mean that it is impossible to show a contradiction. For example, suppose I had 3 axioms:

\begin{gather} p \implies q \\ \lnot q \\ p \end{gather}

Clearly, this is logically inconsistent as I can prove $q$ is true while $\neg q$ is true, a contradiction.

  1. What is the standard method to prove something is logically consistent?
  2. Better yet, how can I get some kind of visualization of the logic (e.g., draw the logic via a graph $G=(V,E)$

EDIT: Could someone draw a sample truth table/tree/tableau of their choosing?

Thanks in advance!

  • $\begingroup$ You make it to simple - what are your rules of inference ? - are you using axioms or axiomscheme's? The standard way to prove a logic consistent is to prove that some formula is NOT provable, you can do this by using many-valued logics. Make some many valued truth tables for each connective: - so that all axioms are true(designated), - all rules of inference are truthpreserving and there is at least one formula that is not true (designated). $\endgroup$
    – Willemien
    Commented Sep 13, 2013 at 22:10

2 Answers 2


By the completeness theorem for classical propositional logic, $\varphi_1, \ldots, \varphi_6$ are syntactically consistent [entail no contradiction] if and only if they are semantically consistent [there is a valuation of their atoms on which there are all true].

So use a truth-table. Look for a line of the truth table assigning values to all the atoms in at least one of the $\varphi_i$ which makes all six propositions come out true. If there is one, they are consistent, if not, then not.

That's brute force. It would typically speed things up to use a propositional tableau ("truth-tree") if you know about those.

  • $\begingroup$ This is just what I am looking for! However, could you post a tiny example? I am not familiar with all of the language. $\endgroup$ Commented Aug 28, 2013 at 1:41

In propositional logic, a set of logical statements is consistent if there is a truth assignment that make them evaluate to true. Therefore, to check their consistency is a SAT problem. You can use DPLL algorithm to do. There are also powerful tools to check it, e.g. MiniSat.

I think what @PeterSmith mentioned is semantic tableau, which is favoured by mathematicians. But it is very very expensive in time and space comparing to DPLL. I do not aware of any SAT solver implementing semantic tableau.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .