Re: FOL vs HOL vs MML

Matthew L. Ginsberg <ginsberg@cs.uoregon.edu>
Date: Sat, 11 Dec 93 15:51:15 PST
From: Matthew L. Ginsberg <ginsberg@cs.uoregon.edu>
Message-id: <9312112351.AA01199@t.uoregon.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU, sowa@turing.pacss.binghamton.edu
Subject: Re:  FOL vs HOL vs MML
Amazing.  A semantics with all the "practical" power of HOL but
computationally equivalent to nested FOLs.  I remember when things
like this used to be subject to peer review and publication, as
opposed to simply announced as standards.

Anyway, to keep you from escaping the peer review process completely,
I wonder if you could answer the following:

(1) Do you have a proof that your MML cannot express paradoxes?
I've asked this before and never gotten more than vague arguments;
what I'm hoping for is a *proof*.

(2) In your "practically equivalent" MML, do you have any way to
express the fact that relation R' is exactly the transitive closure
of relation R?

						Matt Ginsberg