What holds in a context?

Abstract

In order to establish that ℒ[A] = ℒ[B] follows from a set of assumptions Γ often one proves A =B and then invokes the principle of substitution of equals for equals. It has been observed that in the ancillary proof of A =B one is allowed to use, in addition to those assumptions of Γ which are free for ℒ, certain (open) sentences P which may not be part of Γ and may not follow from Γ, but are related to the context ℒ. We show that in an appropriate formal system there is a closed form solution to the problem of determining precisely what sentences P can be used. We say that those sentences hold in the context ℒ under the set of assumptions Γ. We suggest how the solution could be exploited in an interactive theorem prover. © 1993 Kluwer Academic Publishers.