[Prev][Next][Index][Thread]

Paper on propositional equality


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