Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Definition of consistency is: A set of formulas ⊆ WFF is consistent iff there is no A ∈ WFF such that Σ ⊢ A and Σ ⊢ (¬A).

Say you have a set of propositions statements (i.e. $A \lor B \rightarrow C$, etc.) and let's call this "Set1".

I know that to prove that set is inconsistent, you find an "A" such that Set1 ⊢ A and Set1 ⊢ (¬A).

But what are the steps to prove that the set is consistent?

share|improve this question
add comment

2 Answers 2

up vote 3 down vote accepted

The most useful technique for proving $\Sigma$ consistent is to provide a model for it -- that is, an interpretation of the primitive symbols in it that makes every formula in $\Sigma$ true. If the logic is sound, it cannot conclude something false from true, so whenever $\Sigma\vdash A$, then $A$ will also be true in that model. Since $A$ and $\neg A$ cannot both be true in the same interpretation, this means that $\Sigma$ is consistent.

If the logic is complete then every consistent $\Sigma$ will have a model. Usual propositional logic and first-order logic are both complete.

In the case of propositional logic, an interpretation is simply a table that shows which propositional letters we take to be true and which ones we take to be false. If $\Sigma$ contains finitely many different propositional letters, we can in principle try all interpretations until we find one that is a model.

The situation is less nice for first-order logic. It is still true that every consistent $\Sigma$ has a model, but the model may need to contain infinitely many elements for the quantifiers to range over, and is not necessarily easy to describe. Even if we have a description for a model, proving that it is actually a model can be very difficult -- in some sense it can be exactly as difficult as proving the $\Sigma$ is consistent.

And due to Gödel's incompleteness theorems, we know that are first-order theories that are consistent but cannot be proved to be consistent (from any given meta-system we wish to conduct this proof in).

share|improve this answer
add comment

If you are working with propositional logic (I assume it from the text of your answer) and $Set_1$ is a finite set of formulas (like your : $A \lor B \rightarrow C$), you can use the Method of analytic tableaux :

the semantic tableau (or truth tree) is it is a decision procedure for sentential and related logics.

In case $Set_1$ is consistent, it gives you a model of it (because $Set_1$ is consistent iff it is satisfiable).

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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