When checking whether a formula is a logical consequence of a set of premises, is it always necessary to check whether the set is satisfiable before?

Question

(Propositional logic problem):

Lets say that I have to decide whether this formula B really is a logical consequence of a set of premises {A, ¬A∨B}. Formally written: {A, ¬A∨B}⊧B . To find out, I can can reduce it to a problem of whether this formula is a tautology: (A∧(¬A∨B))⇒B. If this formula is a tautology, it means that formula B is a logical consequence of the premises. But it is possible that the premises are unsatisfiable (=they have no model). In that case anything could be a logical consequence.

I can also reduce the problem of whether B is a logical consequence of premises {A, ¬A∨B} to a problem of whether formula A∧(¬A∨B)∧¬B is unsatifiable. If the formula is unsatifiable it means that the formula B is a consequence. If the premises are unsatifiable the formula B will be a logical consequence and any other formula as well.

My question is: Is it always necessary to check whether a set of premises are satifiable in order to find out whether the formula really flows from these premises? In my textbook they never check whether premises are satifiable and just solve whether the problem reduced to previous problems is a tautology/contradiction. Because of my textbook I am confused if it is always really necessary (because it takes time to check if premises are satifiable).

Answer 1

The statement $\Gamma\vDash \phi$ has the meaning "in all models where the formulas in $\Gamma$ are true, also the formula $\phi$ is true."

If we want to show that $\Gamma\vDash\phi$, two methods seem reasonable:

1. If we show that $\phi$ is a direct consequence of (some of) the formulas in $\Gamma$, then we have proved that $\Gamma\vDash\phi$.
2. If we show that $\Gamma$ is insatisfiable, then we have also proved that $\Gamma\vDash\phi$, since vacuously $\phi$ will hold in any model where $\Gamma$ holds.

Showing that $\Gamma$ is satisfiable only proves that the second method will not work. So, although it is perhaps helpful to know that there exist models of $\Gamma$, it does not help in any way to show that $\Gamma\vDash\phi$.

---

In fact, showing that $\Gamma$ is satisfiable can be very hard or even impossible. Take for example a set $\Gamma$ that contains a lot of formulas, as well as $\phi$ itself. Then $\Gamma\vDash\phi$, since $\phi\vDash\phi$. But, finding out if $\Gamma$ is satisfiable will take a lot more effort.

In first-order logic, Gödel's Second Incompleteness Theorem shows that no set of formulas that is strong enough to formulate arithmetic in (for example the set of axioms for Peano Arithmetic) can prove its own consistency. What this means, is that such a set of axioms might be satisfiable, but it is impossible to prove it (within the system itself).

But even if we just look at propositional logic, the task of determining whether a set of formulas is satisfiable is computationally very difficult, and cannot be done efficiently (as far as we know). In fact, it is an archetype of a difficult problem, know as the SAT problem.