Entailment (First-Order Logic)

first-order-logic

Definition

Entailment (First-Order Logic)

Let be formulas. Then entail , written

if for every structure and every variable assignment :

Intuition

Entailment is a claim about all possible worlds. You are saying: no matter how I interpret the symbols — no matter what domain I pick, what the constants name, what the predicates mean — whenever I make the premises true, the conclusion is forced to be true.

What "for every structure" means

A structure fixes what the symbols stand for: which set the variables range over, which object each constant names, which function each function symbol denotes. The definition says: no matter how you interpret the symbols, if the premises come out true, the conclusion is forced.

This is what makes entailment semantic rather than syntactic. You are not checking a proof — you are checking all possible meanings.

Entailment vs. implication

Entailment () lives outside the logic: it is a statement about formulas. Implication () lives inside the logic: it is a connective that builds a new formula.

All humans are mortal

Let and . Then

No structure can make Socrates human and all humans mortal without making Socrates mortal. The conclusion is forced.

Two structures, one entailment

Claim: .

Structure				Premise true?	Conclusion true?
				yes	yes
		apple		no	—

makes the premise true and the conclusion holds. makes the premise false, so it is irrelevant.

No structure makes the premise true and the conclusion false — that is what means.

Entailment vs. Satisfaction

The symbol is overloaded:

Left side	Meaning	Quantifier
	Satisfaction — is true under this structure and assignment	for one
	Entailment — must be true whenever the premises are	for all

Satisfaction checks one interpretation. Entailment checks them all.

Reductions

These equivalences connect the semantic notions:

Here “unsatisfiable” means unsatisfiable formula and “satisfiable” means satisfiable formula.

For finite :