\documentclass{article}
\usepackage[a4paper]{geometry}
\newcommand{\comment}[1]{}
\linespread{1.6}
\begin{document}
\title{C00 Exercise 4: write}
\author{Ramana Kumar (rk436)}
\maketitle
\thispagestyle{empty}
\comment{
How to implement HOL on top of set theory nicely.
- Type theory advantages
- type checking and inference
- functions built in
- succinct/straightforward statements, mainly when semantical membership conditions are dealt with by type inference
- easier to create proofs?
- Type theory disadvantages
- no canonical, well-accepted version; many versions
- hard to create some constructions from mathematics naturally
- From HOL to set theory
- Krauss
- automatic
- produces proofs
- Gordon
- Implementing HOL atop set theory
- Gordon's suggestion
- Implementing both more like a mathematician would
- Use a natural ontology (where, say, relations and sets are different, and separately axiomatizable), but exhibit models for everything in set theory to keep the epistemic basis small
- Ganesalingam
- Current systems leave the modelling in task outside of the system. Instead we can demonstrate the modelling explicitly within the system.
- Metamath?
}
\begin{center}\bfseries{PhD Proposal}\end{center}
Most interactive theorem provers deal with terms of and produce theorems in some type theory.
The generally accepted foundation for mathematics, however, is set theory, ZFC in particular.
Advantages of type theories include: type checking and inference, functions as a primitive notion, and short statements when set membership conditions are implied by types.
But there are many type theories, ranging from the higher-order logic of the HOL system to the calculus of constructions of Coq, which vary both philosophically and practically.
Furthermore, a type system can get in the way of making certain constructions, especially in abstract algebra and category theory.
Mike Gordon [ suggests approaches for getting the best of both worlds, the standardness and expressivity of set theory alongside the usability afforded by types.
\end{document}
]