David Corfield n-theory

From Mike Shulman’s $n$-theory account. Some slides here.

• A 3-theory species the structure of the forms of judgment, the arity and dependency structure.
• A particular 2-theory specifies the “doctrine” in which we write 1-theories, which syntactically means the rules of the deductive system in which we formulate those 1-theories.
• A particular 1-theory in a doctrine specifies generating types, terms, and axioms

Could give this an expressivist/inferentialist account. Why are upper levels more fitting, as opposed to the generating types, terms and axioms at the 1-level.

3-theory specifies forms of judgment. 2-theory specifies deductive rules, makes explicit.

Rather than see his account as providing a classification system, as with animal species, note that the 3-theories he discusses are arranged in terms of greater expressivity. Perhaps better to see this in terms of restrictions.

Leaving aside multiple consequents for the moment (for classical theories), modal DTT as a 3-theory can be restricted by

1. Only allow one mode, so no modality. (DTT)
2. Only allow one level of dependency
3. Allow no dependency (Simple)
4. Only allow one premise (Unary)
5. Force dependent types to be propositions (Typed FOL)
6. Force all types to be propositions (Propositional logic)
7. Only allow one non-dependent type (FOL)

Some of these (the first 4) are specifications for a 3-theory, some for a 2-theory.

So it’s not that ordinary FOL is untyped. It’s unimoded, one non-dependent typed forced to be set, and dependent types are forced to be propositions.

Propositional logic is unimoded, no dependency, all types are propositions.

Restrictions then dictate what it is possible to express within the 2-theories.

Can’t I have one layer of dependency, no restriction to propositions in dependent types? Can I force types to be sets?

Why not take modal DTT as primary? What are the type formation rules? Do those for other logics just arise through restriction.

FOL as a 2-theory

The unique non-dependent type is not mentioned, but there are variables of that type available. No need to mention elements of a power of the domain, since these are tuples.

Don’t explicitly mention function types between powers. As for elements, if codomain is $D^n$, use $n$-tuples. For elements of types $[D^n, D]$ use function $(n \gt 0)$, and constant symbols $(n=0)$.

Don’t mention $Prop$ as a type. Dependent propositions are relations $(n \gt 1)$, predicates $(n =1)$, propositions $(n = 0)$. Since propositions, sub-singletons, don’t mention their elements. Their appearance indicates truth. Don’t mention the propositions, $0$ and $1$.

Product, function, sum, identity type are reflected to propositions in FOL as conjunction, implication, disjunction, equality.

Dependent product as universal quantification. Dependent sum as comprehension. Inhabited dependent sum as existential quantifier.

For single non-dependent type of FOL which is a set, $x=y$ is a prop. No need for equality within its dependent props since sub-singletons.

What of univalent universe, HITs? Don’t usually have type $Prop$, but it explains relations as $D^n \to Prop$. HOL requires such a universe.

The unspecified type of everything, $D$, encourages us not to ask what it is to be a member, whereas in a type theory we have the types that are generated by the system and then add in extra ones with rules. See univocal-equivocal.

This leads to a wish to exceed $D$ as in free logic.

Propositional logic as a 2-theory

A simple type theory, so no dependency, where types are restricted to being propositions, $0$-ary relations.

Has as models the (1,2)-category of Boolean algebras.

A propositional 1-theory specifies types (propositions) and axioms. Has as models a (0,1)-category or (poset), lines of the truth table ordered by $\bottom \lt \top$.