Exportation
is a
valid rule of replacement
In logic, a rule of replacementMoore and Parker is a transformation rule that may be applied to only a particular segment of an logical expression, expression. A logical system may be constructed so that it uses either axioms, rules of inference ...
in
propositional logic. The rule allows
conditional statements having
conjunctive
The subjunctive (also known as conjunctive in some languages) is a grammatical mood, a feature of the utterance that indicates the speaker's attitude towards it. Subjunctive forms of verbs are typically used to express various states of unreality s ...
antecedents to be replaced by statements having conditional
consequents and vice versa in
logical proofs. It is the rule that:
Where "
" is a
metalogical
symbol
A symbol is a mark, sign, or word that indicates, signifies, or is understood as representing an idea, object, or relationship. Symbols allow people to go beyond what is known or seen by creating linkages between otherwise very different conc ...
representing "can be replaced in a proof with." In strict terminology,
is the law of exportation, for it "exports" a proposition from the antecedent of
to its consequent. Its converse, the law of importation,
, "imports" a proposition from the consequent of
to its antecedent.
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
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...
;
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
In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of th ...
of propositional logic:
:
where
,
, and
are propositions expressed in some
logical system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...
.
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.
If my car is on, when I switch the gear to D the car starts going.
If my car is on and I have switched the gear to D, then the car must start going.
Proof
The following proof uses
material implication,
double negation
In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition ''A'' is logically equivalent to ''not (not ...
,
De Morgan's laws, the negation of the conditional statement, the
associative property
In mathematics, the associative property is a property of some binary operations, which means that rearranging the parentheses in an expression will not change the result. In propositional logic, associativity is a valid rule of replacement ...
of conjunction, the negation of another conditional statement, and double negation again, in that order to derive the result.
Relation to functions
Exportation is associated with
currying
In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments into evaluating a sequence of functions, each with a single argument. For example, currying a function f that ...
via the
Curry–Howard correspondence
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relati ...
.
References
{{Reflist
Rules of inference
Theorems in propositional logic