##
Reports on Mathematical Logic

###
No. 28 (1994)

Haydee Werneck POUBEL and Luiz Carlos P. D. PEREIRA

A CATEGORICAL APPROACH TO HIGHER-LEVEL INTRODUCTION AND ELIMINATION RULES
A b s t r a c t.
A natural extension of Natural Deduction was defined by
Schroder-Heister where not only formulas but also rules could be used
as hypotheses and hence discharged. It was shown that this extension allows
the definition of higher-level introduction and elimination schemes and that
the set $\{ \vee, \wedge, \rightarrow, \bot \}$ of intuitionist sentential
operators forms a {\it complete} set of operators modulo the higher level
introduction and elimination schemes, i.e., that any operator whose
introduction and elimination rules are instances of the higher-level schemes
can be defined in terms of $\{ \vee, \wedge, \rightarrow, \bot \}$.

The aim of the present work is to extend the
well-known connections between Proof Theory and Category Theory to
higher-level
Natural Deduction. To be precise,
we will show how an adjointness between cartesian closed categories with
finite coproducts can be associated, in a systematic way, with any operator
$\phi$ defined by the higher-level schemes. The objects in the categories
will be rules instead of formulas.

Back to Main Menu