Differences

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

--- exam [2011/07/19 14:00] – [Calculi] 131.246.18.253
+++ exam [2011/08/02 15:29] (current) – [Core HOL] 188.107.127.174
@@ Line 41: / Line 41: @@
 :?: How are the elements //True// and //False// introduced in HOL?
-  * Since there should always be an infinite set in **U** whose elements and power sets are also fully contained in **U**, there's a guarantee that there will be a set with two elements and that set is going to represent the values //True// and //False// ((Did I miss something?))
+  * Since there should always be a distinguished infinite set in **U** whose elements and subsets are also fully contained in **U**, there's a guarantee that there will be a set with two elements (say the subset {0,1} of the infinite set) and that one is going to be mapped further on to the values //True// and //False// ((Did I miss something?))
 :?: Why must all functions be total in Isabelle/HOL?
@@ Line 56: / Line 56: @@
   * 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$
+      * Soundness: $A \vdash B \longrightarrow A \models B$
-      * Completeness: $A \models B \rightarrow A \vdash B$
+      * Completeness: $A \models B \longrightarrow A \vdash B$
 :?: What are the advantages/disadvantages of the Hilbert  calculus compared to the Gentzen calculus.