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

[Chris Menzel]

On Wed, Nov 14, 2007 at 09:13:08AM -0500, John Sowa wrote:
> ...
> > There is too much foundational work [for IKL] yet to be done.
> > We still do not have a completely guaranteed sound basic semantics,
> > and nothing lie a proof theory.
> 
> There is a very fine subset of IKL that has had a sound semantics
> and a sound proof theory for over 70 years:  Tarski's hierarchy
> of metalanguages.  

John, I don't see any way of embedding Tarski's hierarchy into IKL, at
least not in a way that admits of a Tarskian model theory.  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.  It bears far greater similarities to
frameworks descending from Kripke's work on truth (who was first, or
close to it, to develop a model theory for a language that contains its
own truth predicate), including notably Gupta/Belnap and Herzberger, and
Ray Turner's work on property theory (wherein propositions are just
0-ary properties).

> That state of affairs is not unlike Peano's axioms for arithmetic
> and many other widely used axiomatizations.  You only need one
> model to show that the framework is sound.
> 
>  > IKL is way beyond FOL. I would be very unhappy putting IKL forward
>  > as a candidate for standardization at any predictable date at this
>  > point.
> 
> It took over half a century to untangle the issues involved with
> Peano's axioms.  I wouldn't be surprised if people are still
> arguing about nonstandard models of IKL for another century.

Trouble is, unlike PA, we haven't even rigorously worked out a
*standard* model for IKL (though it's pretty clear to us how to do that,
borrowing heavily from Gupta/Belnap's revision theory of truth).

> Another example is every major programming language in existence
> today:  they all permit programs that cannot be proved to terminate,
> but people have been using them successfully for over 70 years.

That's probably a better example, as there wasn't a decent model theory
for programming languages until Scott's work on domain theory in the 60s
(IIRC).  And note that, again unlike PA, Scott domains are very
complicated structures that are not at all easy to picture.  I think IKL
models will be easier to visualize than Scott domains, but again nothing
like the standard model of PA, or the Tarskian hierarchy.

> But the point is that there is at least one very good and usable
> model (Tarski's hierarchy).  

Good and usable it may be, but it just ain't a model of IKL.

-chris