一阶逻辑：归结原理与子句集不可满足性的悖论疑问

Great question—this is a super common sticking point when learning about resolution and model theory. Let’s break this down step by step to clear up the confusion, no paradox involved.

First, let’s align on core definitions to set the stage:

• Empty clause (□): A clause with no literals, logically equivalent to false (⊥). Why? A clause is a disjunction of literals, and an empty disjunction can never be true (think of it like how an empty conjunction is always true—opposite rules for empty logical operations).
• Unsatisfiable clause set: A set of clauses has no model—there’s no truth value assignment to variables that makes every clause in the set true.
• Logical entailment (⊨): A set S entails a formula φ (written S ⊨ φ) if every model that satisfies S also satisfies φ.

Now, let’s unpack your "paradox" concern:

You’re correct that deriving the empty clause from S means S ⊨ □ (S entails false). But here’s the key logical nuance that resolves the confusion:

For S ⊨ □ to hold, every model that satisfies S must satisfy □. But □ is false—no model can satisfy it.

The only way this entailment can be true is if there are no models that satisfy S in the first place. That’s exactly what "S is unsatisfiable" means!

This isn’t a paradox—it’s a case of vacuous truth. In logic, a universal statement ("all X are Y") is automatically true if there are no Xs. So "all models of S are models of □" is true precisely because there are no models of S to begin with. There’s no contradiction here—just a counterintuitive (but perfectly consistent) logical quirk.

Let’s use a simple concrete example to make this tangible:
Take the clause set S = {P, ¬P}. Resolving these two clauses gives us the empty clause. Unsurprisingly, S is unsatisfiable—no truth assignment can make both P and ¬P true. And S ⊨ □ holds because there are no models of S to violate the entailment rule.

To wrap up:

• Deriving the empty clause from S doesn’t create a paradox—it’s a direct proof that S has no models (i.e., is unsatisfiable).
• The "model of S must be a model of false" condition only sounds contradictory until you realize there are no such models, making the entailment vacuously true.

内容的提问来源于stack exchange，提问作者Qwerto