## Abstract

In doing this work of formalizing a well known body of mathematics, we spent a large amount of time solving mathematical problems, e.g. the Thinning Lemma. Another big problem was maintaining and organizing the formal knowledge, e.g. allowing two people to extend different parts of the data base at the same time, and finding the right lemma in the mass of checked material. We feel that better understanding of mathematical issues of formalization (e.g. names/namefree, intentional/extentional), and organization of formal development are the most useful areas to work on now for the long-term goal of formal mathematics.

Finally, it is not so easy to understand the relationship between some informal mathematics and a claimed formalization of it. Are you satisfied with our definition of reduction? It might be more satisfying if we also defined de Bruijn terms and their reduction, and proved a correspondence between the two representations, but this only changes the degree of the problem, not its nature. What about the choice between the typing rules Lda and Lda'? There may be no “right” answer, as we may have different ideas in mind informally. There is no such thing as certain truth, and formalization does not change this state of affairs.

Finally, it is not so easy to understand the relationship between some informal mathematics and a claimed formalization of it. Are you satisfied with our definition of reduction? It might be more satisfying if we also defined de Bruijn terms and their reduction, and proved a correspondence between the two representations, but this only changes the degree of the problem, not its nature. What about the choice between the typing rules Lda and Lda'? There may be no “right” answer, as we may have different ideas in mind informally. There is no such thing as certain truth, and formalization does not change this state of affairs.

Original language | Undefined/Unknown |
---|---|

Title of host publication | Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings |

Editors | M. Bezem, J.F. Groote |

Publisher | Springer Berlin |

Pages | 289-305 |

Number of pages | 17 |

ISBN (Electronic) | 978-3-540-47586-6 |

ISBN (Print) | 978-3-540-56517-8 |

DOIs | |

Publication status | Published - 18 Mar 1993 |

Event | International Conference on Typed Lambda Calculi and Applications TLCA'93 - Utrecht, Netherlands Duration: 16 Mar 1993 → 18 Apr 1993 Conference number: 1 https://link.springer.com/conference/tlca |

### Conference

Conference | International Conference on Typed Lambda Calculi and Applications TLCA'93 |
---|---|

Abbreviated title | TLCA 1993 |

Country/Territory | Netherlands |

City | Utrecht |

Period | 16/03/93 → 18/04/93 |

Internet address |

## Keywords

- Type Theory
- Typing Rule
- Inductive Type
- Structural Induction
- Lambda Calculus