First Order Logic - unsatisfiable set of formulas

Question

I know what is an unsatisfiable set of formulas in first order logic and I'm studying how to prove the unsatisfiability.

What I don't understand, I'm sorry a think as an engineer, is what get in practice when I prove that set of formulas is unsatisfiable. Can you intuitively explain this to me ?

Answer 1

To be unsatisfiable means the impossibility to find an interpretation that simultaneously satisfies all the formulas of the set.

A typical case will be the set:

$\{ p(x), \lnot p(x) \}$.

There is no way to find a domain $D$ and an object $d \in D$ and a "property" $P^D$ of objects of the domain such that:

both $P^D$ holds of $d$ and $P^D$ does not hold of $d$.

---

There are proof procedures for unsatisfiability: see Resolution.

Answer 2

Intuitively, proving that a set of formulas is unsatisfiable gives you something like the formal version of the engineering maxim: "Cheap. Fast. Reliable. Pick two."

Is this what you were asking?