Recent debates in metaphysics have highlighted the significance of type theories, such as Simple Type Theory (STT), for our philosophical analysis. In this chapter, I present the salient features of a constructive type theory in the style of Martin-Löf, termed CTT. My principal aim is to convey the flavour of this rich, flexible and sophisticated theory and compare it with STT. I especially focus on the forms of quantification which are available in CTT. (...) A further aim is to argue that a comparison between a plurality of theories is beneficial to the philosophical analysis. We may, for example, discover helpful features of one theory that we may want to import into another context, thus enriching our repertoire of formal tools. Or, through comparison with a less well-known theory, we may gain a better understanding of the characteristics of the theories we are familiar with. As argued in this chapter, CTT has much to offer in all of these respects. (shrink)

Martin-Löf Type Theory is both an important and practical formalization and a focus for a charismatic view of the foundations of mathematics. Per Martin-Löf's work has been of huge significance in the fields of logic and the foundations of mathematics, and has important applications in areas such as computing science and linguistics. This volume celebrates the twenty-fifth anniversary of the birth of the subject, and is an invaluable record both of areas of currentactivity and of the early development (...) of the subject. Also published for the first time is one of Per Martin-Löf's earliest papers. (shrink)

This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Lof over the last twenty-five years.

Recent literature on dialogical logic discusses the case of tonk and the notion harmony in the context of a rule-based theory of meaning. Now, since the publications of those papers, a dialogical version of constructive type theory has been developed. The aim of the present paper is to show that, from the dialogical point of view, the harmony of the CTT-rules is the consequence of a more fundamental level of meaning characterized by the independence of players. (...) We hope that the following paper will contribute to a better understanding of the dialogical notion of meaning. (shrink)

The notion of cognitive act is of importance for an epistemology that is apt for constructive type theory, and for epistemology in general. Instead of taking knowledge attributions as the primary use of the verb 'to know' that needs to be given an account of, and understanding a first-person knowledge claim as a special case of knowledge attribution, the account of knowledge that is given here understands first-person knowledge claims as the primary use of the verb 'to (...) know'. This means that a cognitive act is an act that counts as cognitive from a first-person point of view. The method of linguistic phenomenology is used to explain or elucidate our epistemic notions. One of the advantages of the theory is that an answer can be given to some of the problems in modern epistemology, such as the Gettier problem. (shrink)

Taking Per Martin-Löf’s constructive type theory as a starting-point a theory of assertion is developed, which is able to account for the epistemic aspects of the speech act of assertion, and in which it is shown that assertion is not a wide genus. From a constructivist point of view, one is entitled to assert, for example, that a proposition A is true, only if one has constructed a proof object a for A in an act of (...) demonstration. One thereby has grounded the assertion by an act of demonstration, and a grounding account of assertion therefore suits constructive type theory. Because the act of demonstration in which such a proof object is constructed results in knowledge that A is true, the constructivist account of assertion has to ward off some of the criticism directed against knowledge accounts of assertion. It is especially the internal relation between a judgement being grounded and its being known that makes it possible to do so. The grounding account of assertion can be considered as a justification account of assertion, but it also differs from justification accounts recently proposed, namely in the treatment of selfless assertions, that is, assertions which are grounded, but are not accompanied by belief. (shrink)

Taking Per Martin-Löf’s constructive type theory as a starting-point a theory of assertion is developed, which is able to account for the epistemic aspects of the speech act of assertion, and in which it is shown that assertion is not a wide genus. From a constructivist point of view, one is entitled to assert, for example, that a proposition A is true, only if one has constructed a proof object a for A in an act of (...) demonstration. One thereby has grounded the assertion by an act of demonstration, and a grounding account of assertion therefore suits constructive type theory. Because the act of demonstration in which such a proof object is constructed results in knowledge that A is true, the constructivist account of assertion has to ward off some of the criticism directed against knowledge accounts of assertion. It is especially the internal relation between a judgement being grounded and its being known that makes it possible to do so. The grounding account of assertion can be considered as a justification account of assertion, but it also differs from justification accounts recently proposed, namely in the treatment of selfless assertions, that is, assertions which are grounded, but are not accompanied by belief. (shrink)

We introduce a predicative version of topos based on the notion of small maps in algebraic set theory, developed by Joyal and one of the authors. Examples of stratified pseudotoposes can be constructed in Martin-Löf type theory, which is a predicative theory. A stratified pseudotopos admits construction of the internal category of sheaves, which is again a stratified pseudotopos. We also show how to build models of Aczel-Myhill constructive set theory using this categorical structure.

We now move to the demonstration of the left-to-right direction of the equivalence result. Let us assume that there is a winning $$\mathbf {P}$$ P -strategy in the dialogical game for $$\varphi $$ φ.

The standard construction of quotient spaces in topology uses full separation and power sets. We show how to make this construction using only the predicative methods available in constructive type theory and constructive set theory.

This paper is the first in a series whose objective is to study notions of large sets in the context of formal theories of constructivity. The two theories considered are Aczel's constructive set theory and Martin-Löf's intuitionistic theory of types. This paper treats Mahlo's π-numbers which give rise classically to the enumerations of inaccessibles of all transfinite orders. We extend the axioms of CZF and show that the resulting theory, when augmented by the tertium non-datur, is (...) equivalent to ZF plus the assertion that there are inaccessibles of all transfinite orders. Finally, the theorems of that extension of CZF are interpreted in an extension of Martin-Löf's intuitionistic theory of types by a universe. (shrink)

Gödel's dialectica interpretation of Heyting arithmetic HA may be seen as expressing a lack of confidence in our understanding of unbounded quantification. Instead of formally proving an implication with an existential consequent or with a universal antecedent, the dialectica interpretation asks, under suitable conditions, for explicit ‘interpreting’ instances that make the implication valid. For proofs in constructive set theory CZF‐, it may not always be possible to find just one such instance, but it must suffice to explicitly name (...) a set consisting of such interpreting instances. The aim of eliminating unbounded quantification in favor of appropriate constructive functionals will still be obtained, as our ∧‐interpretation theorem for constructive set theory in all finite types CZFω‐ shows. By changing to a hybrid interpretation ∧q, we show closure of CZFω‐ under rules that – in stronger forms – have already been studied in the context of Heyting arithmetic. In a similar spirit, we briefly survey modified realizability of CZFω‐ and its hybrids. Central results of this paper have been proved by Burr 2000a and Schulte 2006, however, for different translations. We use a simplified interpretation that goes back to Diller and Nahm 1974. A novel element is a lemma on absorption of bounds which is essential for the smooth operation of our translation. (shrink)

of type theory has been used successfully to formalize large parts of constructive mathematics, such as the theory of generalized recursive definitions [NPS90, ML79]. Moreover, it is also employed extensively as a framework for the development of high-level programming languages, in virtue of its combination of expressive strength and desirable proof-theoretic properties [NPS90, Str91]. In addition to simple types A, B, . . . and their terms x : A b(x) : B, the theory also (...) has dependent types x : A B(x), which are regarded as indexed families of types. There are simple type forming operations A × B and A → B, as well as operations on dependent types, including in particular the sum x:A B(x) and product x:A B(x) types (see the appendix for details). The Curry-Howard interpretation of the operations A × B and A → B is as propositional conjunction and.. (shrink)

Gödel's dialectica interpretation of Heyting arithmetic HA may be seen as expressing a lack of confidence in our understanding of unbounded quantification. Instead of formally proving an implication with an existential consequent or with a universal antecedent, the dialectica interpretation asks, under suitable conditions, for explicit 'interpreting' instances that make the implication valid. For proofs in constructive set theory CZF-, it may not always be possible to find just one such instance, but it must suffice to explicitly name (...) a set consisting of such interpreting instances. The aim of eliminating unbounded quantification in favor of appropriate constructive functionals will still be obtained, as our ∧-interpretation theorem for constructive set theory in all finite types CZFω- shows. By changing to a hybrid interpretation ∧q, we show closure of CZFω- under rules that – in stronger forms – have already been studied in the context of Heyting arithmetic. In a similar spirit, we briefly survey modified realizability of CZFω- and its hybrids. Central results of this paper have been proved by Burr 2000a and Schulte 2006, however, for different translations. We use a simplified interpretation that goes back to Diller and Nahm 1974. A novel element is a lemma on absorption of bounds which is essential for the smooth operation of our translation. (shrink)

Type theory is a fast-evolving field at the crossroads of logic, computer science and mathematics. This gentle step-by-step introduction is ideal for graduate students and researchers who need to understand the ins and outs of the mathematical machinery, the role of logical rules therein, the essential contribution of definitions and the decisive nature of well-structured proofs. The authors begin with untyped lambda calculus and proceed to several fundamental type systems culminating in the well-known and powerful Calculus of (...) Constructions. The book also covers the essence of proof checking and proof development, and the use of dependent type theory to formalize mathematics. The only prerequisites are a good knowledge of undergraduate algebra and analysis. Carefully chosen examples illustrate the theory throughout. Each chapter ends with a summary of the content, some historical context, suggestions for further reading and a selection of exercises to help readers familiarize themselves with the material. (shrink)

The analysis of atomic sentences and their subatomic components poses a special problem for proof-theoretic approaches to natural language semantics, as it is far from clear how their semantics could be explained by means of proofs rather than denotations. The paper develops a proof-theoretic semantics for a fragment of English within a type-theoretical formalism that combines subatomic systems for natural deduction [20] with constructive (or Martin-Löf) type theory [8, 9] by stating rules for the formation, introduction, (...) elimination and equality of atomic propositions understood as types (or sets) of subatomic proof-objects. The formalism is extended with dependent types to admit an interpretation of non-atomic sentences. The paper concludes with applications to natural language including internally nested proper names, anaphoric pronouns, simple identity sentences, and intensional transitive verbs. (shrink)

Selection type theories solve adaptation problems. Natural selection, clonal selection for antibody production, and selective theories of higher brain function are examples. An abstract characterization of typical selection processes is generated by analyzing and extending previous work on the nature of natural selection. Once constructed, this abstraction provides a useful tool for analyzing the nature of other selection theories and may be of use in new instances of theory construction. This suggests the potential fruitfulness of research to find (...) other theory types and construct their abstractions. (shrink)

I discuss problems with Martin-Löf's distinction between analytic and synthetic judgments in constructive type theory and propose a revision of his views. I maintain that a judgment is analytic when its correctness follows exclusively from the evaluation of the expressions occurring in it. I argue that Martin-Löf's claim that all judgments of the forms a : A and a = b : A are analytic is unfounded. As I shall show, when A evaluates to a dependent function (...) type (x : B) → C, all judgments of these forms fail to be analytic and therefore end up as synthetic. Going beyond the scope of Martin-Löf's original distinction, I also argue that all hypothetical judgments are synthetic and show how the analytic-synthetic distinction reworked here is capable of accommodating judgments of the forms A type and A = B type as well. Finally, I consider and reject an alternative account of analyticity as decidability and assess Martin-Löf's position on the analytic grounding of synthetic judgments. (shrink)

In this article we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. (...) One may regard the results of this article as an alternative solution to the problem of the proliferation of levels of real numbers in Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here also suggests that there is a natural associated notion of predicative elementary topos. (shrink)

Analysability of finiteU-rank types are explored both in general and in the theory${\rm{DC}}{{\rm{F}}_0}$. The well-known fact that the equation$\delta \left = 0$is analysable in but not almost internal to the constants is generalized to show that$\underbrace {{\rm{log}}\,\delta \cdots {\rm{log}}\,\delta }_nx = 0$is not analysable in the constants in$\left$-steps. The notion of acanonical analysisis introduced–-namely an analysis that is of minimal length and interalgebraic with every other analysis of that length. Not every analysable type admits a canonical analysis. Using (...) properties of reductions and coreductions in theories with the canonical base property, it is constructed, for any sequence of positive integers$\left$, a type in${\rm{DC}}{{\rm{F}}_0}$that admits a canonical analysis with the property that theith step hasU-rank${n_i}$. (shrink)

We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.

Contextual type theories are largely explored in their applications to programming languages, but less investigated for knowledge representation purposes. The combination of a constructive language with a modal extension of contexts appears crucial to explore the attractive idea of a type-theoretical calculus of provability from refutable assumptions for non-monotonic reasoning. This paper introduces such a language: the modal operators are meant to internalize two different modes of correctness, respectively with necessity as the standard notion of constructive (...) verification and possibility as provability up to refutation of contextual conditions. (shrink)

This article proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the homotopy type theory book for dependent type theory augmented with axioms for univalence and higher inductive types. We adopt a cartesian cubical type theory proposed by Angiuli, Brunerie, Coquand, Favonia, (...) Harper, and Licata as the implicit foundation, confining our presentation to elementary results such as function extensionality, the derivation of weak connections and path induction, the groupoid structure of types, and the Eckmman–Hilton duality. (shrink)

Homotopy Type Theory is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various questions (...) that a foundation for mathematics might be expected to answer, and find that many of them are not answered by the standard formulation of HoTT as presented in the ‘HoTT Book’. More importantly, the presentation of HoTT given in the HoTT Book is not autonomous since it explicitly depends upon other fields of mathematics, in particular homotopy theory. We give an alternative presentation of HoTT that does not depend upon ideas from other parts of mathematics, and in particular makes no reference to homotopy theory, and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on a new interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory. 1 Introduction2 What Is a Foundation for Mathematics?2.1 A characterization of a foundation for mathematics2.2 Autonomy3 The Basic Features of Homotopy Type Theory3.1 The rules3.2 The basic ways to construct types3.3 Types as propositions and propositions as types3.4 Identity3.5 The homotopy interpretation4 Autonomy of the Standard Presentation?5 The Interpretation of Tokens and Types5.1 Tokens as mathematical objects?5.2 Tokens and types as concepts6 Justifying the Elimination Rule for Identity7 The Foundations of Homotopy Type Theory without Homotopy7.1 Framework7.2 Semantics7.3 Metaphysics7.4 Epistemology7.5 Methodology8 Possible Objections to this Account8.1 A constructive foundation for mathematics?8.2 What are concepts?8.3 Isn’t this just Brouwerian intuitionism?8.4 Duplicated objects8.5 Intensionality and substitution salva veritate9 Conclusion9.1 Advantages of this foundation. (shrink)

The constructive reformulation of the semantic theory suggests two basic principles to be assumed: first, the distinction between proper knowledge, expressed in judgemental form, and the assertion conditions for such knowledge; second, ...

This paper describes an axiomatic theory BT, which is a suitable formal theory for developing constructive mathematics, due to its expressive language with countable number of set types and its constructive properties such as the existence and disjunction properties, and consistency with the formal Church thesis. BT has a predicative comprehension axiom and usual combinatorial operations. BT has intuitionistic logic and is consistent with classical logic. BT is mutually interpretable with a so called theory of (...) arithmetical truth PATr and with a second-order arithmetic SA that contains infinitely many sorts of sets of natural numbers. We compare BT with some standard second-order arithmetics and investigate the proof-theoretical strengths of fragments of BT, PATr and SA. (shrink)

Homotopy Type Theory (HoTT) is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various (...) questions that a foundation for mathematics might be expected to answer, and find that many of them are not answered by the standard formulation of HoTT as presented in the ‘HoTT Book’. More importantly, the presentation of HoTT given in the HoTT Book is not autonomous since it explicitly depends upon other fields of mathematics, in particular homotopy theory. We give an alternative presentation of HoTT that does not depend upon ideas from other parts of mathematics, and in particular makes no reference to homotopy theory (but is compatible with the homotopy interpretation), and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on a new interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory. 1 Introduction2 What Is a Foundation for Mathematics? 2.1 A characterization of a foundation for mathematics 2.2 Autonomy3 The Basic Features of Homotopy Type Theory 3.1 The rules 3.2 The basic ways to construct types 3.3 Types as propositions and propositions as types 3.4 Identity 3.5 The homotopy interpretation4 Autonomy of the Standard Presentation?5 The Interpretation of Tokens and Types 5.1 Tokens as mathematical objects? 5.2 Tokens and types as concepts6 Justifying the Elimination Rule for Identity7 The Foundations of Homotopy Type Theory without Homotopy 7.1 Framework 7.2 Semantics 7.3 Metaphysics 7.4 Epistemology 7.5 Methodology8 Possible Objections to this Account 8.1 A constructive foundation for mathematics? 8.2 What are concepts? 8.3 Isn’t this just Brouwerian intuitionism? 8.4 Duplicated objects 8.5 Intensionality and substitution salva veritate9 Conclusion 9.1 Advantages of this foundation. (shrink)

A logic-enriched type theory is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named and , which we claim correspond closely to the classical predicative systems of second order arithmetic and . We justify this claim by translating each second order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used (...) to formalise different approaches to the foundations of mathematics.The two LTTs we construct are subsystems of the logic-enriched type theory , which is intended to formalise the classical predicative foundation presented by Herman Weyl in his monograph Das Kontinuum. The system has also been claimed to correspond to Weyl’s foundation. By casting and as LTTs, we are able to compare them with . It is a consequence of the work in this paper that is strictly stronger than .The conservativity proof makes use of a novel technique for proving one LTT conservative over another, involving defining an interpretation of the stronger system out of the expressions of the weaker. This technique should be applicable in a wide variety of different cases outside the present work. (shrink)

A version of intuitionistic type theory is presented here in which all logical symbols are defined in terms of equality. This language is used to construct the so-called free topos with natural number object. It is argued that the free topos may be regarded as the universe of mathematics from an intuitionist's point of view.

This is the first of two articles dedicated to the notion of constructive set. In them we attempt a comparison between two different notions of set which occur in the context of the foundations for constructive mathematics. We also put them under perspective by stressing analogies and differences with the notion of set as codified in the classical theory Zermelo–Fraenkel. In the current article we illustrate in some detail the notion of set as expressed in Martin–L¨of (...) class='Hi'>type theory and present the essential characters of this theory. In a second article we shall explore a distinct notion of set, as arising in the context of intuitionistic versions of Zermelo–Fraenkel set theory. The theory we shall analyse there is Aczel’s CZF and we shall supplement its exposition by a succinct account of Aczel’s interpretation of CZF in type theory. This will enable us to compare the two notions in a more precise sense. (shrink)

In the formal semantics based on modern type theories, common nouns are interpreted as types, rather than as predicates of entities as in Montague’s semantics. This brings about important advantages in linguistic interpretations but also leads to a limitation of expressive power because there are fewer operations on types as compared with those on predicates. The theory of coercive subtyping adequately extends the modern type theories and, as shown in this paper, plays a very useful role in (...) making type theories more expressive for formal semantics. It not only gives a satisfactory solution to the basic problem of ‘multiple categorisation’ caused by interpreting common nouns as types, but provides a powerful formal framework to model interesting linguistic phenomena such as copredication, whose formal treatment has been found difficult in a Montagovian setting. In particular, we show how to formally introduce dot-types in a type theory with coercive subtyping and study some type-theoretic constructs that provide useful representational tools for reference transfers and multiple word meanings in formal lexical semantics. (shrink)

A version of intuitionistic type theory is extended with opposite types, allowing a different formalization of negation and obtaining a paraconsistent type theory (⁠|$\textsf{PTT} $|⁠). The rules for opposite types in |$\textsf{PTT} $| are based on the rules of the so-called constructible falsity. A propositions-as-types correspondence between the many-sorted paraconsistent logic |$\textsf{PL}_\textsf{S} $| (a many-sorted extension of López-Escobar’s refutability calculus presented in natural deduction format) and |$\textsf{PTT} $| is proven. Moreover, a translation of |$\textsf{PTT} $| into (...) intuitionistic type theory is presented and some properties of |$\textsf{PTT} $| are discussed. (shrink)

Architectural theory arises from building, when the mind considers its symbolic relations to its own constructions. The intent of this essay is to discuss the intellectual causes that precede building and precede theory. It considers certain fundamental dualities in our thinking about architecture—such as image and word; type and model; imitation and invention—and the role they play in its making, its perfection as an art, and the eventual elaboration of its tenets into a theory. At a (...) time when theories of architecture proliferate as expressions of ‘personal philosophies,’ a careful and incisive philosophical approach to if, how, and when does theory become formative of building, may ensure that architecture remain faithful to its intrinsic purposes. (shrink)

In this paper, we show that non-well-founded sets can be defined constructively by formalizing Hallnäs' limit definition of these within Martin-Löf's theory of types. A system is a type W together with an assignment of ᾱ ∈ U and α̃ ∈ ᾱ → W to each α ∈ W. We show that for any system W we can define an equivalence relation = w such that α = w β ∈ U and = w is the maximal bisimulation. (...) Aczel's proof that CZF can be interpreted in the type V of iterative sets shows that if the system W satisfies an additional condition (*), then we can interpret CZF minus the set induction scheme in W. W is then extended to a complete system W * by taking limits of approximation chains. We show that in W * the antifoundation axiom AFA holds as well as the axioms of CFZ -. (shrink)

The aim of this paper is to define a partial Propositional Type Theory. Our system is partial in a double sense: the hierarchy of (propositional) types contains partial functions and some expressions of the language, including formulas, may be undefined. The specific interpretation we give to the undefined value is that of Kleene’s strong logic of indeterminacy. We present a semantics for the new system and prove that every element of any domain of the hierarchy has a name (...) in the object language. Finally, we provide a proof system and a (constructive) proof of completeness. (shrink)

Pure type systems arise as a generalisation of simply typed lambda calculus. The contemporary development of mathematics has renewed the interest in type theories, as they are not just the object of mere historical research, but have an active role in the development of computational science and core mathematics. It is worth exploring some of them in depth, particularly predicative Martin-Löf’s intuitionistic type theory and impredicative Coquand’s calculus of constructions. The logical and philosophical differences and similarities (...) between them will be studied, showing the relationship between these type theories and other fields of logic. (shrink)

This thesis presents a proof theoretical investigation of some constructive set theories with restricted set induction. The set theories considered are various systems of Constructive Zermelo Fraenkel set theory, CZF ([1]), in which the schema of $\in$ - Induction is either removed or weakened. We shall examine the theories $CZF^\Sigma_\omega$ and $CZF_\omega$, in which the $\in$ - Induction scheme is replaced by a scheme of induction on the natural numbers (only for  formulas in the case of (...) the first theory, for arbitrary formulas in the second theory). Of particular interest is the system CZF− + INAC, which is obtained by removing $\in$ - Induction and by adding an axiom, INAC, for inaccessible sets. The main outcome is that CZF− + INAC is a predicative set theory with inaccessible sets, its proof theoretic ordinal being $\Gamma_0$. The proof theoretic strength of these theories, has been determined by means of proof theoretical reductions. The upper bounds have been obtained by interpreting the set theories in classical theories of (iterated) inductive definitions with ordinals. A significant feature of these interpretations is that they are realizability interpretations, which make an indirect use of Aczel’s interpretation of CZF in Martin Löf type theory, and, in the case of CZF− + INAC, also employ a maximum bisimulation relation to represent equality between sets. The lower bounds are obtained by interpreting appropriate subsystems of intuitionistic second order arithmetic in the set theories. At the conclusion of the thesis we present work unrelated to the previous chapters. It is a preliminary study of the constructible hierarchy in CZF. We begin by formalizing the notion of definability in constructive set theory and then introduce Gödel’s L in CZF. We prove that intuitionistic L is a model of a subsystem of CZF strong enough to include intuitionistic Kripke-Platek set theory, and also that L is a model of the axiom of constructibility, provably in CZF. (shrink)

Among the most interesting features of Homotopy Type Theory is the way it treats identity, which has various unusual characteristics. We examine the formal features of “identity types” in HoTT, and how they relate to its other features including intensionality, constructive logic, the interpretation of types as concepts, and the Univalence Axiom. The unusual behaviour of identity types might suggest that they be reinterpreted as representing indiscernibility. We explore this by defining indiscernibility in HoTT and examine its (...) relationship with identity. We argue that identity types are a primitive component of HoTT and cannot be reduced to indiscernibility. (shrink)

The proofs of universally quantified statements, in mathematics, are given as “schemata” or as “prototypes” which may be applied to each specific instance of the quantified variable. Type Theory allows to turn into a rigorous notion this informal intuition described by many, including Herbrand. In this constructive approach where propositions are types, proofs are viewed as terms of λ-calculus and act as “proof-schemata”, as for universally quantified types. We examine here the critical case of Impredicative Type (...) Theory, i. e. Girard's system F, where type-quantification ranges over all types. Coherence and decidability properties are proved for prototype proofs in this impredicative context. (shrink)

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

In his famous paper Der Wahrheitsbegriff in den formalisierten Sprachen (Polish edition: Nakładem/Prace Towarzystwa Naukowego Warszawskiego, wydzial, III, 1933), Alfred Tarski constructs a materially adequate and formally correct definition of the term “true sentence” for certain kinds of formalised languages. In the case of other formalised languages, he shows that such a construction is impossible but that the term “true sentence” can nevertheless be consistently postulated. In the Postscript that Tarski added to a later version of this paper (Studia Philosophica, (...) 1, 1935), he does not explicitly include limits for the kinds of language for which such a construction is possible. This absence of such limits has been interpreted as an implied claim that such a definition of the term “true sentence” can be constructed for every language. This has far-reaching consequences, not least for the widely held belief that Tarski changed from an universalistic to an anti-universalistic standpoint. We will claim that the consequence of anti-universalism is unwarranted, given that it can be argued that the Postscript is not in conflict with the existence of limits outside of which a definition of “true sentence” cannot be constructed. Moreover, by a discussion of transfinite type theory, we will also be able to accommodate other of the changes made in Tarski’s Postscript within a type-theoretical framework. The awareness of transfinite type theory afforded by this discussion will lead, in turn, to an account of Tarski’s Postscript that shows a gradual change in his logical work, rather than any of the more radical transitions which the Postscript has been claimed to reflect. (shrink)