When reasoning about reasoning one often needs to carry out some proof steps within a different theory and to lift the conclusions back to the original theory. The deductive rules to carry out these steps involve different reflection principles or some other notion of proof in context. Reflection principles have to be carefully restricted in order to avoid paradodex. Such restrictions however. we show that proof in context can replace the most common uses of reflection prionciples. We introduce a generalized rule for proof in context and a convenient notation to express nesting of contexts, which allows us to carry out resanong about reasoning in a safe and natural way.
Proofs in context
ATTARDI, GIUSEPPE;SIMI, MARIA
1994-01-01
Abstract
When reasoning about reasoning one often needs to carry out some proof steps within a different theory and to lift the conclusions back to the original theory. The deductive rules to carry out these steps involve different reflection principles or some other notion of proof in context. Reflection principles have to be carefully restricted in order to avoid paradodex. Such restrictions however. we show that proof in context can replace the most common uses of reflection prionciples. We introduce a generalized rule for proof in context and a convenient notation to express nesting of contexts, which allows us to carry out resanong about reasoning in a safe and natural way.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.