TR-2006002: A Replacement Theorem for LP
Melvin Fitting · CUNY Academic Works (City University of New York) · 2006
The replacement theorem for classical and normal modal logics is a fundamental tool.It says that if A and B have been proved equivalent, occurrences of A in a formula may be replaced with occurrences of B to produce a formula equivalent to the original one.This theorem does not hold for LP, Logic of Proofs.A replacement for replacement is not simple to formulate.In this note I have provided one, along with some machinery for working with LP realizations that may prove useful for other things as well.