Thread: Excluded middle

Hi all,

Could anyone please explain what an excluded middle from the following derivation is?

Many thanks

ssharish

The excluded middle is an axiom schema . This means that A can be replaced by any formula to get an axiom. Equivalently, it is an inference rule with no assumptions.

I should add that the law of excluded middle is just a name for formulas of the form . It does not automatically mean that it has to be used as an axiom. In fact, in natural deduction it is usually derivable using the inference rule of double-negation elimination. Pure natural deduction does not have axioms.