ID | Name | Lemma | Duals |
MKA1 | TBD | $p+ |x\rangle |x^*\rangle p = |x^*\rangle p$ | $p+ |x^*\rangle |x\rangle p = |x^*\rangle p$ $p+ \langle x| \langle x^*| p = \langle x^*|p$ $p+ \langle x^*| \langle x| p = \langle x^*|p$ |
MKA2 | TBD | $|x\rangle p \leq p \Rightarrow |x^*\rangle p \leq p$ | $\langle x| p \leq p \Rightarrow \langle x^*|p \leq p$ |
MKA3 | TBD | $q + |x\rangle p \leq p \Rightarrow |x^*\rangle q \leq p$ | $q + \langle x|p \leq p \Rightarrow \langle x^*|q \leq p$ |
MKA4 | Segerberg's induction axiom | $|x^*\rangle p\cdot \neg p \leq |x^*\rangle (|x\rangle p\cdot \neg p)$ | n/a |
MKA5 | two notions of termination | $div(x)=0 \Leftarrow \forall y (\dom(y)+|x\rangle \dom(y) = |x\rangle \dom(y) \Rightarrow \dom(y)=0)$ | n/a |
MKA6 | two notions of termination | $div(x)=0 \Leftarrow (\forall y \dom(y)+|x^* \rangle (\dom(y) - |x \rangle \dom(y)) = |x^*\rangle (\dom(y) - |x\rangle \dom(y)))$ | n/a |
MKA7 | Loeb's formula and wellfoundedness | $((\forall y (\dom(y)+|x^*\rangle (\dom(y) - |x\rangle \dom(y)) = |x^*\rangle (\dom(y) - |x\rangle \dom(y))) & (\forall y (|x\rangle |x\rangle \dom(y)) = |x\rangle \dom(y))) \Rightarrow (\forall y ( |x\rangle \dom(y) + |x^*\rangle (\dom(y) - |x\rangle \dom | n/a |
©2007. Peter Höfner |