Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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 ...

share|cite|improve this question
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
up vote 5 down vote accepted

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.

share|cite|improve this answer
"[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$.

share|cite|improve this answer

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).

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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