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 Sep 13 '13 at 22:10

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$ – CodeKingPlusPlus Aug 28 '13 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.


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.