# IRC log for #isabelle, 2016-05-20

All times shown according to UTC.

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 andromeda-galaxy "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 andromeda-galaxy these features/seem like they can only be proved that way but can in fact be proved in HOL would be welcome)
02:13 andromeda-galaxy 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 andromeda-galaxy (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 andromeda-galaxy: 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 well-developed, 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 dependently-typed 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