Proof of $\bot \Rightarrow p$

Question

I am asked to prove that $\bot \Rightarrow p$.

Of course, this is trivially true from the definition of a valuation, regardless of the value of $p$.

However it seems to me that this is 'jumping out of the system'. I interpreted 'proof' in this question as a formal proof, i.e. a finite sequence of propositions $t1,t2,...tn$, each of which is either a)an axiom, b)in the set of premises S, which here is the empty set, c) is such that if $\exists j,k <i$ s.t. $t_j=t_k \Rightarrow t_i$ then we have $t_i$. Essentially, modus ponens. Then each of the proportitions $t_i$ is true.

The axiom schemes are the sets of tautologies:

• $p \Rightarrow (q \Rightarrow p))$ $\\ \ \ \ \ \forall p,q \in L$
• $p \Rightarrow (q \Rightarrow r)) \Rightarrow ((p\Rightarrow q) \Rightarrow (q \Rightarrow r)$ $\\ \ \ \ \ \forall p,q,r \in L$
• $\neg \neg p \Rightarrow p$ $\ \ \ \ \forall p \in L$

However I have been messing around with the axioms and cannnot seem to get this to work. And in fact, I don't think it is possible to prove this 'within the system', precisely because the axioms are for general symbols, and if you were to replace $\bot$ by one of these, clearly $p\Rightarrow q$ is not generally true for any $p,q$. i.e. I think we have to explicitly use the information about the valuation. Is this an implicit axiom then?

EDIT: I see now that for the third axiom to hold for arbitrary $q\in L$, we need $\bot $ to be false (at least, provided that there is at least one otherwise false $p$)

Answer 1

We have to assume the abbreviation $¬p =_{\text {def}} p → \bot$.

If so :

1) $\bot$ --- assumed

2) $\vdash \bot \to ((p \to \bot) \to \bot)$ --- Ax.1

3) $(p \to \bot) \to \bot$ --- from 1) and 2) by MP

4) $\lnot \lnot p$ --- from 3) by abbreviation

5) $p$ --- from 4) and Ax.3 by MP.

Answer 2

You are correct that these are two fundamentally different types of argument in logic. To attach some vocabulary to it, you have been engaging in syntactical reasoning up to this point, simply treating $\neg$ and $\Rightarrow$ as meaningless symbols that can be manipulated only as the axioms and rules of inference allow. By contrast, semantic reasoning ties those symbols to the notions of negation and implication and we can investigate whether the propositions we've been developing syntactically can be used as a model for rhetorical reasoning.

So, you're faced with the challenge that you've been asked to prove that $\bot\Rightarrow p$. You certainly won't be able to prove $q\Rightarrow p$ in your system (since SPOILER WARNING propositional logic is consistent), so $\bot$ isn't an arbitrary literal. But if the symbol hasn't been defined in the system, then you are formally unable to reason with it until you are given either a definition or an axiom that describes how it can be used in the system.