How to state precisely this requirement relative to the application of natural deduction rules?

Question

• Contrary to replacement rules, in natural deduction, rules of infrence need to be applied " to an entire line" .

• For example, I cannot use Modus Ponens in the following way

Premise (1) : $( A \rightarrow (B\rightarrow C)) $

Premise (2) : $B$

Conclusion : $C$ ( wrongly applying MP to the consequent in premise (1) ) .

• What is the ( standard) formal statement of this requirement?

Answer 1

First, and as an aside, let me just say that the example:

Premise (1) : $( A \rightarrow (B\rightarrow C)) $

Premise (2) : $B$

Conclusion : $C$ ( wrongly applying MP to the consequent in premise (1) ) .

is really weird! If this is supposed to be an application of an inference rule as applied to part of a larger statement, one would expect that one applies the $B$ to the $B \to C$ as it occurs within the larger statement, and thus have the result $C$ to be still part of that same larger statement, thus resulting in $A \to C$, rather than just $C$.

I mean, this is how it works for rules of replacement. That is, when applying double negation on $A \to \neg \neg B$, the result is $A \to B$, rather than merely $B$.

So, the real analogue should be:

Premise (1) : $( A \rightarrow (B\rightarrow C)) $

Premise (2) : $B$

Conclusion : $A \to C$ ( wrongly applying MP to the consequent in premise (1) ) .

Unfortunately, this argument is in fact valid!

So ... this is a really bad demonstration as to why one should not apply inference rules to partial statements.

Here is a better example to demonstrate why you should not apply inference rules to parts of statements the way you can with rules of replacement.

Let's take the simple inference rule of Simplification (also known as $\land$ Elim):

$P \land Q$

$\therefore P$

Now suppose we try to apply this as follows:

$Premise (1) : (A \land B) \to C$

$Conclusion: B \to C $ ( wrongly applying Simplification to the antecedent of premise (1) )

OK, now we really have an invalid inference on our hands: If $B$ is True but $A$ and $C$ are false, then the premise is true, but the conclusion is false.

And so it is with almost all inference rules: sometimes when you try to apply them to part of a statement you actually end up with a valid argument ... but other times you end up with an invalid argument. So ... better to just not allow the application of inference rules to parts of a statement at all, and that is how inference rules are typically defined.

OK, so that gets us to your actual question: How do inference rules formalize the fact that they can only be applied to whole lines only? Well, actually that is really easy.

Modus Ponens, for example, says that if you have any statement of the form $\varphi \to \psi$, and another of the form $\varphi$, then you can infer $\psi$.

With that, can we apply Modus Ponens to go from $A \to (B \to C)$ and $B$ to $A \to C$? No, for the very simple reason that $A \to (B \to C)$ is not of the form $B \to ...$

That is, when the inference rule says "If you have a statement of the form ....", then it is already implied that that statement is a line in your proof, i.e. a whole statement. So with that, inference rules can by definition only be applied to whole statements. And there is no further formalization needed for how the rule should not be applied.

Answer 2

You cannot apply Modus Ponens that way in no proof system, because the inference is not sound.

If $B$ is true and both $A$ and $C$ are false, we have that both premises are true while the conclusion $C$ is false.

To correctly apply MP you have to assume $A$ and then (using MP twice) derive $C$.

Then conclude with $A \to C$ by CP.

The (now correct) result is the derivation:

$A → (B → C), B \vdash A \to C$.