3
$\begingroup$

I am looking for axioms/inference rules that satisfy the following 3 conditions:

  1. can be added to predicative intensional Martin-Löf type theory, so $\Pi$, $\Sigma$, equality type, with W-types, boolean type, and infinite universe hierarchy
  2. increases proof strength to the level of impredicative prop + infinite hierarchy of predicative universes
  3. maintains the uniformity of large eliminations across universes, i.e. no inferences distinguishing the levels of universe hierarchy from one another. Other than that a smaller universe is contained in a larger universe and that the bottom universe includes the booleans. This condition is somewhat tricky to state as resizing also does not distinguish levels. But it eventually distinguishes the bottom universe as special.

If anyone has suggestions about how to make 3. formal, they are welcome.

One way to resolve this was proposed by Monnier and Bos in Is Impredicativity Implicitly Implicit, but this aims to recover the impredicative $\Pi$-types, while I am wondering about proof principles keeping $\Pi$-types predicative in flavor.

The kind of way I am imagining this is it would distribute the proof strength of impredicative Prop accross the predicative universes in a form of new induction schemas, in style of W-types or induction-recursion.

We can just add the necessary arithmetic theorems to the lowest universe, but that feels like cheating, it would be nicer to add new schema to all universes as we do with W-types and induction-recursion.

Has there been research into candidates for principles, that can have large elimination, have a linear hierarchy of uniform universes, keep normalization, yet have impredicative proof strength? How far did research in this area progress beyond induction-recursion?

One principle that should increase strength is something like propositional resizing, but there we end up with a different flavor of putting things into the smallest universe and restricting elimination via a quotient. I am wondering about a way that does not make the smallest universe special other than it containing booleans.

Improve this question
$\endgroup$
6
  • $\begingroup$ What about rephrasing the propositional resizing this way: The map $\mathsf {Prop}_i \to\mathsf {Prop}_{i+1}$ is an equivalence? This doesn't mention the smallest universe anywhere. $\endgroup$
    – Trebor ♦
    Commented Nov 9, 2022 at 2:21
  • $\begingroup$ It does not mention the smallest universe, but in effect puts a wide range of principles into the smallest universe, by getting an equivalence between Prop0 and Propi. I guess I mean this semantically rather than syntactically. But I still have to think about a way of excluding other pathological examples, that make the bottom universe special. $\endgroup$
    – Ilk
    Commented Nov 9, 2022 at 3:30
  • $\begingroup$ Then I would not say "no rules", because rules are purely syntactic. $\endgroup$
    – Trebor ♦
    Commented Nov 9, 2022 at 3:46
  • 1
    $\begingroup$ Tarski-style or Russell-style universes? Cummulative or not? $\endgroup$
    – Andrej Bauer
    Commented Nov 10, 2022 at 17:46
  • $\begingroup$ @AndrejBauer I have a slight preference for Tarski without cummulativity, but I would be surprised if a principle extending the proof strength in one case could not be adapted to another without change in proof strength. In general I don't mind these variations in the proof principles, but I might be wrong and there could be interesting examples of interaction with impredicativity that are hard/impossible to adapt from one presentation to the other. $\endgroup$
    – Ilk
    Commented Nov 10, 2022 at 21:39

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.