Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu



You can see definitions that way, but then almost everything can be codified as an inference system. 

Of course I am not criticising your work, it's a positive contribution. Everything we can do to catch user errors is constructive. Note also how sledgehammer warns you if it can prove your theorem directly from an inconsistency in your assumptions. And we also have nitpick to catch user errors in theorem statements. But there is a difference between failing to catch a user error and performing incorrect deductions.

Larry

> On 21 Aug 2016, at 20:41, OndÅej KunÄar <kuncar at in.tum.de> wrote:
> 
> I see. I guess the whole discrepancy boils down to the question if definitions are part of logical reasoning. For me, this is the case since you can view definitions as the following inference rule:
> 
>     T
> ----------- [side conditions]
> T' |- c = t
> 
> And if "c = t" allows you to prove False, then I call it an inconsistency.
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.