I have a project to write a proof assistant that is as simple as possible while still usable. A kind of turing tar pit but for proofs instead of programs. Some early attempts did not quite work out. I try to get it off the ground using the calculus of constructions (not the calculus of inductive constructions) together with a small set of axioms. As axioms I aim, at the moment, to use a hilbert epsilon operator to contstruct objects from theorems that state their existence, proof irrelevance and an infinity axiom that states that an infinite set exists. Also I do use an infinite hierarchy of Types a bit like the universes of coq. I am still debating with myself whether I also should provide the luxury of not having to specify universe levels and just keep constraints between them like in coq.
The article proposes the calculus of inductive constructions but I think that is just too big and complicated to be a good candidate for a foundation of mathematics. I think it makes more sense to use a more concise foundation and maybe attempt to prove that the calculus of inductive constructions is a conservative extension of that.
The article proposes the calculus of inductive constructions but I think that is just too big and complicated to be a good candidate for a foundation of mathematics. I think it makes more sense to use a more concise foundation and maybe attempt to prove that the calculus of inductive constructions is a conservative extension of that.