Scott Induction and Equational Proofs
Z. Ésik, L. Bernátsky · Electronic Notes in Theoretical Computer Science · 1995
The equational properties of the iteration operation in Lawvere theories are captured by the notion of iteration theories axiomatized by the Conway identities together with a complicated equation scheme, the “commutative identity”. The first result of the paper shows that the commutative identity is implied by the Conway identities and the Scott induction principle formulated to involve only equations. Since the Scott induction principle holds in free iteration theories, we obtain a relatively simple first order axiomatization of the equational properties of iteration theories. We show, by means of an example that a simplified version of the Scott induction principle does not suffice for this purpose: There exists a Conway theory satisfying the scalar Scott induction principle which is not an iteration theory. A second example shows that there exists an iteration theory satisfying the scalar version of the Scott induction principle in which the general form fails. Finally, an example is included to verify the expected fact that there exists an iteration theory violating the scalar Scott induction principle. Interestingly, two of these examples are ordered theories in which the iteration operation is defined via least pre-fixed points.