0

I am reading Rosser's Logic for Mathematicians, here ($P \supset Q$ means $P \rightarrow Q$):

enter image description here

If we have $P \supset Q$ and $P$ proved, how come we have $Q$ without having to use modus ponens? It's as If for such occasion, there are two ways. It's not clear what are these ways. I know what using modus ponens is, but this alternate way is completely mysterious to me.

Red Banana
  • 23,956
  • 20
  • 91
  • 192
  • Remember that at that point of the book, Rosser has not yet formalized the notion of "deduction" (derivation : $\vdash$). Thus, IMO, he is simply alluding to the transitivity of $\vdash$: if we have a derivation of $P$ from, say, some set of axioms/assumptions $\Gamma$, i.e. we have $\Gamma \vdash P$ and we have a deduction of $Q$ from $P$, i.e. $P \vdash Q$, we can conclude with $\Gamma \vdash Q$. – Mauro ALLEGRANZA Jun 05 '18 at 07:04

2 Answers2

3

He is saying if you have a deduction of $P$ and you also have a deduction of $Q$ from $P,$ then you can just concatenate those deductions into one long deduction of $Q.$ This won't use modus ponens. In fact, you never even deduce $P\to Q.$

  • What would be a deduction of $Q$ from $P$? We have that $P$ is true, and $Q$ is true because of $P$, isn't this the same as $P\rightarrow Q$? – Red Banana Jun 02 '18 at 04:32
  • In symbols, we might write that he is saying {P, (P $\vdash$ Q)} $\vdash$ Q. – Doug Spoonwood Jun 02 '18 at 04:32
  • No, "Q is true because of P" is not the same as (P$\rightarrow$Q). That's am object language formula. "Q is true because of P" is the meta-linguistic (P $\vdash$ Q). Or perhaps better (|= P $\vdash$ |= Q) – Doug Spoonwood Jun 02 '18 at 04:34
  • @DougSpoonwood I see. I knew there was something strange, and I heard about this distinction before, but I guess Rosser didn't mention it before in his book. – Red Banana Jun 02 '18 at 04:36
  • 1
    @BillyRubina The details of this are somewhat sensitive to the deductive system you're working in. Generally, if you can, starting from a premise $P,$ derive $Q,$ we write, as Doug said, $P\vdash Q.$ As a separate matter, the existence of such a deduction generally implies that we also can prove $P\supset Q$ (which would be written $\vdash P\supset Q,$ indicating it is proved unconditionally). This is usually a non-trivial theorem in Hilbert-style systems https://en.wikipedia.org/wiki/Deduction_theorem whereas it is a fundamental inference rule in natural deduction systems. – spaceisdarkgreen Jun 02 '18 at 04:41
  • Yes. What you guys told me seems to be far from trivial (up to the current page I am reading), is there any known reason why Rosser would put it so early? (Notice that I could be the case that he talked about it before in the book and I didn't catch). – Red Banana Jun 02 '18 at 04:50
  • @BillyRubina I haven't looked at this book before and I took a quick look. Yes it seems it's the first time the word 'deduction' is even mentioned in the book, although it is quite dense before that so it's possible something was said. I think he's (perhaps misguidedly) trying to inure the reader to some of the subtleties here. His example is nice: if you prove the contrapositive, then infer $A\supset B$ from that, then that is not the same thing structurally as assuming $A$ and proving $B,$ though both allow you to conclude $B$ if you have $A$ (but only the first needs MP) – spaceisdarkgreen Jun 02 '18 at 05:26
  • @BillyRubina (Actually I lied.. the first deduction will probably need MP in order to infer $A\supset B$ from the contrapositive, but this is something Rosser hedges as well.) – spaceisdarkgreen Jun 02 '18 at 05:34
0

Suppose we proved $(P⊃Q)$. Also, suppose that in proving $(P⊃Q)$, we knew that $P$ held true, and then deduced $Q$. Thus, $Q$ is true. We do NOT need to assume $(P⊃Q)$ and $P$ and use modus ponens to deduce $Q$. Instead, we can just assume $P$, since we know that $P$ is true, and thus deduce $Q$.

In symbols, if we assume $P$ and deduce $Q$ we can write,

$$P\vdash Q$$

That differs from modus ponens,

$$\{P, (P⊃Q)\} \vdash Q$$