**Mail folder:**Interlingua Mail**Next message:**Michael R. Genesereth: "kif"**Previous message:**Ramesh Patil: "Re: FOL vs HOL vs MML"**In-reply-to:**sowa: "FOL vs HOL vs MML"

From: attardi@ICSI.Berkeley.EDU (Giuseppe Attardi) Date: Tue, 14 Dec 93 12:06:27 PST Message-id: <9312142006.AA14871@icsib66.ICSI.Berkeley.EDU> To: sowa@turing.pacss.binghamton.edu Cc: cg@cs.umn.edu, interlingua@ISI.EDU In-reply-to: <9312111905.AA13466@turing.pacss.binghamton.edu> (message from sowa on Sat, 11 Dec 93 14:05:39 EST) Subject: Re: FOL vs HOL vs MML

Maria Simi and myself share the concerns expressed by Ginsberg and Patil about paradoxes in your MML construction. You can certainly express the induction axiom in L1 exploiting a suitable naming device and a regular predicate, let's call it HOLDS (or AXIOM), saying that a term (Induction) representing the induction axiom holds. For example: forall x . HOLDS('Induction(,x)') here x ranges over predicate symbols and ",x" means that x appears unquoted in the term representing the induction axiom. The problem is that, for doing something useful with it you need some form of reflection. Otherwise the induction axiom remains separate >From other Peano axioms which are stated at the object level (or so it looks from your description) and you can never reason with all the axioms together. (I don't think that doing everything at the metalevel is a reasonable alternative). But the formulation of reflection rules is a delicate issue. For example you could think of a reflection rule such as the following: If T1 |- HOLDS('S') then T0 |- S where S is an instance of the induction axiom and Tj is the theory with language Lj. This is safe provided that T1 is a meta-image of T0, but this is not the case since T1 is a richer theory than meta-T0, for example it includes HOLDS('S'). You could then think of a stronger reflection rule such as If T1 |- HOLDS('S') then T1 |- S but with this you can also prove T1 |- HOLDS('S') => S If you also have a corresponding reification rule: If T1 |- S then T1 |- HOLDS('S') you are in trouble, because then you can prove: T1 |- HOLDS('HOLDS('S') => S') which together with other obvious properties of HOLDS make T1 inconsistent (and T2, ..., T* consequently), according to Montague's theorem. We dealt with exactly these issues in the paper: "A Formalization of Viewpoints", G. Attardi and M. Simi ICSI TR-93-062 (accepted for publication) available for ftp from ftp.icsi.berkeley.edu in /techreports/1993/tr-93-062.ps.Z In the paper we propose a reflective first-order theory which includes its own metalevel. There is no need for an infinite tower of levels. The reflections rules are carefully formulated to avoid the paradoxes and the theory is proved consistent. -- Beppe and Maria