I hope it is the right choice to put this on math.SE and not SO.
I am trying to wrap my head around Curry-Howard correspondence for first order logic. It seems convenient to consider FOL with identity. I am aware that it is no proper weakening to consider FOL without identity, for I can add the axioms of identity
-- define a predicate Eq (binary): data Eq a b = Eq a b -- the reflexivity axiom corresponds to a function of type -- (recall that all free variables are implicitly universally -- quantified over) ref :: Eq a a -- so why not choose ref = undefined undefined
And similarly for transitivity. Can someone confirm that this is the way to go?
Now for every predicate $P$ (and also every function symbol) I encounter in my alphabet, I have to add an axiom $a=a' \to P a b c \to P a' b c$ (here, for ternary $P$).
However, it might get quite clumsy to write these down… To do this in Haskell, I guess I'd have to do
-- define a predicate P (ternary) data P a b c = P a b c -- The statement a=a' -> (P a b c -> P a' b c) -- corresponds to a function eq1 :: Eq a a' -> P a b c -> P a' b c -- so we chose eq1 (Eq x x') (P x'' y z) = P x'' y z
and similarly for $b=b' \to P a b c \to P a b' c$ etc. If I have plenty of predicates and functions, this will get quite messy. Is there a better way to treat identity?
Here, it gets even worse. What do functions correspond to? Kinds? If so, as an equivalent of $a=a' \to f a = f a'$ (for an unary function $f$) we'd probably want a function of type
F :: * -> * => Eq a a' -> Eq (F a) (F a')
What I have written down corresponds a SOL expression (since we quantify over the function $f$). Instead, for each particular function $f$ we have to do:
-- Take some type of some kind, e.g. F = Maybe :: * -> * -- To state that a = a' implies F a = F a' we need a function funeq :: Eq a a' -> Eq (Maybe a) (Maybe a') funeq (Eq x x') = Eq (Just x) (Just x')
This is my no means elegant. Do you have any suggestions to do this in a better way?