Re: Review of FLD

On Tue, 26 May 2009 10:02:04 -0400
Chris Welty <cawelty@gmail.com> wrote:

> 
> 
> Michael Kifer wrote:
> > 
> > On Tue, 19 May 2009 09:11:24 -0400
> > Chris Welty <cawelty@gmail.com> wrote:
> > 
> >>> Is ?X("abc"^^xs:string ?W)(?Y ?Z(?V "33"^^xs:integer)) an instance of Henkin's
> >>> or CL syntax? Hint: check what plays the role of a function here.  
> >> Ah, I see.  Henkin did not have functions.  Yes, this is valid CL syntax, and is 
> >> still compact so still first order.  My understanding of compactness is that 
> >> functions and constants are interchangeable in terms of their impact on it.
> > 
> > Are you saying that CL allows f(a)(b)(?X, foo) and things like that?
> > I remember SKIF didn't have it and when I pointed this out to Pat he vigorously
> > objected to this kind of terms.
> > 
> > As far as I am aware, these terms were first introduced in HiLog - more than 10
> > years before CL.
> 
> Yes CL allows that, and references HiLog appropriately.  Chris Menzel even 
> pointed at you while acknowledging that fact at the opening RIF meeting 
> presentation on CL (you must have been reading your email).

Menzel did mention it verbally, but please do search the CL document for HiLog
and report the results.

Regarding CL allowing such terms, I now see that it might. In the definition, it
uses the notion of "function term," which it never defines, but assuming it is
the same as "term" then ok.

> CL is *not* KIF.  KIF and HiLog are ancestors of CL in a lot of ways, but CL is 
> neither HiLog nor KIF.  It definitely is a far cry from SKIF.  SKIF was invented 
> by Adam Pease and was thrown out, along with Adam, of the CL effort on day 1. 
> CL allows everything that, as of 2005, was provably first-order, plus it adds 
> sequences (which are not).

This is news to me and I highly doubt it. Hayes and Menzel wrote the SKIF
paper in 2001, which was basically a restricted HiLog modulo the row vars (which
are not first order).
http://www.google.com/url?sa=t&source=web&ct=res&cd=1&url=http%3A%2F%2Fwww.ihmc.us%2Fusers%2Fphayes%2FHayesMenzel-2001-KIF.ps&ei=IgscStDgF-HJtgfRvu3tDA&usg=AFQjCNFLk1wFqX8h1I8b5kj1R-UCre3CIA&sig2=atD9cESDYgX84OYNwrdLbw

I am afraid you are confusing something. They don't even mention Pease, and
searching for Pease and SKIF together does not reveal anything interesting.

> Anyway, my point is that saying the FLD syntax "generalizes first order syntax" 
> is not accurate, in my understanding.  It *is* first order syntax.

You are confusing syntax and semantics (expressiveness). Henkin's logic is
always referred to as having higher-order syntax. So do Hayes and Mentzel in
reference to SKIF.

-- 
    -- michael

Received on Tuesday, 26 May 2009 15:55:27 UTC