LARA

Differences

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

Link to this comparison view

sav08:propositional_logic_syntax [2009/04/08 18:34]
philippe.suter
sav08:propositional_logic_syntax [2015/04/21 17:30]
Line 1: Line 1:
-====== Propositional Logic Syntax ====== 
  
-Let $V$ be a [[countable set]] of //​propositional variables//,​ denoted by non-terminal //​V//​. ​ The context-free grammar of propositional logic formulas ${\cal F}$ is the following: 
- 
-\[ 
-   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 [[:Notes on Context-Free Grammars|context-free grammar]] by ${\cal F}$.  Each propositional formula is a finite sequence of symbols, given by the above context-free grammar. ​ The set ${\cal F}$ 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 parentheses:​ 
-  * $\land$, $\lor$ associative 
-  * priorities, from strongest-binding:​ $(\lnot)\ ;\ (\land, \lor)\ ;\ (\rightarrow,​ \leftrightarrow)$ 
-When in doubt, use parenthesis. 
- 
-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| 
-\[ 
-\begin{array}{c|c} ​ 
-\mbox{math} & \mbox{Isabelle} \\ \hline 
-\land & \verb!&​! \\ 
-\lor  & \verb!|! \\ 
-\lnot & \verb!~! \\ 
-\rightarrow & \verb!-->​! \\ 
-\leftrightarrow & \verb!=! \\ 
-{\it true} & \verb!True! \\ 
-{\it false} & \verb!False! \\ 
-\end{array} 
-\] 
-Rendering and input in math notation is also possible using ProofGeneral or Eclipse. 
- 
-Type of propositional formulas is //bool//. 
-++++ 
- 
-Usually we work with syntax trees, as in [[Homework01#​Problem_3|Problem 3 in Homework 1]]. 
- 
-$FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows: 
-\[\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(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//.