Questions tagged [metatheory]

In mathematics and mathematical logic, a metatheory is a mathematical theory about another mathematical theory. (Source: Wikipedia)

Filter by
Sorted by
Tagged with
5 votes
1 answer
160 views

State of art for observational equality, on the injectivity requirement

I am reading through the papers, "Observational equality: Now for good" (${TT}^{obs}$) and "Impredicative Observational Equality" (${CC}^{obs}$) by Pujet and Tabareau, and I am ...
Ilk's user avatar
  • 517
2 votes
0 answers
109 views

How to deal with axioms in a proof assistant?

I'm currently formalizing a little language which has somehow ended up looking a lot like Lawvere theories/finite product theories. I guess it's starting to look a little like Twelf? What I would love ...
Molly Stewart-Gallus's user avatar
10 votes
1 answer
274 views

What is realignment and is it useful in non-univalent theories?

From my rough understanding, an (external/internal) realignment property says that given a type $A$, a proposition $p : \Omega$, and a partial isomorph $B : p \to \sum_{A'} A' \cong A$, we can extend ...
Trebor's user avatar
  • 3,718
15 votes
3 answers
384 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
21 votes
3 answers
476 views

Programming language metatheory in Lean 4?

I'm looking for developments of programming language metatheory done in Lean 4. We have a calculus with a lot of mutually recursive judgements and we want to formalise its denotational semantics. ...
Neel Krishnaswami's user avatar