In logic and/or math pedagogy, do the "knockout principles" have an accepted name?

Question

In its usual, implicative form, modus ponens says:

$$A \wedge (A \rightarrow B) \rightarrow B$$

There's also an equational version, namely:

$$A \wedge (A \rightarrow B) = A \wedge B$$

Now define that the implicative knockout principle is: $$\neg A \wedge (A \vee B) \rightarrow B$$

And the equational knockout principle is $$\neg A \wedge (A \vee B) = \neg A \wedge B$$

So basically, they let you knock-out some possibilities from a disjunction, based on knowledge of the falseness of those possibilities. We do this all the time, of course, though these principles aren't often made explicit, perhaps due to ease of derivation. In particular, the two implicative statements can be easily inter-derived, by replacing each copy $A$ with $\neg A$. Similarly with the two equational statements. In any event, I think its pedagogically useful to state the two "knockout" principles explicitly, since they're actually pretty useful.

The word "knockout" is my own, so I'm wondering:

In logic and/or math pedagogy, do these principles have an accepted name?

Answer 1

The implicative form

$$\neg A \wedge (A \vee B) \rightarrow B$$

is the conditional version of Disjunctive Syllogism ... which is better known as the inference

$$\neg A$$

$$A \vee B$$

$$\therefore B$$

The equational form

$$\neg A \wedge (A \vee B) \Leftrightarrow \neg A \wedge B$$

is sometimes referred to as Reduction (in the context of $\neg A$, the term $A \vee B$ 'reduces' to just $B$). But few texts do, and it is clearly not as 'standard' as, say, Absorption.

... which is too bad! Indeed, yes, I totally agree with you, Reduction should be more prominently taught and be part of our standard logic toolbox, as it is a very useful little short-cut to doing Distribution, Complement, and Identity. Here are a few posts where I used Reduction:

How to find logical equivalence?

Simplify the following expression using Boolean Algebra into sum-of-products (SOP) expressions

Also, Reduction is a special case of the more general Resolution, whose implicate form would be:

$$((\neg A \lor C) \wedge (A \vee B)) \rightarrow (C \lor B)$$

and whose equational form would be:

$$(\neg A \lor C) \wedge (A \vee B) \Leftrightarrow (\neg A \lor C) \wedge (A \vee B) \land (C \lor B)$$

Answer 2

In classical logic, your "knockout" principles are exactly tje modus ponens, because of the following :

$A \iff \neg \neg A$

$(A\implies B) \iff (\neg A \lor B)$

So your implicative knockout principle becomes : $\neg A \land (\neg \neg A \lor B) \rightarrow B$, which then becomes $\neg A \land (\neg A \implies B) \rightarrow B$, which is indeed a special case of modus ponens. Same thing for the "equational knockout principle"

Answer 3

This is an instance of resolution which is so useful for calculation that is the basis for many (classical) logic provers. The general resolution rule takes your "knockout" idea to the logical conclusion.