Proof I: From Ernest (1998, p.35)

Notation:

a(x,y)=x+y

s(x)="the increment of x"

A1 | a(x,s(y))=s(a(x,y)) | AXIOM | x+sy=s(x+y) |
---|---|---|---|

T2 | a(1,s(y))=s(a(1,y)) | FROM A1 | 1+sy=s(1+y) |

T3 | a(1,s(0))=s(a(1,0)) | FROM T2 | 1+s0=s(1+0) |

A4 | a(x,0)=x | AXIOM | x+0=x |

T5 | a(1,0)=1 | FROM A4 | 1+0=1 |

T6 | a(1,s(0))=s(1) | FROM T3 AND T5 | 1+s0=s1 |

D7 | s(0)=1 | DEFINITION | s0=1 |

T8 | a(1,1)=s(1) | FROM T6 AND D7 | 1+1=s1 |

D9 | s(1)=2 | DEFINITION | s1=2 |

T10 | a(1,1)=2 | FROM T8 AND D9 | 1+1=2 |

Expression tree of this proof structure

Expression trees of the structure of these statements

x+sy=s(x+y) | |||||
---|---|---|---|---|---|

1+sy=s(1+y) | x+0=x | ||||

1+s0=s(1+0) | 1+0=1 | ||||

1+s0=s1 | s0=1 | ||||

1+1=s1 | s1=2 | ||||

1+1=2 |

Alternative Proof II

Notation:

a(x,y)=x+y

i(x)="the increment of x"

d(x)="the decrement of x"

A1 | a(x,y)=a(i(x),d(y)) | AXIOM |

T2 | a(1,y)=a(i(1),d(y)) | FROM A1 |

T3 | a(1,1)=a(i(1),d(1)) | FROM T2 |

D4 | i(1)=2 | DEFINITION |

T5 | a(1,1)=a(2,d(1)) | FROM T3 AND D4 |

D6 | i(0)=1 | DEFINITION |

T7 | a(1,1)=a(2,d(i(0))) | FROM T5 AND D6 |

A8 | d(i(x))=x | AXIOM |

T9 | d(i(0))=0 | AXIOM |

T10 | a(1,1)=a(2,0) | FROM T7 AND D9 |

A11 | a(x,0)=x | AXIOM |

T12 | a(2,0)=2 | FROM A11 |

T13 | a(1,1)=2 | FROM T10 AND T12 |

Links to other sites...

Created 16/8/99