Proof Principle for Structural Induction on Inference Rules

发布于 2022-08-07  201 次阅读


  Define a single inference rule as an ordered pair \langle X/y\rangle, where X is a (possibly empty or infinite) set of premises, and y is the conclusion that can be derived if all premises in X can be established. Let R be a set of inference rules, we say a set Q is R-closed iff for all rules \langle X/y\rangle in R, X\sube Q\implies y\in Q.
  From the Tarski's fixedpoint theorem, let I_R be the intersection of all R-closed set, we have:

  1. The set I_R is itself R-closed.
  2. If Q is R-closed, then I_R\sube Q

this two conclusions actually state that I_R is the minimal set satisfying the rules R, which, in other words, is the set inductively defined by R.
  Let P be a property on R, define Q=\lbrace x\in I_R| P(x)\rbrace. Now, the Tarski's theorem gives us a useful hint if we want to show that P hold for all x\in I_R. From the definition of Q and the definition of I_R we can see that \forall x\in I_R. P(x)\iff I_R\sube Q, to show that I_R\sube Q it is sufficient to prove that Q is R-closed (from Tarski's theorem), that is, show that for all rule instances \langle X/y\rangle:

\forall x\in X. x\in Q\implies y\in Q

which is equivalent to

\forall x\in X. x\in I_R\land P(x)\implies y\in I_R\land P(y)

however, since I_R is R-closed, \forall x\in X. x\in I_R\implies y\in I_R is trivial, thus shortened the original proposition to:

\forall x.\in X. x\in I_R\land P(x)\implies y\in P(y)

Combined with the fact that what we are about to prove is P(x) holds for all x\in I_R, this give us the most solid foundation of structural induction on inference rules. It says: if we want to prove that P(x) holds for all x\in I_R, it is sufficient to show that, if all of the premises hold, then must be the conclusion.


We Choose to Go to the Moon