# Denotational Semantics

### Example: language of propositional logic

**Syntactic Categories**
P in Prop (propositions)
F in Form (formulae)

**Syntax BNF**
F ::= P | ~ F | F ==> F

**Value Domains**
Bool = { true, false } boolean logic values
rho in Assign = P --> Bool truth assignments

**Semantic Functions**
MM : Form --> Assign --> Bool
means MM mapps a formula and an assignment into a boolean value
the assignment tells the truth values of atomic propositions

**Semantic Equations**
MM [P] rho = rho(P)
MM [~F] rho = ~ MM [F] rho
MM [F1 ==> F2] rho = ~ MM [F1] rho v MM [F2] rho