# Exportation

<https://en.wikipedia.org/wiki/Exportation_(logic>)

Exportation is a valid *rule of replacement* in propositional logic. The rule allows conditional statements having conjunctive antecedents to be replaced by statements having conditional consequents and vice versa in logical proofs.

```
(p ∧ q) → r ⇔ p → (q → r)
```

where ⇔ is a metalogical symbol representing "can-be-replaced-with" relation.

* Exportation is associated with **currying** via the *Curry-Howard correspondence*.

The logical conjunction, `a ∧ b`, is translated to to the type theory as product type, and the canonical form of product types is a pair or 2-tuple, i.e. `(a, b)`. In the set theory, this is represented by the Carthesian product between two sets, `A×B`.

```
logic       sets        types
a ∧ b       A×B         (a, b)
a → b                   a -> b

(a ∧ b) -> c <=> a -> (b -> c)
  A × B -> C <=> A -> B -> C
 (a, b) -> c <=> a -> b -> c

f :: (a, b) -> c
g :: a -> b -> c
```

* The exportation rule may be written in sequent notation where the symbol `⊣⊢` replaces `⇔` from above. The symbol `⊣⊢` is a metalogical symbol meaning that the LHS is a syntactic equivalent of the RHS in some logical system.
* The exportation rule may be written in rule form:

  \`\`\` (p ∧ q) → r p → (q → r)

p → (q → r) (p ∧ q) → r

\`\`\` where the rule is that wherever an instance of one appears on a line of proof, it may be replaced by the instance of the other, and vice versa.

* The exportation rule may be written as the statement of a truth-functional tautology or theorem of propositional logic:  &#x20;

  (p ∧ q) → r ↔ p → (q → r)   &#x20;

  where P, Q, R are propositions expressed in some logical system.

At any time, if `P → Q` is true, it can be replaced by `P → (P ∧ Q)`

* One possible case is when both `P`and `Q` are true; thus `P ∧ Q` is also true, and `P → (P ∧ Q)` is true.
* Another possibility is when P=false and Q=true, then `P ∧ Q` is false and&#x20;

  `P → (P ∧ Q)` is false, which means the overall expr is true.
* The last case is when both P and Q are false; so, `P ∧ Q` is false and&#x20;

  `P → (P ∧ Q)` is true.

## Proof

p → (q → r) ==> (p ∧ q) → r

| Proposition   | Derivation                           |
| ------------- | ------------------------------------ |
| p → (q → r)   | Given proposition                    |
| ¬p ∨ (q → r)  | Material implication, φ → ψ ≡ ¬φ ∨ ψ |
| ¬p ∨ (¬q ∨ r) | Material implication, φ → ψ ≡ ¬φ ∨ ψ |
| ¬p ∨ ¬q ∨ r   | Associativity of ∨                   |
| ¬(p ∧ q) ∨ r  | De Morgan's law, ¬φ ∨ ¬ψ ≡ ¬(φ ∧ ψ)  |
| (p ∧ q) → r   | Material implication, ¬φ ∨ ψ ≡ φ → ψ |


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://mandober.gitbook.io/math-debrief/300-logic/logic-inference/exportation.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.