Definition of $\lnot P$ versus treating it as an inference rule?

Question

I sometimes see people say that $\lnot P$ can be defined as shorthand via $\lnot P := P \to \bot$.

This seems a little funny to me because it's the only time I've ever seen syntax in natural deduction referred to as shorthand (or sometimes an "abbreviation") rather than achievable through some kind of inference rule or axiom.

What is the difference between that "shorthand" and instead treating it as an inference rule: $\lnot P \vdash P \to \bot$.

Is this a valid way to go or are there nuances being overlooked?

Answer 1

We can have $\bot$ as part of the language.

In this case, we define $\lnot P$ as $P \to \bot$.

In classical logic, this is consistent with the truth table for $\lnot$.

In this way, in classical logic we can replace the adequate set of connectives : $\{ \lnot, \to \}$ with $\{ \bot, \to \}$.

Having done this, we can derive the rule for $\lnot$ :

$(\lnot \text {-I})$ : $$\frac {\frac {[A]} \bot} {\lnot A}$$ is obtained from $(\to\text {-I})$ and

$(\lnot \text {-E})$ : $$\frac {A \quad \lnot A} \bot$$ from $(\to\text {-I})$.

Answer 2

First, $\neg P\vdash P\to \bot$ wouldn't be enough since we also want $P\to\bot$ to entail $\neg P$.

Regardless, a shorthand is an informal, meta-theoretic notion that basically states "whenever you see $\neg P$, mentally replace it with $(P\to \bot)$." This makes, for example, $\neg P\to\neg Q$ literally the same formula as $(P\to\bot)\to(Q\to\bot)$, not just provably equivalent formulas. If we just had rules like $\neg P\vdash P\to\bot$ and $P\to\bot\vdash\neg P$ (which are not the best rules structurally), it would require a tedious, non-trivial (but easy) proof to show that these are equivalent.

However, the point of using a shorthand is to not need to introduce additional inference rules. We're (technically) not even extending the formal language. The benefit is that when we prove meta-theoretic results about formulas or derivations, we don't need to consider the $\neg$ connective or any inference rules related to $\neg$. We often prove such results by structural induction over formulas/derivations and additional connectives/rules mean additional cases in the induction. Similarly, we don't need to define the semantics of $\neg$, which simplifies defining interpretations and proving things about them as well.

The main reason not to define away as much as possible via shorthands is that we may want to consider sublanguages with different connectives. If we define $\neg P$ as $P\to\bot$, then we can't remove $\bot$ without removing $\neg$. Of course, this problem exists too if we have rules like $\neg P\vdash P\to\bot$ which is part of why they are not good rules. So another reason not to define away a connective is so that we can explicitly articulate the most appropriate rules for that connective.

There's also a fairly subtle philosophical thing happening. Classical logic doesn't actually fit that well into natural deduction, at least not as well as intuitionistic logic. In particular, $\neg$ is awkward to characterize with rules. (Compare with the sequent calculus.) The definition $\neg P\equiv P\to\bot$ works just fine for intuitionistic logic, but it presents negation as a secondary, derived notion. For intuitionistic logic, this is fine because negation really is a more secondary notion, especially compared to $\to$ and $\bot$. This makes less sense for classical logic where $\neg$ is rather fundamental.