Proving and Modeling Logical Consistence 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.


*

*What is the standard method to prove something is logically consistent?

*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!
 A: 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.
A: 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.
