Red Herring?

Konrad Slind <slind@informatik.tu-muenchen.de>

Mail folder: QED
Next message: Dewey Val Schorre: "Theorem generators and Theory Generators"
Previous message: Konrad Slind: "Cold water"
In-reply-to: Robert S. Boyer: "Red Herring?"

From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: boyer@CLI.COM
Cc: qed@mcs.anl.gov
In-Reply-To: <qed-owner@mcs.anl.gov>'s message of Fri, 23 Apr 1993 02:02:28 +0200 <9304230002.AA19396@axiom.CLI.COM>
Subject: Red Herring?
Message-id: <93Apr23.032248met_dst.8079@sunbroy14.informatik.tu-muenchen.de>
Date: 	Fri, 23 Apr 1993 03:22:39 +0200
Sender: qed-owner
Precedence: bulk


Just a side comment on reflection: one has to distinguish "logical"
reflection from "computational" reflection. The examples that Robert S.
Boyer gives (simplifiers and decision procedures) are of algorithms
whose acceptance (after correctness has been proven) as new inference
rules in no way increase the power of the logic. This is computational
reflection.

> (I admit that my vision becomes myopic when I start to think about
> reflection. It is still terribly worrisome to me that a reflection axiom
> can sometimes strengthen a logic by the addition of its consistency.)

This is logical reflection. I think it would be hard to justify the
restriction to a simple logic on one hand and the addition of such a
powerful axiom on the other hand.

Of course Boyer already knows this, as demonstrated in his and Moore's
"Metafunctions" paper.

Konrad.