// laws and rules · Logical equivalence
Exportation law_
The exportation law states that “if p and q, then r” is equivalent to “if p, then (if q, then r)”. The formula ((p ∧ q) ⇒ r) ⇔ (p ⇒ (q ⇒ r)) is a three-variable tautology. It turns several hypotheses into a chain of conditionals and is the logical version of currying in functional programming.
Example
((p ∧ q) ⇒ r) ⇔ (p ⇒ (q ⇒ r))
What the variables mean
- ▸ p: “You have a ticket”
- ▸ q: “You arrive before 8”
- ▸ r: “You may enter”
In plain words
“If you have a ticket and arrive before 8, you may enter” is equivalent to “if you have a ticket, then if you arrive before 8, you may enter”.
Truth table
| p | q | r | p ∧ q | (p ∧ q) ⇒ r | q ⇒ r | p ⇒ (q ⇒ r) | ((p ∧ q) ⇒ r) ⇔ (p ⇒ (q ⇒ r))★ |
|---|---|---|---|---|---|---|---|
| T | T | T | T | T | T | T | T |
| T | T | F | T | F | F | F | T |
| T | F | T | F | T | T | T | T |
| T | F | F | F | T | T | T | T |
| F | T | T | F | T | T | T | T |
| F | T | F | F | T | F | T | T |
| F | F | T | F | T | T | T | T |
| F | F | F | F | T | T | T | T |
Classification: Tautology · 8 rows
Statement
((p ∧ q) ⇒ r) ⇔ (p ⇒ (q ⇒ r)). Exporting means pulling one hypothesis out of the antecedent and turning it into a nested conditional; importing is the reverse.
With three variables the table has 8 rows.
Why it is a tautology: reading the table
The left side (p ∧ q) ⇒ r is F only when p = T, q = T and r = F. The right side p ⇒ (q ⇒ r) is F only when p = T and q ⇒ r is F, i.e. q = T and r = F. It is exactly the same row.
In the other seven rows both sides are T: if p or q is F, the left antecedent is F and on the right either p is F or q ⇒ r is T. And if r = T both implications are T. The columns coincide.
How it is used in proofs
It justifies proving a theorem with several hypotheses by assuming them one at a time: to prove p ⇒ (q ⇒ r) we assume p, then assume q and derive r, the same as assuming p ∧ q at once.
In the lambda calculus and functional languages, a two-argument function f(p, q) = r is curried into p ↦ (q ↦ r); exportation is its logical counterpart via the Curry–Howard correspondence.
Examples
Programming: `if (a && b) { run(); }` is equivalent to `if (a) { if (b) { run(); } }`. Compilers rely on this equivalence for `&&` short-circuiting.
Mathematics: “if n is even and n > 2, then n is not prime” can be stated as “if n is even, then if n > 2, n is not prime”.
Relation to other laws
It is proved with material implication and De Morgan: (p ∧ q) ⇒ r ⇔ ¬(p ∧ q) ∨ r ⇔ ¬p ∨ ¬q ∨ r ⇔ ¬p ∨ (q ⇒ r) ⇔ p ⇒ (q ⇒ r).
It underlies the hypothetical syllogism: chaining implications amounts to exporting intermediate hypotheses.
Try it yourself
Edit the expression in the calculator and watch how every step of the table changes.
Open in the calculator →Related operators
Frequently asked questions
What does it have to do with currying? ▼
A function taking (p, q) and returning r is equivalent to a function taking p and returning another function that takes q and returns r. Exportation is the same idea for propositions.
Does it work with more than two hypotheses? ▼
Yes: (p ∧ q ∧ s) ⇒ r is equivalent to p ⇒ (q ⇒ (s ⇒ r)) by applying the law repeatedly.
Why does the table have 8 rows? ▼
Because there are three variables (p, q, r) and 2³ = 8 combinations.