Inductive Proof System

An Inductive Proof System is an Accelerated Simulator and Decider which operates by automatically detecting and proving transition rules using Mathematical Induction.

Inductive Rule

An inductive rule is a general transition rule (a start and end configuration, generalized with variables for repetition counts) along with a proof. The proof generally has two pieces: the base case and the inductive case. Each is a list of steps where each step is (A) a specific TM transition, (B) an application of the inductive hypothesis, (C) an application of a previously defined rule.

Rule Levels

We can assign levels to any Inductive Rule. A Level 0 (L0) rule does not depend on any previously defined inductive rules. A Level 1 (L1) rule depends only upon previously proven L0 rules, etc. All L0 Rules (which only invoke the inductive hypothesis once) are Shift rules.

Example Proofs

Notation

In this article we will use the following notation for an Inductive Rule and its proof:

$P(n)$

• Proof by induction on n:
  • Base case: List of steps to prove the base case $P(0)$. Often this is the empty list since $P(0)$ is trivially true (in zero steps).
  • Inductive case: List of steps to prove $P(n+1)$ of which some can be "IH" the inductive hypothesis that $P(n)$.

Bouncer

Consider the bouncer 1RB0RC_0LC---_1RD1RC_0LE1RA_1RD1LE (bbch). We can prove the following Inductive Rules:

1. Shift (L0) Rule: $C(n):{\textrm {C>}}\;1^{n}\to 1^{n}\;{\textrm {C>}}$
   • Proof by induction on n
     • Base case: []
       $${\textrm {C>}}\;1^{0}=1^{0}\;{\textrm {C>}}$$
     • Inductive case: [C1, IH]
       $${\textrm {C>}}\;1^{n+1}\xrightarrow {C1} 1\;{\textrm {C>}}\;1^{n}\xrightarrow {IH} 1^{n+1}\;{\textrm {C>}}$$
2. Shift (L0) Rule: $E(n):1^{n}\;{\textrm {<E}}\to {\textrm {<E}}\;1^{n}$
   • Proof by induction on n
     • Base case: []
     • Inductive case: [E1, IH]
3. L1 Rule: $A(n):{\textrm {A>}}\;1^{n}\;0^{\infty }\to 1^{2n}\;{\textrm {A>}}\;0^{\infty }$
   • Proof by induction on n
     • Base case: []
     • Inductive case: [A1, C(n), C0, D0, E(n+1), E0, D1, IH]
       $${\begin{array}{l}\\{\textrm {A>}}\;1^{n+1}\;0^{\infty }&\xrightarrow {A1} &0\;{\textrm {C>}}\;1^{n}\;0^{\infty }\\&\xrightarrow {C(n)} &0\;1^{n}\;{\textrm {C>}}\;0^{\infty }\\&\xrightarrow {C0} &0\;1^{n+1}\;{\textrm {D>}}\;0^{\infty }\\&\xrightarrow {D0} &0\;1^{n+1}\;{\textrm {<E}}\;0^{\infty }\\&\xrightarrow {E(n+1)} &0\;{\textrm {<E}}\;1^{n+1}\;0^{\infty }\\&\xrightarrow {E0} &1\;{\textrm {D>}}\;1^{n+1}\;0^{\infty }\\&\xrightarrow {D1} &1^{2}\;{\textrm {A>}}\;1^{n}\;0^{\infty }\\&\xrightarrow {IH} &1^{2(n+1)}\;{\textrm {A>}}\;0^{\infty }\\\end{array}}$$
4. L2 Rule: $0^{\infty }\;1^{a}\;{\textrm {A>}}\;0^{\infty }\to 0^{\infty }\;1^{2a+6}\;{\textrm {A>}}\;0^{\infty }$
   • Proof: [A0, B0, C1, C0, D0, E(a+2), E0, D1, A(a+1)]
     $${\begin{array}{l}\\0^{\infty }\;1^{a}\;{\textrm {A>}}\;0^{\infty }&\xrightarrow {A0,B0,C1,C0,D0} &0^{\infty }\;1^{a+2}\;{\textrm {<E}}\;0^{\infty }\\&\xrightarrow {E(a+2)} &0^{\infty }\;{\textrm {<E}}\;1^{a+2}\;0^{\infty }\\&\xrightarrow {E0,D1} &0^{\infty }\;1^{2}\;{\textrm {A>}}\;1^{a+1}\;0^{\infty }\\&\xrightarrow {A(a+1)} &0^{\infty }\;1^{2a+4}\;{\textrm {A>}}\;0^{\infty }\\\end{array}}$$

We can see now that the last rule can be applied repeatedly forever, so if it is ever applied once, the TM will never halt. In fact, in this case the start config is equal to $0^{\infty }\;1^{0}\;{\textrm {A>}}\;0^{\infty }$ and thus this TM will never halt.