[isabelle-dev] Isabelle/HOL axiom ext is redundant
Makarius wrote: On Thu, 12 Nov 2009, Lucas Dixon wrote: this is interesting to me: I don't understand why you couldn't just use the -- and ALL of HOL to do exactly what == and !! are doing? Isn't that what SPL by Zammit did? The dependencies (in Isabelle, stored in hyps) can all be recorded outside the logic (as they are in SPL). If done correctly, like Isar, the final theorems can be re-constructed easily enough from the recorded structure of the proof text... or so it seems to me. :) The hyps are not involved at this point. This is about what I've called the visible part of ND reasoning before. The nice thing of explicitly outlined ND rules via == and !! is that the system knows how to combine them from their shape. It is not about two versions of certain connectives, but a ND rule calculus that is used together with a fully featured object-logic. Because, as discussed, the notions correspond in HOL, one could emulate ND by defining new constants equal to the existing object logic implication and universal quantification. One would then prove the ND rules in terms of these. As Makarius said, one would then also have to reinvent the implementation of things like resolution over these connectives in order to get that nice uniformity that Isaballe already has. Of course, I also believe that one might emulate this nice uniformity in theorems and reasoning by writing sufficiently clever ML code (which would be parameterised by appropriate theorems, say). When the logic reaches its limits (for example, in the construction of algebraic datatypes we can't express the idea of type existence as a theorem), this is the last recourse that all the HOL systems must stoop to. Michael.
[isabelle-dev] Isabelle/HOL axiom ext is redundant
This sort of discussion is analogous to suggesting that we get rid of and/or/not/implies and write all formulas using the Scheffer stroke (NAND), or that Gentzen's sequent calculus should be replaced by the much simpler Hilbert system. It can be done, but who would want to do it? Larry On 12 Nov 2009, at 20:50, Lucas Dixon wrote: this is interesting to me: I don't understand why you couldn't just use the -- and ALL of HOL to do exactly what == and !! are doing? Isn't that what SPL by Zammit did? The dependencies (in Isabelle, stored in hyps) can all be recorded outside the logic (as they are in SPL). If done correctly, like Isar, the final theorems can be re-constructed easily enough from the recorded structure of the proof text... or so it seems to me. :)
[isabelle-dev] Isabelle/HOL axiom ext is redundant
I was really wondering what the principle was that makes -- and ALL fail (or be inappropriately convoluted) than using the meta-level connectives: is there a small example that illustrates it? My own understanding was that the meta-level of Isabelle, and the use of it by Isar, facilitated the genericity natural deduction-style reasoning. Generic proof tools can be written that work across logics. Makarius, if I understood correctly, was saying that these meta-level logical mechanisms have a utility even when just within one logic, but I didn't understand what this would be, except perhaps distinguishing between ND syntax and other logical syntax (which is my interpretation of Michael's reply). best, lucas Lawrence Paulson wrote: This sort of discussion is analogous to suggesting that we get rid of and/or/not/implies and write all formulas using the Scheffer stroke (NAND), or that Gentzen's sequent calculus should be replaced by the much simpler Hilbert system. It can be done, but who would want to do it? Larry On 12 Nov 2009, at 20:50, Lucas Dixon wrote: this is interesting to me: I don't understand why you couldn't just use the -- and ALL of HOL to do exactly what == and !! are doing? Isn't that what SPL by Zammit did? The dependencies (in Isabelle, stored in hyps) can all be recorded outside the logic (as they are in SPL). If done correctly, like Isar, the final theorems can be re-constructed easily enough from the recorded structure of the proof text... or so it seems to me. :) -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] Isabelle/HOL axiom ext is redundant
On Fri, 13 Nov 2009, Lucas Dixon wrote: I was really wondering what the principle was that makes -- and ALL fail (or be inappropriately convoluted) than using the meta-level connectives: is there a small example that illustrates it? My own understanding was that the meta-level of Isabelle, and the use of it by Isar, facilitated the genericity natural deduction-style reasoning. Generic proof tools can be written that work across logics. Makarius, if I understood correctly, was saying that these meta-level logical mechanisms have a utility even when just within one logic, but I didn't understand what this would be, except perhaps distinguishing between ND syntax and other logical syntax (which is my interpretation of Michael's reply). Yes, this distinguishing is an important aspect. If we go back to Isar calculations again, print_trans_rules will tell you that there are also variants of modus ponens as part of the game. If you would dedicate -- for (homegrown) transitivity rule outlines, you would somehow need to mark such rules or even transitivity over -- as special. Another example are plain intro/elim rules for --: impI: (A == B) == (A -- B) mp: (A -- B) == (A == B) The system can make sense out of them declaratively. In pure Isar you do not even need the rule vs. erule distinction in the text. By collapsing the structure of the framework, you would only get amorphic (A -- B) -- (A -- B). Yet another example, which of a slightly different category. The framework represents goal states via iterated == (another really nice idea by Larry from 20 years ago). So A1 == A2 == C means subgoals A1 and A2 are sufficient to establish the main conclusion C. If C is itself an implication, we get into problems. As an extra-logical solution one could pass around the length of the initial prefix (here 2) that counts as subgoals. Internally there are indeed some (awkward) ML operations like that. It has turned out much more practical to internalize the goal outline structure, this time using the prop marker (identity on propositions), which is often printed as # in my papers. The latter is rarely encountered in user space -- similar to Pure.conjunction. So one could ask if !! == could be hidden like that as well. In that case, the user would be limited to flat rules. One would also need to come up with extra ideas do reprent more deeply nested things like well-founded induction. Makarius
[isabelle-dev] Isabelle/HOL axiom ext is redundant
On Thu, Nov 12, 2009 at 2:06 PM, Andreas Schropp schropp at in.tum.de wrote: In a sense, eq_reflection is a meta-thereom, but Pure is not a meta-logic, so it cannot be proven within the system. ?Thus we need to add it as an axiom. But we can prove all instances of the eq_reflection propagation theorem, right? I would consider this as an implementation detail, and not worry about it any further. Tools that operate on the level of proof terms can then eliminate eq_reflection, as was pointed out first by Stefan Berghofer some years ago, IIRC. ?(I also learned from him that it is better to speak about Pure as logical framework, and not use term meta logic anymore.) Yeah, Stefan does this in HOL/Tools/rewrite_hol_proof.ML (which was tested quite thoroughly since 5e20f9c20086, so also in Isa09). This is very interesting... I'd like to learn more about the status of eq_reflection as a meta-theorem. Is there a paper about this? - Brian
