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]]