Proving that $a \dot{-} (b+1) = (a \dot{-} b) \dot{-} 1$

Question

This should be an easy exercise from Hodel's Introduction to Mathematical Logic, but for some reason I'm not getting it right. Define $a \dot{-} b$ as $a-b$ if $a \geq b$ and as $0$ otherwise. Recursively, this can be defined as $\mu x [(a=b+x) \vee (a<b)]$. Using this information, I'm supposed to prove that $a \dot{-} (b+1) = (a \dot{-} b) \dot{-} 1$. I've tried using induction on $a$ and induction on $b$ to get the desired result, but I got stuck as I see no way of applying the induction step (basically, I couldn't reduce the case, say, $a \dot{-} ((n+1)+1)$ to the induction hypothesis). Any hints?

Answer 1

The proof is mechanical if one uses the universal property of the $\,\rm max\,$ function

$$ x \ge y,z\color{#c00}\iff x \ge m(y,z),\ \ m = \rm max\qquad\qquad\qquad\ \ $$

Using this property to eliminate then reintroduce $\,m = \rm max\,$ we obtain (in gory detail)

$$\begin{array}{rrl} &x\ \ge&\ \,(a \dot- b)\! \dot-\! 1\\ \iff &x\ \ge&\!\!\!m( a \dot- b\! -\!1, 0)\\ \color{#c00}\iff &x\ \ge& \ \ \ a\dot- b\!-\!1, 0\\ \iff &1\!+\!x\ \ge& \ \ \ a \dot- b,\quad \ \, 1\\ \iff &1\!+\!x\ \ge&\!\!\!m(a\!-\!b,0), 1\\ \color{#c00}\iff &1\!+\!x\ \ge&\ \ \,a\!-\!b,\,0, \ 1\\ \iff &1\!+\!x\ \ge&\,\ \ a\!-\!b,\quad\,\ 1\\ \iff &x\ \ge&\ \ \ a\!-\!b\!-\!1, 0\\ \color{#c00}\iff &x\ \ge&\!\!\! m(a\!-\!b\!-\!1, 0)\\ \iff &x\ \ge&\ \ \ a\dot- (b\!+\!1) \end{array}\qquad\quad$$

Remark $\ $ With hindsight, one can abstract from the proof a lemma about max, $\ m(x,y)-z\, =\, m(x\!-\!z,y\!-\!z).\,$ Using this shortens the above proof to

$$\begin{align} (a \dot- b) \dot- 1\, &=\,m(m(a\!-\!b,0) -1,\ 0)\\ &=\, m(m(a\!-\!b\!-\!1,-1),0)\\ & =\, m(a\!-\!b\!-\!1,0)\\ &=\,a\dot- (b\!+\!1)\end{align}\qquad\quad $$

Answer 2

fix $b.$ and consider three cases: $$(a\dot{-} b) \dot{-} 1 = \begin{cases} 0 \dot{-} 1 = 0 & \text{ if } a < b \\ (a-b)\dot{-}1 = 0 & \text{ if } b < a < b + 1\\ a-b-1 =a-(b+1) & \text{ if } b + 1 < a \end{cases} $$

therefore $$ (a\dot{-} b) \dot{-} 1 = a\dot{-}(b+1).$$