Skip to main content

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
3 votes
2 answers

Enumerating all formulae of any first-order language

I'm formalizing the metatheory of first-order logic with Coq. I want to enumerate all expressions of any first-order language. The syntax of terms and formulae are: ...
Kijeong Lim's user avatar
5 votes
1 answer

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
  • 547
2 votes
0 answers

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 ...
Ms. Molly Stewart-Gallus's user avatar
10 votes
1 answer

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
  • 4,025
15 votes
3 answers

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
22 votes
3 answers

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