# IRC log for #isabelle, 2015-02-21

All times shown according to UTC.

Time Nick Message
09:30 eng500 joined #isabelle
10:42 ThreeOfEight joined #isabelle
10:47 safinaskar hi. i heard that isabelle has "small kernel". and i should trust this kernel only, and not to whole isabelle. what this means?
10:55 ThreeOfEight I think you probably misunderstood the statement
10:55 ThreeOfEight Isabelle has a small kernel through which every statement that becomes a theorem has to pass
10:55 ThreeOfEight i.e. only the small, well-understood kernel can actually produce theorems
10:56 ThreeOfEight so a bug outside the kernel cannot compromise soundness of Isabelle
10:56 ThreeOfEight That means that if you trust the kernel, you can trust every theorem in Isabelle.
10:56 ThreeOfEight you don't have to trust that the entire huge code base is bug-free, like in other provers with a big kernel
11:13 safinaskar ThreeOfEight: thanks. i heard this works so: if i want some theorem to became theorem, i should provide proof of it, and this proof is constructed inside isabelle as ML proof object, right? but why inside isabelle wrong proof object (i. e. which proofs wrong theorem) cannot be constructed?
11:13 ThreeOfEight Yes.
11:13 ThreeOfEight construction of theorems happens in thm.ML
11:14 ThreeOfEight the functions that construct theorems in thm.ML correspond to the usual operations in natural deduction, such as introduction/elimination of universal quantifiers ec.
11:14 ThreeOfEight *etc.
11:14 ThreeOfEight outside of thm.ML, you do not have access to the thm datatype constructors
11:15 ThreeOfEight meaning that if you want to create a theorem, you have to use the functions from thm.ML
11:15 ThreeOfEight which are trusted and (relatively) simple
11:15 ThreeOfEight maybe you should have a look at HOL Light, it has the same approach but is a lot more lightweight than Isabelle
11:15 ThreeOfEight so its code may be easier to read
11:43 safinaskar ThreeOfEight: thanks i understand
12:07 safinaskar why zfc is stronger than hol? it seems for me that even second order logic covers zfc, because it is possible to express zfc in terms of second order logic
12:19 ThreeOfEight ZFC isn't really stronger than HOL, as far as I know
12:19 ThreeOfEight you can simulate one in the other
12:20 ThreeOfEight but there are some things that can't be expressed in HOL as directly as in ZF
12:20 ThreeOfEight such as the von Neumann construction for natural numbers
12:21 ThreeOfEight where 0 = {}, 1 = {0}, 2 = {0, 1}, etc.
12:21 ThreeOfEight the entire natural numbers are then a set {{}, {{}}, {{}, {{}}}, ...}
12:22 ThreeOfEight something like that would not type-check in Isabelle
12:22 ThreeOfEight but you can model it indirectly in HOL somehow
12:22 ThreeOfEight and those things do not really occur a lot in practice
12:26 safinaskar mathematically zfc is stronger than hol. isabelle manual says so :)
12:27 safinaskar ThreeOfEight: there is ZF in hol. it lives in ~~/src/HOL/ZF/ZFHOL.thy or something like that
12:28 safinaskar ThreeOfEight: but still, mathematically real zfc stronger than hol (and even than that ZFHOL.thy). and i am trying to understand why
12:40 ThreeOfEight Really? I was not aware of that. I'll have a look at it later, maybe.
12:41 ThreeOfEight Tobias Nipkow once told me that HOL and ZFC are pretty much equivalent, in a sense. But maybe I misunderstood him.
12:43 safinaskar ThreeOfEight: ~~/src/HOL/ZF/HOLZF.thy is actual name. available in 2013-2
14:13 enicodei joined #isabelle