# Proof $p \vdash q \Rightarrow p$

Firstly, how do I read it? Is below right? With braces

$$p \vdash (q \Rightarrow p)$$

The given proof is:

1. ${p}$, premise
2. ${q}$, assumption
1. $p$ by (1) // what???
3. ${q} \Rightarrow p$ by implication introduction with 2 and 2.1 QED...

I can't really get the link between $p$ and $q$ in 2.1 ...

-
What's your formal system? What rules of inference and axioms do you have? –  Doug Spoonwood Sep 28 '12 at 15:01
Doesn't $p \vdash (q \implies p)$ mean $(p \land q) \implies ( p \land p )$? –  xavierm02 Sep 28 '12 at 16:26

The point of the claim is that there is no link between $p$ and $q$ in 2.1. Once $p$ is a premise, anything implies $p$, because an implication can only be false if its consequent is false.

-
"[A]n implication can only be false if its consequent is false." I wonder if you really believe that! :-) Do you really think, e.g. that Gödel's Incompleteness Theorem implies Fermat's Last Theorem? Or wouldn't you, in ordinary mathematical chat, in fact distinguish a genuine implication relation from the material conditional (which is what is in play here)?? –  Peter Smith Sep 28 '12 at 18:51
Of course I don't believe that every English statement of the form, for instance "foo is true because bar" is true whenever "foo" is. Nor does my claim hold in various modern logics. I'm personally not picky about using the word "implication" for formal sentences including arrows when the context, as now, is clear. –  Kevin Carlson Sep 28 '12 at 20:11

There doesn't have to be any intuitive connection. If you can somehow derive $p$ after (not necessarily because) you assume $q$, then you're allowed to conclude $q\Rightarrow p$.

In this case, $p\vdash\cdots$ means that you're explicitly allowing yourself to prove $p$ from nothing. Then you can also prove $q\Rightarrow p$.

-

Many/most systems of natural deduction for classical (non-relevantist) logic allow (i) reiteration, and also (ii) unrestricted discharge of assumptions -- so we are allowed to write

1. $p\quad\quad\quad$ Premiss
2. $\quad|\quad q\quad$ Supposition
3. $\quad|\quad p\quad$ From (1), by reiteration
4. $q \to p\quad\$ Conditional Proof, by proof from (2) to (3)

There is indeed no 'link' between $p$ and $q$ at step (3). But that isn't needed at step (4), in most systems. The CP rule is: given a sub-proof starting from $A$ and concluding $B$ we can discharge the assumption $A$ and infer $A \to B$ (on the remaining assumptions/premisses). We don't, in typical classical systems, have to check that the assumption $A$ is actually invoked in getting to $B$.

Does that mean we shouldn't like reiteration and/or should restrict discharge? Well, actually that wouldn't much affect things in the presence of other standard rules. Thus consider the proof

1. $p\quad\quad\quad\quad$ Premiss
2. $\quad|\quad q\quad\quad$ Supposition
3. $\quad|\quad p \land q\quad$ From (1), (2)
4. $\quad|\quad p\quad\quad$ From (3)
5. $q \to p\quad\quad\$ Conditional Proof, by proof from (2) to (4)

And now $q$ is invoked en route to getting to line (4).

-
Another method involving a natural deduction system would involve invoking p as another supposition (note all suppositions have scope) as follows. 1. p [premise], 2. | q [supposition] 3. || p [premise] 4. | (p->p) [3-3 conditional introduction] 5. |p [1., 4. conditional elimination] 6. (q->p) [2.-5. conditional introduction] –  Doug Spoonwood Sep 28 '12 at 15:08