LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:proof_theory_for_propositional_logic [2008/03/11 16:38]
vkuncak
sav08:proof_theory_for_propositional_logic [2015/04/21 17:30] (current)
Line 15: Line 15:
  
 System $S$ is sound if for every formula $F$, System $S$ is sound if for every formula $F$,
-\[+\begin{equation*}
     (\vdash_S F) \rightarrow (\models F)     (\vdash_S F) \rightarrow (\models F)
-\]+\end{equation*}
 We can only prove true formulas. We can only prove true formulas.
  
Line 23: Line 23:
  
 System $S$ is complete if for every formula $F$, System $S$ is complete if for every formula $F$,
-\[+\begin{equation*}
     (\models F) \rightarrow (\vdash F)     (\models F) \rightarrow (\vdash F)
-\]+\end{equation*}
 We can prove all valid formulas. We can prove all valid formulas.
  
Line 35: Line 35:
  
 **Rule 1:** Case analysis rule: **Rule 1:** Case analysis rule:
-\[+\begin{equation*}
     \frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}}     \frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}}
          {P}          {P}
-\]+\end{equation*}
  
 **Rule 2:** Evaluation rule: derive $P$ if $P$ has no variables and it evaluates to //true//. **Rule 2:** Evaluation rule: derive $P$ if $P$ has no variables and it evaluates to //true//.