Red Herring?

Konrad Slind <>
From: Konrad Slind <>
To: boyer@CLI.COM
In-Reply-To: <>'s message of Fri, 23 Apr 1993 02:02:28 +0200 <9304230002.AA19396@axiom.CLI.COM>
Subject: Red Herring?
Message-id: <>
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

> (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.