Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Tue, 23 Feb 1993 20:11:39 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15833; Tue, 23 Feb 93 11:48:24 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA15828; Tue, 23 Feb 93 11:48:13 -0800 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Tue, 23 Feb 1993 19:47:49 +0000 To: info-hol@edu.uidaho.cs.ted Subject: Nonstandard Analysis Date: Tue, 23 Feb 93 19:47:44 +0000 From: John Harrison Message-Id: <"swan.cl.ca.993:23.02.93.19.47.51"@cl.cam.ac.uk> Hi, Garrel's remarks on Nonstandard Analysis (hereinafter NSA) set me thinking once again about the following issue. As I understand it, much of the power of NSA devolves from general metatheorems such as the Transfer Principle, the elementary equivalence of standard and nonstandard models and properties of internal sets. Suppose one develops the hyperreals as a type in HOL (I did this a few months ago -- given Zorn's Lemma, in the new wellorder library, it's quite easy to carry through Luxemburg's ultrafilter construction). Suppose further that one wants to proceed in rigorous HOL style without any cheating. This doesn't mean eschewing metalogical reasoning entirely: ML is a sort of metalogic -- just a recursive one. Is there much in the general NSA metatheorems that can be made *effective*? John.