# Paper on propositional equality

• To: types@dcs.gla.ac.uk
• Subject: Paper on propositional equality
• From: Ruy de Queiroz <ruy@di.ufpe.br>
• Date: Mon, 06 Jun 1994 17:23:06 -0500 (EST)
• Approved: types@dcs.gla.ac.uk


The paper with the abstract given below has just been made available at the
electronic archive

theory.doc.ic.ac.uk

directory

papers/deQueiroz

file name

ac9.{dvi,ps}.gz

(In paper form: Proceedings of the Ninth Amsterdam Colloquium, Paul Dekker and
Martin Stokhof (editors), ILLC/Department of Philosophy, University of
Amsterdam, 1994, pp. 546-565.)

--------------------------------------------------------------------------------
Equality in Labelled Deductive Systems and the functional interpretation of
propositional equality

Ruy J. G. B. de Queiroz & Dov M. Gabbay

\begin{abstract}

Within the context of natural deduction for {\em Labelled Deductive Systems\/},
we formulate what appears to be a middle ground solution to the intensional'
vs.\ extensional' dichotomy which permeates most of the work on characterising
propositional equality (as in, e.g., P.\ Martin-L\"of's type theories). The
intensional aspect is dealt with in the functional calculus on the labels,
whereas the extensionality is kept to the logical calculus on the formulas.
Equalities which are dependent on the deduction/computation path (context) are
handled by the functional calculus on the labels. Those equalities are usually
definitional, and may come from the geometry' of deduction (e.g.\ $\beta$,
$\eta$, $\zeta$, $\mu$), and thus carry essentially intensional' information.
On the other hand, equality in the logical calculus (propositional equality) is
essentially extensional' as it refers to the existence' of a way of rewriting
a referent into another one.

We look at propositional equality ($\doteq$') as a Skolem-type' connective
(such as disjunction and existential quantification), where notions like
dependent variables' and choice' play a crucial role. This means that in the
elimination rule for $\doteq$' we need to introduce identifiers (new symbols)
for compositions of equalities denoting arbitrary rewriting paths. We believe
this provides a new perspective on the connections Gentzen--Herbrand (i.e.\
the sharpened Hauptsatz').

\end{abstract}
--------------------------------------------------------------------------------

--
Ruy J. G. B. de Queiroz
Departamento de Informatica
Universidade Federal de Pernambuco (UFPE) em Recife
Caixa Postal 7851
Recife, PE 50732-970
Brasil

ruy@di.ufpe.br          tel.: +55 81 271 8430           fax: +55 81 271 4925