4
$\begingroup$

With a truth table its easy to see that the two formulae $A\land B \to C$ and $A \to B \to C$ are not equivalent, for example, if $A = B = C = 0$, than the first evaluates to $1$ and the second to $0$ (because $A \to B$ is truth, and then $(A\to B) \to C$) is false).

But here

How do I memorize axioms of a Hilbert system?

it is referred to this transformation as currying, and there

http://www.daimi.au.dk/~ko/teaching/pl/curryhoward.pdf

on page 9 it is stated that

  • Curry and Uncurry are proofs of $$\forall P,Q,R. (P \land Q) \to R \leftrightarrow (P \to Q \to R)$$

So i am confused, when are these expressions equivalent, and if not how can I use them for "uncurrying"?

$\endgroup$
2
  • 1
    $\begingroup$ Right arrows like $\to$ or $\implies$, etc., are usually right-associative, that is $A \to B \to C$ means $A \to (B \to C)$, not $(A \to B) \to C$. $\endgroup$
    – dtldarek
    Jan 25, 2013 at 13:16
  • $\begingroup$ Huh? C is not equivalent to (A->B). $\endgroup$ Jan 25, 2013 at 13:23

2 Answers 2

7
$\begingroup$

The devils is hidden in details. Be careful with parenthesis (and conventions about them).

Indeed, it's true that

  • Curry and Uncurry are proofs of $$\forall P,Q,R. (P \land Q) \to R \leftrightarrow (P \to (Q \to R))$$
$\endgroup$
5
$\begingroup$

I think $P \to Q \to R$ means $P \to (Q \to R)$ but not $(P \to Q) \to R$.

$(A \land B) \to C \leftrightarrow A\to (B\to C)$ is true.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .