Re: SUO: Re: Common Logic Standard

[Chris Menzel <cmenzel@tamu.edu>]

On Mon, Apr 08, 2002 at 12:10:22PM +0200, Jean-Luc Delatre wrote:
> So, thanks to your announce: http://suo.ieee.org/email/msg08241.html
> I read http://cl.tamu.edu/minutes/stanford-minutes.html
> 
> And apart from the usual scrambling around various boring 
> (yet needed, alas) syntactical issues I spotted *real trouble*!
> 
>  "Sorted KIF" 
> 
> I entirely agree that typing is needed to such a point that in some cases
> you cannot ensure consistency if you do not have a typing mechanism.

Consistency in general cannot be assured by any mechanism.
 
> But, from all I have seen on the subject I can tell you, typing is HELL!
> You are going to be in DEEP SHIT for these reasons:
> 
> - There is *no* GOOD choice, only tradeoffs. This has to do with the 
>   Godel stuff, no matter how *powerfull* the typing is there are always
>   things that are not expressible anymore once you choose a typing.

Godel's results in general have nothing to do with typing.  He happens
to have chosen a typed system in his original paper to illustrate his
results concretely, but, as the title of the paper itself indicates ("On
Formally Undecidable Propositions of Principia Mathematica _and Related
Systems_"), the results apply to any theory containing the requisite bit
of arithmetic, typed or not.

Be that as it may, the kind of iterative typing found in Principia
Mathematica or the simple theory of types has nothing to do with the
issue of sorting under discussion in the Common Logic working group.

Chris Menzel