Re: [isabelle] Isabelle: A logic of total functions (?)

Yes itâs possible, e.g. a logic with a definedness predicate could be defined. LCF and HOLCF are also, in effect, logics of definedness, in that you can reason about whether or not something is the value UU (undefined), which really is treated specially, in that it induces a partial ordering on all types.

They are all a pain to use.

Larry Paulson

> On 17 Apr 2015, at 16:43, Andrew Butterfield <Andrew.Butterfield at> wrote:
> Hmmm - a little bit off topic  .. is the meta-Logic of Isabelle also in effect a logic of total functions as well?
> Or could you build a logic of partial functions on top of it ? â not that this would help Alfio muchâ
> My understanding about undefinedness and/or partial functions is that there are a variety
> of ways to work with them - three-valued logics, adding bottom elements to semantic domains, having definedness side-conditions (everywhere)
> all with their plusses and minusses - but there is no way to avoid some pain. You have find whatever hurts leasts (which depends on what you are trying to do), and stick with that.

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