3

I have to prove $P \land\lnot\bot$ with the following assumption:

$$P \lor \bot$$

I have never seen the contradiction sign in a line not being by itself before, so I am not sure how to go forward. I'm assuming I won't be able to use Fitch? It doesn't really seem to respond well to the contradiction sign in combination with other variables in a line.

Appreciating all the help I can get.

k170
  • 9,045
John Snoe
  • 313

3 Answers3

4

I'll use Natural Deduction for the derivation (you can easily translate it into a Ficht-style one).

We need $\lor$-elimination

1) $P \lor \bot$ --- premise

2) $P$ --- assumed [a] for $\lor$-elim

<blockquote>
  <p>3) $\bot$ --- assumed [b]</p>

  <p>4) $\lnot P$ --- from 3) by $\bot$-elim</p>

  <p>5) $\bot$ --- from 2) and 4) by $\to$-elim</p>
</blockquote>

<p>6) $\lnot \bot$ --- from 3) and 5) by $\to$-intro, discharging [b] ($\lnot \bot$ is $\bot \to \bot$)</p>

<p>7) $P \land \lnot \bot$ --- from 2) and 6) by $\land$-intro</p>

=======

8) $\bot$ --- assumed [c] for $\lor$-elim

<p>9) $P \land \lnot \bot$ --- from 8) by $\bot$-elim</p>

10) $P \land \lnot \bot$ --- from 2)-7) and 8)-9) and 1) by $\lor$-elim, discharging [a] and [c].

If we assume classical logic, things are simpler ...

In classical logic, $\lnot P \to Q$ is equivalent to $P \lor Q$, and $P \land \lnot Q$ is equivalent to $\lnot (P \to Q)$.

Thus, we can rewrite the premise as : $\lnot P \to \bot$, which is equivalent to : $\lnot \lnot P$.

The conclusion in turn is equivalent to : $\lnot (P \to \bot)$, which is again $\lnot \lnot P$.

Mauro ALLEGRANZA
  • 94,169
1

The symbol for contradiction can be substituted with $0$ or $\mbox{false}$. This comes from the law of non-contradiction, which is the second of the three classic laws of thought. So now we have $$ p\lor\bot\equiv p\lor\mbox{false}\equiv p$$ And $$ p\land\lnot\bot \equiv p\land\lnot\mbox{false} \equiv p\land\mbox{true}\equiv p$$ Therefore $$ p\lor\bot\equiv p\land\lnot\bot$$

k170
  • 9,045
0

Here is a proof of the result using a Fitch-style proof checker:

enter image description here

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

Frank Hubeny
  • 1,527
  • It's cleaner with a proof by cases dirrectly from the premise, as Mauro suggested. We can derive $P\land\lnot\bot$ from the premise of $P\lor\bot$; because on assuming $P$ we may derive $P\land\lnot\bot$ since $\bot$ cannot be true, while on assuming $\bot$ we may derive $P\land\lnot\bot$ by explosion. – Graham Kemp Aug 02 '19 at 03:09
  • $$\small\def\fch#1#2{\quad\begin{array}{|l}#1\\hline#2\end{array}}\fch{1.~P\lor\bot}{\fch{2.~P}{\fch{3.~\bot}{}\4.~\lnot\bot\qquad\quad\lnot~{\sf I}~3{-}3\5.~P\land\lnot\bot\quad\land{\sf I}~2,4}\\fch{6.~\bot}{7.~P\land\lnot\bot\quad~\text{EFQ}~6}\8.~P\land\lnot\bot\qquad~~\lor{\sf E}~1,2{-}5,6{-}7}$$ – Graham Kemp Aug 02 '19 at 03:09
  • Ah, $EFQ$ is called $X$ (for eXplosion, or $\bot E$ under Rules for Cambridge). – Graham Kemp Aug 02 '19 at 03:18