The "internal logic" of type theory UTT is defined in LF as follows:

enter image description here

What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - we have the universe of propositions, and to every proposition (i.e., every object of type $Prop$) there corresponds a type of its proofs via $\textbf{Prf}$ (here, I also don't have intuition on why this would be a reasonable/useful thing to have); $\forall$ stands for the usual universal quantification. But what's the intuition behind $(9.4), (9.5), (9.6)$?

And by the way, what exactly does the term "internal logic" mean? Maybe there isn't a rigorous definition of this term, but for example why doesn't the "internal logic" described above say anything about predicative universes (which also exist in UTT; but they are described separately, after the introduction of internal logic)?


1 Answer 1

  1. $\mathit{Prop}$ is a universe and $\mathrm{Prf}$ is its decoding function. (Often called $T$ for Tarski-style universe.)
  2. $\Lambda$ is the introduction rule for universal quantification.
  3. $\mathbf{E}_\forall$ is the elimination rule for universal quantification.
  4. Equation (9.6) is the computation rule explaining what happens when we eliminate an introduction form.

You should compare these rules with the rules for universal quantifiers in type theory.

Internal logicis a broad term that cannot be explained in this answer. I will not even try.

  • $\begingroup$ Many thanks. Do you happen to know a non-HoTT-oriented source (maybe a textbook) that discusses universal quantifiers in dependent type theory? $\endgroup$
    – user175254
    Commented Mar 30, 2023 at 0:11
  • 1
    $\begingroup$ You could go to the source, for instance around pages 13 and 17 of the Padova notes. $\endgroup$ Commented Mar 30, 2023 at 7:35

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.