\begin{equation*} \mathcal{T}= V\vert C\vert \mathcal{T}\mathcal{T}\vert \lambda V{:}\mathcal{T}.\mathcal{T}\vert \Pi V{:}\mathcal{T}.\mathcal{T} \end{equation*}

\begin{equation*} \mathcal{T}= V \mid C \mid \mathcal{T}\mathcal{T} \mid \lambda V{:}\mathcal{T}.\mathcal{T} \mid \Pi V{:}\mathcal{T}.\mathcal{T} \end{equation*}

Now for the rules and axioms that describe expressions, which for present purposes, are strings of the form $\phi\mathbin{:}\psi$ (which can be derived from the empty typing context). My audience is familiar with presentations of first-order logic languages that invoke clauses like ``For all natural numbers n, there are infinitely many predicates $P^{1}$, $P^{2}$, and so on, of arity $n$.'' So I have formulated principles for pure type systems that are structurally similar. Here is an example. Let $S=\{\ast,\Box\}\subseteq C$ be the set of sorts. Then consider the principles below. (for brevity, in what follows, I omit additional clauses guaranteeing that each constant/variable gets associated with a unique pseudo-expression)

Consistency is often defined, in pure type systems, like this: a pure type system is consistent just in case the type $\bot$ is not inhabited, where $\bot$ is usually taken to be something like $\Pi x\mathbin{:}\ast.x$. Call this the `standard definition' of consistency.

My second question concerns the fact that, for my audience, trivially violating the standard definition of consistency isn't actually a bad thing. My audience cares more about using pure type systems to formulate logical principles that are terms with proposition type (again, for brevity, I can't explain why...it is based on a different interpretation of the Curry-Howard correspondence from the standard interpretation...this is part of what makes my presentational task difficult). Those principles need to be consistent, but just in the following sense: given a collection of terms with proposition type, and given a collection of inference rules among those terms specifically, there is no way to derive a contradiction. This other definition of consistency -- call it the `second definition' -- is, of course, different from the standard definition given above.

So my second question is: when higher-order logical principles -- i.e. terms of proposition type which invoke higher-order quantification, etc. -- are formulated using the pure type systems in the $\lambda$-cube, are the resulting formal systems consistent in the second sense? For instance, are there collections of higher-order logical principles, formulated in the calculus of constructions, which (i) formalize things like "Every term, of every type, is self-identical" in a single sentence, (ii) include lots of other standard classical axioms and inference rules, and (iii) are consistent in the sense of the second definition?

Now for the rules and axioms that describe expressions, which for present purposes, are strings of the form $\phi\mathbin{:}\psi$ (which can be derived from the empty typing context). My audience is familiar with presentations of first-order logic languages that invoke clauses like “For all natural numbers $n$, there are infinitely many predicates $P^{1}$, $P^{2}$, and so on, of arity $n$.” So I have formulated principles for pure type systems that are structurally similar. Here is an example. Let $S=\{\ast,\Box\}\subseteq C$ be the set of sorts. Then consider the principles below. (For brevity, in what follows, I omit additional clauses guaranteeing that each constant/variable gets associated with a unique pseudo-expression.)

Consistency is often defined, in pure type systems, like this: a pure type system is consistent just in case the type $\bot$ is not inhabited, where $\bot$ is usually taken to be something like $\Pi x\mathbin{:}\ast.x$. Call this the ‘standard definition’ of consistency.

My second question concerns the fact that, for my audience, trivially violating the standard definition of consistency isn't actually a bad thing. My audience cares more about using pure type systems to formulate logical principles that are terms with proposition type (again, for brevity, I can't explain why…it is based on a different interpretation of the Curry–Howard correspondence from the standard interpretation…this is part of what makes my presentational task difficult). Those principles need to be consistent, but just in the following sense: given a collection of terms with proposition type, and given a collection of inference rules among those terms specifically, there is no way to derive a contradiction. This other definition of consistency — call it the ‘second definition’ — is, of course, different from the standard definition given above.

So my second question is: when higher-order logical principles — i.e. terms of proposition type which invoke higher-order quantification, etc. — are formulated using the pure type systems in the $\lambda$-cube, are the resulting formal systems consistent in the second sense? For instance, are there collections of higher-order logical principles, formulated in the calculus of constructions, which (i) formalize things like “Every term, of every type, is self-identical” in a single sentence, (ii) include lots of other standard classical axioms and inference rules, and (iii) are consistent in the sense of the second definition?