importance of implication vs its tautology

Question

I'm self-taught in logic, started with programming. Texts stress the importance of the implication operator but I fail to see operator's importance. It was always intuitively clear that,

$$ p \rightarrow q \equiv \neg \ p \lor q $$

Keeping that in mind, my questions are:

• Does implication allow for additional rewrite rules or higher understanding in some form?
• Is sequent form, with its heavy use of implication rules, more "powerful" than nth-order logic with propositional syntax? Are there additional, or significantly simpler rewrite rules for some class of statements?
• The operator itself is counterintuitive, YMMV. Having the statement true in case the first operand is not, doesn't seem right or necessary at all. What am I missing?

I hope the question itself isn't too vague. I've hit these roadblocks in understanding of logic and haven't found answers in a long time.

Answer 1

This is a surprisingly interesting question. I think part of the reason for the confusion is that propositional logic is a kind of two-headed beast:

• On one hand, it is a system for calculating with the truth values "yes" and "no", digital logic and so forth. In this use it is also the prototypical example of a Boolean algebra (which ought to be a familiar word for someone coming from software).

• On another hand, propositional logic is commonly taught in mathematical-logic texts for the sole purpose of being a didactic stepping stone towards proof system for predicate logic, which is what mathematical logicians are interested in for the purpose of formalizing proofs in mainstream mathematics.

It so happens that in the first of these usages of propositional logic, you hardly ever see a $\to$. For these purposes, $\land$ and $\lor$ and $\neg$ (as well as, in some cases, XOR, NAND, NOR ...) serve us quite fine.

Where you do see $\to$ is in logic texts that are written with the ulterior motive of introducing quantifiers later on. This is because $\to$ is basically designed to be useful together with a quantifier: We can express, for example

All dogs are mammals

symbolically as $$ \forall x(\mathit{dog}(x) \to \mathit{mammal}(x)) $$

In this particular context the $\to$ makes better sense; together with $\forall$ it is part of a team that expresses that if we're looking at a dog, then implicitly we're also looking at a mammal.

It is technically convenient to split the "all A are B" into one part -- the $\forall$ -- that is about making universal claims in general and one part -- the $\to$ -- that helps formulating this particular kind of universal claim.

Once we have $\forall x$ that will allow us to express claims about more than one thing (perhaps an infinity of things) at once, what we need in order to get all the way to "all dogs are mammals" is to express: No matter what you're looking at, it will be either a dog and a mammal, or a non-dog mammal, or something that is neither a dog nor a mammal. If and only if it is true for everything in the world that it falls into one of those three classes, then it is true in general that all dogs are mammals.

The truth table for $\to$ is then what collects this potential-property-of-everything into a single uniform claim for each $x$ that we can apply our $\forall$ to.

The downside of this split is only that it makes it irresistable for textbook authors to present a flood of rules and exercises for this nice new connective before they introduce the $\forall$ -- but before we have $\forall$ there is no really good motivation for how $\to$ behaves in the first place, and attempts to explain it generally ends up as linguistic smoke and mirrors at best, or blantant arguments from authority at worst.

In summary: Once you put the $\to$ below a $\forall$ it makes perfect sense. If you don't have a relevant $\forall$ around the $\to$, the meaning often ends up counterintuitive and can only be understood simply by having accepted that this is the truth table we want.

Consider for example the drinker paradox:

$$ \exists x( p(x)\to\forall x(p(x)) $$

which is logically valid according to both the proof rules and the official semantics of predicate logic, but fails to make a lot of intuitive sense because the $\to$ has been written under an $\exists$ instead of under a $\forall$.

---

For completeness I should mention that there are some after-the-fact applications of propositional logic that fall into neither of the two broad categories above. One prominent example of this is the Curry-Howard correspondence between proof systems for propositional calculus (in particular for intuitionistic logic) and type systems for functional programming languages. Here the $\to$ connective achieves fundamental importance -- even though quantifiers are rarely around -- it is what turns out to correspond to function types on the type-system side of things.

Answer 2

It is interesting that you say that it is 'intuitively clear' to you that:

$p \rightarrow q \equiv \neg p \lor q$

but you also say that 'having the statement true when the first operand is not doesn't seem right'

since $\neg p \lor q$ is true whenever $p$ is not.

Anyway, here are some further equivalence rules for the conditional:

$\neg (p \rightarrow q) \equiv p \land \neg q$ (Negation Implication)

$p \rightarrow q \equiv \neg q \rightarrow \neg p$ (Contraposition)

$p \rightarrow (q \rightarrow r) \equiv (p \land q) \rightarrow r$ (Exportation)

$p \rightarrow (q \land r) \equiv (p \rightarrow q) \land (p \rightarrow r)$ (left Distribution $\rightarrow$ over $\land$)

$(p \lor q) \rightarrow r \equiv (p \rightarrow r) \land (q \rightarrow r)$ (right 'distribution' ... But not really since the $\lor$ becomes a $\land$)

Answer 3

The operator does seem counterintuitive, but it correctly captures what we mean by "if" in many cases. For example, "If we're out of milk, then I'll go to the store" isn't saying that I won't go to the store anyway if we have plenty of milk - we might be out of eggs. For a more mathematical example, "if $p$ is a prime greater than $2$, then $p$ is not even" is not making any claims about the parity of non-primes. It's certainly true that there are many cases in which we don't want this interpretation; "if I say 'run', run!" seems to mean that you shouldn't run if I don't tell you to. But the formalism of propositional logic doesn't allow us to change the interpretation of a connective by context, so we had to choose one. The one that was chosen, by convention, is the first interpretation.

As for why we use it: it's certainly true that it isn't necessary. Then again, $\vee$ isn't necessary either; by DeMorgan's laws we can make do with $\wedge$ and $\neg$. But additional symbols like $\vee$ and $\to$ vastly improve clarity (the meaning of $p \vee q$, for example, is much easier to understand than $\neg(\neg p \wedge \neg q)$). They also allow us to use new inference rules or equivalences - the rules governing $\vee$ and $\to$ are consequences of the rules for $\wedge$ and $\neg$, but it's much easier to use (for example) modus ponens rather than a huge chain of rules about negations and disjunctions.

So, to reiterate: $\to$ is not at all necessary, but it improves clarity and makes proofs much more convenient.