Re: FOL vs HOL vs MML

Ramesh Patil <ramesh@ISI.EDU>
Date: Sat, 11 Dec 1993 20:55:41 -0800
Message-id: <>
To: Matthew L. Ginsberg <>
From: Ramesh Patil <ramesh@ISI.EDU>
Subject: Re:  FOL vs HOL vs MML
Cc:, interlingua@ISI.EDU,
It appears to me that what Matt is asking for is reasonable.  I would like
to see a formal proof for the claims of KIF/CG etc. being paradox free and
first order being submitted for peer review.  Even better send them to Matt
and have him review it.  I am sure Matt will be more than willing to review
  - Ramesh

>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