Differences

This shows you the differences between two versions of the page.

--- sav08:propositional_logic_syntax [2008/03/10 16:30]
vkuncak
+++ sav08:propositional_logic_syntax [2008/03/18 11:10]
vkuncak
@@ Line 6: / Line 6: @@
    F ::= V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F)
 \]
-We denote the set of all propositional formulas given by the above grammar by ${\cal F}$.  This is a countable set: we can order all formulas in this set in a sequence (for example, by writing them down in binary alphabet and sortign the resulting strings alphabetically).
+We denote the set of all propositional formulas given by the above grammar by ${\cal F}$.  This is a countable set: we can order all formulas in this set in a sequence (for example, by writing them down in binary alphabet and sorting the resulting strings alphabetically).
 Omitting parantheses:
-  * $\land$, $\lor$ commutative
+  * $\land$, $\lor$ associative
   * priorities, from strongest-binding: $(\lnot)\ ;\ (\land, \lor)\ ;\ (\rightarrow, \leftrightarrow)$
 When in doubt, use parenthesis.
@@ Line 15: / Line 15: @@
 Notation: when we write $F_1 \equiv F_2$ this means that $F_1$ and $F_2$ are identical formulas (with identical syntax trees).  For example, $p \land q \equiv p \land q$, but it is not the case that $p \land q \equiv q \land p$.
-In [[Isabelle theorem prover]] we use this ++++ASCII notation for Propositional Logic|
+In [[Isabelle theorem prover]] we use this ++++ASCII notation for First-Order Logic|
 \[
 \begin{array}{c|c}
@@ Line 38: / Line 38: @@
 \[\begin{array}{l}
   FV(p) = \{ p \}, \mbox{ for } p \in V \\
+  FV(\lnot F) = FV(F) \\
   FV(F_1 \land F_2) = FV(F_1) \cup FV(F_2) \\
   FV(F_1 \lor F_2) = FV(F_1) \cup FV(F_2) \\
-  FV(\lnot F) = FV(F) \\
   FV(F_1 \rightarrow F_2) = FV(F_1) \cup FV(F_2) \\
   FV(F_1 \leftrightarrow F_2) = FV(F_1) \cup FV(F_2) \\
 \end{array}\]
+If $FV(F) = \emptyset$, we call $F$ a //ground formula//.