Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
On 22.08.2016 19:39, Ken Kubota wrote:
Yes, such extreme measures would greatly simplify the story from a
theoretical point of view, but we are talking here of implemented logic:
it needs to provide extra provisions to make it usable in practice.
In Q0/R0 there are no such declarations.
In summary, the solution would be not allowing declarations in the mathematical language, but only definitions, like in Q0/R0.
Also, implementing definitions within the logical core contradicts to the LCF philosophy of a small trusted kernel.
For this reason, definitions in R0 are mere abbreviations located outside of the logical kernel.
They also can be removed at any time (and re-introduced again) without modifying the theorems already obtained.
Abbreviations that are always expanded would render the system
impractical due to huge terms in expanded internal form.
Ruling out declarations that are separated from definitions greatly
simplify things, but prevent important applications like type class
There is always a tradeoff in theoretical simplicity versus complexity
required for practical applications of logic.
Without that tradeoff, making a usable theorem proving environment like
Isabelle would be a trivial exercise, and not an effort of 30 years.
This archive was generated by a fusion of
Pipermail (Mailman edition) and