Re: FOL vs HOL vs MML

attardi@ICSI.Berkeley.EDU (Giuseppe Attardi)
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