We give a formal interpretation of Martin-Löf's Constructive Theory of Types in Elementary Topos Theory which is presented as a formalised theory with intensional equality of objects. Types are interpreted as arrows and variables as sections of their types. This is necessary to model correctly the working of the assumption x ∈ A. Then intensional equality interprets equality of types. The normal form theorem which asserts that the interpretation of a type is (...) intensional equal to the pullback of its “alignment” along some “base” arrow relates this interpretation to categorical semantic of types. (shrink)

We introduce a certain extension of -calculus, and show that it has the Church-Rosser property. The associated open-term extensional combinatory algebra is used as a basis to construct models for theories of Explict Mathematics (formulated in the language of "types and names") with positive stratified comprehension. In such models, types are interpreted as collections of solutions (of terms) w.r. to a set of numerals. Exploiting extensionality, we prove some consistency results for special ontological axioms which are refutable under (...) elementary comprehension. (shrink)

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 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 this paper we examine two approaches to the formal treatment of the notion of problem in the paradigm of algorithmic semantics. Namely, we will explore an approach based on Martin-Löf’s Constructive Type Theory, which can be seen as a direct continuation of Kolmogorov’s original calculus of problems, and an approach utilizing Tichý’s Transparent Intensional Logic, which can be viewed as a non-constructive attempt of interpreting Kolmogorov’s logic of problems. In the last section we propose Kolmogorov and (...) CTT-inspired modifications to TIL-based approach. The focus will be on non-empirical problems only. (shrink)

This paper presents several independence results concerning the topos-valid and the intuitionistic predicative theory of locales. In particular, certain consequences of the consistency of a general form of Troelstra's uniformity principle with constructive set theory and type theory are examined.

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)

In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects. Because of these intended applications, we deal with categories that lack equalisers and just have weak ones, but whose objects can be regarded as collections of global elements. In this (...) context, we study the internal logic of the categories involved, and employ this analysis to give a sufficient condition for the local cartesian closure of an exact completion. Finally, we apply this result to show when an exact completion produces a model of CETCS. (shrink)

J. N. Crossley [1] raised the question of whether the implication 2 + A = A ⇒ 1 + A = A is true for constructive order types (C.O.T.'s). Using an earlier definition of constructive order type, A. G. Hamilton [2] presented a counterexample. Hamilton left open the general question, however, since he pointed out that Crossley considers only orderings which can be embedded in a standard dense r.e. ordering by a partial recursive function, and that his (...) counterexample fails to meet this requirement. We resolve the question by finding a C.O.T. A which meets Crossley's requirement and such that 2 + A = A but 1 + A ≠ A. At the suggestion of A. B. Manaster and A. G. Hamilton we easily extend this construction to show that for any n ≧ 2, there is a C.O.T. A such that n + A = A but m + A ≠ A for 0 < m < n. Hence, Theorem 3 of [2] and all of its corollaries hold with the new definition of C.O.T. The construction is not difficult and requires no priority argument. The techniques are similar to those developed in [3], but no outside results are needed here. (shrink)

In this article I try to show the philosophical continuity of Russell's ideas from his paradox of classes to Principia mathematica. With this purpose, I display the main results (descriptions, substitutions and types) as moments of the same development, whose principal goal was (as in his The principles) to look for a set of primitive ideas and propositions giving an account of all mathematics in logical terms, but now avoiding paradoxes. The sole way to reconstruct this central period in (...) Russell is to resort to unpublished manuscripts, which show the publications of these years to be the extremities of one same iceberg. Thus the logical problems (doubts about propositions, matrices and functions) are parallel to the ontological (the searching for genuine logical subjects) and methodological ones (the status of eliminative reduction). Paradoxes were the cause that the kind of (constructive) definition already applied by Russell, as an inheritance of Moorean analysis, obtained a new trait: ontological elimination, which, beginning with a ?no classes theory? and the theory of descriptions, led to a new theory of judgment (already present in manuscripts from 1906), ?incomplete symbols, and logical constructions. (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)

One of the central problems arising from just the descriptive aspect of Kuhn's theory of scientific development by revolutions concerns the problem of generality. Is Kuhn's theory general enough to encompass the development of all the sciences, including both the natural sciences and the social sciences? The answer to this question is no. It is argued that this negative answer is due not to the nature of the sciences themselves but to the nature of Kuhn's theory and, (...) in particular, its local and reductionistic perspective. First steps toward the construction of a more global and more pluralistic descriptive theory of scientific development are taken. The development of significant episodes in the history of sciences other than physics and chemistry are considered. The immediate goals are to correct the narrow base from which Kuhn starts, to show how some of his basic ideas might be preserved, and to indicate how a theory of types would proceed. (shrink)

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)

We shall present two novel ways of deriving simply typed combinatory models. These are of interest in a constructive setting. First we look at extension models, which are certain subalgebras of full function space models. Then we shall show how the space of singletons of a combinatory model can itself be made into one. The two and the algebras in between will have many common features. We use these two constructions in proving: There is a model of constructive (...) set theory in which every closed extensional theory of simple typed combinatory logic is the theory of a full function space model. (shrink)

We continue the study of the theories of Baldwin–Shi hypergraphs from [5]. Restricting our attention to when the rank δ is rational valued, we show that each countable model of the theory of a given Baldwin–Shi hypergraph is isomorphic to a generic structure built from some suitable subclass of the original class used in the construction. We introduce a notion of dimension for a model and show that there is a an elementary chain $\left\{ {\mathfrak{M}_\beta :\beta \leqslant \omega } (...) \right\}$ of countable models of the theory of a fixed Baldwin–Shi hypergraph with $\mathfrak{M}_\beta \preccurlyeq \mathfrak{M}_\gamma $ if and only if the dimension of $\mathfrak{M}_\beta $ is at most the dimension of $\mathfrak{M}_\gamma $ and that each countable model is isomorphic to some $\mathfrak{M}_\beta $. We also study the regular types that appear in these theories and show that the dimension of a model is determined by a particular regular type. Further, drawing on a large body of work, we use these structures to give an example of a pseudofinite, ω-stable theory with a nonlocally modular regular type, answering a question of Pillay in [11]. (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)

Alfred Schutz’s theory of the social world, often neglected in philosophy, has the potential to capture the interplay of identity and difference which shapes our action, interaction, and experience in everyday life. Compared to still dominant identity-based models such as that of Jürgen Habermas, who assumes a coordination of meaning built on the idealisation of stable rules, Schutz’s theory is an important step forward. However, his central notion of a “type” runs into a difficulty which requires constructive (...) criticism. Against the background of Schutz’s theory of meaning inspired by Bergson and Husserl, his idea of types “taken for granted until further notice” is shown to express a primacy of identity which, in the final analysis, leads into the implausible scenario of ‘ubiquitous tunnel vision’. This makes it necessary to go beyond Schutz and assume an inherently motivated tendency towards difference in meaning termed ‘spontaneity’. Where spontaneity and the opposed tendency towards identity of meaning work together in the application of types, they enable embodied subjects to interact with the world and with each other in the routine yet flexible and sometimes innovative ways which we all know. (shrink)

We give two slight generalizations of results of Poizat about elementary theories of groups obtained by free constructions. The first-one concerns generic types and the non-superstability of such groups in many cases. The second-one concerns the connectedness of most free products of groups without amalgamation.

In this paper I draw on Einstein's distinction between “principle” and “constructive” theories to isolate two levels of physical theory that can be found in both classical and (special) relativistic physics. I then argue that when we focus on theoretical explanations in physics, i.e. explanations of physical laws, the two leading views on explanation, Salmon's “bottom-up” view and Kitcher's “top-down” view, accurately describe theoretical explanations for a given level of theory. I arrive at this conclusion through an (...) analysis of explanations of mass—energy equivalence in special relativity. (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)

We introduce a new model construction for Martin-Löf intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines, by gluing along the functor from the category of contexts to the category of groupoids, the syntactic model with a notion of realizability. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it has the (...) same homotopy type as the free groupoid generated by G. (shrink)

We present a formal theory of propositions and combinator terms, and in this theory we give an interpretation of Martin-Löf's type theory. The construction of the interpretation is inspired by the semantics for type theory, but it can also be viewed as a formalized realizability interpretation.

In constructive mathematics it is of interest to consider a more general, but classically equivalent, notion of linear order, a so-called pseudo-order. The prime example is the order of the constructive real numbers. We examine two kinds of constructive completions of pseudo-orders: order completions of pseudo-orders and Cauchy completions of ordered groups and fields. It is shown how these can be predicatively defined in type theory, also when the underlying set is non-discrete. Provable choice principles, in (...) particular a generalisation of dependent choice, are used for showing set-representability of cuts. (shrink)

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.

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)

In this article, a new, idealizing-hermeneutic methodological approach to developing a theory of philosophical arguments is presented and carried out. The basis for this is a theory of ideal philosophical theory types developed from the analysis of historical examples. According to this theory, the following ideal types of theory exist in philosophy: 1. descriptive-nomological, 2. idealizing-hermeneutic, 3. technical-constructive, 4. ontic-practical. These types of theories are characterized in particular by what their basic (...) types of theses are. The main task of this article is then to determine the types of arguments that are suitable for justifying these types of theses. Surprisingly, practical arguments play a key role here. (shrink)

The Lovász local lemma (LLL) is a technique from combinatorics for proving existential results. There are many different versions of the LLL. One of them, the lefthanded local lemma, is particularly well suited for applications to two player games. There are also constructive and computable versions of the LLL. The chief object of this thesis is to prove an effective version of the lefthanded local lemma and to apply it to effectivise constructions of non-repetitive sequences.The second goal of this (...) thesis is to categorize some classes of cohesive powers. We completely describe both the isomorphism types of cohesive powers of equivalence structures and injection structures, as well as clarify the relationship between these cohesive powers and their original structures. We also describe the finite condensation of cohesive powers of computable copies of the integers as a linear order by cohesive sets whose complement are computably enumerable.Finally, we investigate the possibility of decomposing problems in the Weihrauch degrees into a product of first order part and second order part. We give a preliminary result in this direction.Abstract prepared by Daniel Mourad.E-mail: [email protected]: https://daniel-mourad.scholar.uconn.edu/wp-content/uploads/sites/2530/2023/06/ThesisFinalWithRevisio ns-2.pdf. (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.

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)

This article explores the implicit theories of morality, or the conceptions regarding the patterns of stability, continuity and change in moral dispositions, both in lay and academic discourses. The controversies surrounding these conceptions and the fragmentation of the models and perspectives in metaethics and moral psychology endangers the pursuit of adequate operationalizations of morally relevant constructs. The current debate between situationists, who deny that character is an useful concept for understanding human behavior, which is better explained by contextual factors (Doris (...) 1998; Harman 1998) and dispositionists, who advocate the cross-situational stability of traits, is also present in the lay discourse, through the existence of competing commonsense ontological assumptions regarding the mutability or alterability of moral features, namely the implicit theories perspective (Chiu, Dweck, Tong, & Fu 1997). These personal theories are primary suspects in the affective and cognitive reactions to transgressions: the type of attended information in formulating evaluative judgments, the calibration of moral responsibility and blameworthiness, the assignment of retribution or reparatory recommendations to transgressors. In the second part of the study we attempt to advance toward a more fine-grained inspection of these lay beliefs, arguing that the construct of implicit theories of morality, as it is currently treated and measured, tends to be restrictive and oversimplifying. (shrink)

This book offers a powerful, comprehensive and compelling rereading of Hobbes's theory of representation, by reinstating it in a wider pattern of Hobbes’s theorizing about human thought and action in relation to images, roles and fictions of various types.

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)

In this paper, we will examine the role that intuitions and responses to thought experiments play in confirming or disconfirming theories of reference, using insights from both debates as our starting point. Our view is that experimental evidence of the type elicited by MMNS does play a central role in the construction of theories of reference. This, however, is not because such theory construction is accurately characterized by "the method of cases." First, experimental philosophy does not directly collect data (...) about intuitions, but rather about peoples responses to thought experiments, which may reflect their intuitions but may well not. Second, unusually in the case of the theory of reference, experimental prompts involve elicitation of the phenomenon under investigation—that is, referring—and it is the reference facts rather than the intuitions that a theory of reference should capture. Finally, "best fit" models like the method of cases are inconsistent with the actual practice of semantic theorists, who appeal to general principles of theory construction as well as considerations native to the theory of reference, often in the service of rejecting intuitions. Indeed, Kripke himself viewed several claims of his theory as unintuitive, but felt no pressure to alter them on that account. These facts, we'll argue, suggest that the relevance of experimental methods in the theory of reference cannot be straightforwardly extended to other fields: an experimental prompt containing Newtons two rocks tied together in empty space may elicit referring, and may also elicit intuitions, but it doesn't also elicit the phenomenon under investigation. Furthermore, the considerations native to the theory of reference are not part of physics, which has its own distinct set of principles and considerations. This suggests that an evaluation of the centrality of intuitions/ responses to thought experiments in philosophical methodology must proceed in a piecemeal fashion. We conclude that the potential contributions of experimental philosophy will take different forms in different sub-fields of philosophical inquiry. (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)

The central problem in the quantum theory of measurement, how to describe the process of state reduction in terms of the quantum mechanical formalism, is solved on the basis of the relativity of quantal states, which implies that once the apparatus is detected in a well-defined state, the object state must reduce to a corresponding one. This is a process termed by Schrödinger disentanglement. Here, it is essential to observe that Renninger's negative result does constitute an actual measurement process. (...) From this point of view, Heisenberg's interpretation of his microscope experiment and the Einstein-Podolsky-Rosen arguments are reinvestigated. Satisfactory discussions are given to various experimental situations, such as the Stern-Gerlach-type experiment, successive measurements, macroscopic measurements, and Schrödinger's cat. Finally it is proposed to regard a state vector in quantum mechanics as an irreducible physical construct, in Margenau's sense, that is not further analyzable both mathematically and conceptually. (shrink)

The “Slicing Problem” is a thought experiment that raises questions for substrate-neutral computational theories of consciousness, including those that specify a certain causal structure for the computation like Integrated Information Theory. The thought experiment uses water-based logic gates to construct a computer in a way that permits cleanly slicing each gate and connection in half, creating two identical computers each instantiating the same computation. The slicing can be reversed and repeated via an on/off switch, without changing the amount of (...) matter in the system. The question is what do different computational theories of consciousness believe is happening to the number and nature of individual conscious units as this switch is toggled. Under a token interpretation, there are now two discrete conscious entities; under a type interpretation, there may remain only one. Both interpretations lead to different implications depending on the adopted theoretical stance. Any route taken either allows mechanisms for “consciousness-multiplying exploits” or requires ambiguous boundaries between conscious entities, raising philosophical and ethical questions for theorists to consider. We discuss resolutions under different theories of consciousness for those unwilling to accept consciousness-multiplying exploits. In particular, we specify three features that may help promising physicalist theories to navigate such thought experiments. (shrink)

The nature of self has been discussed for centuries, with myriad theories specifying propositions of the form ‘The self is X’. Recently, psychology and neuroscience have added further such propositions and have sought to specify neural correlates for X. In this thesis, theories leading to all such propositions are subjected to methodological criticism. Specifically targeted are those theories that construct metaphysical, essentialist propositions on the nature of the self, and all other abstract concepts, more generally. On this point, it is (...) concluded that theories of this type would benefit from taking into account the nature of language and the role it plays in the development of a theory. Theories that fail to consider language, run the risk of producing theoretical work affected by linguistic biases, those inherent to the language faculty. In this thesis, the biases of interest are referred to as ‘noun phrase reification’ and ‘clausal reification’, and an awareness of these is important for they can subvert the meanings of propositions, rendering them, and the theories built upon them, true by definition. In consideration of this methodological critique, a new theoretical approach to the self and to other abstract concepts is argued for. This new way of theorising combines aspects of basic scientific methodology with statistical modelling and linguistic theory, in which, the triangulation between two or more people, engaged in the act of naming objects and behaviours plays a formative role. Building on this new method in the context of the self, two experiments are performed using the electroencephalography neuroimaging technique; first in neurotypical adults, then in patients with a diagnosis of schizophrenia, a disorder commonly associated with an attenuated selfhood. It is hoped that this body of theoretical and empirical work will facilitate and catalyse progress on abstract concepts and their associated problems. (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.

ABSTRACT Theories of sets such as Zermelo Fraenkel set theory are usually presented as the combination of two distinct kinds of principles: logical and set-theoretic principles. The set-theoretic principles are imposed ‘on top’ of first-order logic. This is in agreement with a traditional view of logic as universally applicable and topic neutral. Such a view of logic has been rejected by the intuitionists, on the ground that quantification over infinite domains requires the use of intuitionistic rather than classical logic. (...) In the following, I consider constructive set theories, which use intuitionistic rather than classical logic, and argue that they manifest a distinctive interdependence or an entanglement between sets and logic. In fact, Martin-Löf type theory identifies fundamental logical and set-theoretic notions. Remarkably, one of the motivations for this identification is the thought that classical quantification over infinite domains is problematic, while intuitionistic quantification is not. The approach to quantification adopted in Martin-Löf’s type theory is subtly interconnected with its predicativity. I conclude by recalling key aspects of an approach to predicativity inspired by Poincaré, which focuses on the issue of correct quantification over infinite domains and relate it back to Martin-Löf type theory. (shrink)