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  AC  BC
	------------------- [+E]
                C
      
	A ⊢ B
	------- [=>I]
	A => B
      
	AB   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
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 | formulas syntax | proofs definition | info | download | home Last Modified : 23-Feb-2023