Skip to main content

Questions tagged [consistency-strength]

Use this tag when discussing the relative logical strength of axiom sets or foundations of theorem provers

Filter by
Sorted by
Tagged with
0 votes
0 answers
24 views

An unexpectedly hard question about type equality (of sigma types)

Suppose you have A: Type and P Q: A -> Prop such that {x : A | P x} = {x : A | Q x}. Can ...
Veky's user avatar
  • 101
15 votes
3 answers
419 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 ...
It'sNotALie.'s user avatar
  • 1,445
13 votes
1 answer
163 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 ...
Pedro Sánchez Terraf's user avatar
20 votes
0 answers
273 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 ...
Wojowu's user avatar
  • 1,058