Questions tagged [consistency-strength]
Use this tag when discussing the relative logical strength of axiom sets or foundations of theorem provers
3
questions
15
votes
3
answers
356
views
What is known about the consistency of proof assistant metatheories?
I realised I don't know the status of consistency of theorem provers' metatheories - what is currently known? For example, as far as I know Lean's type theory is equiconsistent to ZFC+countably many ...
- 1,427
13
votes
1
answer
142
views
Attempts to accommodate theories of different consistency strength in single assistant
TL;DR: How / where to formalize results concerning the logical strength of systems? Are proof assistants having a weak base theory but also enough infrastructure to make it feasible?
I'll start by ...
19
votes
0
answers
247
views
Can we automatically get around set-theoretic difficulties?
One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large ...
- 1,038