On the theorem $(p \cdot q) \supset (p \supset q)$ In the book Gödel's Proof, by Nagel and Newman, the authors write (p. 119):


  There is a theorem in logic which reads:
  $$(p \cdot q) \supset (p \supset q)$$
  
  or when translated, 'If both $p$ and $q$, then (if $p$ then $q$)'.


As the authors' translation at the end of the quote shows, they use $\cdot$ to denote logical conjunction (aka $\wedge$ or $\&amp;$), and $\supset$ to denote implication (aka $\Rightarrow$).  Furthermore, elsewhere in the text, they use $\sim$ for logical negation (aka $\lnot$), and the $\vee$ for logical disjunction.  To minimize confusion, I will adopt the authors' notation for the rest of this post.

If I convert the implications to disjunctions, the theorem becomes

$$ \sim\! (p \cdot q) \vee (\sim\! p \vee q)$$

...and applying de Morgan's law to the first disjunct above, we are left with

$$ \sim\! p \; \vee \sim\! q\; \vee \sim\! p \vee q $$

This is clearly a tautology, but the role of $p$ in the whole thing seems to me entirely superfluous.  In other words, the theorem here looks to me like an unnecesarily cluttered rendition of $\sim\! q \vee q$. 

I find this very confusing.

Part of my confusion stems from two senses of the word "theorem".  For example, according to one of these senses, the equation

$$139 - 31 = 3^3 \times 2^2$$

is "a theorem of number theory", but according to the other sense it isn't, since nobody calls this equation "a theorem of number theory"; that designation is reserved to things like "The Infinitude of Primes", "Fermat's Last Theorem", "The Chinese Remainder Theorem", etc.

I am left wondering which of the two senses of "theorem" did Nagel and Newman intend when they described $(p \cdot q) \supset (p \supset q)$ as "a theorem in logic".

Either way, why invoke a theorem that includes a clearly superfluous reference to $p$?  Or to put it differently, why invoke such an obfuscated form of $\sim\! q \vee q$?  It's as if, in a number theory proof, one were to invoke the "theorem"


  Either there are infinitely many primes or $\pi^{\sqrt {2.6 + e}} &lt; 1\frac{3}{32}$.


It is true, but why would anyone bother to use such a thing in a proof?

Clearly I'm missing the authors' point, and would appreciate a cluebrick or two.
"Theorem" in propositional calculus means a formula derivable form propositional axioms : see Nagel &amp; Newman, page 49 for the propositional axioms used into Principia Mathematica.

The axiom may vary but we want that they are enough to derive all tautologies usung the modus ponens rule of inference (see page 54).

A theorem is number theory is a formula expressible in the language of arithmetic that is derivable from the axioms of logic and the specific axioms of arithmetics : Peano's axioms.

Consider the tautology $p ∨ ¬p$, which is derivable from logical axioms alone. 

We have that $∀x(x=0) ∨ ¬∀x(x=0)$ is a theorem of arithmetic because we can derive it from axioms (in this case without using the specific arithmetical ones).

Of course, we need the specific arithmetical axioms to derive more "interesting" arithmetical theorems, like e.g. commutativity of $+$.



The formula in page 119 is used in the context of the formalization of Euclid's argument.

It is used to derive from the intermediate result : (6) $Pr (x) \land (\exists z) [Pr (z) \land Gr (z, x)]$ the final arithmetical theorem : (7) $(x) [Pr (x) \to (\exists z)(Pr (z) \land Gr (z, x))]$. 

Thus, the authors use the tautology : $(p \land q) \to (p \to q)$ and modus ponens (the Rule of Detachment) to derive from (6) :


  (6') $Pr (x) \to (\exists z)[Pr (z) \land Gr (z, x))]$


and then "generalize" it to get (7).

The gist of the example is to produce an "exercise in formalization" : in the context of a standard mathematical proof, having proved that ‘$x$ is a Prime and there is at least one other Prime $z$ such that $z$ is Greater than $x$’ ( i.e. $Pr (x) \land (\exists z) [Pr (z) \land Gr (z, x)]$) it is enough to conclude, without further steps, that ‘for every $x$, if $x$ is Prime, then there is at least one other Prime $z$ that is greater than $x$’ ( i.e. $(x) [Pr (x) \to (\exists z)(Pr (z) \land Gr (z, x))]$).
I am left wondering which of the two senses of "theorem" did Nagel and Newman intend when they described $(p \cdot q) \supset (p \supset q)$ as "a theorem in logic".


This statement corresponds to usual first row of the truth table for implication: If  the antecedent and consequent are both true, then the implication is true. It is theorem that can be derived using only (1) a premise rule to introduce assumptions, (2) a conclusion rule to discharge assumptions and (3) a rule to eliminate conjunctions. See my formal proof.