An extended type system with lambda-typed lambda-expressions

TL;DR

The paper introduces an extended lambda-typed system called $ exttt{d}$ that incorporates lambda-typed lambda-expressions, existential abstraction, propositional operators, and classical negation, ensuring normalization and consistency.

Contribution

It extends existing lambda-typed systems with new operators and properties, providing a normalizing, consistent, and confluence-preserving framework for formal proofs and formulas.

Findings

$eta$-reduction normalizes negated expressions

System $ exttt{d}$ is confluent and strongly normalizing

$ exttt{d}$ maintains consistency and unique types

Abstract

We present the 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. $\beta$-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 type axiom for a constant $\tau$ 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.