An extended type system with lambda-typed lambda-expressions (extended version)
Matthias Weber
TL;DR
This work presents $\mathtt{d}$, an extended type system that unifies lambda-typed lambda-expressions with existential abstraction and classical propositional operators, while normalizing proofs and formulas uniformly as functional expressions. It introduces a reflexive primitive $\tau$ with $\tau:\tau$ to prevent certain paradoxes, and augments the core kernel with existential abstraction, products, sums, and a neutral negation operator, together with explicit casting mechanisms. The paper provides a formal definition, a broad set of motivating examples, and a rigorous development of key meta-theoretical properties: confluence, subject reduction, uniqueness of types, strong normalization, and consistency, along with discussions of extensions and alternatives. It also shows how, depending on the chosen axioms for negation and for additional mathematical structures, additional assumptions are necessary to realize full classical logic and standard mathematics within the framework. The resulting system offers a conceptually simpler, purely functional foundation for structured mathematical reasoning with flexible deduction interfaces.
Abstract
We present the type system $\mathtt{d}$, an extended type system with lambda-typed lambda-expressions. It is related to type systems originating from the Automath project. $\mathtt{d}$ extends existing lambda-typed systems by an existential abstraction operator as well as propositional operators. $β$-reduction is extended to also normalize negated expressions using a subset of the laws of classical negation, hence $\mathtt{d}$ is normalizing both proofs and formulas which are handled uniformly as functional expressions. $\mathtt{d}$ is using a reflexive typing axiom for a constant $τ$ to which no function can be typed. Some properties are shown including confluence, subject reduction, uniqueness of types, strong normalization, and consistency. We illustrate how, when using $\mathtt{d}$, due to its limited logical strength additional axioms must be added both for negation and for the mathematical structures whose deductions are to be formalized. Several appendices deal with extensions and variations of the proposed system.