# How do you prove law of excluded middle using tertium non datur?

I’m in my second year of an undergraduate philosophy degree. Last year we did classical logic (TFL and FOL truth tables and fitch style natural deductions). This year, one of the topics we are studying is intuitionistic logic.

Today, the lecturer said that intuitionistic logic does not contain tertium non dater (TND) as a rule because you can use TND to prove the law of excluded middle (LEM). Could somebody please post a natural deduction in which LEM is proved using TND? Would appreciate it if you used Fitch style natural deduction.

Apparently there are different names for the rule I am calling tertium non dater (TND), but what I mean is this rule:

|A (assumption).
|B (proved from A).

|not-A (Assumption).
|B (proved from not-A).

B (TND discharging assumptions)

• What do you mean with Tertium Non Datur ? It is the Latin name of Excluded Middle. – Mauro ALLEGRANZA Nov 7 '18 at 19:00
• Yes, I know this. However, I am using it to refer to the rule which I presented as a natural deduction in my OP. TND is just the name that my lecturer used for this rule. – Aprilpearl Nov 7 '18 at 19:06
• I also am confused. The TND rule is the LEM. – user20253 Nov 8 '18 at 11:39

1) A --- assumption [a]

2) A ∨ ¬A --- from 1) by ∨-intro

3) ¬A --- assumption [b]

4) A ∨ ¬A --- from 2) by ∨-intro

5) A ∨ ¬A --- from 1)-2) and 3)-4) using the rule called "TND", discharging [a] and [b].

Apparently there are different names for the rule I am calling tertium non dater (TND), but what I mean is this rule:

This is just disjunction elimination with an unstated invocation of LEM. If you have derived B from assumptions of A and not-A, then...

|A (assumption).
|B (proved from A).

|not-A (Assumption).
|B (proved from not-A).

A or not-A (LEM)

B (TND discharging assumptions)

So, you can use this to prove LEM by using disjunction introduction to derive A or not-A from each assumptions. But...