On the theorem $(p \cdot q) \supset (p \supset q)$

Question

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 $\&$), 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}} < 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.

Answer 1

"Theorem" in propositional calculus means a formula derivable form propositional axioms : see Nagel & 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))]$).

Answer 2

I suggest that you back up and work with a set of axioms in some propositional calculus and try to derive tautologies from that set of axioms. At the very least, I have found that I need to consistently invoke such theorems to prove much.

For instance, two common axioms are:

1. (p$\rightarrow$(q$\rightarrow$p))
2. ((p$\rightarrow$(q$\rightarrow$r))$\rightarrow$((p$\rightarrow$q)$\rightarrow$(p$\rightarrow$r)))

But, then I'll end up deriving (p$\rightarrow$(q$\rightarrow$(r$\rightarrow$q))) or

(p$\rightarrow$((q$\rightarrow$(r$\rightarrow$s))$\rightarrow$((q$\rightarrow$r)$\rightarrow$(q$\rightarrow$s))))

The former and the latter both have a "superfluous" reference to 'p' in terms of knowing them as true. However, both the former and the latter (up to re-lettering) seem rather difficult to avoid in axiomatic proofs.

In the axiom set for Principia Mathematica we have (~q$\lor$(p$\lor$q)) as an axiom, which has the same sort of superfluous reference. But, if we kept all of the other axioms the same and replaced (~q$\lor$(p$\lor$q)) with (~q $\lor$ q), we probably would end up with an axiom set which can't prove all tautologies under the same set of rules of inference.

Also, you ask this:

"Of all the ways one could obfuscate ∼q∨q, why this particular way?"

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

Except a theorem in a propositional calculus is a sequence of symbols derivable purely by the axioms using only the rules of the inference of the propositional calculus. Thus, a theorem is an object which has gotten recorded on a page. So, (~q V q) is a different theorem than ((∼p∨∼q)∨(∼p∨q)). And yes, I would call those two different theorems. I would also say that ((∼p∨∼q)∨(∼p∨q)) is one theorem and (∼p∨(∼q∨(∼p∨q))) is another theorem. I would also say that ((∼p∨∼q)∨(r∨q)) is a different theorem.

Answer 3

Formal logic is concerned with using mathematical techniques to build a mathematical model of mathematical reasoning itself, such that we can study the limits and potential of mathematical reasoning.

Like every mathematical model, the model formal logic builds deliberately ignores some facets of the thing being modeled, the better to focus on the facets that it does model. In particular, one of the aspects of mathematical reasoning that formal logic does not aim to model is the question "is what we're concluding here even interesting? Or useful?"

Questions like that are what in actual mathematics decides whether something is worth calling a "theorem". But logic doesn't care about them, and instead co-opts the word with a technical meaning instead:

In mathematical logic, "theorem" means something that has a valid proof. Nothing more, nothing less.

This is related to the use of "theorem" in actual mathematics, in that the intention is that the kind of claims that mathematicians in general call "theorems" ought to map to something within the formal model that have valid proofs. But not everything that has a valid proof is interesting enough to be called a theorem in real life. This distinction simply has to be learned.

The theorem (in the technical sense) you have found is a logical formula that would probably never appear in a formalization of an actual mathematical argument -- because, as you note, its intuitive meaning is convoluted and contains irrelevant details. However that doesn't mean that the formula cannot be a useful example for thinking about how the model works. We want to convince ourselves that everything the model says is a valid proof at least maps to a thought process where an actual mathematician would agree that the conclusion is true -- even though he may well point out that it's a boring truth.

(Note well that when logicians make claims about their model, they use the same words for them as mathematics in general. So stuff that happens on the metalevel gets to be called theorems, lemmas, corollaries, or random uninteresting facts, depending on interest and utility).

Answer 4

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.