This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
exam [2011/07/19 14:16] 131.246.18.253 [Calculi] |
exam [2011/08/02 15:29] (current) 188.107.127.174 [Core HOL] |
||
---|---|---|---|
Line 41: | Line 41: | ||
:?: How are the elements //True// and //False// introduced in HOL? | :?: 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? | :?: Why must all functions be total in Isabelle/HOL? |