2

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!

CodeKingPlusPlus
  • 7,342
  • 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).

     – Willemien Sep 13 '13 at 22:10

2 Answers2

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.

Peter Smith
  • 54,743
1

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.

sean
  • 200