Currying and Uncurrying of logical formulas, is $(A \land B) \to C \leftrightarrow (A\to B)\to C$

Question

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"?

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$. — dtldarek, Jan 25 '13 at 13:16

score 7 · Accepted Answer · answered Jan 25 '13 at 13:02

7

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))$$

answered Jan 25 '13 at 13:02

PHL

262

score 5 · Answer 2 · answered Jan 25 '13 at 12:59

5

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.

answered Jan 25 '13 at 12:59

Ashot

4,753
3
34
61

Currying and Uncurrying of logical formulas, is $(A \land B) \to C \leftrightarrow (A\to B)\to C$

2 Answers2