Re: FOL vs HOL vs MMLRamesh Patil <ramesh@ISI.EDU>
Date: Sat, 11 Dec 1993 20:55:41 -0800
To: Matthew L. Ginsberg <email@example.com>
From: Ramesh Patil <ramesh@ISI.EDU>
Subject: Re: FOL vs HOL vs MML
Cc: firstname.lastname@example.org, interlingua@ISI.EDU, email@example.com
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
>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