I am new to natural deduction and upon reading about various methods online, I came across the rule of bottom-elimination in the following example.

enter image description here

I do not understand the step in line 10.

Upon inspection, my initial thought would be that the assumption of ¬p and p both being true is absurd, hence anything can be inferred ( in this case 'p'). However, if this were the case where would you stop (this seems to be an overly powerful tool)? So I assume that this idea is wrong.

Could someone help me understand the rule?

NOTE: I came to StackExchange due to the lack of resources and specific information online.

  • $\begingroup$ This strikes me as more appropriate for Mathematics. Perhaps it should be migrated there? $\endgroup$ – Yuval Filmus May 10 '20 at 6:34

Usually in practice we weld the two steps together and just say that from $p$ and $\lnot p$ anything follows, but in formal logic this is a combination of two rules of inference:

  1. $p$ and $\lnot p$ both together entail falsehood $\bot$,
  2. from $\bot$ anything follows.

These are precisely lines 9 and 10 in your proof.

We often take $\lnot p$ to be an abbreviation for $p \Rightarrow \bot$, in which case the rule "from $p$ and $\lnot p$ follows $\bot$" is just a special case of modus ponens "from $p$ and $p \Rightarrow r$ follows $r$".

  • $\begingroup$ Please excuse my lack of understanding, but for clarification, does step 2. of your answer imply that ANYTHING at all can be made true? If so, can't things that aren't true be made true just by assuming p and ¬p i.e. can't everything be made true by the repeated use of p & ¬p? $\endgroup$ – Newbie123 May 9 '20 at 16:47
  • $\begingroup$ Anything can be made true if you already proved or assumed $\bot$. And you cannot "repeatedly use $p$ and $\lnot p$" unless you already know that they are both true. $\endgroup$ – Andrej Bauer May 9 '20 at 16:49
  • $\begingroup$ In fact that is the whole point of rule 2: if you know something that is false (namely $\bot$) then you can conclude anything you like. The rule does not say "everything is true"! $\endgroup$ – Andrej Bauer May 9 '20 at 16:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.