Differences
This shows you the differences between two versions of the page.
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//. |