Propositional Logic
Syntax
The syntax of propositional logic defines the allowable sentences. The atomic sentences consist of a single proposition symbol. Each such symbol stands for a proposition that can be true or false. We use symbols that start with an uppercase letter and may contain other letters or subscripts.
There are two proposition symbols with fixed meanings: True is the always-true proposition and False is the always-false proposition.
Complex sentences are constructed from simpler sentences, using parentheses and operators called logical connectives:
- negation: If $\alpha$ is a sentence, $\neg\alpha$ is a sentence
- conjunction: If $\alpha$ and $\beta$ are sentences, $\alpha \land \beta$ is a sentence
- disjunction: If $\alpha$ and $\beta$ are sentences, $\alpha \lor \beta$ is a sentence
- implication: If $\alpha$ and $\beta$ are sentences, $\alpha \implies \beta$ is a sentence
- biconditional: If $\alpha$ and $\beta$ are sentences, $\alpha \iff \beta$ is a sentence
Validity and satisfiability
A sentence is valid if it is true in all models. Validity is connected to entailment via the deduction theorem: $KB \models \alpha$ if and only if $KB \implies \alpha$ is valid.
- A sentence is satisfiable if it is true in some model
- A sentence is unsatisfiable if it is true in no models
- Satisfiability is connected to entailment via the following (refutation or contradiction): $KB \models \alpha$ if and only if $KB \land \lnot\alpha$ is unsatisfiable
Inference procedures for propositional logic
Our goal now is to decide whether $KB \models \alpha$ for some sentence $\alpha$.