# An extended type system with lambda-typed lambda-expressions

Matthias Weber  Faculty of Computer Science, Technical University of Berlin
<EMAIL_ADDRESS>
###### 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.

###### keywords:

Typed lambda calculus, Higher-order logic, Strong normalization

##  1 Introduction and Overview

In this paper, we will present an extended type system with lambda-typed
lambda-expressions. Since such systems have received little attention we begin
with some general remarks to provide some context.

Most type systems contain subsystems that can be classified as instances of
pure type systems (PTS) (e.g. [4]). As one of their properties, these systems
use distinct operators to form dependent products and functional (i.e.
$\lambda$)-abstractions. This reflects their underlying semantic distinction
between the domains of functions and types. In contrast, in the semantics of
lambda-typed systems there is a single domain of (partial) functions and
typing is a binary relation between total functions. As a consequence a
function participating in the type relation may play the role of an element or
of a type. Moreover, since in general the domain and range of the type
relation are not disjoint a function can (and will usually) have a double role
both as element and as type. Therefore in lambda-typed calculi one has to
separate three aspects of an operator: its functional interpretation, i.e. the
equivalence class of entities it represents, its role as a type, i.e. the
entities on the element side related to its entities in the type relation, and
its role as an element, i.e. the entities on the type side related to its
entities in the type relation. From this point of view, the semantic
distinction between dependent products and $\lambda$-abstractions can be
reduced to the distinction between the type-role or the element-role of a
single underlying function and therefore, from a calculational viewpoint, a
single operator is sufficient.

Type systems outside of PTS using a single operator for dependent products and
functional (i.e. $\lambda$)-abstractions (i.e. $\lambda$-structured types)
have been investigated in early type systems such as $\Lambda$ [10][25], as
well as more recent approaches [15][18]. In particular [18] introduces the
single-binder based $\flat$-cube, a variant of the $\beta$-cube which does not
keep uniqueness of types and studies $\lambda$-structured type variants of
well-known systems within this framework.

Before we present the basic elements of $\mathtt{d}$, we would like to point
out its additional underlying semantic assumptions:

  * •

The range of the type relation is a subset of its domain, i.e. every type has
a type.

  * •

The type relation includes entities typing to itself, which allows for
generating type hierarchies of arbitrary size from a finite set of distinct
base entities. We discuss below why this assumption does not lead to well-
known paradoxes in $\mathtt{d}$.

  * •

There should be no inequivalent types of an element, or in other words, the
type relation is restricted to be a function. This means that $\mathtt{d}$
needs to satisfy the type uniqueness property (see Section 35). We will review
this assumption in Section 5.4.

It is well known that types can be interpreted as propositions and elements as
proofs [16]. In our semantic setting this analogy is valid and we will make
use of it throughout the paper, for example when motivating and describing the
roles of operators we will frequently use the viewpoint of propositions and
proofs.

Note that in our setting the interest is in formalization of structured
mathematical reasoning rather than in computational proof content.

Finally we would like to make a notational remark related to $\mathtt{d}$ but
also to lambda-typed calculi in general. Since an operator in $\mathtt{d}$ can
be interpreted both as element and as type (or proposition), there is, in our
view, a notational and naming dilemma. For example, one and the same entity
would be written appropriately as a typed lambda-abstraction $\lambda
x\\!:\\!a.b$ in its role as an element and universal quantification $\forall
x\\!:\\!a.b$ in its role as a proposition and neither notation would
adequately cover both roles. Therefore, in this case we use a more neutral
notation $[x:a]b$ called universal abstraction. As will be seen this
notational issue also applies to other operators of $\mathtt{d}$.

After these remarks we can now turn to the core of $\mathtt{d}$ which is the
system $\lambda^{\lambda}$ [14], a reconstruction of a variation [25] of
$\Lambda$, modified with a reflexive type axiom with a constant $\tau$, see
Table 1 for its type rules.

$\displaystyle{\it(ax)}\;$ $\displaystyle\frac{}{\vdash\,\tau:\tau}$
$\displaystyle{\it(start)}\;\frac{\Gamma\vdash\,a:b}{\Gamma,x:a\vdash\,x:a}\qquad\qquad\qquad\qquad$
$\displaystyle{\it(weak)}\;$
$\displaystyle\frac{\Gamma\vdash\,a:b\qquad\Gamma\vdash\,c:d}{\Gamma,x:c\vdash\,a:b}$
$\displaystyle{\it(conv)}\;\frac{\Gamma\vdash\,a:b\qquad
b=_{\lambda}c\qquad\Gamma\vdash\,c:d}{\Gamma\vdash\,a:c}$
$\displaystyle{\it(abs_{U})}\;$
$\displaystyle\frac{\Gamma,x:a\vdash\,b:c}{\Gamma\vdash\,[x:a]b:[x:a]c}$
$\displaystyle{\it(appl)}\;\frac{\Gamma\vdash\,a:[x:b]c\qquad\Gamma\vdash\,d:b}{\Gamma\vdash\,(a\,d):c[d/x]}\qquad\;$

Table 1: The kernel of $\mathtt{d}$: The system $\lambda^{\lambda}$ [14]
modified with $\tau:\tau$

As usual, we use contexts $\Gamma=(x_{1}:a_{1},\ldots,x_{n}:a_{n})$ declaring
types of distinct variables and a $\beta$-conversion induced congruence
$=_{\lambda}$ on expressions. We use the notation $a[b/x]$ to denote the
substitution of all free occurrences of $x$ in $a$ by $b$.

Element-roles and type-roles can now be illustrated by two simple examples:
Let $C=[x:\tau]\tau$ be the constant function delivering $\tau$, for any given
argument of type $\tau$. In its role as a type $C$ corresponds to an
implication (“$\tau$ implies $\tau$”) and its proofs include the identity
$I=[x:\tau]x$ over $\tau$, i.e. $\vdash\,I:C$ using essentially the rules
start and absU. In its role as an element $C$ corresponds to a constant
function and it will type to itself, i.e. $\vdash\,C:C$ using essentially the
rules ax and absU. $I$, which as an element is obviously the identity
function, in its role as a type corresponds to the proposition “everything of
type $\tau$ is true” which of course should not have any elements (this is
shown in Section 4.4).

More generally, in the rule appl the type-role of a universal abstraction
($[x:b]c$) can be intuitively understood as an infinite conjunction of
instances ($c[b_{1}/x]\wedge c[b_{2}/x]\ldots$ where $b_{i}:b$ for all $i$).
Individual instances ($c[b_{i}/x]$) can be projected by means of the
application operator. Intuitively, a proof of a universal abstraction
($[x:a]c$) must provide an infinite list of instances
($b[a_{1}/x],b[a_{2}/x],\ldots$ where $b[a_{i}/x]:c[a_{i}/x]$ for all $i$).
Consequently, in the rule absU a universal abstraction ($[x:a]b$ where
$x:a\\!\vdash\\!b:c$) has the element-role of being a proof of another
universal abstraction ($[x:a]c$).

As another example, the introduction and elimination rules for universal
quantification can be derived almost trivially. Note that in this and the
following examples we write $[a\\!\Rightarrow\\!b]$ to denote $[x:a]b$ if $x$
does not occur free in $b$:

$\displaystyle P:[a\\!\Rightarrow\\!b]\;\;\vdash\,\;\;[x:[y:a](P\,y)]x$
$\displaystyle:$ $\displaystyle[[y:a](P\,y)\\!\Rightarrow\\![y:a](P\,y)]$
$\displaystyle{}P:[a\\!\Rightarrow\\!b]\;\;\vdash\,\;\;[x:a][z:[y:a](P\,y)](z\,x)$
$\displaystyle:$ $\displaystyle[x:a][[y:a](P\,y)\\!\Rightarrow\\!(P\,x)]$

When substituting $P$ by a constant function $[a\\!\Rightarrow\\!c]$ (where
$\\!\vdash\\!c:b$) the deductions simplify to two variants of the modus ponens
rule:

$\displaystyle\vdash\,\;\;[x:[a\\!\Rightarrow\\!c]]x$ $\displaystyle:$
$\displaystyle[[a\\!\Rightarrow\\!c]\\!\Rightarrow\\![a\\!\Rightarrow\\!c]]$
$\displaystyle{}\vdash\,\;\;[x:a][z:[a\\!\Rightarrow\\!c]](z\,x)$
$\displaystyle:$
$\displaystyle[a\\!\Rightarrow\\![[a\\!\Rightarrow\\!c]\\!\Rightarrow\\!c]]$

In contrast to other type systems with $\lambda$-structured types,
$\mathtt{d}$ is using a reflexive axiom (ax). This might seem very strange as
the use of a reflexive axiom in combination with basic rules of PTS leads to
paradoxes, e.g. [6][17], see also [4](Section 5.5). However, as will be seen,
in our setting of $\lambda$-structured types, the axiom ax leads to a
consistent system. This is actually not very surprising since
$\lambda^{\lambda}$ does not have an equivalent to the product rule used in
PTS:

$\displaystyle{\it(product)}\;\;$
$\displaystyle\frac{\Gamma\vdash\,a:s_{1}\quad\Gamma,x:a\vdash\,b:s_{2}}{\Gamma\vdash\,(\Pi
x:a.b):s_{3}}\quad\text{where}\;s_{i}\in S,\;\text{$S$ is a set of sorts}$

Adding such a rule, appropriately adapted, to the kernel of $\mathtt{d}$ would
violate uniqueness of types [18] and allow for reconstructing well-known
paradoxes [32] (see also Section 5.4). Without such a rule, functions from
$\tau$ such as $I$ do not accept functional arguments such as $C$111In fact,
$(I\;C)$ cannot be typed since $()\\!\vdash\\!I:[x:\tau]\tau$, hence $I$ is
expecting arguments of type $\tau$, but $()\\!\vdash\\!C:C$ and
$\tau\neq_{\lambda}C$. The lack of functions of type $\tau$ is the reason for
achieving both consistency and $\tau:\tau$.

Unlike instances of PTS (e.g. [21]), systems with $\lambda$-structured types
have never been extended by existential or classical propositional operators.
While the kernel of $\mathtt{d}$ is sufficiently expressive to axiomatize
basic mathematical structures (Sections 3.2, 3.3) the expressive and
structuring means of deductions can be enhanced by additional operators. We
begin with an operator that effectively provides for a deduction interface,
i.e. a mechanism to hide details of interdependent deductions. For this
purpose, in analogy to a universal abstraction ($[x:a]b$), $\mathtt{d}$
introduces an existential abstraction ($[x!a]b$) (see Table 2 for its type
rules).

$\displaystyle{\it(def)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b\quad\Gamma\\!\vdash\\!c:d[a/x]\quad\Gamma,x:b\\!\vdash\\!d:e}{\Gamma\\!\vdash\\![x\\!\doteq\\!a,c:d]:[x!b]d}$
$\displaystyle{\it(abs_{E})}\;\;$
$\displaystyle\frac{\Gamma,x:a\\!\vdash\\!b:c}{\Gamma\\!\vdash\\![x!a]b:[x:a]c}$
$\displaystyle{\it(ch_{I})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[x!b]c}{\Gamma\\!\vdash\\!a.1:b}$
$\displaystyle{\it(ch_{B})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[x!b]c}{\Gamma\\!\vdash\\!a.2:c[a.1/x]}$

Table 2: Type rules for existential abstractions

The notation is intended to maximise coherence with universal abstraction. The
type-role of a existential abstraction ($[x!b]d$) can be intuitively
understood as an infinite disjunction ($d[b_{1}/x]\vee d[b_{2}/x]\ldots$ where
$b_{i}:b$ for all $i$). A proof of an existential abstraction ($[x!b]d$) must
prove one of the instances (say $d[b_{j}/x]$), i.e. it must provide an
instance of the quantification domain ($b_{j}:b$) and an element proving the
instantiated formula ($c:d[b_{j}/x]$). This is formalized in rule def with a
new operator called protected definition combining the two elements and a tag
for the abstraction type ($[x\\!\doteq\\!a,c:d]$)222The type tag $d$ in
$[x\\!\doteq\\!a,c:d]$ is necessary to ensure uniqueness of types. This means
that two deductions ($a$ and $c$), where one ($c$) is using the other one
($a$) in its type, are simultaneously abstracted from in an existential
abstraction type. The element-role of a existential abstraction ($[x!a]b$) is
not one of a logical operator but of an entity providing an infinite list of
instances ($b[a_{1}/x]$, $b[a_{2}/x]$, $\ldots$ where $a_{i}:a$ for all $i$).
But, as we just discussed above with respect to typing of universal
abstractions (absU), this is sufficient to type it to a universal abstraction
(absE). Hence the element-roles of universal and existential abstraction are
equivalent. Pragmatically the element-role of existential abstraction is less
frequently used and of less importance. This is the reason why the notation
for existential abstractions is more “type-oriented” than that of universal
abstraction.

In analogy to the type-elimination of universal abstraction, projections
($a.1$ and $a.2$ 333A postfix notation has been chosen since it seems more
intuitive for projection sequences.) are introduced as type-eliminators for
existential abstraction with obvious equivalence laws.

$[x\\!\doteq\\!a,b:c].1=_{\lambda}a\qquad[x\\!\doteq\\!a,b:c].2=_{\lambda}b$

The type rules chI and chB for projections are similar to common rules for
$\Sigma$ types, e.g. [21].

As an example, the introduction and elimination rules for existential
quantification can be derived as follows (with
$\Gamma=(P,Q:[a\\!\Rightarrow\\!b])$):

$\displaystyle\Gamma\;\vdash\,\;[x\\!:\\!a][z\\!:\\!(P\,x)][y\\!\doteq\\!x,z:(P\,y)]$
$\displaystyle:$ $\displaystyle[x:a][(P\,x)\\!\Rightarrow\\![y!a](P\,y)]$
$\displaystyle\Gamma\;\vdash\,\;[x\\!:\\![y_{1}!a](Py_{1})][z\\!:\\![y_{2}\\!:\\!a][(Py_{2})\\!\Rightarrow\\!(Qy_{2})]]$
$\displaystyle[y_{3}\\!\doteq\\!x.1,((z\>x.1)x.2):(Qy_{3})]$ $\displaystyle:$
$\displaystyle[[y_{1}!a](Py_{1})$
$\displaystyle\;\;\\!\Rightarrow\\![[y_{2}\\!:\\!a][(Py_{2})\\!\Rightarrow\\!(Qy_{2})]\\!\Rightarrow\\![y_{3}!a](Qy_{3})]]$

A more detailed explanation of these deductions is given in Sections 2.2 and
2.3. Note how the second example illustrates in a nutshell the role of
existential abstraction as a deduction interface. It can be understood as the
transformation of a deduction on the basis of a reference ($x$) to its
interface ($[y_{1}!a](Py_{1})]$) followed by the creation of a new interface
($[y_{3}!a](Qy_{3})]$) hiding the transformation details (application of $z$
to the extracted interdependent elements $x.1$ and $x.2$). More applications
will be shown in Section 3, in particular in Sections 3.5(Partial functions),
3.6(Defining functions from deductions), and 3.8(Proof structuring).

The rule absE has the consequence that existential abstractions can now be
instantiated as elements in the elimination rule for universal abstraction,
i.e. the rule appl can be instantiated as follows:

$({\it
appl})[[x!a_{1}]a_{2}/a]\quad\frac{\Gamma\\!\vdash\\![x!a_{1}]a_{2}:[x:b]c\quad\Gamma\\!\vdash\\!d:b}{\Gamma\\!\vdash\\!([x!a_{1}]a_{2}\,d):c[d/x]}$

This motivates the extension of $\beta$-equality to existential abstractions,
i.e. we have

$([x:a]b\;c)\;=_{\lambda}\;b[c/x]\;=_{\lambda}\;([x!a]b\;c)$

Note that this properties merely state that both abstractions have equivalent
functional behaviour when applied to arguments. However, they are not
identical and this semantic distinction is represented by their role in the
type relation. For example, note that from $x:[y!a]b$ and $z:a$ one cannot
conclude $(x\,z):([y!a]b\,z)$. Note that this approach naturally precludes
adding axioms of extensionality as their sole purpose is to deny such
distinctions.

Finally, one might wonder why not type an existential abstraction $[x!a]b$ to
an existential abstraction $[x!a]c$ (assuming $x:a\\!\vdash\\!b:c$)? According
to the intuitive understanding of the type role of an existential abstraction
as an infinite disjunction this would be logically invalid and indeed it is
quite easy to see such a rule would lead to inconsistency444 First, with such
a rule the type $P=[x:\tau][y!x]\tau$ would have itself as an element, i.e.
$\\!\vdash\\!P:P$. However from a declaration of this type one could then
extract a proof of $[z:\tau]z$ as follows
$y:P\\!\vdash\\![z:\tau](y\,z).1:[z:\tau]z$..

The remaining part of $\mathtt{d}$ are some propositional operators (see Table
3 for their type rules).

$\displaystyle{\it(prd)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:c\quad\Gamma\\!\vdash\\!b:d}{\Gamma\\!\vdash\\![a,b]:[c,d]}\quad\;\;\;$
$\displaystyle{\it(sum)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:c\quad\Gamma\\!\vdash\\!b:d}{\Gamma\\!\vdash\\![a+b]:[c,d]}$
$\displaystyle{\it(pr_{L})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[b,c]}{\Gamma\\!\vdash\\!a.1:b}$
$\displaystyle{\it(pr_{R})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[b,c]}{\Gamma\\!\vdash\\!a.2:c}$
$\displaystyle{\it(inj_{L})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b\quad\Gamma\\!\vdash\\!c:d}{\Gamma\\!\vdash\\![a,:\\!c]:[b+c]}$
$\displaystyle{\it(inj_{R})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b\quad\Gamma\\!\vdash\\!c:d}{\Gamma\\!\vdash\\![:\\!c,a]:[c+b]}$
$\displaystyle{\it(case)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[x:c_{1}]d\quad\Gamma\\!\vdash\\!b:[y:c_{2}]d\quad\Gamma\\!\vdash\\!d:e}{\Gamma\\!\vdash\\![a\,?\,b]:[z:[c_{1}+c_{2}]]d}\qquad\qquad\qquad\qquad\quad$
$\displaystyle{\it(neg)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b}{\Gamma\\!\vdash\\!\neg a:b}$

Table 3: Type rules for propositional operators

$\mathtt{d}$ adds a product ($[a,b]$) as a binary variation of universal
abstraction ($[x:a]b$), i.e. with an element-role as a binary pair and an
type-role as a binary conjunction. Due to the same notation dilemma as for
universal abstraction, i.e. neither the notation for pairs $\langle
a,b\rangle$ nor for conjunctions $a\wedge b$ would be satisfactory, we use the
neutral notation $[a,b]$. The type rules prd, prR, and Phys. Rev. Lett. for
products directly encode the introduction and elimination rules for
conjunctions. The equivalence laws for projection are extended in an obvious
way.

$[a,b].1=_{\lambda}a\qquad[a,b].2=_{\lambda}b$

As a example we show that existential abstractions without dependencies (i.e.
$[x!a]b$, where $x$ does not occur free in $b$) are logically equivalent to
products:

$\displaystyle\vdash\,\;\;[y:[x!a]b][y.1,y.2]$ $\displaystyle:$
$\displaystyle[[x!a]b\\!\Rightarrow\\![a,b]]$
$\displaystyle{}\vdash\,\;\;[y:[a,b]][x\\!\doteq\\!y.1,y.2:b]$
$\displaystyle:$ $\displaystyle[[a,b]\\!\Rightarrow\\![x!a]b]$

Similarly $\mathtt{d}$ adds a sum ($[b_{1}+b_{2}]$) as a binary variation of
the existential abstraction ($[x!a]b$), i.e. with an element-role as a binary
pair and an type-role as a binary disjunction. Consequently, there is a type
sequence analogous to existential abstraction: Expressions ($a_{1}:b_{1}$,
$a_{2}:b_{2}$) may be used within injections ($[a_{1},:\\!b_{2}]$,
$[:\\!b_{1},a_{2}]$) (injections are the analogue to protected definitions),
which type to a sum ($[b_{1}+b_{2}]$) which types to a product. The bracket
notation for products and abstractions is extended to injections and sums for
notational coherence. Similarly to existential abstraction we use a more type-
oriented notation for sums. The injection rules directly encode the
introduction rules for disjunctions and rule case introduces a case
distinction operator. Two equivalence laws describe its functional
interpretation.

$([a\,?\,b]\,[c,:\\!d])=_{\lambda}(a\,c)\qquad([a\,?\,b]\,[:\\!c,d])=_{\lambda}(b\,d)$

As an example, the introduction and elimination rules for disjunction can be
derived as follows:

$\displaystyle\vdash\,\;\;[[x:a][x,:\\!b]],[x:a][:\\!b,x]]$ $\displaystyle:$
$\displaystyle[[a\\!\Rightarrow\\![a+b]],[a\\!\Rightarrow\\![b+a]]]$
$\displaystyle{}\vdash\,\;\;[x:[a+b]][y:[a\\!\Rightarrow\\!c]][z:[b\\!\Rightarrow\\!c]]([y\,?\,z]\,x)$
$\displaystyle:$
$\displaystyle[[a+b]\\!\Rightarrow\\![[a\\!\Rightarrow\\!c]\\!\Rightarrow\\![[b\\!\Rightarrow\\!c]\\!\Rightarrow\\!c]]]$

In the second example, in analogy to existential abstractions, a reference
($x$) to an interface ($[a+b]$) is hiding the information which particular
proposition ($a$ or $b$) is proven.

In analogy to the $\beta$-equality for existential abstraction, projection is
extended to sums.

$[a+b].1=_{\lambda}a\qquad[a+b].2=_{\lambda}a$

Finally, to support common mathematical reasoning practices, $\mathtt{d}$
introduces a classical negation operator $\neg a$ which has a neutral type
rule neg and which defines an equivalence class of propositions w.r.t.
classical negation. The central logical properties are double negation and De
Morgan’s laws:

$a=_{\lambda}\neg\neg a\qquad[a,b]=_{\lambda}\neg[\neg a+\neg
b]\qquad[x\\!:\\!a]b=_{\lambda}\neg[x!a]\neg b$

Furthermore, negation has no effect on operators without a possibility of
applying an elimination operator to its use as a type.

$\neg\tau=_{\lambda}\tau\qquad\neg[x\\!\doteq\\!a,b:c]=_{\lambda}[x\\!\doteq\\!a,b:c]$
$\neg[a,:\\!b]=_{\lambda}[a,:\\!b]\qquad\neg[:\\!a,b]=_{\lambda}[:\\!a,b]\qquad\neg[a\,?\,b]=_{\lambda}[a\,?\,b]$

The negation laws define many negated formulas as equivalent which helps to
eliminate many routine applications of logical equivalences in deductions. For
example, the following laws can be derived for arbitrary well-typed
expressions $a,b$.

$\displaystyle\vdash\,\;\;\;[x:a]x$ $\displaystyle:$
$\displaystyle[a\\!\Rightarrow\\!a]\;=_{\lambda}\;[\neg\neg
a\\!\Rightarrow\\!a]\;=_{\lambda}\;[a\\!\Rightarrow\\!\neg\neg a]$
$\displaystyle\vdash\,\;\;\;[x:\neg[a,b]]x$ $\displaystyle:$
$\displaystyle[\neg[a,b]\\!\Rightarrow\\![\neg a\\!+\\!\neg
b]]\;=_{\lambda}\;[[\neg a\\!+\\!\neg b]\\!\Rightarrow\\!\neg[a,b]]$
$\displaystyle\vdash\,\;\;\;[x:\neg[x!a]b]x$ $\displaystyle:$
$\displaystyle[\neg[x!a]b\,\\!\Rightarrow\\!\,[x\\!:\\!a]\neg
b]\;=_{\lambda}\;[[x\\!:\\!a]\neg b\,\\!\Rightarrow\\!\,\neg[x!a]b]$

Truth and falsehood can now be defined as follows:

$\mathbf{ff}:=[x:\tau]x\qquad\mathbf{tt}:=\neg\mathbf{ff}$

Note that falsehood is just a new convenient notation for type role of the
identity ($\mathbf{ff}=I$). The expected properties follow almost directly:

$\displaystyle\vdash\,\;\;[x:\tau][y:\mathbf{ff}](y\,x)$ $\displaystyle:$
$\displaystyle[x:\tau][\mathbf{ff}\\!\Rightarrow\\!x]$
$\displaystyle\vdash\,\;\;[x\\!\doteq\\!\tau,\tau:\neg x]$ $\displaystyle:$
$\displaystyle\mathbf{tt}$

In the proof of $\mathbf{tt}$ note that $\mathbf{tt}=_{\lambda}[x!\tau]\neg x$
and $\tau:\tau=_{\lambda}\neg\tau=_{\lambda}(\neg x)[\tau/x]$.

Equivalence rules for negation obviously do not yield all logical properties
of negation, e.g. they are not sufficient to prove $[a+\neg a]$. Therefore one
has to assume additional axioms. Similarly, due to the limited strength of
$\mathtt{d}$, additional axioms must also be added for the mathematical
structures whose deductions are to be formalized (for both see Section 3).

As this completes the overview of $\mathtt{d}$, one may ask for its general
advantages w.r.t. PTS. While essentially equivalent expressive means could
probably also be defined in a more classical semantic setting, the purely
functional approach of $\mathtt{d}$ can be considered as conceptually more
simple. Independently from the semantic setting the use of common logical
quantifiers and propositional connectors including a classical negation with
rich equivalence laws seems more suitable for modelling mathematical
deductions than encoded operators or operators with constructive
interpretation.

The remainder of this paper is structured as follows: A formal definition of
$\mathtt{d}$ is presented in Section 2 and several application examples are
shown in Section 3. Readers with less focus on the theoretical results can
well read Section 3 before Section 2. The main part of the paper is Section 4
containing proofs of confluence, subject reduction, uniqueness of types,
strong normalization, and consistency.

##  2 Definition

First we summarize the syntax (which has been motivated in Section 1) and
define some basic notions such as free occurrences of variables. We then
define the congruence relation $a=_{\lambda}b$ as transitive and symmetric
closure of a reduction relation $a\to^{*}b$. Finally we define contexts
$\Gamma$ and the type relation $\Gamma\\!\vdash\\!a:b$.

###  2.1 Basic definitions

[Expressions] Let $\mathcal{V}=\\{x,y,z,\ldots\\}$ be an infinite set of
variables. The set of expressions $\mathcal{E}$ is generated by the following
rules

$\displaystyle\mathcal{E}$ $\displaystyle\\!::=\\!$
$\displaystyle\tau\,\mid\,\mathcal{V}$
$\displaystyle\,\mid\,[\mathcal{V}:\mathcal{E}]\mathcal{E}\,\mid\,(\mathcal{E}\,\mathcal{E})$
$\displaystyle\,\mid\,[\mathcal{V}!\mathcal{E}]\mathcal{E}\,\mid\,[\mathcal{V}\\!\doteq\\!\mathcal{E},\mathcal{E}:\mathcal{E}]\,\mid\,\mathcal{E}.1\,\mid\,\mathcal{E}.2$
$\displaystyle\,\mid\,[\mathcal{E},\mathcal{E}]\,\mid\,[\mathcal{E}+\mathcal{E}]\,\mid\,[\mathcal{E},:\\!\mathcal{E}]\,\mid\,[:\\!\mathcal{E},\mathcal{E}]\,\mid\,[\mathcal{E}\,?\,\mathcal{E}]\,\mid\,\neg\mathcal{E}$

Expressions will be denoted by $a,b,c,d,\ldots$,

  * •

$\tau$ is the primitive constant, $x,y,z,\ldots\in\mathcal{V}$ are variables,

  * •

$[x:a]b$ is a universal abstraction, $(a\,b)$ is an application,

  * •

$[x!a]b$ is an existential abstraction, $[x\\!\doteq\\!a,b:c]$ is a protected
definition, $a.1$ and $a.2$ are left- and right-projection,

  * •

$[a,b]$ is a product, $[a+b]$ is a sum, $[a,:\\!b]$ and $[:\\!a,b]$ are left-
and right-injection, $[a\,?\,b]$ is a case distinction, and $\neg a$ is a
negation.

For the sake of succinctness and homogenity in the following definitions we
are using some additional notations for groups of operations:

$\displaystyle[a\oplus b]$ stands for $\displaystyle[a,b]\;\text{or}\;[a+b]$
$\displaystyle\oplus(a_{1},\ldots,a_{n})$ stands for
$\displaystyle\begin{cases}a_{1}.1,a_{1}.2,\text{or}\;\neg
a_{1}&\text{if}\;n=1\\\ (a_{1}\,a_{2}),[a_{1}\oplus
a_{2}],[a_{1},:\\!a_{2}],[:\\!a_{1},a_{2}]\;\text{or}\;[a_{1}\,?\,a_{2}]&\text{if}\;n=2\end{cases}$
$\displaystyle\oplus_{x}(a_{1},\ldots,a_{n})$ stands for
$\displaystyle\begin{cases}[x:a_{1}]a_{2}\;\text{or}\;[x!a_{1}]a_{2}&\text{if}\;n=2\\\
[x\\!\doteq\\!a_{1},a_{2}:a_{3}]&\text{if}\;n=3\end{cases}$

If one of these notations is used more than once in an equation or inference
rule it always denotes the same concrete operation. [Free variables,
substitution] Variables occurring in an expression which do not occur in the
range of a binding occur free in the expression. ${\it FV}(a)$ which denotes
the set of free variables of an expression $a$ is defined as follows:

$\displaystyle{\it FV}(\tau)$ $\displaystyle=$ $\displaystyle\\{\\}$
$\displaystyle{\it FV}(x)$ $\displaystyle=$ $\displaystyle\\{x\\}$
$\displaystyle{\it FV}(\oplus(a_{1},\ldots,a_{n}))$ $\displaystyle=$
$\displaystyle{\it FV}(a_{1})\cup\ldots\cup{\it FV}(a_{n})$ $\displaystyle{\it
FV}(\oplus_{x}(a_{1},\ldots,a_{n})$ $\displaystyle=$ $\displaystyle{\it
FV}(a_{1})\cup\ldots\cup{\it FV}(a_{n-1})\cup({\it
FV}(a_{n})\\!\setminus\\!\\{x\\})$

Note that in a protected definition $[x\\!\doteq\\!a_{1},a_{2}:a_{3}]$ the
binding of $x$ is for $a_{3}$ only. The substitution $a[b/x]$ of all free
occurrences of variable $x$ in expression $a$ by expression $b$ is defined as
follows:

$\displaystyle\tau[b/x]$ $\displaystyle=$ $\displaystyle\tau$ $\displaystyle
y[b/x]$ $\displaystyle=$ $\displaystyle\begin{cases}b&\text{if}\;x=y\\\
y&\text{otherwise}\end{cases}$ $\displaystyle\oplus(a_{1},\ldots,a_{n})[b/x]$
$\displaystyle=$ $\displaystyle\oplus(a_{1}[b/x],\ldots,a_{n}[b/x])$
$\displaystyle\oplus_{y}(a_{1},\ldots,a_{n})[b/x]$ $\displaystyle=$
$\displaystyle\begin{cases}\oplus_{y}(a_{1}[b/x],\ldots,a_{n-1}[b/x],a_{n})\\\
\qquad\text{if}\;x=y\\\ \oplus_{y}(a_{1}[b/x],\ldots,a_{n}[b/x])\\\
\qquad\text{otherwise}\end{cases}$

A substitution $a[b/x]$ may lead to name clashes in case a variable $y$
occurring free in the inserted expression $b$ comes into the range of a
binding of $y$ in the original expression. These name clashes can be avoided
by renaming of variables. [$\alpha$-conversion, Implicit renaming, name-
independent representations] The renaming relation on bound variables is
usually called $\alpha$-conversion and induced by the following axiom (using
the notation $=_{\alpha}$).

$\frac{y\notin{\it
FV}(a_{n})}{\oplus_{x}(a_{1},\ldots,a_{n-1},a_{n})\;=_{\alpha}\;\oplus_{y}(a_{1},\ldots,a_{n-1},a_{n}[y/x])}$

In order not to clutter the presentation, we will write variables as strings
but always assume appropriate renaming of bound variables in order to avoid
name clashes. This assumption is justified because one could also use a less-
readable but name-independent presentation of expressions using e.g. de Bruijn
indexes [8] which would avoid the necessity of renaming all together.

###  2.2 Reduction and congruence

The functional interpretation is defined by the reduction of an expression
into a more basic expression. We will later show that reduction, if it
terminates, always leads to a unique result. [Single-step reduction] Single-
step reduction $a\to b$ is the smallest relation satisfying the axioms and
inference rules of Table 4.

${\it(\beta_{1})}$ $([x:a]b\;c)$ $\to$ $b[c/x]$ ${\it(\beta_{2})}$
$([x!a]b\;c)$ $\to$ $b[c/x]$ ${\it(\beta_{3})}$ $([a\,?\,b]\,[c,:\\!d])$ $\to$
$(a\,c)$ ${\it(\beta_{4})}$ $([a\,?\,b]\,[:\\!c,d])$ $\to$ $(b\,d)$
${\it(\pi_{1})}$ $[x\\!\doteq\\!a,b:c].1$ $\to$ $a$ ${\it(\pi_{2})}$
$[x\\!\doteq\\!a,b:c].2$ $\to$ $b$ ${\it(\pi_{3})}$ $[a,b].1$ $\to$ $a$
${\it(\pi_{4})}$ $[a,b].2$ $\to$ $b$ ${\it(\pi_{5})}$ $[a+b].1$ $\to$ $a$
${\it(\pi_{6})}$ $[a+b].2$ $\to$ $b$ ${\it(\nu_{1})}$ $\neg\neg a$ $\to$ $a$
${\it(\nu_{2})}$ $\neg[a,b]$ $\to$ $[\neg a+\neg b]$ ${\it(\nu_{3})}$
$\neg[a+b]$ $\to$ $[\neg a,\neg b]$ ${\it(\nu_{4})}$ $\neg[x:a]b$ $\to$
$[x!a]\neg b$ ${\it(\nu_{5})}$ $\neg[x!a]b$ $\to$ $[x:a]\neg b$
${\it(\nu_{6})}$ $\neg\tau$ $\to$ $\tau$ ${\it(\nu_{7})}$
$\neg[x\\!\doteq\\!a,b:c]$ $\to$ $[x\\!\doteq\\!a,b:c]$ ${\it(\nu_{8})}$
$\neg[a,:\\!b]$ $\to$ $[a,:\\!b]$ ${\it(\nu_{9})}$ $\neg[:\\!a,b]$ $\to$
$[:\\!a,b]$ ${\it(\nu_{10})}$ $\neg[a\,?\,b]$ $\to$ $[a\,?\,b]$
$\displaystyle{\it(\oplus{\overbrace{(\\_,\ldots,\\_)}^{n}}_{i})}\quad$
$\displaystyle\frac{a_{i}\to
b_{i}}{\oplus(a_{1},\ldots,a_{i},\ldots,a_{n})\to\oplus(a_{1},\ldots,b_{i},\ldots,a_{n})}$
$\displaystyle{\it(\oplus_{x}{\overbrace{(\\_,\ldots,\\_)}^{n}}_{i})}\quad$
$\displaystyle\frac{a_{i}\to
b_{i}}{\oplus_{x}(a_{1},\ldots,a_{i},\ldots,a_{n})\to\oplus_{x}(a_{1},\ldots,b_{i},\ldots,a_{n})}$

Table 4: Axioms and rules for single-step reduction.

All reduction axioms have been motivated and explained in the introduction in
form of equivalence laws. [Reduction] Reduction $a\to^{*}b$ of an expression
$a$ to $b$ is defined as the reflexive and transitive closure of single-step
reduction $a\to b$. The notation $a\to^{n}b$ where $n\geq 0$ is used to
indicate $n$ consecutive single-step reductions. We use the notation
$a\to^{*}b\to^{*}c\ldots$ to indicate reduction sequences. If two expressions
reduce to a common expression we write $a\nabla b$. To show arguments about
equality in arguments about reduction we use the notation
$a_{1}=\ldots=a_{n}\;\to^{*}\;b_{1}=\ldots=b_{m}\>\to^{*}\>c_{1}=\ldots=c_{k}\ldots$.
This will also be used for sequences of $n$-step reductions $\to^{n}$ and
accordingly for sequences containing both notations. [Congruence] Congruence
of expressions, denoted by $a=_{\lambda}b$, is defined as the symmetric and
transitive closure of reduction. The notations for reduction sequences are
extended to contain congruences as well. The following simple examples
illustrate reduction and congruence:

$\displaystyle(([y_{2}:a][y:(P\>y_{2})](Q\>y_{2})\>x.1)\>x.2)$
$\displaystyle\to_{(\beta_{1})}$ $\displaystyle([y:(P\>x.1)](Q\>x.1)\>x.2)$
$\displaystyle\to_{(\beta_{1})}$ $\displaystyle(Q\>x.1)$
$\displaystyle{}[[x\\!\doteq\\!a,b:c],d].1.2$ $\displaystyle\to_{(\pi_{3})}$
$\displaystyle[x\\!\doteq\\!a,b:c].2$ $\displaystyle\to_{(\pi_{2})}$
$\displaystyle b$ $\displaystyle{}[x:\neg[y:\tau]\tau]\neg[a,b]$
$\displaystyle\to_{(\nu_{4})}$ $\displaystyle[x:[y!\tau]\neg\tau]\neg[a,b]$
$\displaystyle\to_{(\nu_{6})}$ $\displaystyle[x:[y!\tau]\tau]\neg[a,b]$
$\displaystyle\to_{(\nu_{2})}$ $\displaystyle[x:[y!\tau]\tau][\neg a+\neg b]$
$\displaystyle{}[x:\neg[a+b]][\neg a,\neg b]$ $\displaystyle=_{\lambda}$
$\displaystyle[x:[\neg a,\neg b]]\neg[a+b]$

###  2.3 Typing and Validity

[Context] A context, denoted by $\Gamma$, is a finite sequence of declarations
$(x_{1}:a_{1},\ldots,x_{n}:a_{n})$, where $x_{i}$ are variables with
$x_{i}\neq x_{j}$ and $a_{i}$ are expressions. The assumption about name-free
representation of bound variables justifies the uniqueness assumption. The
lookup of a variable in a context $\Gamma(x)$ is a partial function defined by
$\Gamma(x_{i})=a_{i}$. ${\it dom}(\Gamma)=\\{x_{1},\ldots,x_{n}\\}$ and ${\it
ran}(\Gamma)=\\{a_{1},\ldots,a_{n}\\}$ denote the domain and range of a
context $\Gamma$. $\Gamma,x:a$ denotes the extension of $\Gamma$ on the right
by a binding $x:a$ where $x$ is a variable not yet declared in $\Gamma$.
$\Gamma_{1},\Gamma_{2}$ denotes the concatenation of two contexts declaring
disjoint variables. The empty context is written as $()$.
$[\Gamma]a=[x_{1}:a_{1}]\ldots[x_{1}:a_{n}]a$ denotes the abstraction of a
context over an expression. [Typing] Typing $\Gamma\\!\vdash\\!a:b$ of $a$ to
$b$, the type of $a$, under a context $\Gamma$ is the smallest ternary
relation on contexts and two expressions satisfying the inference rules of
Table 5 all of which have been motivated and explained in Section 1.

$\displaystyle{\it(ax)}\;\;$ $\displaystyle\\!\vdash\\!\tau:\tau$
$\displaystyle{\it(start)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b}{\Gamma,x:a\\!\vdash\\!x:a}$
$\displaystyle{\it(weak)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b\quad\Gamma\\!\vdash\\!c:d}{\Gamma,x:c\\!\vdash\\!a:b}\qquad$
$\displaystyle{\it(conv)}\;\;$ $\displaystyle\frac{\Gamma\\!\vdash\\!a:b\quad
b=_{\lambda}c\quad\Gamma\\!\vdash\\!c:d}{\Gamma\\!\vdash\\!a:c}$
$\displaystyle{\it(abs_{U})}\;\;$
$\displaystyle\frac{\Gamma,x:a\\!\vdash\\!b:c}{\Gamma\\!\vdash\\![x:a]b:[x:a]c}$
$\displaystyle{\it(abs_{E})}\;\;$
$\displaystyle\frac{\Gamma,x:a\\!\vdash\\!b:c}{\Gamma\\!\vdash\\![x!a]b:[x:a]c}$
$\displaystyle{\it(appl)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[x:c]d\quad\Gamma\\!\vdash\\!b:c}{\Gamma\\!\vdash\\!(a\,b):d[b/x]}$
$\displaystyle{\it(def)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b\quad\Gamma\\!\vdash\\!c:d[a/x]\quad\Gamma,x:b\\!\vdash\\!d:e}{\Gamma\\!\vdash\\![x\\!\doteq\\!a,c:d]:[x!b]d}\qquad\qquad\qquad\qquad\qquad$
$\displaystyle{\it(ch_{I})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[x!b]c}{\Gamma\\!\vdash\\!a.1:b}$
$\displaystyle{\it(ch_{B})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[x!b]c}{\Gamma\\!\vdash\\!a.2:c[a.1/x]}\qquad$
$\displaystyle{\it(prd)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:c\quad\Gamma\\!\vdash\\!b:d}{\Gamma\\!\vdash\\![a,b]:[c,d]}\quad\;\;\;$
$\displaystyle{\it(sum)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:c\quad\Gamma\\!\vdash\\!b:d}{\Gamma\\!\vdash\\![a+b]:[c,d]}$
$\displaystyle{\it(pr_{L})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[b,c]}{\Gamma\\!\vdash\\!a.1:b}$
$\displaystyle{\it(pr_{R})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[b,c]}{\Gamma\\!\vdash\\!a.2:c}$
$\displaystyle{\it(inj_{L})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b\quad\Gamma\\!\vdash\\!c:d}{\Gamma\\!\vdash\\![a,:\\!c]:[b+c]}$
$\displaystyle{\it(inj_{R})}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b\quad\Gamma\\!\vdash\\!c:d}{\Gamma\\!\vdash\\![:\\!c,a]:[c+b]}$
$\displaystyle{\it(case)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:[x:c_{1}]d\quad\Gamma\\!\vdash\\!b:[y:c_{2}]d\quad\Gamma\\!\vdash\\!d:e}{\Gamma\\!\vdash\\![a\,?\,b]:[z:[c_{1}+c_{2}]]d}\qquad\qquad\qquad\qquad\quad$
$\displaystyle{\it(neg)}\;\;$
$\displaystyle\frac{\Gamma\\!\vdash\\!a:b}{\Gamma\\!\vdash\\!\neg a:b}$

Table 5: Axiom and rules for typing.

We often use the notation
$\Gamma\\!\vdash\\!a_{1}=\ldots=a_{n}\>:\>b_{1}=\ldots=b_{m}$ to indicate
arguments about equality of expressions in proofs about the type relation.
Sometimes we also mix the use of $=_{\lambda}$ and $=$ in this notation. As a
simple example consider the introduction and elimination laws for existential
quantification (see Section 1). The type determination of the first law can be
seen as follows: With $\Gamma_{1}=(P:[y:a]b,x:a,z:(P\,x))$) where $y\notin{\it
FV}(b)$ and since $(P\,y)[x/y]=P(\,x)$ by the rules start, weak, and appl we
obtain

$\Gamma_{1}\vdash\,x:a\qquad\Gamma_{1}\vdash\,z:(P\,y)[x/y]\qquad\Gamma_{1}\vdash\,(P\,y):b$

which due to the rule def implies that

$\displaystyle\Gamma_{1}$ $\displaystyle\vdash\,$
$\displaystyle[y\\!\doteq\\!x,z:(P\,y)]:[y!a](P\,y)$

The type relation in Section 1 follows from rule absU. The type determination
of the second law can be seen as follows, let

$\displaystyle\Gamma_{2}$ $\displaystyle=$
$\displaystyle(P:[y:a]b,Q:[y:a]b,x:[y_{1}!a](P\,y_{1}),z:[y_{2}\\!:\\!a][y:(P\,y_{2})](Q\,y_{2}))$

By rules start, weak, and appl we obtain:

$\Gamma_{2}\vdash\,(z\,x.1):[u:(P\,x.1)](Q\,x.1)$

From this, by the same rules we obtain:

$\Gamma_{2}\vdash\,((z\,x.1)\>x.2):(Q\,x.1)=(Q\,y_{3})[x.1/y_{3}]$

Similarly to the first law, by rule def this implies

$\displaystyle\Gamma_{2}$ $\displaystyle\vdash\,$
$\displaystyle[y_{3}\\!\doteq\\!x.1,((z\>x.1)\>x.2):(Q\,y_{3})]\;\;:\;\;[y_{3}!a](Q\,y_{3})$

Again, the remainder follows from rule absU. [Validity] Validity
$\Gamma\\!\vdash\\!a$ of an expression $a$ under a context $\Gamma$ is defined
as the existence of a type:

$\displaystyle\Gamma\vdash\,a$ $\displaystyle\text{if and only if there is a
$b$ such that}\;\;\Gamma\\!\vdash\\!a:b$

Similarly to typing we use the notation
$\Gamma_{1}=\ldots=\Gamma_{n}\\!\vdash\\!a_{1}=\ldots=a_{n}$ to indicate
arguments about equality of contexts and expressions in proofs about validity.
Similarly for congruence $=_{\lambda}$ or combinations of both. We also use
the notation $\Gamma\\!\vdash\\!a_{1},\ldots,a_{n}$ as an abbreviation for
$\Gamma\\!\vdash\\!a_{1}$, $\ldots$, $\Gamma\\!\vdash\\!a_{n}$. As for typing,
we also omit writing the empty context.

##  3 Examples

The purpose of this section is to illustrate the basic style of axiomatizing
theories and describing deductions when using $\mathtt{d}$. Note that the
example are presented with fully explicit expressions of $\mathtt{d}$, i.e. we
do not omit any subexpressions which could be inferred from other parts using
pattern matching or proof tactics and we do not use a module concept for
theories. Such features should of course be part of any practically useful
approach for formal deductions on the basis of $\mathtt{d}$.

######  Remark 1 (Notational conventions).

For convenience, in the examples we write $[x_{1}:a_{1}]\ldots[x_{n}:a_{n}]a$
as $[x_{1}:a_{1};\ldots;x_{n}:a_{n}]a$ and $[x_{1}:a]\ldots[x_{n}:a]b$ as
$[x_{1},\ldots,x_{n}:a]b$ and similar for existential abstractions. We also
use combinations of these abbreviations such that e.g. $[x:a;y_{1},y_{2}!b]c$
is shorthand for $[x:a][y_{1}!b][y_{2}!b]c$. We write $[a\\!\Rightarrow\\!b]$
to denote $[x:a]b$ if $x\notin{\it FV}(b)$. Similarly, we write
$[a_{1}\\!\Rightarrow\\!\ldots[a_{n}\\!\Rightarrow\\!a]\ldots]$ as
$[a_{1};\ldots;a_{n}\\!\Rightarrow\\!a]$. We write nested applications
$(\ldots((a\,a_{1})\,a_{2})\ldots\,a_{n})$ as $(a\,a_{1}\ldots a_{n})$. We
also write $\Gamma\\!\vdash\\!a:b$ as $a:b$ if $\Gamma$ is empty or has been
made clear from the context. When writing $a:b\;({\it name})$ we introduce
$name$ as abbreviation for $a$ of type $b$.

###  3.1 Additional axioms for negation

In Section 1 we explained the necessity of additional negation axioms. Note
that, without additional axioms, even constructive laws of negation are
missing, as for example, the contrapositive laws is not valid. In principle
many different axioms schemes are possible. For example, one could be inspired
by the rules for negation in sequent calculus ($\underline{A}$ stands for a
sequence of formulas $A_{1}$, $\ldots$, $A_{n}$):

$\frac{\underline{C}\\!\vdash\\!A,\underline{B}}{\underline{C},\neg
A\\!\vdash\\!\underline{B}}\;(L\neg)\qquad\frac{\underline{C},A\\!\vdash\\!\underline{B}}{\underline{C}\\!\vdash\\!\neg
A,\underline{B}}\;(R\neg)$

Theses rule together with the negations axioms inspire the following axiom
schemes indexed over expressions $a$ and $b$:

$\neg^{+}_{a,b}:[[a+b]\\!\Rightarrow\\![\neg
a\\!\Rightarrow\\!b]]\qquad\neg^{-}_{a,b}:[[a\\!\Rightarrow\\!b]\\!\Rightarrow\\![\neg
a+b]]\qquad(*)$

where $\neg^{+}_{a,b},\neg^{-}_{a,b}\in\mathcal{V}$ are from a infinite set of
variables ${\it I_{Ax}}$. Formally, typing an expression $c$ to an expression
$d$ under the above axiom scheme could be defined so as to require that ${\it
FV}(d)=\emptyset$ and that there is a context $\Gamma$ consisting of (a finite
sequence of) declarations of variables from ${\it I_{Ax}}$ such that
$\Gamma\\!\vdash\\!c:d$.

Assuming this axiom scheme we can now show the law of the excluded middle:

$\displaystyle\;(\neg^{-}_{\neg a,\neg a}\;[x:\neg a]x)$ $\displaystyle:$
$\displaystyle[a+\neg a]$

Note that $\neg^{-}_{a,b}$ and $\neg^{+}_{\neg a,b}$ state that universal
abstractions without dependencies (i.e. $[a\\!\Rightarrow\\!b]$) are logically
equivalent to the classical definition of implications:

$\neg^{-}_{a,b}:[[a\\!\Rightarrow\\!b]\,\\!\Rightarrow\\![\neg
a+b]]\qquad\neg^{+}_{\neg a,b}:[[\neg
a+b]\\!\Rightarrow\\![a\\!\Rightarrow\\!b]]$

On the basis of this equivalence it is easy to show the remaining laws of
negation.

###  3.2 Equality

Basic axioms about an equality congruence relation on expressions of equal
type can be formalized as context Equality:

$\displaystyle{\it Equality}:=\;(\;(.)\\!=_{(.)}\\!(.)$ $\displaystyle:$
$\displaystyle[S:\tau][S;S\\!\Rightarrow\\!S]$ $\displaystyle E_{1}$
$\displaystyle:$ $\displaystyle[S:\tau;x:S]x\\!=_{S}\\!x$ $\displaystyle
E_{2}$ $\displaystyle:$
$\displaystyle[S:\tau;x,y:S][x\\!=_{S}\\!y\>\\!\Rightarrow\\!\>y\\!=_{S}\\!x]$
$\displaystyle E_{3}$ $\displaystyle:$
$\displaystyle[S:\tau;x,y,z:S][x\\!=_{S}\\!y;y\\!=_{S}\\!z\>\\!\Rightarrow\\!\>x\\!=_{S}\\!z]$
$\displaystyle E_{4}$ $\displaystyle:$
$\displaystyle[S_{1},S_{2}:\tau;x,y:S_{1};F:[S_{1}\\!\Rightarrow\\!S_{2}]][x\\!=_{S_{1}}\\!y\>\\!\Rightarrow\\!\>(F\,x)\\!=_{S_{2}}\\!(F\,y)])$

Here $S$ is an variable used to abstract over the type of the expressions to
be equal. Note that, for better readability, we use the infix notation
$x=_{S}y$, introduced by a declaration
$(.)\\!=_{(.)}\\!(.):[S:\tau][S;S\\!\Rightarrow\\!S]$. Equivalently we could
have written $((.)\\!=_{(.)}\\!(.)\,S\,x\,y)$.

###  3.3 Natural Numbers

Assuming the context Equality, well-known axioms about naturals numbers can be
formalized as context Naturals:

$\displaystyle{\it Naturals}:=\quad(\quad N$ $\displaystyle:$
$\displaystyle\tau$ $\displaystyle 0$ $\displaystyle:$ $\displaystyle N$
$\displaystyle s$ $\displaystyle:$ $\displaystyle[N\\!\Rightarrow\\!N]$
$\displaystyle(.)\\!+\\!(.),(.)\\!*\\!(.)$ $\displaystyle:$
$\displaystyle[N;N\\!\Rightarrow\\!N]$ $\displaystyle S_{1}$ $\displaystyle:$
$\displaystyle[n:N]\neg((s\,n)\\!=_{N}\\!0)$ $\displaystyle S_{2}$
$\displaystyle:$
$\displaystyle[n,m:N][(s\,n)\\!=_{N}\\!(s\,m)\>\\!\Rightarrow\\!\>n\\!=_{N}\\!m]$
$\displaystyle A_{1}$ $\displaystyle:$ $\displaystyle[n:N]0+n=_{N}n$
$\displaystyle A_{2}$ $\displaystyle:$
$\displaystyle[n,m:N](s\,n)+m=_{N}(s\,(n+m))$ $\displaystyle M_{1}$
$\displaystyle:$ $\displaystyle[n:N]0*n=_{N}0$ $\displaystyle M_{2}$
$\displaystyle:$ $\displaystyle[n,m:N](s\,n)*m=_{N}m+(n*m)\quad)$

Note that, for better readability, we use infix notations $n+m$ and $n*m$
abbreviating the expressions $(+\,n\,m)$ and $(*\,n\,m)$. As an example, a
simple property can be (tediously) deduced under the context $({\it
Equality},{\it Naturals},n:N)$ where $1:=(s\,0)$:

$(E_{3}\;N\;(1\\!+\\!n)\;(s\,(0+n))\;(s\,n)$ |  |
---|---|---
$\quad(A_{2}\,0\,n)\;(E_{4}\;N\;N\;(0\\!+\\!n)\;n\;[k:N](s\,k)\;(A_{1}\,n)))$ | : | $1+n\\!=_{N}\\!(s\,n)$

We give two examples of predicates defined on natural numbers as follows
(where $2:=(s\,1)$):

$\displaystyle(.)\geq(.)$ $\displaystyle:=$
$\displaystyle[n,m:N;k!N]n=_{N}m+k$ $\displaystyle{\it even}$
$\displaystyle:=$ $\displaystyle[n:N;m!N]n=2*m$

The property $[n:N][({\it even}\>n)\\!\Rightarrow\\!({\it even}\,(2+n))]$
about even numbers can be deduced on the basis of the following typing

$\displaystyle n\\!:\\!N,x\\!:\\!({\it
even}\>n)\vdash\,[m\\!\doteq\\!1+x.1,({\it law}\,n\,x.1\,x.2):2+n=_{N}2*m]$
$\displaystyle\\!\\!:\\!\\!$ $\displaystyle({\it even}\,(2+n))$

Here ${\it law}$ is an abbreviation for a proof of the following property

$\displaystyle{\it law}$ $\displaystyle:$
$\displaystyle[n,m:N][n\\!=_{N}\\!2\\!*\\!m\\!\Rightarrow\\!\;2\\!+\\!n\\!=_{N}\\!2\\!*\\!(1\\!+\\!m)]$

A definition of law can be derived from the axioms in a style similar (and
even more tedious) to the above deduction. This deduction of the property
about even numbers is correct since

$\displaystyle({\it law}\,n\,x.1\,x.2)$ $\displaystyle:$ $\displaystyle
2+n=_{N}2*(1+x.1)$ $\displaystyle=_{\lambda}$
$\displaystyle(2+n=_{N}2*m)[1\\!+\\!x.1/m]$

Finally, an induction principle can be added to the context as follows:

$\displaystyle ind$ $\displaystyle:$
$\displaystyle[P:[N\\!\Rightarrow\\!\tau]][(P\,0);[n:N][(P\,n)\\!\Rightarrow\\!(P\,(s\,n))]\\!\Rightarrow\\![n:N](P\,n)]$

###  3.4 Casting types to the primitive constant

In many cases, the constraint of universally quantified variables to be of
primitive type, i.e. $x:\tau$, can be relaxed to arbitrary well typed
expressions $a:b$ using an operation to cast arbitrary types to $\tau$. For
this reason we introduce an axiom scheme for a $\tau$-casting function
$()_{a}$ 555For a discussion of axioms schemes see also Section 3.1) and we
also assume the axioms schemes $()_{a}^{+}$ and $()_{a}^{-}$ essentially
stating equivalence between casted and uncasted types:

$\displaystyle()_{a}$ $\displaystyle:$ $\displaystyle[a\\!\Rightarrow\\!\tau]$
$\displaystyle()_{a}^{+}$ $\displaystyle:$
$\displaystyle[x:a][x\\!\Rightarrow\\!(()_{a}\,x)]$ $\displaystyle()_{a}^{-}$
$\displaystyle:$ $\displaystyle[x:a][(()_{a}\,x)\\!\Rightarrow\\!x]$

As an application, we can generalize the property of $\mathbf{ff}$ in Section
1 to arbitrary well-typed $a$:

$x:a\vdash\,[y:\mathbf{ff}](()_{a}^{-}\;x\;(y\>(()_{a}\>x))):[\mathbf{ff}\\!\Rightarrow\\!x]$

As an another example, assuming one already has axiomatized the more general
theory of integers, e.g. with type Int, a constant $0_{I}$, and the usual
relation $\geq$, one could instantiate the declarations of the context
Naturals using casting as follows:

$\displaystyle(N\;:=\;(()_{[n!{\it Int}]\tau}\,[n!{\it Int}](n\geq
0_{I})),\;\;0\;:=\;0_{I},\ldots)$

###  3.5 Formalizing partial functions

In the previous section we have used the application operator in $\mathtt{d}$
to model the application of total functions. As an example of a partial
function consider the predecessor function on natural numbers. To introduce
this function in $\mathtt{d}$, several approaches come to mind:

  * •

The predecessor function can be axiomatized as a total function over the type
$N$.

$\displaystyle p$ $\displaystyle:$ $\displaystyle[N\\!\Rightarrow\\!N]$
$\displaystyle P$ $\displaystyle:$ $\displaystyle[n:N](p\,(s\,n))=_{N}n$

The (potential) problem of this approach is the interpretation of $(p\,0)$
which may lead to unintuitive or harmful consequences. Furthermore, if
additional axioms are to be avoided, the declaration of $p$ must eventually by
instantiated by some (total) function which defines a value for $0$.

  * •

The predecessor function can be defined with an additional argument
formalizing the condition.

$\displaystyle{\it nonZero}$ $\displaystyle:=$
$\displaystyle[i:N;j!N]i=_{N}(s\,j)$ $\displaystyle p$ $\displaystyle:=$
$\displaystyle[n:N;q:({\it nonZero}\;n)]q.1$

While mathematically clean, this definition requires to always provide an
additional argument $c$ when using the predecessor function.

  * •

As a variant of the previous approach, the additional argument can be hidden
into an adapted type of the predecessor function.

$\displaystyle N^{>0}$ $\displaystyle:=$ $\displaystyle[i,j!N]i=_{N}(s\,j)$
$\displaystyle p$ $\displaystyle:=$ $\displaystyle[n:N^{>0}]n.2.1$

While mathematically clean, this approach requires a more complex handling of
the argument $n:N^{>0}$ when using the predecessor function.

Which of these (or other) approaches is best to use seems to depend on the
organization and the goals of the formalization at hand.

###  3.6 Defining functions from deductions

Note that while the predecessor function can be directly defined, more complex
functions and their (algorithmic) properties can be derived from the proofs of
properties. As a sketch of an example consider the following well-known
property

$\displaystyle{\it GCD}$ $\displaystyle:=$ $\displaystyle[x,y:N;k!N]({\it
gcd}\;k\;x\;y)$

where $({\it gcd}\;k\;x\;y)$ denotes the property that $k$ is the greatest
common divisor of $x$ and $y$. Given a (not necessarily constructive)
deduction $P_{{\it GCD}}$ of type GCD, one can then define the greatest common
divisor $x\downarrow y$ and define deductions $d_{1}$ and $d_{2}$ proving
well-known algorithmic properties.

$\displaystyle(.)\downarrow(.)$ $\displaystyle:=$
$\displaystyle[x,y:N](P_{{\it GCD}}\;x\;y).1$ $\displaystyle d_{1}$
$\displaystyle:$ $\displaystyle[x,y:N](x+y)\downarrow x=_{N}y\downarrow x$
$\displaystyle d_{2}$ $\displaystyle:$
$\displaystyle[x,y:N]x\downarrow(x+y)=_{N}x\downarrow y$

###  3.7 Sets

When formalizing mathematical deductions, besides natural numbers and equality
one needs formal systems for many more basic structures of mathematics. For
example, sets can be axiomatized by the following context using a formalized
set comprehension principle.

$\displaystyle{\it Sets}:=\quad(\quad\mathbb{P}$ $\displaystyle:$
$\displaystyle[\tau\\!\Rightarrow\\!\tau],$ $\displaystyle(.)\in_{(.)}(.)$
$\displaystyle:$
$\displaystyle[S:\tau][S;(\mathbb{P}\,S)\\!\Rightarrow\\!\tau],$
$\displaystyle\\{(.)\\}_{(.)}$ $\displaystyle:$
$\displaystyle[S:\tau][[S\\!\Rightarrow\\!\tau]\\!\Rightarrow\\!(\mathbb{P}\,S)],$
$\displaystyle I$ $\displaystyle:$
$\displaystyle[S:\tau;x:S;P:[S\\!\Rightarrow\\!\tau]][(P\,x)\\!\Rightarrow\\!x\in_{S}\\{[y:S](P\,y)\\}_{S}],$
$\displaystyle O$ $\displaystyle:$
$\displaystyle[S:\tau;x:S;P:[S\\!\Rightarrow\\!\tau]][x\in_{S}\\{[y:S](P\,y)\\}_{S}\,\\!\Rightarrow\\!\,(P\,x)]\quad)$

Note that, for better readability, we use the notation $x\in_{S}y$ and
$\\{P\\}_{S}$ abbreviating the expressions $((.)\\!\in_{(.)}\\!(.)\;S\,x\,y)$
and $(\\{(.)\\}_{(.)}\,S\,P)$. One can now define various sets using set
comprehension. Note the use of the $\tau$-casting function to ensure the set-
defining properties are of type $\tau$.

$\displaystyle\emptyset$ $\displaystyle:=$
$\displaystyle[S:\tau]\\{[x:S](()_{[\tau\Rightarrow\tau]}\,\mathbf{ff})\\}_{S}\quad:\quad[S:\tau](\mathbb{P}\,S)$
$\displaystyle{\it Union}$ $\displaystyle:=$
$\displaystyle[S:\tau,A,B:(\mathbb{P}\,S)]\\{[x:S](()_{[\tau,\tau]}\,[x\in_{S}A+x\in_{S}B])\\}_{S}$
$\displaystyle:\quad[S:\tau][(\mathbb{P}\,S);(\mathbb{P}\,S)\\!\Rightarrow\\!(\mathbb{P}\,S)]$
$\displaystyle{\it Even}$ $\displaystyle:=$
$\displaystyle\\{[x:N](()_{[y!N]\tau}\,({\it
even}\;x))\\}_{N}\quad:\quad(\mathbb{P}\,N)$

Properties of individual elements can be deduced on the basis of the axiom
$O$, for example we can extract the property $P:=[n!N](x=_{N}2*n)$ of a member
$x$ of Even using the cast-removal axiom as follows (where ${\it
Even}_{P}:=[x:N](()_{[y!N]\tau}\,({\it even}\>x))$:

$\displaystyle x:N,{\it asm}:x\in_{N}{\it Even}$ $\displaystyle\\!\vdash\\!$
$\displaystyle(()_{[n!N]\tau}^{-}\;P\;(O\;N\;x\;{\it Even}_{P}\;{\it
asm}))\;:\;P$

Note that in this formalization of sets the axiom of choice can be immediately
derived as follows:

$\displaystyle\Gamma$ $\displaystyle=$
$\displaystyle(X,I:\tau,A:[I\\!\Rightarrow\\!(\mathbb{P}\,X)],u:[x:I;y!X]y\in_{X}(A\,i))$
$\displaystyle\Gamma$ $\displaystyle\\!\vdash\\!$
$\displaystyle[F\\!\doteq\\![i:I](u\,i).1\,,[i:I](u\,i).2:([i:I](F\,i)\in_{X}(A\,i))]$
$\displaystyle:$
$\displaystyle[F![I\\!\Rightarrow\\!X];i:I](F\,i)\in_{X}(A\,i)$

Note also that an alternative definition of naturals from integers can be
given with sets as follows:

$\displaystyle(N\;:=\;(()_{(\mathbb{P}\,{\it Int})}\;\\{[n:{\it
Int}](()_{\tau}\,(n\geq 0_{I}))\\}_{\it Int},\;\;0\;:=\;0_{I},\ldots)$

###  3.8 Proof structuring

To illustrate some proof structuring issues, we formalize the property of
being a group as follows (writing $[a_{1},a_{2},\ldots]$ for
$[a_{1},[a_{2},\ldots]]$):

$\displaystyle{\it Group}:=[S:\tau;(.)\\!*(.)![S;S\\!\Rightarrow\\!S];e!S]$
$\displaystyle[$ $\displaystyle[x,y,z:S](x*y)*z=_{S}x*(y*z)$ ,
$\displaystyle[x:S]e*x=_{S}x$ ,
$\displaystyle[x:S;x^{\prime}!S]x^{\prime}*x=_{S}e\quad]$

As an example, assume Integers as the context Naturals (see Section 3.3)
extended with a subtraction operator $a-b$ with corresponding axioms. First,
we can then show that $+$ and $0$ form a group: Obviously, one can construct a
deduction ded with

${\it Equality},{\it Integers}\vdash\,{\it ded}:P_{g}$

where $P_{g}$ describes the group laws:

$\displaystyle P_{g}:=$ $\displaystyle[\;$
$\displaystyle[x,y,z:N]\,(x+y)+z=_{N}x+(y+z)$ ,
$\displaystyle[x:N]\,0+x=_{N}x$ ,
$\displaystyle[x:N,x^{\prime}!N]\,x^{\prime}+x=_{N}0\quad]$

ded can be turned into a proof of $({\it Group}\>N)$ as follows:

$\displaystyle{\it isGroup}$ $\displaystyle:=$
$\displaystyle[*\\!\doteq\\!+,[e\\!\doteq\\!0,{\it
ded}:P_{g}[e/0]]:P_{g}[e/0][*/+]]$ $\displaystyle{\it Equality},{\it
Integers}$ $\displaystyle\vdash\,$ $\displaystyle{\it isGroup}:({\it
Group}\>N)$

It is well-known that the left-neutral element is also right-neutral, this
means, when assuming $g$ to be a group over $S$ there is a proof $p$ such that

$Equality,S:\tau,g:({\it Group}\>S)\vdash\,p:[x:S](g.1\;x\;g.2.1)=_{S}x$

Here $g.1$ is the function of $g$ and $g.2.1$ is the neutral element of $g$.
Note that the use of existential declarations is supporting the proof
structuring as it hides $*$ and $e$ in the assumptions inside the
$g:(Group\>S)$ assumption. On the other hand, one has to explicitly access the
operators using projections.

$p$ can be abstracted to an inference $p^{\prime}:=[S:\tau;g:({\it
Group}\>S)]p$ about a derived property of groups as follows:

$\displaystyle{\it Equality}$ $\displaystyle\vdash\,$ $\displaystyle
p^{\prime}:[S:\tau;g:({\it Group}\>S)][x:S]\;(g.1\;x\;g.2.1)=_{S}x$

Hence we can instantiate $p^{\prime}$ to obtain the right-neutrality property
of $0$ for integers.

${\it Equality},{\it Integers}\vdash\,(p^{\prime}\;N\;{\it
isGroup}):[x:N]\,x+0=_{N}x$

##  4 Properties

In this Section we show confluence of reduction, several properties of typing,
including uniqueness of types, and strong normalisation of valid, i.e.
typable, expressions. On the basis of these properties we show consistency of
$\mathtt{d}$ in the sense that no expression is typing to $[x:\tau]x$ under
the empty context. We show the main proof ideas and indicate important steps
in detail, significantly more detail can be found in [32].

######  Remark 2 (Inductive principles).

Besides structural induction on the definition of $\mathcal{E}$, we will
mainly use structural induction on expressions with context when showing a
property $P(\Gamma,a)$ of expressions. We will make use of the following
inductive inference rules

$\frac{P(\Gamma,a_{1})\quad
P(\Gamma,a_{n})}{P(\Gamma,\oplus(a_{1},\ldots,a_{n}))}\qquad\frac{P(\Gamma,a_{1})\quad
P(\Gamma,a_{n-1})\quad
P((\Gamma,x:a_{1}),a_{n})}{P(\Gamma,\oplus_{x}(a_{1},\ldots,a_{n}))}$

We frequently show properties about reduction relations by induction on the
definition of single-step reduction. Similarly for properties about typing.

######  Remark 3 (Renaming of variables).

Typically when we prove a property using some axiom, inference rule, or
derived property, we just mention the identifier or this axiom, rule, or
property and then use it with an instantiation renaming its variables so as to
avoid name clashes with the proposition to be shown. In order not to clutter
the presentation, these renamings are usually not explicitly indicated.

######  Remark 4 (Introduction of auxiliary identifiers).

We usually explicitly introduce all auxiliary identifiers appearing in
deduction steps. However, there are two important exceptions.

  * •

When using structural induction, if we consider a specific operator and
decompose an expression $a$ e.g. by $a=\oplus(a_{1},,\ldots,a_{n})$ we usually
implicitly introduce the new auxiliary identifiers $a_{i}$.

  * •

When using induction on the definition of reduction, if we consider a specific
axiom or structural rule which requires a syntactic pattern we usually
implicitly introduce the new auxiliary identifiers necessary for this pattern.

We begin with some basic properties of substitution and its relation to
reduction.

######  Lemma 5 (Basic properties of substitution).

For all $a,b,c$ and $x,y$:

  1. 1.

If $x\notin{\it FV}(a)$ then $a[b/x]=a$.

  2. 2.

If $x\neq y$ and $x\notin{\it FV}(c)$ then $a[b/x][c/y]=a[c/y][b[c/y]/x]$.

  3. 3.

If $x\neq y$, $x\notin{\it FV}(c),y\notin{\it FV}(b)$ then
$a[b/x][c/y]=a[c/y][b/x]$.

######  Proof 4.1.

Proof is straightforward by structural induction on $a$.

######  Lemma 6 (Substitution and reduction).

For all $a,b,c$ and $x$: $a\to^{*}b$ implies $a[c/x]\to^{*}b[c/x]$,
$c[a/x]\to^{*}c[b/x]$, and ${\it FV}(b)\subseteq{\it FV}(a)$.

######  Proof 4.2.

Proof is straightforward by induction on the definition of single-step
reduction.

Next we turn to basic decomposition properties of reduction.

######  Lemma 7 (Reduction decomposition).

For all $a_{1},\ldots,a_{n},b,b_{1},\ldots,b_{n}$ and $x$:

  1. 1.

$\oplus(a_{1},a_{2})\\!\to^{*}\\!b$, where
$\oplus(a_{1},a_{2})\neq(a_{1}\,a_{2})$ implies $b=\oplus(b_{1},b_{2})$ where
$a_{1}\\!\to^{*}\\!b_{1}$ and $a_{2}\\!\to^{*}\\!b_{2}$.

  2. 2.

$\oplus_{x}(a_{1},\ldots,a_{n})\to^{*}b$ implies
$b=\oplus_{x}(b_{1},\ldots,b_{n})$, $a_{i}\to^{*}b_{i}$, for $1\leq i\leq n$.

  3. 3.

$a.i\to^{*}\oplus_{x}(b_{1},\ldots,b_{n})$, $i=1,2$, implies
$a\to^{*}[c_{1}\oplus c_{2}]$ or $a\to^{*}[y\\!\doteq\\!c_{1},c_{2}:c_{3}]$,
for some $c_{1},c_{2},c_{3}$ with
$c_{i}\to^{*}\oplus_{x}(b_{1},\ldots,b_{n})$.

  4. 4.

$a.i\to^{*}\oplus(a_{1},a_{2})$, $i=1,2$, where $\oplus(a_{1},a_{2})$ is a
sum, product or injection implies $a\to^{*}[c_{1}\oplus c_{2}]$ or
$a\to^{*}[y\\!\doteq\\!c_{1},c_{2}:c_{3}]$, for some $c_{1},c_{2},c_{3}$ with
$c_{i}\to^{*}\oplus(a_{1},a_{2})$.

  5. 5.

$a_{1}(a_{2})\to^{*}\oplus_{x}(b_{1},\ldots,b_{n})$ implies, for some
$c_{1},c_{2},c_{3},c_{4}$, one of the following cases

    1. (a)

$a_{1}\to^{*}\oplus^{\prime}_{y}(c_{1},c_{2})$, $a_{2}\to^{*}c_{3}$ and
$c_{2}[c_{3}/y]\to^{*}\oplus_{x}(b_{1},\ldots,b_{n})$, or

    2. (b)

$a_{1}\to^{*}[c_{1}\,?\,c_{2}]$ and either $a_{2}\to^{*}[c_{3},:\\!c_{4}]$ and
$(c_{1}\,c_{3})\to^{*}\oplus_{x}(b_{1},\ldots,b_{n})$ or
$a_{2}\to^{*}[:\\!c_{3},c_{4}]$ and
$(c_{2}\,c_{4})\to^{*}\oplus_{x}(b_{1},\ldots,b_{n})$.

  6. 6.

$a_{1}(a_{2})\to^{*}\oplus(b_{1},\ldots,b_{n})$ where
$\oplus(b_{1},\ldots,b_{n})\neq(b_{1}\,b_{2})$ implies, for some $c_{1}$,
$c_{2}$, $c_{3}$, and $c_{4}$, one of the following cases

    1. (a)

$a_{1}\to^{*}\oplus^{\prime}_{y}(c_{1},c_{2})$, $a_{2}\to^{*}c_{3}$, and
$c_{2}[c_{3}/x]\to^{*}\oplus(b_{1},\ldots,b_{n})$, or

    2. (b)

$a_{1}\to^{*}[c_{1}\,?\,c_{2}]$ and either $a_{2}\to^{*}[c_{3},:\\!c_{4}]$ and
$(c_{1}\,c_{3})\to^{*}\oplus(b_{1},\ldots,b_{n})$ or
$a_{2}\to^{*}[:\\!c_{4},c_{3}]$ and
$(c_{2}\,c_{3})\to^{*}\oplus(b_{1},\ldots,b_{n})$.

######  Proof 4.3.

Straightforward inductions, as these properties are very close to the
definition of the reduction relation.

######  Lemma 8 (Reduction decomposition for negation).

For all $a_{1},\ldots,a_{n},b,b_{1},\ldots,b_{n}$ and $x$:

  1. 1.

$\neg a\to^{*}[x:b_{1}]b_{2}$ implies $a\to^{*}[x!c_{1}]c_{2}$ for some
$c_{1},c_{2}$ where $c_{1}\to^{*}b_{1}$ and $\neg c_{2}\to^{*}b_{2}$.

  2. 2.

$\neg a\to^{*}[b_{1},b_{2}]$ implies $a\to^{*}[c_{1}+c_{2}]$ for some
$c_{1},c_{2}$ where $\neg c_{1}\to^{*}b_{1}$ and $\neg c_{2}\to^{*}b_{2}$.

  3. 3.

$\neg a\to^{*}[x!b_{1}]b_{2}$ implies $a\to^{*}[x:c_{1}]c_{2}$ for some
$c_{1},c_{2}$ where $c_{1}\to^{*}b_{1}$ and $\neg c_{2}\to^{*}b_{2}$.

  4. 4.

$\neg a\to^{*}[b_{1}+b_{2}]$ implies $a\to^{*}[c_{1},c_{2}]$ for some
$c_{1},c_{2}$ where $\neg c_{1}\to^{*}b_{1}$ and $\neg c_{2}\to^{*}b_{2}$.

  5. 5.

$\neg a\to^{*}[x\\!\doteq\\!b_{1},b_{2}:b_{3}]$ implies
$a\to^{*}[x\\!\doteq\\!b_{1},b_{2}:b_{3}]$.

  6. 6.

$\neg a\to^{*}[b_{1}\,?\,b_{2}]$ implies $a\to^{*}[b_{1}\,?\,b_{2}]$.

  7. 7.

$\neg a\to^{*}[b_{1},:\\!b_{2}]$ implies $a\to^{*}[b_{1},:\\!b_{2}]$.

  8. 8.

$\neg a\to^{*}[:\\!b_{1},b_{2}]$ implies $a\to^{*}[:\\!b_{1},b_{2}]$.

######  Proof 4.4.

Straightforward inductions, as these properties are very close to the
definition of the reduction relation.

###  4.1 Confluence of reduction

Well-known confluence proofs for untyped $\lambda$-calculus could be used,
e.g. [4] could be adapted to include the operators of $\mathtt{d}$. Due to the
significant number of reduction axioms of $\mathtt{d}$, we use an alternative
approach using explicit substitutions and an auxiliary relation of reduction
with explicit substitution which has detailed substitution steps on the basis
of a definitional environment (this approach was basically already adopted in
the Automath project [9]) and which comprises sequences of negation-related
reduction-steps into single steps. The underlying idea is that reduction with
explicit substitution can be shown to be directly confluent which implies its
confluence. We then show that this implies confluence of reduction
$a\to^{*}b$. There are several approaches to reduction with explicit
substitutions, e.g. [1][2]. Furthermore, there is a significant amount of more
recent work in this context, however, as explicit substitution is not the main
focus of this article we do not give an overview here. The approach introduced
below introduces a definitional environment as part of the reduction relation
to explicitly unfold single substitution instances and then discard
substitution expressions when all instances are unfolded. This approach, as
far as basic lambda calculus operators are concerned, is essentially
equivalent to the system $\Lambda_{sub}$ which has been defined using
substitution [23] or placeholders [20] to indicate particular occurrences to
be substituted. Both approaches slightly differ from ours as they duplicate
the substituted expression on the right-hand side of the $\beta$-rule thus
violating direct confluence. We begin by defining expressions with
substitution. [Expressions with substitution] The set $\mathcal{\dot{E}}$ of
expressions with substitution is an extension of the set $\mathcal{E}$ of
expressions adding a substitution operator.

$\displaystyle\mathcal{\dot{E}}$ $\displaystyle\\!::=\\!$
$\displaystyle\underbrace{\\{\tau\\}\,\mid\,\ldots\,\mid\,\neg\mathcal{\dot{E}}}_{\text{(see
Definition~{}\ref{expression})}}\,\mid\,[\mathcal{V}\\!:=\\!\mathcal{\dot{E}}]\mathcal{\dot{E}}$

Expressions with substitution will be denoted by
$\mathbf{a},\mathbf{b},\mathbf{c},\mathbf{d},\ldots$.
$[x\\!:=\\!\mathbf{a}]\mathbf{b}$ is an internalized substitution. As
indicated by its name, the purpose of $[x\\!:=\\!\mathbf{a}]\mathbf{b}$ is to
internalize the substitution function. The function computing free variables
(Definition 2.1) is extended so as to treat internalized substitutions
identical to abstractions.

$\displaystyle{\it FV}([x\\!:=\\!\mathbf{a}]\mathbf{b})$ $\displaystyle=$
$\displaystyle{\it FV}(\mathbf{a})\cup({\it
FV}(\mathbf{b})\\!\setminus\\!\\{x\\})$

The substitution function (Definition 2.1) is extended analogously.

$\displaystyle([z\\!:=\\!\mathbf{a}]\mathbf{b})[y/x]$ $\displaystyle=$
$\displaystyle\begin{cases}[z\\!:=\\!\mathbf{a}[y/x]]\mathbf{b}&\text{if
}z=x,\\\
[z\\!:=\\!\mathbf{a}[y/x]](\mathbf{b}[y/x])&\text{otherwise}\end{cases}$

Similar for $\alpha$-conversion (Definition 2.1).

$\frac{y\notin{\it
FV}(\mathbf{b})}{[x\\!:=\\!\mathbf{a}]\mathbf{b}\;=_{\alpha}\;[y\\!:=\\!\mathbf{a}]\mathbf{b}[y/x]}$

As for expressions we will write variables as strings but always assume
appropriate renaming of bound variables in order to avoid name clashes. In
order to define reduction with explicit substitution as a directly confluent
relation, we first define the auxiliary notion of negation-reduction
$\mathbf{a}\to^{\neg\,*}\mathbf{b}$ which comprises application sequences of
axioms $\nu_{1}$, $\ldots$, $\nu_{5}$ in a restricted context. [Negation-
reduction] Single-step negation-reduction $\mathbf{a}\to^{\neg}\mathbf{b}$ is
the smallest relation on expressions with explicit substitution satisfying the
axiom and the inference rules of Table 6.

${\it(\nu_{1})}$ $\;\neg\neg\mathbf{a}$ $\to^{\neg}$ $\mathbf{a}$
${\it(\nu_{2})}$ $\;\neg[\mathbf{a},\mathbf{b}]$ $\to^{\neg}$
$[\neg\mathbf{a}+\neg\mathbf{b}]$ ${\it(\nu_{3})}$
$\;\neg[\mathbf{a}+\mathbf{b}]$ $\to^{\neg}$ $[\neg\mathbf{a},\neg\mathbf{b}]$
${\it(\nu_{4})}$ $\;\neg[x:\mathbf{a}]\mathbf{b}$ $\to^{\neg}$
$[x!\mathbf{a}]\neg\mathbf{b}$ ${\it(\nu_{5})}$
$\;\neg[x!\mathbf{a}]\mathbf{b}$ $\to^{\neg}$ $[x:\mathbf{a}]\neg\mathbf{b}$
$\displaystyle\qquad([\\_\oplus\\_]_{1})\quad\frac{\mathbf{a}_{1}\to^{\neg}\mathbf{a}_{2}}{[\mathbf{a}_{1}\oplus\mathbf{b}]\to^{\neg}[\mathbf{a}_{2}\oplus\mathbf{b}]}\qquad([\\_\oplus\\_]_{2})\quad\frac{\mathbf{b}_{1}\to^{\neg}\mathbf{b}_{2}}{[\mathbf{a}\oplus\mathbf{b}_{1}]\to^{\neg}[\mathbf{a}\oplus\mathbf{b}_{2}]}$
$\displaystyle(\oplus_{\\_}(\\_,\\_)_{2})\quad\frac{\mathbf{b}_{1}\to^{\neg}\mathbf{b}_{2}}{\oplus_{x}(\mathbf{a},\mathbf{b}_{1})\to^{\neg}\oplus_{x}(\mathbf{a},\mathbf{b}_{2})}\qquad(\neg{\\_}_{1})\quad\frac{\mathbf{a}_{1}\to^{\neg}\mathbf{a}_{2}}{\neg\mathbf{a}_{1}\to^{\neg}\neg\mathbf{a}_{2}}\qquad$

Table 6: Axioms and rules for negation-reduction.

$n$-step negation-reduction $\mathbf{a}\to^{\neg\,n}\mathbf{b}$ ($n\geq 0$)
and negation-reduction $\mathbf{a}\to^{\neg\,*}\mathbf{b}$ are defined as
follows:

$\displaystyle\mathbf{a}\to^{\neg\,n}\mathbf{b}$ $\displaystyle:=$
$\displaystyle\exists\mathbf{b}_{1},\ldots\mathbf{b}_{n-1}:\mathbf{a}\to^{\neg}\mathbf{b}_{1},\ldots,\mathbf{b}_{n-1}\to^{\neg}\mathbf{b}.$
$\displaystyle\mathbf{a}\to^{\neg\,*}\mathbf{b}$ $\displaystyle:=$
$\displaystyle\exists k\geq 0:\mathbf{a}\to^{\neg\,k}\mathbf{b}$

Not surprisingly, negation-reduction is confluent.

######  Lemma 9 (Confluence of negation-reduction).

$\to^{\neg\,*}$ is confluent, i.e. For all $\mathbf{a},\mathbf{b},\mathbf{c}$:
$\mathbf{a}\to^{\neg\,*}\mathbf{b}$ and $\mathbf{a}\to^{\neg\,*}\mathbf{c}$
imply $\mathbf{b}\to^{\neg\,*}\mathbf{d}$, and
$\mathbf{c}\to^{\neg\,*}\mathbf{d}$ for some $\mathbf{d}$.

######  Proof 4.5.

The proof of confluence of $\to^{\neg\,*}$ is straightforward by induction on
the size ${\it S}(\mathbf{a})$ which counts all nodes and leaves of
$\mathbf{a}$’s expression tree 666This ensures we can apply the inductive
hypothesis e.g. to $\neg\mathbf{a}_{1}$ when considering an
$\mathbf{a}=[\mathbf{a}_{1},\mathbf{a}_{2}]$, since ${\it
S}(\neg\mathbf{a}_{1})={\it S}(\mathbf{a}_{1})+1<{\it S}(\mathbf{a}_{1})+{\it
S}(\mathbf{a}_{2})+1={\it S}(\mathbf{a})$.. For the inductive base, the case
${\it S}(\mathbf{a})=1$ is obviously true. Consider an expression $a$ with
${\it S}(\mathbf{a})=n>0$ and assume confluence for all expressions
$\mathbf{b}$ with ${\it S}(\mathbf{b})<{\it S}(\mathbf{a})$. By systematic
investigation of critical pairs one can show local confluence of
$\to^{\neg\,*}$ from $\mathbf{a}$. Furthermore, $\to^{\neg\,*}$ is terminating
from $\mathbf{a}$ which can be seen by defining a weight function that squares
the weight (incremented by one) in case of negations. Hence one can apply the
diamond lemma [26] to obtain confluence of $\to^{\neg\,*}$ for $\mathbf{a}$,
which completes the inductive step.

In order to define reduction with explicit substitution, we need to introduce
the notion of environments, which are used to record the definitions which are
currently available for substitution. [Environment] Environments, denoted by
$E$, $E_{1}$, $E_{2}$, etc. are finite sequences of definitions
$(x_{1}\\!:=\\!\mathbf{a}_{1},\ldots,x_{n}\\!:=\\!\mathbf{a}_{n})$, where
$x_{i}$ are variables, $x_{i}\neq x_{j}$. $\\{x_{1},\ldots,x_{n}\\}$ is called
the domain of $E$. The lookup of an variable $x$ in the domain of an
Environment $E$ is defined by $E(x)=\mathbf{a}_{i}$. $E,x\\!:=\\!\mathbf{a}$
denotes the extension of $E$ on the right by a definition
$x\\!:=\\!\mathbf{a}$. $E_{1},E_{2}$ denotes the concatenation of two
environments. The empty environment is written as $()$. Similarly to induction
with context we will use induction with environment. [Single-step reduction
with explicit substitution] Single-step reduction reduction with explicit
substitution $E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$ is the smallest
relation on expressions with explicit substitution satisfying the axiom and
the inference rules of Table 7.

${\it(\beta_{1}^{\mu})}$ $E\\!\vdash\\!([x:\mathbf{a}]\mathbf{b}\,\mathbf{c})$
$\to^{:=}$ $[x\\!:=\\!\mathbf{c}]\mathbf{b}$ ${\it(\beta_{2}^{\mu})}$
$E\\!\vdash\\!([x!\mathbf{a}]\mathbf{b}\,\mathbf{c})$ $\to^{:=}$
$[x\\!:=\\!\mathbf{c}]\mathbf{b}$ ${\it(\beta_{3})}$
$E\\!\vdash\\!([\mathbf{a}\,?\,\mathbf{b}]\,[\mathbf{c},:\\!\mathbf{d}])$
$\to^{:=}$ $(\mathbf{a}\,\mathbf{c})$ ${\it(\beta_{4})}$
$E\\!\vdash\\!([\mathbf{a}\,?\,\mathbf{b}]\,[:\\!\mathbf{c},\mathbf{d}])$
$\to^{:=}$ $(\mathbf{b}\,\mathbf{d})$ ${\it(use)}$ $E\\!\vdash\\!x$ $\to^{:=}$
$\mathbf{a}$ if $E(x)=\mathbf{a}$ ${\it(rem)}$
$E\\!\vdash\\![x\\!:=\\!\mathbf{a}]\mathbf{b}$ $\to^{:=}$ $\mathbf{b}$ if
$x\notin{\it FV}(\mathbf{b})$ ${\it(\pi_{1})}$
$E\\!\vdash\\![x\\!\doteq\\!\mathbf{a},\mathbf{b}:\mathbf{c}].1$ $\to^{:=}$
$\mathbf{a}$ ${\it(\pi_{2})}$
$E\\!\vdash\\![x\\!\doteq\\!\mathbf{a},\mathbf{b}:\mathbf{c}].2$ $\to^{:=}$
$\mathbf{b}$ ${\it(\pi_{3})}$ $E\\!\vdash\\![\mathbf{a},\mathbf{b}].1$
$\to^{:=}$ $\mathbf{a}$ ${\it(\pi_{4})}$
$E\\!\vdash\\![\mathbf{a},\mathbf{b}].2$ $\to^{:=}$ $\mathbf{b}$
${\it(\pi_{5})}$ $E\\!\vdash\\![\mathbf{a}+\mathbf{b}].1$ $\to^{:=}$
$\mathbf{a}$ ${\it(\pi_{6})}$ $E\\!\vdash\\![\mathbf{a}+\mathbf{b}].2$
$\to^{:=}$ $\mathbf{b}$ ${\it(\nu_{6})}$ $E\\!\vdash\\!\neg\tau$ $\to^{:=}$
$\tau$ ${\it(\nu_{7})}$
$E\\!\vdash\\!\neg[x\\!\doteq\\!\mathbf{a},\mathbf{b}:\mathbf{c}]$ $\to^{:=}$
$[x\\!\doteq\\!\mathbf{a},\mathbf{b}:\mathbf{c}]$ ${\it(\nu_{8})}$
$E\\!\vdash\\!\neg[\mathbf{a},:\\!\mathbf{b}]$ $\to^{:=}$
$[\mathbf{a},:\\!\mathbf{b}]$ ${\it(\nu_{9})}$
$E\\!\vdash\\!\neg[:\\!\mathbf{a},\mathbf{b}]$ $\to^{:=}$
$[:\\!\mathbf{a},\mathbf{b}]$ ${\it(\nu_{10})}$
$E\\!\vdash\\!\neg[\mathbf{a}\,?\,\mathbf{b}]$ $\to^{:=}$
$[\mathbf{a}\,?\,\mathbf{b}]$ $\displaystyle{\it(\nu)}\quad$
$\displaystyle\frac{\exists
k>0:\mathbf{a}\to^{\neg\,k}\mathbf{b}}{E\vdash\,\mathbf{a}\to^{:=}\mathbf{b}}$
$\displaystyle{\it(\oplus{\overbrace{(\\_,\ldots,\\_)}^{n}}_{i})}\quad$
$\displaystyle\frac{E\vdash\,\mathbf{a}_{i}\to^{:=}\mathbf{b}_{i}}{E\vdash\,\oplus(\mathbf{a}_{1},\ldots,\mathbf{a}_{i},\ldots,\mathbf{a}_{n})\to^{:=}\oplus(\mathbf{a}_{1},\ldots,\mathbf{b}_{i},\ldots,\mathbf{a}_{n})}$
$\displaystyle{\it(\oplus_{x}{\overbrace{(\\_,\ldots,\\_)}^{n}}_{i})}\quad$
$\displaystyle\frac{E\vdash\,\mathbf{a}_{i}\to^{:=}\mathbf{b}_{i}}{E\vdash\,\oplus_{x}(\mathbf{a}_{1},\ldots,\mathbf{a}_{i},\ldots,\mathbf{a}_{n})\to^{:=}\oplus_{x}(\mathbf{a}_{1},\ldots,\mathbf{b}_{i},\ldots,\mathbf{a}_{n})}$
$\displaystyle{\it(L_{:=})}\quad$
$\displaystyle\frac{E\vdash\,\mathbf{a}\to^{:=}\mathbf{b}}{E\vdash\,[x\\!:=\\!\mathbf{a}]\mathbf{c}\to^{:=}[x\\!:=\\!\mathbf{b}]\mathbf{c}}$
$\displaystyle\quad{\it(R_{:=})}\quad$
$\displaystyle\frac{E,x\\!:=\\!\mathbf{a}\vdash\,\mathbf{b}\to^{:=}\mathbf{c}}{E\vdash\,[x\\!:=\\!\mathbf{a}]\mathbf{b}\to^{:=}[x\\!:=\\!\mathbf{a}]\mathbf{c}}$

Table 7: Axioms and rules for single-step reduction with explicit
substitution.

Compared to (general) reduction $\to$, the axiom $\beta_{1}$ and $\beta_{2}$
have been decomposed into several axioms:

  * •

$\beta^{\mu}_{1}$ and $\beta^{\mu}_{2}$ are reformulation of $\beta_{1}$ and
$\beta_{2}$ using internalized substitution

  * •

use is unfolding single usages of definitions

  * •

rem is removing a definition without usage

The axioms $\nu_{1},\ldots,\nu_{5}$, which are not directly confluent e.g. for
$\neg\neg[a,b]$, have been removed and replaced by the rule $\nu$. Furthermore
there are two more structural rules $(L_{:=})$ and $(R_{:=})$ related to
substitution. Note that the rule $(R_{:=})$ is pushing a definition onto the
environment $E$ when evaluating the body of a definition. Furthermore renaming
may be necessary before using this rule to ensure that $E,x\\!:=\\!\mathbf{a}$
is well defined. [Reduction with explicit substitution] Reduction with
explicit substitution $E\\!\vdash\\!\mathbf{a}\to^{:=\,*}b$ of $\mathbf{a}$ to
$b$ is defined as the reflexive and transitive closure of
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$. If two expressions with
definitions $\to^{:=\,*}$-reduce to a common expression we write
$E\\!\vdash\\!\mathbf{a}\nabla^{:=}\mathbf{b}$. Zero-or-one-step reduction
with explicit substitution and $n$-step reduction with explicit substitution
are defined as follows

$\displaystyle E\\!\vdash\\!\mathbf{a}\to^{:=\,01}\mathbf{b}$
$\displaystyle:=$ $\displaystyle
E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}\;\vee\;\mathbf{a}=\mathbf{b}$
$\displaystyle E\\!\vdash\\!\mathbf{a}\to^{:=\,n}\mathbf{b}$ $\displaystyle:=$
$\displaystyle\exists\mathbf{b}_{1},\ldots\mathbf{b}_{n-1}:E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}_{1},\ldots,E\\!\vdash\\!\mathbf{b}_{n-1}\to^{:=}\mathbf{b}.$

######  Remark 10 (Avoidance of name clashes through appropriate renaming).

Note that renaming is necessary to prepare use of the axiom use: For example
when $\to^{:=\,*}$-reducing $y\\!:=\\!x\\!\vdash\\![x:\tau][y,x]$,
$[x:\tau][y,x]$ needs to be renamed to e.g. $[z:\tau][y,z]$ before
substituting $y$ by $x$.

Reduction ($\to^{*}$) can obviously be embedded into $\to^{:=\,*}$.

######  Lemma 11 (Reduction implies reduction with explicit substitution).

For all $a,b$: $a\to^{*}b$ implies $()\\!\vdash\\!a\to^{:=\,*}b$.

######  Proof 4.6.

Proof is by induction on the definition of $a\to^{*}b$.

######  Remark 12 (Sketch of the confluence proof of $\to^{:=\,*}$).

First we show $\to^{:=}$ commutes with $\to^{\neg\,*}$. On the basis of these
results, by induction on expressions with substitution one can establish
direct confluence of $\to^{:=\,*}$, i.e.
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$ and
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{c}$ imply
$E\\!\vdash\\!\mathbf{b}\to^{:=\,01}\mathbf{d}$ and
$E\\!\vdash\\!\mathbf{c}\to^{:=\,01}\mathbf{d}$ for some $\mathbf{d}$.
Confluence follows by two subsequent inductions.

######  Lemma 13 (Commutation of single-step reduction with explicit
substitution and negation-reduction).

For all $\mathbf{a}$, $\mathbf{b}$ and $\mathbf{c}$:
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$ and
$\mathbf{a}\to^{\neg\,*}\mathbf{c}$ imply $\mathbf{b}\to^{\neg\,*}\mathbf{d}$
and $E\\!\vdash\\!\mathbf{c}\to^{:=\,01}\mathbf{d}$ for some $\mathbf{d}$.
This can be graphically displayed as follows (leaving out the environment
$E$):

${\mathbf{a}}$${\mathbf{c}}$${\mathbf{b}}$${\mathbf{d}}$$\scriptstyle{\neg\,*}$$\scriptstyle{:=}$$\scriptstyle{:=\,01}$$\scriptstyle{\neg\,*}$

######  Proof 4.7.

First we prove by induction on $\mathbf{a}$ with environment $E$ that for all
$\mathbf{b}$ and $\mathbf{c}$, $E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$ and
$\mathbf{a}\to^{\neg}\mathbf{c}$ imply $\mathbf{b}\to^{\neg\,*}\mathbf{d}$ and
$E\\!\vdash\\!\mathbf{c}\to^{:=\,01}\mathbf{d}$ for some $\mathbf{d}$.
Obviously we only have to consider those cases in which there exists a
$\mathbf{c}$ such that $\mathbf{a}\to^{\neg}\mathbf{c}$ (see Table 6). In case
of the axioms $\nu_{1}$ to $\nu_{5}$ the proposition follows directly. In case
of the rules for $\mathbf{a}=[\mathbf{a}_{1}\oplus\mathbf{a}_{2}]$ or
$\mathbf{a}=\oplus_{x}(\mathbf{a}_{1},\mathbf{a}_{2})$ the proposition follows
either immediately or from the inductive hypothesis. In case of the rule for
$\mathbf{a}=\neg\mathbf{a}_{1}$ the proposition follows from confluence of
negation-reduction (Lemma 9).

We can now prove the main property by induction on the length $n$ of
$\mathbf{a}\to^{\neg\,n}\mathbf{c}$: In case of $n=0$ the property is trivial.
Otherwise, let $E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$ and
$\mathbf{a}\to^{\neg\,n}\mathbf{c}^{\prime}\to^{\neg}\mathbf{c}$ for some
$\mathbf{c}^{\prime}$. By inductive hypothesis we know there is a
$\mathbf{d}^{\prime}$ such that
$E\\!\vdash\\!\mathbf{c}^{\prime}\to^{:=\,01}\mathbf{d}^{\prime}$ and
$\mathbf{b}\to^{\neg\,*}\mathbf{d}^{\prime}$. This situation can be
graphically summarized as follows (leaving out the environment $E$):

${\mathbf{a}}$${\mathbf{c}^{\prime}}$${\mathbf{c}}$${\mathbf{b}}$${\mathbf{d}^{\prime}}$$\scriptstyle{\neg\,n}$$\scriptstyle{:=}$$\scriptstyle{\neg}$$\scriptstyle{:=\,01}$$\scriptstyle{\neg\,*}$

Be definition of
$E\\!\vdash\\!\mathbf{c}^{\prime}\to^{:=\,01}\mathbf{d}^{\prime}$ there are
two cases:

  1. 1.

$\mathbf{c}^{\prime}=\mathbf{d}^{\prime}$: Then we know that
$\mathbf{b}\to^{\neg\,*}\mathbf{c}^{\prime}$ and hence
$\mathbf{b}\to^{\neg\,*}\mathbf{c}$. Hence $\mathbf{d}=\mathbf{c}$ where
$\mathbf{b}\to^{\neg\,*}\mathbf{d}$ and
$E\\!\vdash\\!\mathbf{c}\to^{:=\,01}\mathbf{d}$. This situation can be
graphically summarized as follows (leaving out the environment $E$):

${\mathbf{a}}$${\mathbf{d}^{\prime}=\mathbf{c}^{\prime}}$${\mathbf{d}=\mathbf{c}}$${\mathbf{b}}$$\scriptstyle{\neg\,n}$$\scriptstyle{:=}$$\scriptstyle{\neg}$$\scriptstyle{\neg\,*}$

  2. 2.

$E\\!\vdash\\!\mathbf{c}^{\prime}\to^{:=}\mathbf{d}^{\prime}$. By the argument
at the beginning of this proof we know there is a $\mathbf{d}$ such that
$\mathbf{d}^{\prime}\to^{\neg\,*}\mathbf{d}$ and
$E\\!\vdash\\!\mathbf{c}\to^{:=\,01}\mathbf{d}$. Hence
$\mathbf{b}\to^{\neg\,*}\mathbf{d}^{\prime}\to^{\neg\,*}\mathbf{d}$ and
$E\\!\vdash\\!\mathbf{c}\to^{:=\,01}\mathbf{d}$ which completes the proof.
This situation can be graphically summarized as follows (leaving out the
environment $E$):

${\mathbf{a}}$${\mathbf{c}^{\prime}}$${\mathbf{c}}$${\mathbf{b}}$${\mathbf{d}^{\prime}}$${\mathbf{d}}$$\scriptstyle{\neg\,n}$$\scriptstyle{:=}$$\scriptstyle{\neg}$$\scriptstyle{:=\,01}$$\scriptstyle{:=\,01}$$\scriptstyle{\neg\,*}$$\scriptstyle{\neg\,*}$

######  Lemma 14 (Direct confluence of reduction with explicit substitution).

For all $E,\mathbf{a},\mathbf{b},\mathbf{c}$:
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$ and
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{c}$ imply
$E\\!\vdash\\!\mathbf{b}\to^{:=\,01}\mathbf{d}$, and
$E\\!\vdash\\!\mathbf{c}\to^{:=\,01}\mathbf{d}$ for some $\mathbf{d}$.

######  Proof 4.8.

Proof is by induction on $\mathbf{a}$ with environment $E$ where in each
inductive step we investigate critical pairs.

Due to the definition of $\to^{:=}$, critical pairs of
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$ and
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{c}$ in which at least one of the steps
is using axiom $\nu$ on top-level, i.e. where $\exists
k>0:\mathbf{a}\to^{\neg\,k}\mathbf{b}$ or $\exists
k>0:\mathbf{a}\to^{\neg\,k}\mathbf{c}$, can be resolved thanks to Lemmas 9 and
13. Note also that the reduction axioms and rules of $\to^{:=\,*}$ do not
duplicate on their right hand side any element appearing on the left hand
side, hence the axiom use may never violate direct confluence in a critical
pair.

Next we show the interesting cases of explicit definitions and applications,
the other cases are straightforward.

  * •

$\mathbf{a}=[x\\!:=\\!\mathbf{a}_{1}]\mathbf{a}_{2}$: The matching axiom and
rules are rem, L:=, and R:=. The use of L:= versus R:= follow directly from
the inductive hypothesis. The interesting cases are the use of rem, versus L:=
or R:=: Hence we may assume that $x\notin{\it FV}(\mathbf{a}_{2})$ and need to
consider the following cases:

    1. 1.

$\mathbf{b}=\mathbf{a}_{2}$ and
$\mathbf{c}=[x\\!:=\\!\mathbf{b}_{1}]\mathbf{a}_{2}$ where
$E\\!\vdash\\!\mathbf{a}_{1}\to^{:=}\mathbf{b}_{1}$. We have
$\mathbf{d}=\mathbf{a}_{2}$ since $x\notin{\it FV}(\mathbf{a}_{2})$ and
$\mathbf{c}$ reduces in one-step to $\mathbf{a}_{2}$. This situation can be
graphically summarized as follows (leaving out the environment $E$):

${\mathbf{a}=[x\\!:=\\!\mathbf{a}_{1}]\mathbf{a}_{2}}$${\mathbf{d}=\mathbf{b}=\mathbf{a}_{2}}$${\mathbf{c}=[x\\!:=\\!\mathbf{b}_{1}]\mathbf{a}_{2}}$$\scriptstyle{:=}$$\scriptstyle{:=}$$\scriptstyle{:=}$

    2. 2.

$\mathbf{b}=\mathbf{a}_{2}$ and
$\mathbf{c}=[x\\!:=\\!\mathbf{a}_{1}]\mathbf{c}_{2}$ where
$E,x\\!:=\\!\mathbf{a}_{1}\\!\vdash\\!\mathbf{a}_{2}\to^{:=}\mathbf{c}_{2}$:
Obviously $x\notin{\it FV}(\mathbf{c}_{2})$ and therefore
$E\\!\vdash\\!\mathbf{a}_{2}\to^{:=}\mathbf{c}_{2}$. Therefore
$\mathbf{d}=\mathbf{c}_{2}$ where
$E\\!\vdash\\!\mathbf{c}\to^{:=}\mathbf{c}_{2}$ and
$E\\!\vdash\\!\mathbf{b}\to^{:=}\mathbf{c}_{2}$. This situation can be
graphically summarized as follows (leaving out the environment $E$):

${\mathbf{a}=[x\\!:=\\!\mathbf{a}_{1}]\mathbf{a}_{2}}$${\mathbf{b}=\mathbf{a}_{2}}$${\mathbf{c}=[x\\!:=\\!\mathbf{a}_{1}]\mathbf{c}_{2}}$${\mathbf{d}=\mathbf{c}_{2}}$$\scriptstyle{:=}$$\scriptstyle{:=}$$\scriptstyle{:=}$$\scriptstyle{:=}$

    3. 3.

The other two cases are symmetric (exchange of $\mathbf{b}$ and $\mathbf{c}$).

  * •

$\mathbf{a}=(\mathbf{a}_{1}\,\mathbf{a}_{2})$: The four matching axiom and two
matching rules are $\beta_{1}^{\mu}$, $\beta_{2}^{\mu}$, $\beta_{3}$,
$\beta_{4}$, $(\\_\,\\_)_{1}$, and $(\\_\,\\_)_{2}$. Several cases have to be
considered: The use of $(\\_\,\\_)_{1}$ versus $(\\_\,\\_)_{2}$ can be argued
in a straightforward way using the inductive hypothesis. The simultaneous
application of two different axioms on top-level is obviously not possible.
The interesting remaining cases are the usage of one of the four axioms versus
one of the structural rules.

    1. 1.

The first case is the use of $\beta_{1}^{\mu}$, i.e.
$\mathbf{a}_{1}=[x:\mathbf{a}_{3}]\mathbf{a}_{4}$ and
$\mathbf{b}=[x\\!:=\\!\mathbf{a}_{2}]\mathbf{a}_{4}$, versus one of the rules
$(\\_\,\\_)_{1}$, and $(\\_\,\\_)_{2}$. Two subcases need to be considered:

      1. (a)

Use of rule $(\\_\,\\_)_{1}$, i.e.
$\mathbf{c}=(\mathbf{c}_{1}\,\mathbf{a}_{2})$ where
$E\\!\vdash\\!\mathbf{a}_{1}=[x:\mathbf{a}_{3}]\mathbf{a}_{4}\to^{:=}\mathbf{c}_{1}$:
By definition of $\to^{:=}$, there are two subcases:

        1. i.

$\mathbf{c}_{1}=[x:\mathbf{c}_{3}]\mathbf{a}_{4}$ where
$E\\!\vdash\\!\mathbf{a}_{3}\to^{:=}\mathbf{c}_{3}$: This means that
$E\\!\vdash\\!\mathbf{c}\to^{:=}[x\\!:=\\!\mathbf{a}_{2}]\mathbf{a}_{4}=\mathbf{b}$,
i.e. $\mathbf{d}=\mathbf{b}$ is a single-step reduct of $\mathbf{c}$. This
situation can be graphically summarized as follows (leaving out the
environment $E$):

${\mathbf{a}=(\mathbf{a}_{1}\,\mathbf{a}_{2})=([x:\mathbf{a}_{3}]\mathbf{a}_{4}\,\mathbf{a}_{2})}$${\mathbf{d}=\mathbf{b}=[x\\!:=\\!\mathbf{a}_{2}]\mathbf{a}_{4}}$${\mathbf{c}=(\mathbf{c}_{1}\,\mathbf{a}_{2})=([x:\mathbf{c}_{3}]\mathbf{a}_{4}\,\mathbf{a}_{2})}$$\scriptstyle{:=}$$\scriptstyle{:=}$$\scriptstyle{:=}$

        2. ii.

$\mathbf{c}_{1}=[x:\mathbf{a}_{3}]\mathbf{c}_{4}$ where
$E\\!\vdash\\!\mathbf{a}_{4}\to^{:=}\mathbf{c}_{4}$: By definition of
$\to^{:=}$ we know that also
$E\\!\vdash\\![x\\!:=\\!\mathbf{a}_{2}]\mathbf{a}_{4}\to^{:=}[x\\!:=\\!\mathbf{a}_{2}]\mathbf{c}_{4}$.
Hence $\mathbf{d}=[x\\!:=\\!\mathbf{a}_{2}]\mathbf{c}_{4}$ with
$E\\!\vdash\\!\mathbf{b}=[x\\!:=\\!\mathbf{a}_{2}]\mathbf{a}_{4}\to^{:=}[x\\!:=\\!\mathbf{a}_{2}]\mathbf{c}_{4}=\mathbf{d}$
and
$E\\!\vdash\\!\mathbf{c}=(\mathbf{c}_{1}\,\mathbf{a}_{2})=([x:\mathbf{a}_{3}]\mathbf{c}_{4}\,\mathbf{a}_{2})\to^{:=}[x\\!:=\\!\mathbf{a}_{2}]\mathbf{c}_{4}=\mathbf{d}$.
This situation can be graphically summarized as follows (leaving out the
environment $E$):

${\mathbf{a}=(\mathbf{a}_{1}\,\mathbf{a}_{2})=([x:\mathbf{a}_{3}]\mathbf{a}_{4}\,\mathbf{a}_{2})}$${\mathbf{b}=[x\\!:=\\!\mathbf{a}_{2}]\mathbf{a}_{4}}$${\mathbf{c}=(\mathbf{c}_{1}\,\mathbf{a}_{2})=([x:\mathbf{a}_{3}]\mathbf{c}_{4}\,\mathbf{a}_{2})}$${\mathbf{d}=[x\\!:=\\!\mathbf{a}_{2}]\mathbf{c}_{4}}$$\scriptstyle{:=}$$\scriptstyle{:=}$$\scriptstyle{:=}$$\scriptstyle{:=}$

      2. (b)

The use of rule $(\\_\,\\_)_{2}$ can be argued in a similar style.

    2. 2.

The second case is the use of $\beta_{2}^{\mu}$ and can be argued in a similar
style.

    3. 3.

The third case is the use of $\beta_{3}$, i.e.
$\mathbf{a}_{1}=[\mathbf{a}_{3}\,?\,\mathbf{a}_{4}]$,
$\mathbf{a}_{2}=[\mathbf{a}_{5},:\\!\mathbf{a}_{6}]$ and
$\mathbf{b}=\mathbf{a}_{3}(\mathbf{a}_{5})$, versus one of the rules
$(\\_\,\\_)_{1}$, and $(\\_\,\\_)_{2}$. The property follows by an obvious
case distinction on whether
$E\\!\vdash\\![\mathbf{a}_{3}\,?\,\mathbf{a}_{4}]\to^{:=}\mathbf{c}$ is
reducing in $\mathbf{a}_{3}$ or $\mathbf{a}_{4}$, and similarly for
$E\\!\vdash\\![\mathbf{a}_{5},:\\!\mathbf{a}_{6}]\to^{:=}\mathbf{c}$.

    4. 4.

The fourth case is symmetric to the third one.

######  Lemma 15 (Confluence of $\to^{:=\,*}$-reduction).

For all $E,\mathbf{a},\mathbf{b},\mathbf{c}$:
$E\\!\vdash\\!\mathbf{a}\to^{:=\,*}\mathbf{b}$ and
$E\\!\vdash\\!\mathbf{a}\to^{:=\,*}\mathbf{c}$ implies
$E\\!\vdash\\!\mathbf{b}\nabla^{:=}\mathbf{c}$.

######  Proof 4.9.

Using Lemma 14, by structural induction on the number $n$ of transition steps
one can show that
$E\\!\vdash\\!\mathbf{a}=\mathbf{b}_{0}\to^{:=\,n}\mathbf{b}_{n}=\mathbf{b}$
and $E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{c}$ implies
$E\\!\vdash\\!\mathbf{b}\to^{:=\,01}\mathbf{d}$, and
$E\\!\vdash\\!\mathbf{c}\to^{:=\,n^{\prime}}\mathbf{d}$ where $n^{\prime}\leq
n$ for some $\mathbf{d}$. Using this intermediate result, by structural
induction on the number of transition steps $n$ one can show for any $m$ that
$E\\!\vdash\\!\mathbf{a}\to^{:=\,n}\mathbf{b}$ and
$E\\!\vdash\\!\mathbf{a}\to^{:=\,m}\mathbf{c}$ implies
$E\\!\vdash\\!\mathbf{b}\to^{:=\,m^{\prime}}\mathbf{d}$ and
$E\\!\vdash\\!\mathbf{c}\to^{:=\,n^{\prime}}\mathbf{d}$ where $n^{\prime}\leq
n,m^{\prime}\leq m$ for some $\mathbf{d}$. This proves confluence of
$\to^{:=\,*}$-reduction.

By Lemma 11 we know that reduction implies reduction with explicit
substitution. The reverse direction is obviously not true. However we can show
that $E\\!\vdash\\!\mathbf{a}\to^{:=\,*}\mathbf{b}$ implies
$\mathbf{a}^{\prime}\to^{*}\mathbf{b}^{\prime}$ where $\mathbf{a}^{\prime}$
and $\mathbf{b}^{\prime}$ result from $\mathbf{a}$ and $\mathbf{b}$ by maximal
evaluation of definitions, i.e. by maximal application of the axioms use and
rem. Therefore we introduce the relation
$E\\!\vdash\\!\mathbf{a}\to^{=}\mathbf{b}$ of definition evaluation [Single-
step definition-evaluation] Single-step definition-evaluation
$E\\!\vdash\\!\mathbf{a}\to^{=}\mathbf{b}$ is defined just like single-step
reduction with explicit substitution
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$ (see Table 7) but without the rule
$\nu$ and without any axioms except rem and use.

######  Lemma 16 (Confluence of definition-evaluation).

For all $E,\mathbf{a},\mathbf{b}$: The reflexive and transitive closure of
$E\\!\vdash\\!\mathbf{a}\to^{=}\mathbf{b}$ is confluent.

######  Proof 4.10.

By removing all the axiom cases except rem and use and the rule $\nu$ in the
proof of Lemma 14 (where these axioms only interacted with the structural
rules for internalized substitution) it can be turned into a proof of direct
confluence of $E\\!\vdash\\!\mathbf{a}\to^{=}\mathbf{b}$. The confluence of
the reflexive and transitive closure of
$E\\!\vdash\\!\mathbf{a}\to^{=}\mathbf{b}$ then follows as in the proof of
Lemma 15.

######  Lemma 17 (Strong normalization of definition-evaluation).

There are no infinite chains
$E\\!\vdash\\!\mathbf{a}_{1}\to^{=}\mathbf{a}_{2}\to^{=}\mathbf{a}_{3}\to^{=}\ldots$

######  Proof 4.11.

Since all definitions are non-recursive the property is straightforward. One
way to see this is to define a weight $W(E,\mathbf{a})$ such that

$E\vdash\,\mathbf{a}\to^{=}\mathbf{b}\quad\text{implies}\quad
W(E,\mathbf{b})<W(E,\mathbf{a})$

This can be achieved by defining $W(E,x)=W(E,E(x))+1$ if $x$ is in the domain
of $E$ otherwise $W(E,x)=1$,
$W(E,[x\\!:=\\!\mathbf{a}]\mathbf{b})=W(E,\mathbf{a})+W((E,x:=\mathbf{a}),\mathbf{b})+1$,
and so on.

[Definitional normal form] For any $\mathbf{a}$, let
$\mathcal{N}^{=}_{E}(\mathbf{a})$ denote the definitional normal form, i.e.
the expression resulting from $\mathbf{a}$ by maximal application of
definition evaluation steps under environment $E$. This definition is sound
since due to Lemma 17 the evaluation of definitions always terminates and by
Lemma 16 the maximal evaluation of definitions delivers a unique result.

######  Lemma 18 (Basic properties of $\mathcal{N}^{=}_{E}(\mathbf{a})$).

For all $E,x,\mathbf{a}_{1},\ldots\mathbf{a}_{n}$:

  1. 1.

$\mathcal{N}^{=}_{E}(\oplus(\mathbf{a}_{1},\ldots,\mathbf{a}_{n}))=\oplus(\mathcal{N}^{=}_{E}(\mathbf{a}_{1}),\ldots,\mathcal{N}^{=}_{E}(\mathbf{a}_{n}))$.

  2. 2.

$\mathcal{N}^{=}_{E}(\oplus_{x}(\mathbf{a}_{1},\ldots,\mathbf{a}_{n}))=\oplus_{x}(\mathcal{N}^{=}_{E}(\mathbf{a}_{1}),\ldots,\mathcal{N}^{=}_{E}(\mathbf{a}_{n}))$.

  3. 3.

$\mathcal{N}^{=}_{E}([x\\!:=\\!\mathbf{a}_{1}]\mathbf{a}_{2})=\mathcal{N}^{=}_{E}(\mathbf{a}_{2}[\mathbf{a}_{1}/x])=\mathcal{N}^{=}_{E}(\mathbf{a}_{2})[\mathcal{N}^{=}_{E}(\mathbf{a}_{1})/x]=\mathcal{N}^{=}_{E,x:=\mathbf{a}_{1}}(\mathbf{a}_{2})$.

######  Proof 4.12.

  1. 1.

The proof is by induction on the length of an arbitrary definition evaluation
$E\\!\vdash\\!\oplus(\mathbf{a}_{1},\ldots,\mathbf{a}_{n})\to^{=}\mathcal{N}^{=}_{E}(\oplus(\mathbf{a}_{1},\ldots,\mathbf{a}_{n}))$.
It is obvious since the outer operation is never affected by definition
evaluation.

  2. 2.

Similarly to (1)

  3. 3.

Using (1), (2), and the Lemmas 5, 11, and 16, these equalities can be shown
either directly or by straightforward inductive arguments.

######  Lemma 19 (Embedding property of reduction with explicit substitution).

For all $E,\mathbf{a},\mathbf{b}$:
$E\\!\vdash\\!\mathbf{a}\to^{:=\,*}\mathbf{b}$ implies
$\mathcal{N}^{=}_{E}(\mathbf{a})\to^{*}\mathcal{N}^{=}_{E}(\mathbf{b})$. As a
consequence, for all $a$ and $b$, $\\!\vdash\\!a\nabla^{:=}b$ implies $a\nabla
b$.

######  Proof 4.13.

First we show by induction on single-step reduction with explicit substitution
that $E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{b}$ implies
$\mathcal{N}^{=}_{E}(\mathbf{a})\to^{*}\mathcal{N}^{=}_{E}(\mathbf{b})$. The
proof is straightforward using Lemmas 6 and 18, and the fact that, for any
$E$, $\mathbf{a}\to^{\neg\,n}\mathbf{b}$ implies
$\mathcal{N}^{=}_{E}(\mathbf{a})\to^{n}\mathcal{N}^{=}_{E}(\mathbf{b})$ which
follows by a straightforward induction on the definition of
$\mathbf{a}\to^{\neg\,n}\mathbf{b}$.

Now we turn to the main proposition. Obviously, we have
$E\\!\vdash\\!\mathbf{a}\to^{:=\,n}\mathbf{b}$ for some $n$. The proof is by
induction on $n$. For $n=0$ the property is trivial. For $n>0$ assume
$E\\!\vdash\\!\mathbf{a}\to^{:=}\mathbf{c}\to^{:=\,n-1}\mathbf{b}$. By
inductive hypothesis
$\mathcal{N}^{=}_{E}(\mathbf{c})\to^{*}\mathcal{N}^{=}_{E}(\mathbf{b})$. By
the above argument we know that
$\mathcal{N}^{=}_{E}(\mathbf{a})\to^{*}\mathcal{N}^{=}_{E}(\mathbf{c})$ which
implies the proposition.

For the immediate consequence assume that there is a $\mathbf{c}$ such that
$\\!\vdash\\!a\to^{:=\,*}\mathbf{c}$ and $\\!\vdash\\!b\to^{:=\,*}\mathbf{c}$.
We have just shown that also
$\mathcal{N}^{=}_{()}(a)\to^{*}\mathcal{N}^{=}_{()}(\mathbf{c})$ and
$\mathcal{N}^{=}_{()}(b)\to^{*}\mathcal{N}^{=}_{()}(\mathbf{c})$. The property
follows since obviously $a=\mathcal{N}^{=}_{()}(a)$ and
$b=\mathcal{N}^{=}_{()}(b)$. Hence $a\nabla b$.

######  Theorem 20 (Confluence of reduction).

For all $a,b,c$: $a\to^{*}b$ and $a\to^{*}c$ implies $b\nabla c$. As a
consequence $a=_{\lambda}b$ implies $a\nabla b$.

######  Proof 4.14.

By Lemma 11 we know that $\\!\vdash\\!a\to^{:=\,*}b$ and
$\\!\vdash\\!a\to^{:=\,*}c$. Due to confluence of $\to^{:=\,*}$-reduction
(Lemma 15) we know that $\\!\vdash\\!b\nabla^{:=}c$. By Lemma 19 we obtain
$b\nabla c$. The consequence follows by induction on the definition of
$a=_{\lambda}b$.

As an immediate consequence of confluence we note some basic properties of
congruence.

######  Corollary 21 (Basic properties of congruence).

For all $x,y,a,b,c,d$:

  1. 1.

$a=_{\lambda}b$ implies $a[c/x]=_{\lambda}b[c/x]$ and
$c[a/x]=_{\lambda}c[b/x]$.

  2. 2.

$\oplus_{x}(a_{1},\ldots,a_{n})=_{\lambda}\oplus_{y}(b_{1},\ldots,b_{n})$ iff
$x=y$ and $a_{i}=_{\lambda}b_{i}$ for $i=1,\ldots,n$.

  3. 3.

$[a\oplus b]=_{\lambda}[c\oplus d]$iff $a=_{\lambda}c$ and $b=_{\lambda}d$.

######  Proof 4.15.

Follow from Lemmas 6 and 7, and Theorem 20.

###  4.2 Properties of typing

Based on the confluence result we can now show the main properties of typing,
in particular subject reduction and uniqueness of types. We frequently show
properties of typing by induction on the definition of typing where the
inductive base corresponds to the type axiom and the inductive step
corresponds to one of the type inference rules. We begin by two properties
(22,23) related to the rule weak, a property (24) related to the rule start,
and a property (25) related to the rule conv.

######  Lemma 22 (Context weakening).

For all $\Gamma_{1},\Gamma_{2},x,a,b,c$:
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a:b$ and $\Gamma_{1}\\!\vdash\\!c$ imply
$(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!a:b$.

######  Proof 4.16.

Proof is by induction on the definition of
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a:b$. For all the different type rules the
property follows directly from the definition of typing and the inductive
hypothesis.

######  Lemma 23 (Context extraction).

For all $\Gamma_{1},\Gamma_{2},a,b$:
$(\Gamma_{1},x:a,\Gamma_{2})\\!\vdash\\!b$ implies $\Gamma_{1}\\!\vdash\\!a$

######  Proof 4.17.

$(\Gamma_{1},x:a,\Gamma_{2})\\!\vdash\\!b$ means that there is a $c$ where
$(\Gamma_{1},x:a,\Gamma_{2})\\!\vdash\\!b:c$. The property that
$(\Gamma_{1},x:a,\Gamma_{2})\\!\vdash\\!b:c$ implies $\Gamma_{1}\\!\vdash\\!a$
is shown by induction on the definition of
$(\Gamma_{1},x:a,\Gamma_{2})\\!\vdash\\!b:c$. For all the different type rules
the property follows directly from the definition of typing and the inductive
hypothesis.

######  Lemma 24 (Start property).

For all $\Gamma,x,a,b$: $\Gamma,x:a\\!\vdash\\!x:b$ implies $a=_{\lambda}b$.

######  Proof 4.18.

The proof is by induction on $\Gamma,x:a\\!\vdash\\!x:b$. Obviously the rules
start and conv are only relevant. In case of start, we directly obtain $a=b$.
In case of conv, we know that $\Gamma,x:a\\!\vdash\\!x:c$ for some $c$ where
$c=_{\lambda}b$. By inductive hypothesis $a=_{\lambda}c$ hence obviously
$a=_{\lambda}b$.

######  Lemma 25 (Context equivalence and typing).

Let $\Gamma_{a}=(\Gamma_{1},x:a,\Gamma_{2})$ and
$\Gamma_{b}=(\Gamma_{1},x:b,\Gamma_{2})$ for some
$\Gamma_{1},\Gamma_{2},x,a,b$ where $a=_{\lambda}b$ and
$\Gamma_{1}\\!\vdash\\!b$: For all $c,d$: If $\Gamma_{a}\\!\vdash\\!c:d$ then
$\Gamma_{b}\\!\vdash\\!c:d$.

######  Proof 4.19.

Let $\Gamma_{a}$ and $\Gamma_{b}$ where $a=_{\lambda}b$ and
$\Gamma_{1}\\!\vdash\\!b$ as defined above: The property is shown by induction
on the definition of $(\Gamma_{1},x:a,\Gamma_{2})\\!\vdash\\!c:d$. In all
cases, the property follows directly from the definition of typing and the
inductive hypothesis.

Next we list several decomposition properties of typing and of validity.

######  Lemma 26 (Typing decomposition).

For all $\Gamma,x,a_{1},a_{2},a_{3},b$:

  1. 1.

$\Gamma\\!\vdash\\!\oplus_{x}(a_{1},a_{2}):b$ implies $b=_{\lambda}[x:a_{1}]c$
for some $c$ where $(\Gamma,x:a_{1})\\!\vdash\\!a_{2}:c$.

  2. 2.

$\Gamma\\!\vdash\\![a_{1},:\\!a_{2}]:b$ implies $b=_{\lambda}[c+a_{2}]$ for
some $c$ where $\Gamma\\!\vdash\\!a_{1}:c$ and $\Gamma\\!\vdash\\!a_{2}$.

$\Gamma\\!\vdash\\![:\\!a_{1},a_{2}]:b$ implies $b=_{\lambda}[a_{1}+c]$ for
some $c$ where $\Gamma\\!\vdash\\!a_{2}:c$ and $\Gamma\\!\vdash\\!a_{1}$.

  3. 3.

$\Gamma\\!\vdash\\![a_{1}\oplus a_{2}]:b$ implies $b=_{\lambda}[c_{1},c_{2}]$
for some $c_{1}$, $c_{2}$ where $\Gamma\\!\vdash\\!a_{1}:c_{1}$ and
$\Gamma\\!\vdash\\!a_{2}:c_{2}$.

  4. 4.

$\Gamma\\!\vdash\\!\neg a_{1}:b$ implies $b=_{\lambda}c$ for some $c$ where
$\Gamma\\!\vdash\\!a_{1}:c$.

  5. 5.

$\;\\!\vdash\\!\tau:b$ implies $b=_{\lambda}\tau$.

  6. 6.

$\Gamma\\!\vdash\\!(a_{1}\,a_{2}):b$ implies $b=_{\lambda}c_{2}[a_{2}/x]$
where $\Gamma\\!\vdash\\!a_{1}:[x\\!:\\!c_{1}]c_{2}$ and
$\Gamma\\!\vdash\\!a_{2}\\!:\\!c_{1}$ for some $c_{1}$,$c_{2}$.

  7. 7.

$\Gamma\\!\vdash\\!a_{1}.1:b$ implies $b=_{\lambda}c_{1}$ where
$\Gamma\\!\vdash\\!a_{1}:[x!c_{1}]c_{2}$ or
$\Gamma\\!\vdash\\!a_{1}:[c_{1},c_{2}]$ for some $c_{1}$, $c_{2}$.

  8. 8.

$\Gamma\\!\vdash\\!a_{1}.2:b$ implies, for some $c_{1}$, $c_{2}$, that either
$b=_{\lambda}c_{2}$ where $\Gamma\\!\vdash\\!a_{1}:[c_{1},c_{2}]$ or
$b=_{\lambda}c_{2}[a_{1}.1/x]$ where $\Gamma\\!\vdash\\!a_{1}:[x!c_{1}]c_{2}$.

  9. 9.

$\Gamma\\!\vdash\\![x\\!\doteq\\!a_{1},a_{2}:a_{3}]:b$ implies
$b=_{\lambda}[x!c]a_{3}$ for some $c$ where $\Gamma\\!\vdash\\!a_{1}:c$,
$\Gamma\\!\vdash\\!a_{2}:a_{3}[a_{1}/x]$, and $(\Gamma,x:c)\\!\vdash\\!a_{3}$.

  10. 10.

$\Gamma\\!\vdash\\![a_{1}\,?\,a_{2}]:b$ implies
$b=_{\lambda}[x:[c_{1}+c_{2}]]c$ for some $c_{1}$, $c_{2}$, and $c$ where
$\Gamma\\!\vdash\\!a_{1}:[x:c_{1}]c$, $\Gamma\\!\vdash\\!a_{2}:[x:c_{2}]c$ and
$\Gamma\\!\vdash\\!c$.

######  Proof 4.20.

In all cases the proof is by induction on the definition of typing or by a
straightforward application of previous properties. In particular, Lemmas 7,
20, and 22 are needed.

######  Lemma 27 (Validity decomposition).

For all $\Gamma,x,a_{1},\ldots,a_{n}$:

  1. 1.

$\Gamma\\!\vdash\\!\oplus(a_{1},,\ldots a_{n})$ implies
$\Gamma\\!\vdash\\!a_{1}$, $\ldots$, $\Gamma\\!\vdash\\!a_{n}$.

  2. 2.

$\Gamma\\!\vdash\\!\oplus_{x}(a_{1},a_{2})$ implies $\Gamma\\!\vdash\\!a_{1}$
and $(\Gamma,x:a_{1})\\!\vdash\\!a_{2}$

  3. 3.

$\Gamma\\!\vdash\\![x\\!\doteq\\!a_{1},a_{2}:a_{3}]$ implies
$\Gamma\\!\vdash\\!a_{2}$ and $\Gamma\\!\vdash\\!a_{1}:b$ for some $b$ where
$(\Gamma,x:b)\\!\vdash\\!a_{3}$

######  Proof 4.21.

In all cases the proof is by induction on the definition of typing or by a
straightforward application of previous properties. In particular, Lemma 23 is
needed.

A central prerequisite to the proof of closure of reduction and typing against
validity is the following substitution property of typing. In order to state
the property, we need an auxiliary definition. [Context substitution] The
substitution function (Definition 2.1) is extended to contexts $\Gamma[a/x]$,
where $a$ is an expression, as follows:

$\displaystyle()[a/x]$ $\displaystyle=$ $\displaystyle()$
$\displaystyle(y:b,\Gamma)[a/x]$ $\displaystyle=$
$\displaystyle\begin{cases}(y:b[a/x],\Gamma)&\text{if}\;x=y\\\
(y:b[a/x],\Gamma[a/x])&\text{otherwise}\end{cases}$

######  Lemma 28 (Substitution and typing).

Assume that $\Gamma_{a}=(\Gamma_{1},x:a,\Gamma_{2})$ and
$\Gamma_{b}=(\Gamma_{1},\Gamma_{2}[b/x])$ for some
$\Gamma_{1},\Gamma_{2},x,a,b$ where $\Gamma_{1}\\!\vdash\\!b:a$. For all
$c,d$: If $\Gamma_{a}\\!\vdash\\!c:d$ then
$\Gamma_{b}\\!\vdash\\!c[b/x]:d[b/x]$.

######  Proof 4.22.

Let $\Gamma_{a}$ and $\Gamma_{b}$ as defined above and assume
$\Gamma_{1}\\!\vdash\\!b:a$. The proof that $\Gamma_{a}\\!\vdash\\!c:d$
implies $\Gamma_{b}\\!\vdash\\!c[b/x]:d[b/x]$ is by induction on the
definition of $\Gamma_{a}\\!\vdash\\!c:d$. We show two interesting cases.

  * •

Rule conv: We have $\Gamma_{a}\\!\vdash\\!c:d^{\prime}$ for some $d^{\prime}$
where $d^{\prime}=_{\lambda}d$ and $\Gamma_{a}\\!\vdash\\!d^{\prime}:e$ for
some $e$. By inductive hypothesis
$\Gamma_{b}\\!\vdash\\!c[b/x]:d^{\prime}[b/x]$ and
$\Gamma_{a}\\!\vdash\\!d^{\prime}[b/x]:e[b/x]$. By Lemma 21(1) we can infer
that $d^{\prime}[b/x]=_{\lambda}d[b/x]$. Therefore we can apply the rule conv
to obtain $\Gamma_{b}\\!\vdash\\!c[b/x]:d[b/x]$. This can be graphically
illustrated as follows (IH denotes the use of an inductive hypothesis):

$\inferrule*[left={\em
conv}]{\inferrule*[left=\ref{congr.basic}(1)]{d^{\prime}=_{\lambda}d}{d^{\prime}[b/x]=_{\lambda}d[b/x]}\;\inferrule*[left=IH]{\Gamma_{a}\\!\vdash\\!c:d^{\prime}}{\Gamma_{b}\\!\vdash\\!c[b/x]:d^{\prime}[b/x]}\;\inferrule*[left=IH]{\Gamma_{a}\\!\vdash\\!d^{\prime}:e}{\Gamma_{a}\\!\vdash\\!d^{\prime}[b/x]:e[b/x]}}{\Gamma_{b}\vdash\,c[b/x]:d[b/x]}$

  * •

Rule appl: We have $c=(c_{1}\,c_{2})$, $d=d_{2}[c_{2}/y]$ for some $y$,
$c_{1}$, $c_{2}$, and $d_{2}$ where $\Gamma_{a}\\!\vdash\\!(c_{1}\,c_{2}):d$,
$\Gamma_{a}\\!\vdash\\!c_{1}:[y:d_{1}]d_{2}$, and
$\Gamma_{a}\\!\vdash\\!c_{2}:d_{1}$. Obviously, we can assume that $x\neq y$.
We need to show that
$\Gamma_{b}\\!\vdash\\!(c_{1}\,c_{2})[b/x]:d_{2}[c_{2}/y][b/x]$. We have:

$\displaystyle\Gamma_{b}\vdash\,$ $\displaystyle c_{1}[b/x]$ $\displaystyle:$
(inductive hypothesis on $\Gamma_{a}\\!\vdash\\!c_{1}:[y:d_{1}]d_{2}$)
$\displaystyle([y:d_{1}]d_{2})[b/x]$ $\displaystyle=$ (definition of
substitution) $\displaystyle[y:d_{1}[b/x]](d_{2}[b/x])$

Furthermore, since $\Gamma_{a}\\!\vdash\\!c_{2}:d_{1}$, by inductive
hypothesis we know that $\Gamma_{b}\\!\vdash\\!c_{2}[b/x]:d_{1}[b/x]$. Hence
by type rule appl we obtain

$\Gamma_{b}\\!\vdash\\!(c_{1}[b/x]\,c_{2}[b/x]):d_{2}[b/x][c_{2}[b/x]/y]\qquad(\ast)$

We can now argue as follows:

$\displaystyle\Gamma_{b}\vdash\,$ $\displaystyle(c_{1}\,c_{2})[b/x]$
$\displaystyle=$ (definition of substitution)
$\displaystyle(c_{1}[b/x]\,c_{2}[b/x])$ $\displaystyle:$ (see $\ast$)
$\displaystyle d_{2}[b/x][c_{2}[b/x]/y]$ $\displaystyle=$ (Lemma 5(2))
$\displaystyle d_{2}[c_{2}/y][b/x]$

The other cases can be shown in a similar style.

We begin the closure properties with the relatively straightforward property
that validity is closed against typing.

######  Lemma 29 (Valid expressions have valid types).

For all $\Gamma,a,b$: If $\Gamma\\!\vdash\\!a:b$ then $\Gamma\\!\vdash\\!b$.

######  Proof 4.23.

By induction on the definition of $\Gamma\\!\vdash\\!a:b$ we show that
$\Gamma\\!\vdash\\!a:b$ implies $\Gamma\\!\vdash\\!b$. As an example, we
illustrate the rule for applications

  * •

Rule appl: We have $a=(a_{1}\,a_{2})$ and $b=b_{2}[a_{2}/x]$ for some $x$,
$a_{1}$, $a_{2}$, and $b_{2}$ where $\Gamma\\!\vdash\\!a_{1}:[x:b_{1}]b_{2}$
for some $b_{1}$ and $\Gamma\\!\vdash\\!a_{2}:b_{1}$. From the inductive
hypothesis we know that $\Gamma\\!\vdash\\![x:b_{1}]b_{2}$. By Lemma 27(2)
this implies $\Gamma,x:b_{1}\\!\vdash\\!b_{2}$. From
$\Gamma,x:b_{1}\\!\vdash\\!b_{2}$ and from substitution (Lemma 28, note that
$\Gamma\\!\vdash\\!a_{2}:b_{1}$) we can infer that
$\Gamma\\!\vdash\\!b_{2}[a_{2}/x]=b$.

The other cases can be shown in a similar style.

We are now ready to show the preservation of types under a reduction step.

######  Lemma 30 (Preservation of types under reduction steps).

For all $\Gamma,a,b,c$: $\Gamma\\!\vdash\\!a:c$ and $a\to b$ imply
$\Gamma\\!\vdash\\!b:c$.

######  Proof 4.24.

Proof by induction on the definition of $a\to b$. Note that in all cases of
the inductive proof, by Lemma 29, we have $\Gamma\\!\vdash\\!c$. This means
that in order to show $\Gamma\\!\vdash\\!b:c$, it is sufficient to show
$\Gamma\\!\vdash\\!b:b_{1}$ for some $b_{1}$ where $b_{1}=_{\lambda}c$.
$\Gamma\\!\vdash\\!b:c$ then follows by applying rule conv. We show the cases
of axiom $\beta_{1}$ and of structural rule $\oplus_{x}(\\_,\\_)_{1}$ in
detail:

  * •

Axiom $\beta_{1}$: We have $a=([x:a_{1}]a_{2}\;a_{3})$ and $b=a_{2}[a_{3}/x]$
and $\Gamma\\!\vdash\\!([x:a_{1}]a_{2}\;a_{3}):c$ where
$\Gamma\\!\vdash\\!a_{3}:a_{1}$. The following type relations can be derived:

$\displaystyle\Gamma\\!\vdash\\!([x:a_{1}]a_{2}\;a_{3}):c$
$\displaystyle\Rightarrow$ (Lemma 26(6))
$\displaystyle\Gamma\\!\vdash\\![x:a_{1}]a_{2}:[x:d]e\quad\text{where
$c=_{\lambda}e[a_{3}/x]$ ($\ast$) and $\Gamma\\!\vdash\\!a_{3}:d$}$
$\displaystyle\Rightarrow$ (Lemma 26(1))
$\displaystyle(\Gamma,x:a_{1})\\!\vdash\\!a_{2}:b_{2}\quad\text{where
$[x:d]e=_{\lambda}[x:a_{1}]b_{2}$}$ $\displaystyle\Rightarrow$ (Lemma 28,
since $\Gamma\\!\vdash\\!a_{3}:a_{1}$)
$\displaystyle\Gamma\\!\vdash\\!a_{2}[a_{3}/x]:b_{2}[a_{3}/x]$

From $[x:d]e=_{\lambda}[x:a_{1}]b_{2}$, by Lemma 21(2) it follows that
$e=_{\lambda}b_{2}$. We can therefore argue as follows:

$\displaystyle b_{2}[a_{3}/x]$ $\displaystyle=_{\lambda}$ (by Lemma 21(1)
since $e=_{\lambda}b_{2}$) $\displaystyle e[a_{3}/x]$
$\displaystyle=_{\lambda}$ (see $\ast$ in the first argument chain)
$\displaystyle c$

Therefore we can apply rule conv to derive
$\Gamma\\!\vdash\\!b=a_{2}[a_{3}/x]:c$. This can be graphically illustrated as
follows:

$\inferrule*[left={\em
conv}]{\Gamma\\!\vdash\\!a_{2}[a_{3}/x]:b_{2}[a_{3}/x]\qquad
b_{2}[a_{3}/x]=_{\lambda}c\qquad\Gamma\\!\vdash\\!c}{\Gamma\vdash\,a_{2}[a_{3}/x]:c}$

  * •

Rule $\oplus_{x}(\\_,\\_)_{1}$: We have $a=\oplus_{x}(a_{1},a_{3})$,
$b=\oplus_{x}(a_{2},a_{3})$ where $a_{1}\to a_{2}$, and
$\Gamma\\!\vdash\\!\oplus_{x}(a_{1},a_{3}):c$. By Lemma 26(1),
$c=_{\lambda}[x:a_{1}]c_{3}$ for some $c_{3}$ where
$(\Gamma,x:a_{1})\\!\vdash\\!a_{3}:c_{3}$. By Lemma 23 this implies that
$\Gamma\\!\vdash\\!a_{1}$ and therefore by inductive hypothesis we know that
$\Gamma\\!\vdash\\!a_{2}$. Therefore we can apply Lemma 25 which implies that
$(\Gamma,x:a_{2})\\!\vdash\\!a_{3}:c_{3}$. By definition of typing
$\Gamma\\!\vdash\\!\oplus_{x}(a_{2},a_{3}):[x:a_{2}]c_{3}$. Since
$[x:a_{2}]c_{3}=_{\lambda}[x:a_{1}]c_{3}=_{\lambda}c$, we can apply type rule
conv to derive $\Gamma\\!\vdash\\!b=\oplus_{x}(a_{2},a_{3}):c$.

The other cases can be shown in a similar style using also Lemma 6.

A simple inductive argument extends Lemma 30 to general reduction. This
property is often referred to as subject reduction.

######  Theorem 31 (Subject reduction: Types are preserved under reduction).

For all $\Gamma,a,b,c$: $a\to^{*}b$ and $\Gamma\\!\vdash\\!a:c$ imply that
$\Gamma\\!\vdash\\!b:c$.

Lemma 31 can be reformulated using the validity notation.

######  Corollary 32 (Valid expressions are closed against reduction).

For all $\Gamma,a,b$: $\Gamma\\!\vdash\\!a$ and $a\to^{*}b$ implies
$\Gamma\\!\vdash\\!b$

A straightforward argument leads to a closure result of validity w.r.t.
context reduction.

######  Lemma 33 (Validity is closed against context reduction).

For all $\Gamma_{1},\Gamma_{2},x,a,b,c$: If
$(\Gamma_{1},x:b,\Gamma_{2})\\!\vdash\\!a$ and $b\to^{*}c$ then
$(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!a$

######  Proof 4.25.

From $(\Gamma_{1},x:b,\Gamma_{2})\\!\vdash\\!a$ by repeated application of the
type rule for universal abstraction we can infer
$(\Gamma_{1},x:b)\\!\vdash\\![\Gamma_{2}]a$. By Lemma 23, it follows that
$\Gamma\\!\vdash\\!b$. By Corollary 32 we know that $\Gamma_{1}\\!\vdash\\!c$.
Obviously $b=_{\lambda}c$ and hence Lemma 25 can be applied which implies
$(\Gamma_{1},x:c)\\!\vdash\\![\Gamma_{2}]a$. By repeated application of Lemma
27(2) we obtain $(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!a$.

Before we show uniqueness of types, we need a Lemma about the effect of
removing unnecessary type declarations from a context.

######  Lemma 34 (Context contraction).

For all $\Gamma_{1},\Gamma_{2},x,a,b,c$:
$(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!a:b$ and $x\notin{\it
FV}([\Gamma_{2}]a)$ implies $(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a:b^{\prime}$
and $b\to^{*}b^{\prime}$ for some $b^{\prime}$.

Note that in this lemma $x\notin{\it FV}([\Gamma_{2}]a)$ does not necessarily
imply $x\notin{\it FV}([\Gamma_{2}]b)$, for example take
$x:\tau\\!\vdash\\!\tau:([y:\tau]\tau\,x)$, and hence the reduction of the
type to some expression where $x$ does not occur free, in the example
$([y:\tau]\tau\,x)\to^{*}\tau$, is necessary.

######  Proof 4.26.

Proof by induction on the definition of
$(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!a:b$. We show two interesting cases

  * •

Rule conv: We have $(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!a:b$ where
$(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!a:b_{1}$ for some $b_{1}$ where
$b_{1}=_{\lambda}b$ and $(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!b$.

Assume that $x\notin{\it FV}([\Gamma_{2}]a)$. By inductive hypothesis there is
a $b_{1}^{\prime}$ with $b_{1}\to^{*}b_{1}^{\prime}$ and
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a:b_{1}^{\prime}$. Since
$b_{1}=_{\lambda}b$, by Theorem 20 we know that $b_{1}\to^{*}b_{2}$ and
$b\to^{*}b_{2}$ for some $b_{2}$. Since $b_{1}\to^{*}b_{1}^{\prime}$ and
$b_{1}\to^{*}b_{2}$, by Theorem 20 we know that $b_{2}\to^{*}b^{\prime}$ and
$b_{1}^{\prime}\to^{*}b^{\prime}$ for some $b^{\prime}$. Obviously
$b\to^{*}b^{\prime}$. We have to show
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a:b^{\prime}$.

From $(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a:b_{1}^{\prime}$, by Lemma 29 we
know that $(\Gamma_{1},\Gamma_{2})\\!\vdash\\!b_{1}^{\prime}$. Since
$b_{1}^{\prime}\to^{*}b^{\prime}$, by Lemma 32 we know that
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!b^{\prime}$. Since
$b_{1}^{\prime}=_{\lambda}b^{\prime}$ we can apply rule conv to infer that
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a:b^{\prime}$. This can be graphically
illustrated as follows:

$\inferrule*[left={\em
conv}]{\inferrule*[left=IH]{\Gamma_{1},x:c,\Gamma_{2}\\!\vdash\\!a:b}{\Gamma_{1},\Gamma_{2}\\!\vdash\\!a:b_{1}^{\prime}}\quad
b_{1}^{\prime}=_{\lambda}b^{\prime}\quad\inferrule*[left=\ref{valid.rd}]{\inferrule*[left=\ref{valid.type}]{\inferrule*[left=IH]{\Gamma_{1},x:c,\Gamma_{2}\\!\vdash\\!a:b}{\Gamma_{1},\Gamma_{2}\\!\vdash\\!a:b_{1}^{\prime}}}{\Gamma_{1},\Gamma_{2}\\!\vdash\\!b_{1}^{\prime}}}{\Gamma_{1},\Gamma_{2}\\!\vdash\\!b^{\prime}}}{\Gamma_{1},\Gamma_{2}\\!\vdash\\!a:b^{\prime}}$

  * •

Rule appl: We have $a=(a_{1}\,a_{2})$, $b=e[a_{2}/y]$ for some $y$, $a_{1}$,
$a_{2}$, and $e$ where
$(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!(a_{1}\,a_{2}):e[a_{2}/x]$ and
$(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!a_{1}:[y:d]e$ and
$(\Gamma_{1},x:c,\Gamma_{2})\\!\vdash\\!a_{2}:d$ for some $d$.

Since $x\notin{\it FV}((a_{1}\,a_{2}))$ we know that $x\notin{\it
FV}(a_{1})\cup{\it FV}(a_{2})$. By inductive hypothesis
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a_{1}:e^{\prime}$ for some $e^{\prime}$
where $[y:d]e\to^{*}e^{\prime}$ and
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a_{2}:d^{\prime}$ for some $d^{\prime}$
where $d\to^{*}d^{\prime}$. By Lemma 7(1) we know that
$e^{\prime}=[y:d_{1}]e_{1}$ for some $d_{1}$ and $e_{1}$ where $d\to^{*}d_{1}$
and $e\to^{*}e_{1}$ ($\ast$). By Theorem 20 we therefore know that
$d^{\prime}\to^{*}d_{2}$ ($\dagger$) and $d_{1}\to^{*}d_{2}$ ($\ddagger$) for
some $d_{2}$.

We will show $(\Gamma_{1},\Gamma_{2})\\!\vdash\\!(a_{1}\,a_{2}):b^{\prime}$
where $b^{\prime}=e_{1}[a_{2}/x]$. According to rule appl, this requires to
show that $a_{2}$ has a type which matches the domain of $a_{1}$ (both under
$(\Gamma_{1},\Gamma_{2})$).

By Lemma 29 we know that
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!e^{\prime}=[y:d_{1}]e_{1}$. By Lemma 32 we
know that also $(\Gamma_{1},\Gamma_{2})\\!\vdash\\![y:d_{2}]e_{1}$. Since
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a_{1}:e^{\prime}=[y:d_{1}]e_{1}$ and
($\ddagger$), we can apply rule conv to infer that
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a_{1}:[y:d_{2}]e_{1}$. From
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\![y:d_{2}]e_{1}$ by Lemma 27(2) we know
that $(\Gamma_{1},\Gamma_{2})\\!\vdash\\!d_{2}$. Since
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a_{2}:d^{\prime}$ and ($\dagger$) we can
apply rule conv to infer that
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!a_{2}:d_{2}$.

Hence by definition of typing (appl) we know that
$(\Gamma_{1},\Gamma_{2})\\!\vdash\\!(a_{1}\,a_{2}):e_{1}[a_{2}/x]$. The
proposition follows since by ($\ast$) and Lemma 6 we have
$b=e[a_{2}/x]\to^{*}e_{1}[a_{2}/x]=b^{\prime}$.

The other cases can be shown in a similar style using also the Lemmas 28 and
33.

We can now show uniqueness of types. Most cases are straightforward, except
for the weakening rule where we need the context contraction result above.

######  Theorem 35 (Uniqueness of types).

For all $\Gamma,a,b,c$: $\Gamma\\!\vdash\\!a:b$ and $\Gamma\\!\vdash\\!a:c$
implies $b=_{\lambda}c$.

######  Proof 4.27.

Proof by induction on the definition of $\Gamma\\!\vdash\\!a:b$. We show three
interesting cases: In each case, if we look at a type rule
$\Gamma\\!\vdash\\!a:b$ we have to show that if also $\Gamma\\!\vdash\\!a:c$
then $b=_{\lambda}c$.

  * •

Rule start: We have $a=x$, $\Gamma=(\Gamma^{\prime},x:b)$ for some
$\Gamma^{\prime}$ and $x$ where $(\Gamma^{\prime},x:b)\\!\vdash\\!x:b$ and
$\Gamma^{\prime}\\!\vdash\\!b:d$ for some $d$: Let
$(\Gamma^{\prime},x:b)\\!\vdash\\!x:c$. By Lemma 24 we know that
$b=_{\lambda}c$.

  * •

Rule weak: We have $\Gamma=(\Gamma^{\prime},x:d)$ for some $\Gamma^{\prime}$
and $x$ where $(\Gamma^{\prime},x:d)\\!\vdash\\!a:b$,
$\Gamma^{\prime}\\!\vdash\\!a:b$, and $\Gamma^{\prime}\\!\vdash\\!d:e$ for
some $e$.

Let $(\Gamma^{\prime},x:d)\\!\vdash\\!a:c$. Since $x\notin{\it FV}(a)$, by
Lemma 34 we know that $\Gamma^{\prime}\\!\vdash\\!a:c^{\prime}$ for some
$c^{\prime}$ with $c\to^{*}c^{\prime}$. By inductive hypothesis
$b=_{\lambda}c^{\prime}$ which implies $b=_{\lambda}c$.

  * •

Rule appl: We have $a=(a_{1}\,a_{2})$ and $b=b_{2}[a_{2}/x]$ for some $x$,
$a_{1}$, $a_{2}$, and $b_{2}$ where
$\Gamma\\!\vdash\\!(a_{1}\,a_{2}):b_{2}[a_{2}/x]$,
$\Gamma\\!\vdash\\!a_{1}:[x:b_{1}]b_{2}$, and $\Gamma\\!\vdash\\!a_{2}:b_{1}$.

Let $\Gamma\\!\vdash\\!(a_{1}\,a_{2}):c$. By Lemma 26(6) we know that
$c=_{\lambda}c_{2}[a_{2}/y]$ for some $c_{1}$, $c_{2}$ where
$\Gamma\\!\vdash\\!a_{1}:[y:c_{1}]c_{2}$ and $\Gamma\\!\vdash\\!a_{2}:c_{1}$.
By inductive hypothesis applied to $\Gamma\\!\vdash\\!a_{1}:[x:b_{1}]b_{2}$ it
follows that $[x:b_{1}]b_{2}=_{\lambda}[y:c_{1}]c_{2}$. Hence obviously $x=y$
and by basic properties of congruence (Lemma 21(2)) it follows that
$b_{2}=_{\lambda}c_{2}$. Using Lemma 21(1) we can argue
$b=_{\lambda}b_{2}[a_{2}/x]=_{\lambda}c_{2}[a_{2}/x]=_{\lambda}c$.

The other cases can be shown in a similar style.

###  4.3 Strong normalization

The idea for the proof of strong normalization of valid expressions in
$\mathtt{d}$ is to classify expressions according to structural properties, in
order to make an inductive argument work. For this purpose we define
structural skeletons called norms as the subset of expressions built from the
primitive $\tau$ and binary products only and we define a partial function
assigning norms to expressions. Norms are a reconstruction of a concept of
simple types, consisting of atomic types and product types, within
$\mathtt{d}$777The construction of norms inside $\mathtt{d}$ is due to
convenient reuse of existing structures and definitions, norms could also be
introduced as a separate mathematical structure. Analogously to simple types,
norms provide a handle to classify valid expressions into different degrees of
structural complexity. The idea of the strong normalisation argument is first
to prove that all valid expressions are normable, i.e they are in the domain
of the norming function, and then to prove that all normable expressions are
strongly normalizable, i.e they are not the origin of an infinite reduction
sequence.

The good news is that in $\mathtt{d}$ we are not dealing with unconstrained
parametric types as for example in System F (see e.g. [12]), and therefore we
will be able to use more elementary methods to show strong normalisation as
used for the simply typed lambda calculus. A common such method is to define a
notion of reducible expressions satisfying certain reducibility conditions
suitable for inductive arguments both on type structure and on reduction
length, and then to prove that all reducible expressions satisfy certain
reducibility properties including strong normalisation, and to prove that that
all typable expressions are reducible ([29],[11]). We will basically adopt
this idea, but the bad news is that common definitions of reducibility (e.g.
[12]) apparently cannot be adapted to include the reduction of negation. A
more suitable basis for our purposes was found to be the notion of computable
expressions as defined in language theoretical studies of Automath [31], see
also [30]. This approach is basically extended here to cover additional
operators, including negation.

We motivate the basic idea of the proof (precise definitions can be found
below): Consider the following condition necessary to establish strong
normalization for an application $(a\,b)$ in the context of an inductive proof
(where ${\mathcal{S}}$ denotes the set of strongly normalizable expressions):

  * •

If $a\to^{*}[x:c_{1}]c_{2}\in{\mathcal{S}}$ and $b\in{\mathcal{S}}$ then
$c_{2}[b/x]\in{\mathcal{S}}$.

Similarly, the following condition is necessary to establish strong
normalization for a negation $\neg a$ in the context of an inductive proof.

  * •

If $a\to^{*}[x:c_{1}]c_{2}\in{\mathcal{S}}$ then $\neg c_{2}\in{\mathcal{S}}$.

These and other properties inspire the definition of the set of computable
expressions $C_{\Gamma}$ which are normable, strongly normalizable, and
satisfy the property that $a,b\in C_{\Gamma}$ implies $\neg a,(a\,b)\in
C_{\Gamma}$. Unfortunately, the closure properties of computable expressions
do not include existential and universal abstraction. Instead, we need to
prove the stronger property that normable expressions are computable under
norm-preserving substitutions of their free variables to computable
expressions.

This property implies that all normable expressions are computable and
therefore that normability and computability are equivalent notions. The
logical relations between the various notions can be summarized as follows:

$\Gamma\\!\vdash\\!a\quad\Rightarrow\quad\Gamma\\!\models\\!a\quad\Leftrightarrow\quad
a\in{\it C}_{\Gamma}\quad\Rightarrow\quad a\in{\mathcal{S}}$

We begin with some basic definitions and properties related to strong
normalization. [Strongly normalizable expressions] The set of strongly
normalizable expressions is denoted by ${\mathcal{S}}$. An expression $a$ is
in ${\mathcal{S}}$ iff there is no infinite sequence of one-step reductions
$a\to a_{1}\to a_{2}\to a_{3}\ldots$

######  Lemma 36 (Basic properties of strongly normalizable expressions).

For all $a,b,c,x$:

  1. 1.

$a[b/x]\in{\mathcal{S}}$ and $b\to^{*}c$ imply $a[c/x]\in{\mathcal{S}}$

  2. 2.

$a,b,c\in{\mathcal{S}}$ implies $\oplus_{x}(a,b)\in{\mathcal{S}}$, $a.1$,
$a.2\in{\mathcal{S}}$, $[x\\!\doteq\\!a,b:c]\in{\mathcal{S}}$, $[a,b]$,
$[a+b]$, $[a,:\\!b]$, $[:\\!a,b]$, and $[a\,?\,b]\in{\mathcal{S}}$.

######  Proof 4.28.

These properties can be shown through a proof by contradiction using
elementary properties of reduction (Lemmas 6 and 7).

Next we show conditions under which applications and negations are strongly
normalizing.

######  Lemma 37 (Strong normalization conditions).

  1. 1.

For all $a,b\in{\mathcal{S}}$: $(a\,b)\in{\mathcal{S}}$ if for any $c_{1}$,
$c_{2}$, $d_{1}$, $d_{2}$, and $x$, the following conditions are satisfied:

     * $(C_{1})$

$a\to^{*}\oplus_{x}(c_{1},c_{2})$ implies that $c_{2}[b/x]\in{\mathcal{S}}$

     * $(C_{2})$

$a\to^{*}[c_{1}\,?\,c_{2}]$ and $b\to^{*}[d_{1},:\\!d_{2}]$ implies
$(c_{1}\,d_{1})\in{\mathcal{S}}$

     * $(C_{3})$

$a\to^{*}[c_{1}\,?\,c_{2}]$ and $b\to^{*}[:\\!d_{1},d_{2}]$ implies
$(c_{2}\,d_{2})\in{\mathcal{S}}$

  2. 2.

For all $a\in{\mathcal{S}}$: $\neg a\in{\mathcal{S}}$ if for any $b$ and $c$,
the following conditions are satisfied:

     * $(C_{1})$

$a\to^{*}[b\oplus c]$ implies $\neg b$, $\neg c\in{\mathcal{S}}$

     * $(C_{2})$

$a\to^{*}\oplus_{x}(b,c)$ implies $\neg c\in{\mathcal{S}}$

######  Proof 4.29.

These properties can be shown through a proof by contradiction using
elementary properties of reduction (Lemmas 6, 7, and 8) and of strong
normalisation (Lemma 36).

Norms are a subset of expressions representing structural skeletons of
expressions. Norms play an important role to classify expressions in the
course of the proof of strong normalization. [Norm, norming, normable
expressions] The set of norms $\mathcal{\bar{E}}$ is generated by the
following rules

$\displaystyle\mathcal{\bar{E}}$ $\displaystyle\\!::=\\!$
$\displaystyle\tau\,\mid\,[\mathcal{\bar{E}},\mathcal{\bar{E}}]$

Obviously $\mathcal{\bar{E}}\subset\mathcal{E}$. We will use the notation
$\bar{a}$, $\bar{b}$, $\bar{c}$, $\ldots$ to denote norms. The partial norming
function $\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma}$ defines for some
expressions $a$ the norm of $a$ under an environment $\Gamma$. It is defined
by the equations in Table 8.

$\displaystyle\,\parallel\\!\\!\tau\\!\\!\parallel_{\Gamma}$ $\displaystyle=$
$\displaystyle\tau$ $\displaystyle\,\parallel\\!\\!x\\!\\!\parallel_{\Gamma}$
$\displaystyle=$
$\displaystyle\,\parallel\\!\\!\Gamma(x)\\!\\!\parallel_{\Gamma}\quad\text{if}\;\Gamma(x)\;\text{is
defined}$
$\displaystyle\,\parallel\\!\\!\oplus_{x}(a,b)\\!\\!\parallel_{\Gamma}$
$\displaystyle=$
$\displaystyle[\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma},\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma,x:a}]$
$\displaystyle\,\parallel\\!\\!(a\,b)\\!\\!\parallel_{\Gamma}$
$\displaystyle=$
$\displaystyle\bar{c}\quad\text{if}\;\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma}=[\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma},\bar{c}]$
$\displaystyle\,\parallel\\!\\![x\\!\doteq\\!a,b:c]\\!\\!\parallel_{\Gamma}$
$\displaystyle=$
$\displaystyle[\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma},\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma}]\quad\text{if}\;\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma}=\,\parallel\\!\\!c\\!\\!\parallel_{\Gamma,x:a}$
$\displaystyle\,\parallel\\!\\![a\oplus b]\\!\\!\parallel_{\Gamma}$
$\displaystyle=$
$\displaystyle[\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma},\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma}]$
$\displaystyle\,\parallel\\!\\!a.1\\!\\!\parallel_{\Gamma}$ $\displaystyle=$
$\displaystyle\bar{a}\quad\text{if}\;\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma}=[\bar{a},\bar{b}]$
$\displaystyle\,\parallel\\!\\!a.2\\!\\!\parallel_{\Gamma}$ $\displaystyle=$
$\displaystyle\bar{b}\quad\text{if}\;\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma}=[\bar{a},\bar{b}]$
$\displaystyle\,\parallel\\!\\![a,:\\!b]\\!\\!\parallel_{\Gamma}$
$\displaystyle=$
$\displaystyle[\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma},\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma}]$
$\displaystyle\,\parallel\\!\\![:\\!a,b]\\!\\!\parallel_{\Gamma}$
$\displaystyle=$
$\displaystyle[\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma},\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma}]$
$\displaystyle\,\parallel\\!\\![a\,?\,b]\\!\\!\parallel_{\Gamma}$
$\displaystyle=$
$\displaystyle[[\bar{a},\bar{b}],\bar{c}]\quad\text{if}\;\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma}=[\bar{a},\bar{c}],\;\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma}=[\bar{b},\bar{c}]$
$\displaystyle\,\parallel\\!\\!\neg a\\!\\!\parallel_{\Gamma}$
$\displaystyle=$ $\displaystyle\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma}$

Table 8: Norming

The partial norming function is well-defined, in the sense that one can show
by structural induction on $a$ with context $\Gamma$ that, if defined,
$\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma}$ is unique. An expression $a$ is
normable relative under context $\Gamma$ iff
$\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma}$ is defined. This is written as
$\Gamma\\!\models\\!a$. Similarly to typing we use the notation
$\Gamma\\!\models\\!a_{1},\ldots,a_{n}$ as an abbreviation for
$\Gamma\\!\models\\!a_{1}$, $\ldots$, $\Gamma\\!\models\\!a_{n}$.

######  Remark 38 (Examples).

There are valid and invalid normable expressions and there are strongly
normalisable expression which are neither valid nor normable. We present some
examples. We will show later that all valid expressions are normable (43) and
that all normable expressions are strongly normalizable (52 and 53). Let
$\Gamma=(p,q\\!:\\!\tau,\;z\\!:\\![x\\!:\\!p][y\\!:\\!q]\tau,\;w\\!:\\![x\\!:\\!\tau]x)$.
Consider the expression $[x:p](z\,x)$:

  * •

We have $\Gamma\\!\vdash\\![x\\!:\\!p](z\,x)$.

  * •

We have $\Gamma\\!\models\\![x\\!:\\!p](z\,x)$ since
$\,\parallel\\!\\![x\\!:\\!p](z\,x)\\!\\!\parallel_{\Gamma}=[\tau,\,\parallel\\!\\!(z\,x)\\!\\!\parallel_{\Gamma,x:p}]=[\tau,[\tau,\tau]]$.
The latter equality is true since
$\,\parallel\\!\\!z\\!\\!\parallel_{\Gamma,x:p}=\,\parallel\\!\\![x\\!:\\!p][y\\!:\\!q]\tau\\!\\!\parallel_{\Gamma,x:p}=[\tau,[\tau,\tau]]$
and
$\,\parallel\\!\\!x\\!\\!\parallel_{\Gamma,x:p}=\,\parallel\\!\\!p\\!\\!\parallel_{\Gamma,x:p}=\tau$.

Consider the expression $[x\\!:\\!p](z\,p)$:

  * •

We do not have $\Gamma\\!\vdash\\![x:p](z\,p)$ since we do not have
$\Gamma\\!\vdash\\!p:p$.

  * •

We have $\Gamma\\!\models\\![x:p](z\,p)$ since
$\,\parallel\\!\\![x:p](z\,p)\\!\\!\parallel_{\Gamma}=[\tau,[\tau,\tau]]$ and
$\,\parallel\\!\\!p\\!\\!\parallel_{\Gamma,x:p}=\tau$

As a third example consider the expression $[x:[y:\tau]y](x\,x)$:

  * •

Obviously $[x:[y:\tau]y](x\,x)\in{\mathcal{S}}$.

  * •

We do not have $\;\\!\vdash\\![x:[y:\tau]y](x\,x)$ since the application
$(x\,x)$ cannot be typed.

  * •

We do not have $\;\\!\models\\![x:[y:\tau]y](x\,x)$: The definition of norming
leads us to the expression
$\,\parallel\\!\\!(x\,x)\\!\\!\parallel_{x:[y:\tau]y}$ which is not defined
since this would require that
$\,\parallel\\!\\!x\\!\\!\parallel_{x:[y:\tau]y}=[\,\parallel\\!\\!x\\!\\!\parallel_{x:[y:\tau]y},\bar{a}]$
for some $\bar{a}$. Hence the norming condition for application is violated.

We show several basic properties of normable expressions culminating in the
property that all valid expressions are normable. Some of these properties and
proofs are structurally similar to the corresponding ones for valid
expressions. However, due to the simplicity of norms, the proofs are much
shorter.

######  Lemma 39 (Norm equality in context).

Let $\Gamma_{a}=(\Gamma_{1},x:a,\Gamma_{2})$ and
$\Gamma_{b}=(\Gamma_{1},x:b,\Gamma_{2})$ for some
$\Gamma_{1},\Gamma_{2},x,a,b$. For all $c$: If $\Gamma_{1}\\!\models\\!a,b$,
$\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma_{1}}=\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma_{1}}$,
and $\Gamma_{a}\\!\models\\!c$ then $\Gamma_{b}\\!\models\\!c$ and
$\,\parallel\\!\\!c\\!\\!\parallel_{\Gamma_{a}}=\,\parallel\\!\\!c\\!\\!\parallel_{\Gamma_{b}}$.

######  Proof 4.30.

The straightforward proof is by structural induction on the definition of
$\,\parallel\\!\\!c\\!\\!\parallel_{\Gamma_{a}}$.

######  Lemma 40 (Substitution and norming).

Let $\Gamma_{a}=(\Gamma_{1},x:a,\Gamma_{2})$ and
$\Gamma_{b}=(\Gamma_{1},\Gamma_{2}[b/x])$ for some
$\Gamma_{1},\Gamma_{2},x,a,b$. For all $c$: If $\Gamma_{1}\\!\models\\!a,b$,
$\,\parallel\\!\\!a\\!\\!\parallel_{\Gamma_{1}}=\,\parallel\\!\\!b\\!\\!\parallel_{\Gamma_{1}}$,
and $\Gamma_{a}\\!\models\\!c$ then $\Gamma_{b}\\!\models\\!c[b/x]$ and
$\,\parallel\\!\\!c\\!\\!\parallel_{\Gamma_{a}}=\,\parallel\\!\\!c[b/x]\\!\\!\parallel_{\Gamma_{b}}$.