Entailment

Informal:
Which formulas BB are true when AA is true?

Formal:
For all Assignments φ\varphi which satisfy AA, do these assignments also satisfy BB ?

AA entails/models BB:

A⊨BA \models B

Entailment is the ideal outcome of reasoning.

Deduction is the process of an actual computer trying to reason about entailment.

A⊨B⟺(A∪{¬B})⊨⊥.A \models B \Longleftrightarrow(A \cup\{\neg B\}) \models \perp .

Examples

Modus Ponens