Re: Comments on CASL v0.95 FINAL DRAFT

[Till Mossakowski <till@informatik.uni-bremen.de>]

A reply to Andrzej's comment on my comment:

>I do not like empty carriers either, but I dislike any manipulation
>with free variables even more. (So, my "ideal" solution would be to
>remove the non-empty carrier assumption and deal with closed sentences
>as axioms only.) Given that people say that variable declarations as a
>means to avoid some tedious quantification are a must, I'd rather have
>the non-empty carriers assumption than arbitrary models and some rules
>about closure wrt to variables that actually occur free in formulae,
>or a separate and distinct treatment of free variables in the logic. I
>would therefore also stick to the current text in the proposal, about
>universal closure fo the axioms over the variables declared in the
>given list of basic items. Just my opinion though...

Actually, if non-empty carriers are the default, as Peter suggests,
then it might be not a problem to quantify over all variables
in a VAR-DECL, since if the user uses empty-carrier sorts, he/she
just has to remember that special effects like is-empty(empty)
being true even it is not literally the case (due to variables
in a VAR-DECL which vary over an empty carrier) may occur.
In fact, then all axioms are (implicitly) closed.
Concerning the separate and distinct treatment of free variables
in the logic, I think this is rather natural because it solves not
only the proof-theoretic problems of possibly-empty-carrier-models elegantly,
but more importantly, allows to keep the standard substitution rule,
while shifting definedness considerations to the quantifier rules.
And to keep the substitution rule seems to be central to keep
proof methods based on unification, while quantifier rules are used
less frequently. This at least was the opinion of somebody in Bremen
who works heavily with the HOL logic in the Isabelle system.

Of course, this largely is a matter of the proof system, but it shows
that the proof-theoretic problems with empty carriers can be solved
within the present language (but if soundness is wanted for the individual
rules and not only for derivations, a different semantics for free
sentences has to be assumed. But this might even be shifted to the
proof theory section, because in the model theory, we only deal with
closed sentences).

Greetings,
Till