[Prev][Next][Index][Thread]
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. 546565.)

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.\ MartinL\"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 `Skolemtype' 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 GentzenHerbrand (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 50732970
Brasil
ruy@di.ufpe.br tel.: +55 81 271 8430 fax: +55 81 271 4925