Re: a multilingual approach

• Mail folder: QED
• Next message: John Harrison: "Formalizability as a Criterion for Mathematical Rigour"
• Previous message: David McAllester: "a multilingual approach"
• In-reply-to: David McAllester: "a multilingual approach"
• Reply: Phil Windley: "Re: a multilingual approach "
• Reply: guttman@linus.mitre.org: "Re: a multilingual approach "

Message-id: <9304132110.AA10474@circe.mitre.org>
To: dam@ai.mit.edu (David McAllester)
Cc: qed@mcs.anl.gov
Subject: Re: a multilingual approach 
In-reply-to: Your message of "Tue, 13 Apr 93 15:35:55 EDT."
             <9304131935.AA00351@spock> 
X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730
X-Telephone-Number: 617 271 2654; Fax 617 271 3816
Date: Tue, 13 Apr 93 17:10:38 -0400
From: guttman@linus.mitre.org
Sender: qed-owner
Precedence: bulk

>  From: dam@ai.mit.edu (David McAllester)
>  Subject: a multilingual approach

    [paragraph deleted]

>  Of course I can see no objection to collecting libraries of first
>  order validities, I am just not sure how to use them.  Perhaps the
>  IMPS notion of a "little theory" is relevant here.  A little theory is
>  a signature, a set of axioms, and a set of consequences.  I probably
>  could translate any IMPS theory directly into a set of Ontic theorems.

I think one of the advantages of the little theories version of the
axiomatic method is this:  The little theory is a natural unit for
interchanging results.  By organizing mathematics into a network of
relatively fine theories, it lets us see exactly what assumptions we
must discharge to justify using a particular group of theorems in a
different framework.

	Josh