[Flirts] Curry-Howard for more complex logics

[Valeria.dePaiva at parc.com]

Dear Till and Razvan,
A small clarification:
>Hence, for equational or first-order logic, you need dependent types.
Actually you don't *need* dependent types, it's customary to have
dependent types as they fit better with
the intuitionistic conception of FOL. But Martin Coen, for example,
implemented FOL with proof terms Curry-Howard compliant in Isabelle for
his thesis in 1992. I believe his FOL-with-terms (and no dependent
types)
logic was in the official distribution of Isabelle for several years,
but I don't know if it still is or not. 

Best,
Valeria

Dr Valeria de Paiva
PARC
3333 Coyote Hill Road
Palo Alto, CA 94304
USA


-----Original Message-----
From: flirts-bounces at informatik.uni-bremen.de
[mailto:flirts-bounces at informatik.uni-bremen.de] On Behalf Of Till
Mossakowski
Sent: Monday, August 22, 2005 3:22 AM
To: Razvan Diaconescu
Cc: FLIRTS
Subject: [Flirts] Curry-Howard for more complex logics

Dear Razvan,

> About Curry-Howard, I still want to ask you whether this is applicable
 > to things like equational logic, or even first order logic.

so far Joseph and I have written proposals for institutionalizing the
propositional part of Curry-Howard. I summarize the relevant features.
Note that we have a formal definition of all these features in the
institutional setting.

propositions       - types
proofs             - terms / functional programs

having true        - having singeltons
having false       - having the empty type
having conjunction - having pairing/projections (products) having
disjunction - having sum injections/case (coproducts) having implication
- having lambda abstraction (function spaces)

Now this can be extended as follows (with a bit of handwaving, I am not
an expert on this, the details need to be studied in the institutional
setting):

having propositional constants - having type constants having
quantification (over propositions) - having polymorphism having
(higher-order) functions (over propositions) -
                         having (higher-order) type constructors having
individuals and relations - having dependent types
   (dependent types also lead to the respetive quantifications etc.)
intuitionistic higher-order logic - having all of above

having not-not-elimination (being classic) - having call/cc
                                   (or \mu-abstraction) re-use of
subproofs - \tilde{\mu}-abstraction


Hence, for equational or first-order logic, you need dependent types.
It seems that then terms for individuals at the left hand side
correspond to terms for individuals at the right hand side, likewise for
function symbols, if one does not want to repesent them as relations
(i.e. dependent types). Equality is then a dependent type with some
inhabitants:

refl a : Eq a a
symm a b : Eq a b -> Eq b a
trans a b c : Eq a b * Eq b c -> Eq a c
cong a b : Eq a b -> Eq (f a) (f b)
or in the relational representation
cong a b : Eq a b * F a a' * F b b' -> Eq a' b'

Greetings,
Till
-- 
Till Mossakowski               Phone +49-421-218-4683
Dept. of Computer Science      Fax +49-421-218-3054
University of Bremen           till at tzi.de
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till
_______________________________________________
Flirts mailing list
Flirts at mail.informatik.uni-bremen.de
http://www.informatik.uni-bremen.de/mailman/listinfo/flirts