This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
exam [2011/07/13 15:18] 131.246.18.253 [Core HOL] |
exam [2011/07/19 14:00] 131.246.18.253 [Calculi] |
||
---|---|---|---|
Line 51: | Line 51: | ||
:?: Why do we need calculi. | :?: Why do we need calculi. | ||
+ | * Basically, calculi are the tools we use to derive (and prove) theorems. Given a set of valid formulas and a sound calculus, new valid formulas (tautologies) can be derived. As far as I know, the semantic notion of "validity" corresponds to "provability" in the calculus, since it does not consider any notion of "truth". | ||
:?: Please explain the following properties: Soundness (Correctness), Completeness, ... | :?: Please explain the following properties: Soundness (Correctness), Completeness, ... | ||
+ | * A deductive system is sound if all provable formulas are valid. It is complete if all valid formulas are provable. | ||
+ | * Validity is a semantic property ($A \models B$), while provability a syntactic one ($A \vdash B$). So, in other words we have: | ||
+ | * Soundness: $A \vdash B \rightarrow A \models B$ | ||
+ | * Completeness: $A \models B \rightarrow A \vdash B$ | ||
+ | |||
:?: What are the advantages/disadvantages of the Hilbert calculus compared to the Gentzen calculus. | :?: What are the advantages/disadvantages of the Hilbert calculus compared to the Gentzen calculus. |