Skip to main content
19 votes

What is known about the consistency of proof assistant metatheories?

This is more of a comment than an answer. I really look forward to the answers, but it should be noted that there are a lot of subtleties when saying that a system is consistent. First, a logical ...
Jason Rute's user avatar
  • 8,665
11 votes

What is known about the consistency of proof assistant metatheories?

I am not familiar enough with the literature on this question to be able to point to specific papers, but allow me to make a basic sketch on how one can set up set-theoretic models of type theories. I ...
Andrej Bauer's user avatar
  • 9,144
9 votes
Accepted

Attempts to accommodate theories of different consistency strength in single assistant

You could address your goals by using a generic proof assistant, one that supports user-definable theories, such as Isabelle and Metamath, and I am sure there are others. These allow you to define ...
Andrej Bauer's user avatar
  • 9,144
6 votes

What is known about the consistency of proof assistant metatheories?

Because HOL is so weak, it has had a quite a bit of work done on its semantics and soundness, both at the logic level, and in terms of implementations. The bibliography in Oskar Abrahamsson’s recent ...
Michael Norrish's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible