Time 
Nick 
Message 
01:47 

ilbot3 joined #isabelle 
01:47 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
02:13 
andromedagalaxy 
"The QED manifesto revisited" claims that "For formal mathematics it is essential to have both dependent types and some form of subtying" as arguments against Isabelle/HOL (interestingly, there seem to be fewer arguments against Isabelle/HOL than against Coq/Mizar). Does anyone know of a good resource showing whether this is really true? (Examples/counterexamples of theorems that can only be proved with 
02:13 
andromedagalaxy 
these features/seem like they can only be proved that way but can in fact be proved in HOL would be welcome) 
02:13 
andromedagalaxy 
Relatedly, is there a good reference for the various available Isabelle inner logics anywhere? Has anyone tried constructing a dependently typed inner logic (ideally something close to the CiC used in Coq)? 
02:15 
andromedagalaxy 
(as a specific example, that paper claims that "Every field has an algebraic closure" can't be proved in any HOL because it is impossible to write a formal equivalent of "For all fields". Is this true?) 
03:45 

fracting joined #isabelle 
05:53 
ThreeOfEight 
andromedagalaxy: WHat do you mean by "inner logic"? The object logics? 
05:53 
ThreeOfEight 
There is http://isabelle.in.tum.de/dist/Isabelle2016/doc/logics.pdf, which is marked as deprecated 
05:54 
ThreeOfEight 
the short answer to "What logics are there?" is "There's HOL and that's pretty much it." 
05:54 
ThreeOfEight 
The slightly longer answer is "Oh and there's ZF, but no one really uses that these days." 
05:55 
ThreeOfEight 
And another addendum might be "Oh and there's HOLCF but that is rarely used either; it has some nice ideas but it can get a bit tedious." 
05:55 
ThreeOfEight 
As for "theorems that cannot be proved in HOL", well, that's not an easy question… 
05:55 
ThreeOfEight 
HOL is equivalent to ZF, so any statement that you can write and prove in one of them, you can write and prove in the other 
05:56 
ThreeOfEight 
but that uses an encoding, which is, of course, usually not what you want to do 
05:57 
ThreeOfEight 
it is true that you cannot quantify over types in Isabelle, which is a problem when it comes to things like "every field has an algebraic clusure"; or defining things like "a formula is semantically valid if it is valid in all models" 
05:58 
ThreeOfEight 
as for the fields, I forgot how the construction works, but perhaps you could simply construct a type "'a alg_closure" for every "'a :: field". 
05:58 
ThreeOfEight 
Whether that works or not depends on how the construction for the field extension works 
05:58 
ThreeOfEight 
but I do agree that it may be difficult. 
05:59 
ThreeOfEight 
As for dependent types, well, our Algebra library is not very welldeveloped, and some people say it is because we don't have dependent types and those carrier sets and locales are really annoying for Algebra 
05:59 
ThreeOfEight 
I'm not sure if that's true, but it is plausible 
06:00 
ThreeOfEight 
However, while we often run into issues where we think "Wow, it would be so great if we had dependent types now, that would solve all our problems", I've heard that dependent types cause many problems of their own and that even in dependentlytyped logics, people often don't use dependent types for the things where I thought they'd solve all the problems because of that 
06:00 
ThreeOfEight 
I don't know if that's true since I've never really worked with dependent types myself. 
06:00 
ThreeOfEight 
Maybe I should have a look at Lean some time 
06:13 
larsrh 
"As a kid, I always asked myself why wizards don't just use magic everytime to solve a problem. Now I've seen dependent types and I understand" 
07:15 

fracting joined #isabelle 
08:10 

fracting joined #isabelle 
09:04 

fracting joined #isabelle 
10:12 

fracting joined #isabelle 
11:24 

fracting joined #isabelle 
12:07 

xenthree3 joined #isabelle 
12:07 

xenthree3 left #isabelle 
12:15 

fracting joined #isabelle 
16:21 

fracting joined #isabelle 