Constructive Proof of Material Implication

[Hugo Ferreira]

Hi,

I'm struggling to find a constructive proof (through natural deduction) of the material implication replacement rule (i.e., that (a => b) <=> (~a \/ b). I believe the only possible way would be through contradiction, but I can't seem to get to it. Is it even possible?

Thx.

[JSuarez]

IF by "constructive proof" in a natural deduction system you mean a proof using only intuitionistic rules, then it's not possible: the implication

\left(p\rightarrow q\right)\rightarrow\left(\neg p \vee q\right)

is not intuitionistically valid, whereas the reverse one:

\left(\neg p \vee q\right)\rightarrow\left(p\rightarrow q\right)

is, so this one may be proved only with intuitionistic rules.

The first implication is only classically valid, so its proof must use a non-intuitionistic rule, like

\Phi,\neg\alpha\vdash\bot \Rightarrow \Phi\vdash\alpha