Theory Entailment (First-Order Logic)

first-order-logic

Definition

Theory Entailment (First-Order Logic)

A theory entails a sentence , written , if for every structure :

where means for all .

Examples

Example

Does hold?

No. Let , , , and .

• , so .
• For every : if then , so .
• But , so .

The premises are true, the conclusion is false — therefore the entailment fails.

Example

Does hold?

Yes. In every structure , the domain is non-empty. If , then . Since , there is some , so .

Example

Does hold?

No. Let , , .

• For every : , so the antecedent is false and the implication is true. Hence .
• But , so .

The implication is vacuously true when nothing has ; that does not force anything to have .

Example

Given the three formulas below, show that none is entailed by the other two.

For each pair, provide a structure satisfying the two but not the third:

Without	Structure
reflexivity	, — symmetric and transitive, but is not related to itself
symmetry	, — reflexive and transitive (a partial order), but while
transitivity	, — reflexive and symmetric, but while

Each structure witnesses the independence of one axiom from the other two.