Time 
Nick 
Message 
09:30 

eng500 joined #isabelle 
10:42 

ThreeOfEight joined #isabelle 
10:47 

safinaskar 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:47 
safinaskar 
how this works? 
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, wellunderstood 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 bugfree, 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 typecheck 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 20132 
14:13 

enicodei joined #isabelle 
15:05 

safinaskar joined #isabelle 
15:13 

safinaskar left #isabelle 
16:22 

enicodei joined #isabelle 
18:57 

safinaskar joined #isabelle 
18:59 
safinaskar 
hi. please say me some way to verify programs. c programs would be great, but any other language will go. i want some kickstart, i cannot find some easytoinstallandwork tools in internet 
21:16 

eng500 joined #isabelle 
23:21 

mal`` joined #isabelle 
23:57 

eng500 joined #isabelle 