Natural Deduction Rules 

A    B
------ [&I]
A & B

A & B
------ [&E1]
  A

A & B
------ [&E2]
  B

  A
------ [+I1]
A + B

  B
------ [+I2]
A + B

A + B  A ⊢ C  B ⊢ C
---------------------- [+E]
          C

A => B    B => A
-----------------[<=>I]
     A <=> B


A <=> B
----------[<=>E1]
A => B

A <=> B
----------[<=>E2]
B => A

A ⊢ B
----------[=>I]
A => B

A   A =>B
---------[=>E]
  B

A |- F
--------[-I]
  -A

A    -A
-------[-E]
   B

 F
---- [Efq]
 A 

-- A
------- [Raa]
   A

The conjunction is written &, the disjonction is written +
I = introduction, E = elimination,
=>E = modus ponens,
Efq = ex falso quodlibet, Raa = reductio ad absurdum

examples | rules | formulas syntax | proofs definition | info | download | home Last Modified : 23-Feb-2023