Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF

Chris Menzel <cmenzel@kbssun1.tamu.edu>
From: Chris Menzel <cmenzel@kbssun1.tamu.edu>
To: fritz@rodin.wustl.edu
Cc: cg@cs.umn.edu, interlingua@ISI.EDU, srkb@cs.umbc.edu,
        E.Hunt@cgsmtp.comdt.uscg.mil, bhacker@nara.gov,
        duschka@cs.stanford.edu, genesereth@cs.stanford.edu,
        jksharp@sandia.gov, msingh@bcr.cc.bellcore.com,
        msmith@vax2.cstp.umkc.edu, roger@ci.deere.com, scott@ontek.com,
        sharadg@atc.boeing.com, skperez@mcimail.com, tony@ontek.com,
        zeleny@math.ucla.edu
In-reply-to: <9409091531.AA08687@rodin.wustl.edu> (fritz@rodin.wustl.edu)
Subject: Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF
Message-id: <94Sep9.120526cdt.9765@kbssun1.tamu.edu>
Date: 	Fri, 9 Sep 1994 12:05:24 -0500
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk

Fritz,

Thank you very much for your thoughtful reply.  You wrote:

       Chris Menzel said of Scott domains:
  FL:>>   Actors" in Conceptual Graphs are
  >>   procedural.  Genesereth has stated often that KIF is declarative
  >>   and not procedural.  To provide declarative semantics for
  >>   procedures requires correct treatment of recursive functions,
  >>   functions of functions, and programs which loop infinitely and
  >>   never halt; this requires "reflexive" algebraic structures of
  >>   partial functions like the continuous lattices of Dana Scott, which
  >>   leads to domain theory and necessary distinctions which are
  >>   strongly higher-order.
  CM:>Once again, mere quantification over functions, functions of
  >functions, etc. does not necessarily mean you are using a higher-order
  >logic.  These are all first-order objects in set theory.  Scott
  >domains in particular are definable (and typically, are defined, even
  >in Scott's own papers) in first-order set theory.

  Scott structures include continuous lattices. The required lattice
  definition "For every subset X \subseteq B, the supremum \bigvee X
  exists" is second order and strongly so (Dickmann, in Barwise &
  Feferman, p. 324).

Sorry, I was unclear; I should have said Scott domains were
"definable_1" in set theory in the sense introduced in my previous
post, i.e., the definitions (stated in the language of set theory)
pick out the right notions in a standard model of set theory.  They
are of course not first-order definable in the stronger sense that
guarantees nothing unintended falls under the definition; for that you
need to ensure that the "for every subset X \subseteq B" quantifier,
if written in a second-order language, does indeed range over all
subsets of B, and that's just what true second-order semantics
guarantees.  My question, once again, had *not* to do with the
undeniable value and importance of higher-order model theory, but with
whether, *in the context of an Interlingua*, using a higher-order
language with the stipulation that it be interpreted with full
higher-order model theory buys you any more than using first-order set
theory with the stipulation that it be interpreted in a standard
model.

Best wishes,

Chris Menzel

=================================================================
Christopher Menzel		  |  Internet -> cmenzel@tamu.edu
Philosophy, Texas A&M University  |  Phone ---->   (409) 845-8764
College Station, TX  77843-4237   |  Fax ------>   (409) 845-0458
=================================================================