The idea that it is rational to respect symmetry when assigning beliefs led us in the previous chapters to formulate the Principles of Constant and Predicate Exchangeability, Strong Negation and Atom Exchangeability. Since these have proved rather fruitful it is natural to ask if there are other symmetries we might similarly exploit, and in turn this begs the question as to what we actually mean by a ‘symmetry’. In this chapter we will suggest an answer to this question, and then consider some of its consequences.

First recall the context in which we are proposing our ‘rational principles of belief assignment’: Namely we imagine an agent inhabiting some world or structure M in TL who is required to assign probabilities w(θ) to the θ ∈ SL in an arguably rational way despite knowing nothing about which particular structure M from TL s/he is inhabiting. Given this framework it seems (to us at least) clear that the agent should act the same in this framework as s/he would in any isomorphic copy of it, on the grounds that with zero knowledge the agent should have no way of differentiating between his/her framework and this isomorphic copy.

To make sense of this idea we need an appropriate formulation of an ‘automorphism’ of the framework. Arguing that all the agent knows is L, TL and for each θ ∈ SL the conditions under which θ holds, equivalently the set of structures in TL in which θ is true, suggests that what we mean by an ‘automorphism’ is an automorphism σ of the two sorted structure BL with universe TL together with all the subsets of TL of the form

[θ] = {M ∈ TL|M ⊧ θ}

for θ ∈ SL, and the binary relation ∈ between elements of TL and the sets [θ].

Extension of λC to the system λD0

In the present chapter we investigate the formal aspects of adding definitions to a type system. In this we follow the pioneering work of N.G. de Bruijn (cf. de Bruijn, 1970). As the basic system we take λC, the most powerful system in the λ-cube. System λC is suitable for the PAT-interpretation, because it encapsulates λP. But it also covers the nice second order aspects of λ2. Therefore, λC appears to be enough for the purpose of ‘coding’ mathematics and mathematical reasonings and is an excellent candidate for the natural extension we want, being almost inevitable for practical applications: the addition of definitions.

We start with an extension leading from λC to a system called λD0. This system contains a formal version of definitions in the usual sense, the so-called descriptive definitions, so it can be used for a great amount of applications in the realm of logic and mathematics. But λD0 does not yet allow a satisfactory representation of axioms and axiomatic notions; these will be considered in the following chapter, in which a small, further extension of λD0 leads to our final system λD. (We have noticed before that we do not consider inductive and recursive definitions, since we can do without them; see Section 8.2.)

In order to give a proper description of λD0, we first extend our set of expressions, as given in Definition 6.3.1 for λC.

Aim and scope

The aim of the book is, firstly, to give an introduction to type theory, an evolving scientific field at the crossroads of logic, computer science and mathematics. Secondly, the book explains how type theory can be used for the verification of mathematical expressions and reasonings.

Type theory enables one to provide a ‘coded’ version – i.e. a full formalisation – of many mathematical topics. The formal system underlying type theory forces the user to work in a very precise manner. The real power of type theory is that well-formedness of the formalised expressions implies logical and mathematical correctness of the original content.

An attractive property of type theory is that it becomes possible and feasible to do the encoding in a ‘natural’ manner, such that one follows (and recognises) the way in which these subjects were presented originally. Another important feature of type theory is that proofs are treated as first-class citizens, in the sense that proofs do not remain meta-objects, but are coded as expressions (terms) of the same form as the rest of the formalisation.

The authors intend to address a broad audience, ranging from university students to professionals. The exposition is gentle and gradual, developing the material at a steady pace, with ample examples and comments, cross-references and motivations. Theoretical issues relevant for logic and computer science alternate with practical applications in the area of fundamental mathematical subjects.