Differences
This shows you the differences between two versions of the page.
sav08:propositional_logic_semantics [2008/03/11 14:51] vkuncak |
sav08:propositional_logic_semantics [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Propositional Logic Semantics ====== | ||
- | |||
- | Recall [[homework01]]. | ||
- | |||
- | Let ${\cal B} = \{{\it true}, {\it false}\}$. | ||
- | |||
- | **Interpretation** for propositional logic is a function $I : V \to {\cal B}$. | ||
- | |||
- | We next define evaluation function: | ||
- | \[ | ||
- | e : F \to (I \to {\cal B}) | ||
- | \] | ||
- | ++++by recursion on formula syntax tree:| | ||
- | \[\begin{array}{l} | ||
- | e(p)(I) = I(p), \mbox{ for } p \in V \\ | ||
- | e({"\lnot "}\> F)(I) = \lnot (e(F)(I)) \\ | ||
- | e(F_1\> {"\land "}\> F_2)(I) = e(F_1)(I) \land e(F_2)(I) \\ | ||
- | e(F_1\> {"\lor "}\> F_2)(I) = e(F_1)(I) \lor e(F_2)(I) \\ | ||
- | e(F_1\> {"\rightarrow "}\> F_2)(I) = (e(F_1)(I) \rightarrow e(F_2)(I)) \\ | ||
- | e(F_1\> {"\leftrightarrow "}\> F_2)(I) = (e(F_1)(I) \leftrightarrow e(F_2)(I)) | ||
- | \end{array} | ||
- | \] | ||
- | |||
- | We wrote symbols like $" \land "$ on left in quotes to emphasize that those are syntactic entities, in contrast to symbols like $\land$ on right-hand side that denote propositional operations given by truth tables (stated in [[Propositional Logic Informally]]). | ||
- | ++++ | ||
- | |||
- | This definition follows one in the formula evaluator in [[homework01]]. | ||
- | |||
- | |||
- | We denote $e(F)(I) = {\it true}$ by | ||
- | \[ | ||
- | I \models F | ||
- | \] | ||
- | and denote $e(F)(I) = {\it false}$ by | ||
- | \[ | ||
- | I \not\models F | ||
- | \] | ||
- | |||
- | ===== Validity and Satisfiability ===== | ||
- | |||
- | Formula is valid iff $\forall I. I \models F$. We write this simply | ||
- | \[ | ||
- | \models F | ||
- | \] | ||
- | |||
- | Formula is satisfiable iff $\exists I. I \models F$ | ||
- | |||
- | Formula is contradictory iff $\forall I. I \not\models F$ | ||
- | |||
- | [[Satisfiability of Sets of Formulas]] | ||