Exportation (logic)

Formal notation

The exportation rule may be written in sequent notation:

where is a metalogical symbol meaning that is a syntactic equivalent of in some logical system;

or in rule form:

,

where the rule is that wherever an instance of "" appears on a line of a proof, it can be replaced with "" and vice versa;

or as the statement of a truth-functional tautology or theorem of propositional logic:

where , , and are propositions expressed in some logical system.

Natural language

Truth values

At any time, if P→Q is true, it can be replaced by P→(P∧Q).
One possible case for P→Q is for P to be true and Q to be true; thus P∧Q is also true, and P→(P∧Q) is true.
Another possible case sets P as false and Q as true. Thus, P∧Q is false and P→(P∧Q) is false; false→false is true.
The last case occurs when both P and Q are false. Thus, P∧Q is false and P→(P∧Q) is true.

Example

It rains and the sun shines implies that there is a rainbow.
Thus, if it rains, then the sun shines implies that there is a rainbow.

Relation to functions

Exportation is associated with Currying via the Curry–Howard correspondence.

References

0.011721