Is there a name for the propositional tautology (and it's associated rule) $Q\Rightarrow(P\Rightarrow Q)$?

Question

I have the tautology $Q\Rightarrow(P\Rightarrow Q)$. I can prove this intuitionistically:

Rule 
  Conclusion
    Q=>(P=>Q)
  Proof
    Suppose
      Q
    Hence
      Suppose
        P
      Hence
        Q
      P=>Q
    Q=>(P=>Q)

This gives the corresponding inference rule:

$$ \frac{Q}{P\Rightarrow Q}\quad\text{[VacuousImplicationIntroduction]} $$

The proof, which relies on the tautology, is:

Rule (VacuousImplicationIntroduction)
  Premise
    Q
  Conclusion
    P=>Q
  Proof
    Q=>(P=>Q)
    Q
    P=>Q by ModusPonens

I've called this rule 'vacuous implication introduction', which is a pretty poor name. Is there a standard or at least a better one?

Answer 1

Different authors have called the formula (not the rule) different names.

I've seen 'positive paradox', 'simplification', and 'Simp'.

I prefer to call the formula [p => (q => p)] or CpCqp in Polish notation, recursive variable prefixing. Why? Because under the the rule of detachment (also called modus ponens) it allows you to prefix any formula with a variable. And since you can do that for any formula, you can recursively prefix each new formula with a variable in a proof sequence with prefixed formulas. Or perhaps better, it allows to demonstrate metalogically that where 't' indicates a theorem or an axiom, that

$\vdash$Ca$_1$Ca$_2$...Ca$_n$t

CpCqp may look dull, but taking it as the only axiom under the rule of condensed detachment, which I'll call {CpCqp}, any theorem t which replaces CpCqp as the sole axiom has the same consequences as {CpCqp}.

In other words, where $\vdash$t in {CpCqp},

{t} |-| {CpCqp}

where |-| indicates deductive equivalence.

Not many non-trivial systems have that sort of property.