0
$\begingroup$

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?

Predicates

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?

Functions

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?

$\endgroup$
0
$\begingroup$

For Curry-Howard correspondence, the $Eq a b$ data type is not sufficient to prove equality. Maybe you should compare the two elements before concluding they are equal? Notice this requirement means $a = b$ as types. Notice for each statement that you prove, you should produce a certificate of proof under Curry-Howard correspondence in such way that programs (in Haskell) correspond to specific proofs. This means types describe the claims proven, and validity under the type checker should describe validity of proofs.

$\endgroup$
1
  • $\begingroup$ After having slept over it, I feel deeply dissatisfied with ref = ⟂ ⟂, but for another reason: When types correspond to logical formulae and proofs correspond to providing a function, what do variables, predicates and functions correspond to? $\endgroup$ – Bubaya Mar 1 '20 at 12:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.