Introduction to Logic proof 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.
 A: 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

3) $\bot$ --- assumed [b]
4) $\lnot P$ --- from 3) by $\bot$-elim
5) $\bot$ --- from 2) and 4) by $\to$-elim

6) $\lnot \bot$ --- from 3) and 5) by $\to$-intro, discharging [b] ($\lnot \bot$ is $\bot \to \bot$)
7) $P \land \lnot \bot$ --- from 2) and 6) by $\land$-intro


=======


8) $\bot$ --- assumed [c] for $\lor$-elim
9) $P \land \lnot \bot$ --- from 8) by $\bot$-elim

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$. 
A: 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$$
A: Here is a proof of the result using a Fitch-style proof checker:


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