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  [=>I] A => B 
A A => B  [=>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
In addition to these rules, we define the negation and the equivalence by
A = A => F
A <=> B = (A => B) & (B => A)
In a proof, one can replace every Formula by an other Formula equal when we replace the Negations and
the Equivalences by their Definitions.
examples  rules  syntax  info  download  home  Last Modified : 27Feb2023 