Constructive Implication ⇒.

Costructive implication A⇒B is different from material implication A→B, and equivalent to A→B only if we have full Classical Logic. ``A⇒B'' means: ``if we assume that A is true, then B is true''. When we use material implication A→B, we do not include A⇒B in our language. However, when we include constructive implication A⇒B in our language, we include A→B, too, and interpret A⇒B as a conjunction whose only immediate subformula is A→B. This subformula relation is used only in constructive reasoning, and superflous in most cases: usually, we can identify A⇒B with A→B. However, there are a few constructive reasoning using nested implication in an essential way, which cannot be faithfully interpreted in the game semantic without using the intermediate subformula A→B.

Created by Mathematica  (October 17, 2006)