[CL] inconsistency in Annex B? (actually types in general)

[John F. Sowa]

Chris,

I realize that the untyped style of CL and IKL makes it impossible
to have a typed model that supports the full language.  But it is
possible to write axioms for a typed system in an untyped logic.

 > Tarski's hierarchy is highly typed; the truth predicate and sentence
 > names for a given language Ln in the hierarchy are not in Ln.  That
 > is exactly not the case in IKL (though think "proposition name"
 > instead of "sentence name").  IKL is radically type-free; there is
 > no hierarchy, and it (in effect) contains its own truth predicate,
 > which is exactly why it can't have a Tarskian model theory.

I agree with that.  But isn't it possible in IKL to axiomatize
a stratified, Tarski-style hierarchy, which imposes restrictions
on the kinds of statements one can make about propositions?

If so, it would be possible to define Tarski-style language levels
with a truth predicate for level n, that was only expressible at
level n+1.  This truth predicate would not be identical to the
unrestricted IKL truth predicate.  But it should be consistent
with the unrestricted IKL predicate on statements for which both
are defined.

 > Good and usable [Tarski's hierarchy] may be, but it just ain't
 > a model of IKL.

I agree.  But the reason why I gave up my objections to the untyped
style of CL is that one could define multiple kinds of restricted
systems within CL.  Then people would be free to choose whichever
typed system they pleased and embed it within the untyped CL.

The only restriction would be that anything stated in the more
restricted language could always be exported to a less restricted,
but the converse would only be true for a subset of the unrestricted.

In order to show that IKL is usable safely, it is only necessary
to show that it is possible to define one or more very useful
(and paradox-free) systems within IKL.  Then people can be given
appropriate warnings about where the dragons lie.

John