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 : 27-Feb-2023