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:

    (p ∧ q) β†’ r ↔ p β†’ (q β†’ r)

    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 Pand 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

    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

    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, ¬φ ∨ ψ ≑ Ο† β†’ ψ

PreviousDisjunctive syllogismNextimplication-elimination

Last updated

Was this helpful?