Conjunction and Implication

Theorems

Conjunction Equivalent to Negation of Implication of Negative

Formulation 1

$p \land q \dashv \vdash \neg \paren {p \implies \neg q}$

Formulation 2

$\vdash \paren {p \land q} \iff \paren {\neg \paren {p \implies \neg q} }$

Implication Equivalent to Negation of Conjunction with Negative

Formulation 1

$p \implies q \dashv \vdash \neg \paren {p \land \neg q}$

Formulation 2

$\vdash \paren {p \implies q} \iff \paren {\neg \paren {p \land \neg q} }$

Conjunction with Negative Equivalent to Negation of Implication

Formulation 1

$p \land \neg q \dashv \vdash \neg \paren {p \implies q}$

Formulation 2

$\vdash \paren {p \land \neg q} \iff \paren {\neg \paren {p \implies q} }$

Modus Ponendo Tollens

Formulation 1

$\neg \left({p \land q}\right) \dashv \vdash p \implies \neg q$

Formulation 2

$\vdash \paren {\neg \paren {p \land q} } \iff \paren {p \implies \neg q}$

Law of Excluded Middle

Note that the Modus Ponendo Tollens:

$\neg \paren {p \land q} \dashv \vdash p \implies \neg q$

can be proved in both directions without resorting to Law of Excluded Middle.

All the others:

$p \land q \vdash \neg \paren {p \implies \neg q}$

$p \implies q \vdash \neg \paren {p \land \neg q}$

$p \land \neg q \vdash \neg \paren {p \implies q}$

are not reversible in intuitionistic logic.

Also see

• Negation of Conditional implies Antecedent‎
• Negation of Conditional implies Negation of Consequent‎