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)

Church’s type theory, aka simple type theory, is a formal logical language which includes classical first-order and propositional logic, but is more expressive in a practical sense. It is used, with some modifications and enhancements, in most modern applications of type theory. It is particularly well suited to the formalization of mathematics and other disciplines and to specifying and verifying hardware and software. It also plays an important role in the study of the formal (...) semantics of natural language. When utilizing it as a meta-logic to semantically embed expressive non-classical logics further topical applications are enabled in artificial intelligence and philosophy. A great wealth of technical knowledge can be expressed very naturally in it. With possible enhancements, Church’s type theory constitutes an excellent formal language for representing the knowledge in automated information systems, sophisticated automated reasoning systems, systems for verifying the correctness of mathematical proofs, and a range of projects involving logic and artificial intelligence. Some examples and further references are given in Sections 1.2.2 and 5 below. Type theories are also called higher-order logics, since they allow quantification not only over individual variables, but also over function, predicate, and even higher order variables. Type theories characteristically assign types to entities, distinguishing, for example, between numbers, sets of numbers, functions from numbers to sets of numbers, and sets of such functions. As illustrated in Section 1.2.2 below, these distinctions allow one to discuss the conceptually rich world of sets and functions without encountering the paradoxes of naive set theory. Church’s type theory is a formulation of type theory that was introduced by Alonzo Church in Church 1940. In certain respects, it is simpler and more general than the type theory introduced by Bertrand Russell in Russell 1908 and Whitehead & Russell 1927a. Since properties and relations can be regarded as functions from entities to truth values, the concept of a function is taken as primitive in Church’s type theory, and the λ-notation which Church introduced in Church 1932 and Church 1941 is incorporated into the formal language. Moreover, quantifiers and description operators are introduced in a way so that additional binding mechanisms can be avoided, λ-notation is reused instead. λ-notation is thus the only binding mechanism employed in Church’s type theory. (shrink)

Instead of the half-century old foundational feud between set theory and category theory, this paper argues that they are theories about two different complementary types of universals. The set-theoretic antinomies forced naïve set theory to be reformulated using some iterative notion of a set so that a set would always have higher type or rank than its members. Then the universal u_{F}={x|F(x)} for a property F() could never be self-predicative in the sense of u_{F}∈u_{F}. But the (...) mathematical theory of categories, dating from the mid-twentieth century, includes a theory of always-self-predicative universals--which can be seen as forming the "other bookend" to the never-self-predicative universals of set theory. The self-predicative universals of category theory show that the problem in the antinomies was not self-predication per se, but negated self-predication. They also provide a model (in the Platonic Heaven of mathematics) for the self-predicative strand of Plato's Theory of Forms as well as for the idea of a "concrete universal" in Hegel and similar ideas of paradigmatic exemplars in ordinary thought. (shrink)

Colours appear to instantiate a number of structural properties: for instance, they stand in distinctive relations of similarity and difference, and admit of a fundamental distinction into unique and binary. Accounting for these structural properties is often taken to present a serious problem for physicalist theories of colour. This paper argues that a prominent attempt by Byrne and Hilbert to account for the structural properties of the colours, consistent with the claim that colours are types of surface spectral reflectance, is (...) unsuccessful. Instead, it is suggested that a better account of the structural properties of the colours is provided by a form of non-reductive physicalism about colour: a naïve realist theory of colour, according to which colours are superficial mind-independent properties. (shrink)

The Internalization Hypothesis (I.H.), as expressed in GM II 16 of On the Genealogy of Morals, is the essential albeit under-theorized principle of Nietzsche’s psychology. In the following essay, I investigate the purpose I.H. serves concerning Nietzsche’s theory of drives as well as the Hypothesis’s epistemic warrant. I demonstrate that I.H. needs a Neo-Darwinian underpinning for two reasons: 1) to answer the Time-Crunch Problem of Transformation, and 2) in order to render it coherent with Nietzsche’s physiological determinism as articulated (...) in Twilight of the Idols. My re-examination of I.H., then, serves to underwrite the Hypothesis on solid empirical footing. In addition, my analysis provides further evidence to think that Brian Leiter’s initial (but naïve) type-fact reading of Nietzsche’s philosophy of psychology is accurate, deterministic warts and all. (shrink)

This study investigates how dispute-mediators handle impasse in the re-negotiation of divorce decrees by divorced couples. Three sources of impasse and three strategies for handling impasse are identified based on analysis of mediation transcripts. The concern here lies not so much in the disputant's arguments but in the discussion procedures dispute-mediators use to craft the disputant's argumentation into a tool to solve conflict. Their moves are understood here as a practice of reconstructing argumentative discourse that is neither naïve nor critical (...) but reconstruction as design. Mediator's reconstruction reveals a type of communication work in contemporary societies involved in the crafting of forums and formats that mediate argumentative communication. This work is often invisible and strategic which makes its interpretation, judgment, and development a challenge for pragma-dialectical theory. How reconstruction as design can be understood is discussed by building on prior pragma-dialectical theory and research. (shrink)

Colours appear to instantiate a number of structural properties: for instance, they stand in distinctive relations of similarity and difference, and admit of a fundamental distinction into unique and binary. Accounting for these structural properties is often taken to present a serious problem for physicalist theories of colour. This paper argues that a prominent attempt by Byrne and Hilbert to account for the structural properties of the colours, consistent with the claim that colours are types of surface spectral reflectance, is (...) unsuccessful. Instead, it is suggested that a better account of the structural properties of the colours is provided by a form of non-reductive physicalism about colour: a naïve realist theory of colour, according to which colours are superficial mind-independent properties. (shrink)

This study focuses on a particular type of Naïve Realism known as objectivism, which suggests that the explanation of perceptual phenomenology is based on environmental things that the subject becomes acquainted with. Section 2 introduces a subtype of objectivism, “selectivism”, which aims to overcome a traditional kind of objection. However, this section highlights that the cases these objections invoke may still posit challenges (demands for explanations) to selectivism. Section 3 discusses a recent objection to objectivism and demonstrates how it (...) can be addressed by selectivism so becomes only a challenge of this kind. However, it is important to note that, despite not providing positive refutations, these challenges are still significant. Sections 4 and 5 present the main contribution of this study, as they provide novel arguments that conclusively refute objectivism. Section 4 presents an argument that shows the falsity of objectivism as it has been presented in the literature. Nevertheless, a modified version of objectivism is proposed that could address it, although it still faces some non-definitive challenges. This reformulated theory is a novel type within the realm of Naïve Realism as a whole, as it posits that perceptions involve acquaintance with facts relative to sense organs. In contrast, Section 5 proposes an argument that positively refutes objectivism, which cannot be salvaged by any modification. Section 6 raises objections to an alternative option of Naïve Realism and, also based on the issues raised earlier in the article regarding objectivism, concludes that Naïve Realism must be subjectivist. (shrink)

We propose a solution concept for games that are played among players with present-biased preferences that are possibly naive about their own, or about their opponent’s future time inconsistency. Our perception-perfect outcome essentially requires each player to take an action consistent with the subgame perfect equilibrium, given her perceptions concerning future types, and under the assumption that other present and future players have the same perceptions. Applications include a common pool problem and Rubinstein bargaining. When players are naive (...) about their own time inconsistency and sophisticated about their opponent’s, the common pool problem is exacerbated, and Rubinstein bargaining breaks down completely. (shrink)

Alexius Meinong's Gegenstandstheorie is subject to a formal semantic paradox. The theory of defective objects originally developed by Meinong in response to Ernst Mally's paradox about self-referential thought is rejected as a general solution to paradox in the object theory. The intentionality thesis is also refuted by the counter-example of the unapprehended mountain. It is argued that despite these difficulties, an object theory is required in order to make intuitively correct sense of ontological commitment. ;A version of (...) Meinong's theory is formalized. The logic has non-standard truth value semantics and an objectual interpretation of quantifiers for a domain of existent and non-existent objects. Theories of intentional, referential, and extensional identity are offered, together with two theories of definite description, lambda abstraction, eight systems of alethic modal logic, and formal metatheory. The logic avoids the incompleteness and undecidability limitations of Godel and Church, and all logical, semantic, and set theoretical paradoxes, without type theory or Tarskian hierarchy of metalanguages. It is naively complete and mechanically decidable. ;Wittgenstein's private language argument is refuted as an obstacle to defining private mental objects in the logic. The argument is shown to be valid, but unsound. The object theory logic may therefore provide a mixed or impure private language, and its domain may contain private mental objects as well as ordinary public and non-existent objects. This means that it constitutes an object theory logic of intention, and can be used to represent the logical structure of intentional and specifically phenomenological philosophical theories that require the intelligible designation of private mental objects. ;Appendices include Henkin-type consistency, completeness, and compactness proofs ; criticism of Kazimierz Twardowski's arguments for the distinction between content and object in phenomenological psychology; translation of and commentary on Mally's essay, "Uber die Unabhangigkeit der Gegenstande vom Denken"; a discussion of the distinction between nuclear and extra-nuclear properties, and the eliminability of the modal moment; and a philosophical application of the logic to a solution of the paradox of analysis. (shrink)

The epistemological literature on conspiracy theory has established that strict generalism about conspiracy theories is untenable. This chapter argues, however, that this does not license a move to naive or strict particularism. Rather, any consideration of specific conspiracy claims needs to address conspiracy theory not simply as a formal category of explanation, but as a distinctive social practice, with a history and explanatory repertoire that can give us important, if defeasible, reasons for rejecting at least some such (...) types of claim. These reasons are not merely epistemic. The moral costs of participating in such practices, and of levelling conspiracy accusations in general, generate corresponding ethical requirements for reticence about entertaining conspiracy theories. This doesn’t mean we can retreat to generalism; but it does mean particularism must be governed by a reluctance that, in practice, will rule out a great many conspiracy theory claims as candidates for serious investigation. (shrink)

I formulate the Zermelo-Russell paradox for naive set theory. A sketch is given of Zermelo’s solution to the paradox: the cumulative type structure. A careful analysis of the set formation process shows a missing component in this solution: the necessity of an assumed imaginary jump out of an infinite universe. Thus a set is formed by a suitable combination of concrete and imaginary operations all of which can be made or assumed by a Turing machine. Some consequences (...) are drawn from this improved analysis of the concept of set, for the theory of sets and for the philosophy and foundations of mathematics. (shrink)

The present research examines psychological momentum (PM), a perceived force that lay intuition suggests influences performance. PM theory is proposed to account for how momentum perceptions arise, and four studies demonstrate the influence of lay intuitions about PM on expectations regarding performance outcomes. Study 1 establishes that individuals share intuitions about the types of events that precipitate PM, and Study 2 finds that defeating a rival increases momentum perception. Study 3 provides evidence for the lay belief that as more (...) PM accumulates during a prior task, there should be more residual momentum left to carry over to a subsequent task, and Study 4 finds that an individual whose PM is interrupted is expected to have greater difficulty completing a task than is an individual whose steady progress is interrupted. Discussion focuses on linkages between PM and related constructs. (shrink)

Social categorization is an early emerging and robust component of social cognition, yet the role that social categories play in children's understanding of the social world has remained unclear. The present studies examined children's explanations of social behavior to provide a window into their intuitive theories of how social categories constrain human action. Children systematically referenced category memberships and social relationships as causal-explanatory factors for specific types of social interactions: harm among members of different categories more than harm among members (...) of the same category. In contrast, they systematically referred to agents' mental states to explain the reverse patterns of behaviors: harm among members of the same category more than harm among members of different categories. These data suggest that children view social category memberships as playing a causal-explanatory role in constraining social interactions. (shrink)

We present a novel treatment of set theory in a four-valued paraconsistent and paracomplete logic, i.e., a logic in which propositions can be both true and false, and neither true nor false. Our approach is a significant departure from previous research in paraconsistent set theory, which has almost exclusively been motivated by a desire to avoid Russell’s paradox and fulfil naive comprehension. Instead, we prioritise setting up a system with a clear ontology of non-classical sets, which can (...) be used to reason informally about incomplete and inconsistent phenomena, and is sufficiently similar to ${\mathrm {ZFC}}$ to enable the development of interesting mathematics.We propose an axiomatic system ${\mathrm {BZFC}}$, obtained by analysing the ${\mathrm {ZFC}}$ -axioms and translating them to a four-valued setting in a careful manner, avoiding many of the obstacles encountered by other attempted formalizations. We introduce the anti-classicality axiom postulating the existence of non-classical sets, and prove a surprising results stating that the existence of a single non-classical set is sufficient to produce any other type of non-classical set.Our theory is naturally bi-interpretable with ${\mathrm {ZFC}}$, and provides a philosophically satisfying view in which non-classical sets can be seen as a natural extension of classical ones, in a similar way to the non-well-founded sets of Peter Aczel [1].Finally, we provide an interesting application concerning Tarski semantics, showing that the classical definition of the satisfaction relation yields a logic precisely reflecting the non-classicality in the meta-theory. (shrink)

A splendid introduction to set theory. By leaning heavily on modern logic, Quine develops a substantial amount of set theory axiomatically without either being naive about the antinomies or prejudicing the issue of infinite classes. This development felicitously allows Quine a neutral ground on which, in his concluding chapters, to describe, compare and connect various conflicting full-blooded systems: Russell's theory of types, Zermelo's system, two of Quine's own, and von Neumann's. This treatment of set theory, (...) allowing formalism without sectionalism, is singular and should instruct and delight the theorist as well as the beginning reader.—K. J. (shrink)

Questions about mental phenomena may be questions about the true nature of such phenomena. They may also be questions about the true nature of our everyday conceptions of such phenomena. This last type of questions belong to the study of what is called naïve, or folk, psychology.

The perceptual symbol approach to knowledge representation combines structured frames and dynamic imagery. The perceptual symbol approach provides a good account of the representation of scientific models, of some types of naive theories held by children and adults, and of certain reconstructive memory phenomena. The ontological status of perceptual symbols is unclear and this form of representation does not succeed in accounting for all forms of human knowledge.

This is a general account of metavaluations and their applications, which can be seen as an alternative to standard model-theoretic methodology. They work best for what are called metacomplete logics, which include the contraction-less relevant logics, with possible additions of Conjunctive Syllogism, & →.A→C, and the irrelevant, A→.B→A, these including the logic MC of meaning containment which is arguably a good entailment logic. Indeed, metavaluations focus on the formula-inductive properties of theorems of entailment form A→B, splintering into two types, M1- (...) and M2-, according to key properties of negated entailment theorems. Metavaluations have an inductive presentation and thus have some of the advantages that model theory does, but they represent proof rather than truth and thus represent proof-theoretic properties, such as the priming property, if ├ A $\vee$ B then ├ A or ├ B, and the negated-entailment properties, not-├ ∼ and ├ ∼ iff ├ A and ├ ∼ B. Topics to be covered are their impact on naive set theory and paradox solution, and also Peano arithmetic and Godel’s First and Second Theorems. Interesting to note here is that the familiar M1- and M2-metacomplete logics can be used to solve the set-theoretic paradoxes and, by inference, the Liar Paradox and key semantic paradoxes. For M1-logics, in particular, the final metavaluation that is used to prove the simple consistency is far simpler than its correspondent in the model-theoretic proof in that it consists of a limit point of a single transfinite sequence rather than that of a transfinite sequence of such limit points, as occurs in the model-theoretic approach. Additionally, it can be shown that Peano Arithmetic is simply consistent, using metavaluations that constitute finitary methods. Both of these results use specific metavaluational properties that have no correspondents in standard model theory and thus it would be highly unlikely that such model theory could prove these results in their final forms. (shrink)

Naive set theory, as found in Frege and Russell, is almost universally believed to have been shown to be false by the set-theoretic paradoxes. The standard response has been to rank sets into one or other hierarchy. However it is extremely difficult to characterise the nature of any such hierarchy without falling into antinomies as severe as the set-theoretic paradoxes themselves. Various attempts to surmount this problem are examined and criticised. It is argued that the rejection of (...) class='Hi'>naive set theory inevitably leads one into a severe scepticism with regard to the feasibility of giving a systematic semantics for set theory. It is further argued that this is not just a problem for philosophers of mathematics. Semantic scepticism in set theory will almost inevitably spill over into total pessimism regarding the prospects for an explanatory theory of language and meaning in general. The conclusion is that those who wish to avoid such intellectual defeatism need to look seriously at the possibility that it is the logic used in the derivation of the paradoxes, and not the naive set theory itself, which is at fault. (shrink)

Acquiring perceptual expertise is slow and effortful. However, untrained novices can accurately make difficult classification decisions by reformulating the task as similarity judgment. Given a query image and a set of reference images, individuals are asked to select the best matching reference. When references are suitably chosen, the procedure yields an implicit classification of the query image. To optimize reference selection, we develop and evaluate a predictive model of similarity-based choice. The model builds on existing psychological literature and accommodates stochastic, (...) dynamic shifts of attention among visual feature dimensions. We perform a series of human experiments with two stimulus types and nine classification tasks to validate the model and to demonstrate the model's potential to boost performance. Our system achieves high accuracy for participants who are naive as to the classification task, even when the classification task switches from trial to trial. (shrink)

Part I: The representation of life -- Can life be given a real definition? -- The representation of the living individual -- The representation of the life-form itself -- Part II: Naive action theory -- Types of practical explanation -- Naive explanation of action -- Action and time -- Part III: Practical generality -- Two tendencies in practical philosophy -- Practices and dispositions as sources of the goodness of individual actions -- Practice and disposition as sources of (...) individual action. (shrink)

In ‘Quantifiers and Propositional Attitudes’ (1956), Quine demonstrated that the naïve model-theoretic formalization of belief ascriptions de re, applied to cases of recognition failure, produces two unwelcome effects: 1) the seeming inconsistency of belief systems ascribed to rational agents, and 2) the contradictoriness of some (apparently well justified) belief reports. In the paper under discussion, Domanov claims that proof-theoretical formalization of belief ascriptions, based on the constructive type theory, precludes those effects. I challenge this claim by showing that (...) the formalism used by him reproduces at least the first of them. I suggest that this is so because of the identifying of variables from different contexts in Domanov’s definition of context extension functions. (shrink)

A Naive Realist Theory of Colour defends the view that colours are mind-independent properties of things in the environment, that are distinct from properties identified by the physical sciences. This view stands in contrast to the long-standing and wide-spread view amongst philosophers and scientists that colours don't really exist - or at any rate, that if they do exist, then they are radically different from the way that they appear. It is argued that a naive realist (...) class='Hi'>theory of colour best explains how colours appear to perceiving subjects, and that this view is not undermined either by reflecting on variations in colour perception between perceivers and across perceptual conditions, or by our modern scientific understanding of the world. A Naive Realist Theory of Colour also illustrates how our understanding of what colours are has far-reaching implications for wider questions about the nature of perceptual experience, the relationship between mind and world, the problem of consciousness, the apparent tension between common sense and scientific representations of the world, and even the very nature and possibility of philosophical inquiry. (shrink)

In their recent paper, “Practical Knowledge without Luminosity,” Bob Beddor and Carlotta Pavese (2022) claim that the doctrine of essentially intentional actions, or “essentialism,” is false. Essentialism states that some actions are essentially intentional, such that, “whenever they are performed, they are performed intentionally” (2022, p. 926). Beddor and Pavese work to reject essentialism, which figures as a key premise in Juan Piñeros Glasscock’s anti-luminosity argument against the knowledge condition for intentional action (Piñeros Glasscock, p. 1240). Historically, essentialism has received (...) little attention from philosophers since its inception in Elizabeth Anscombe’s Intention (2000, §47). However, I believe that essentially intentional actions can play an important role in an ontology of action. In my paper, I develop and argue for a variety of essentialism in the context of naive action theory, which I call naive essentialism. Naive essentialism is a two-fold thesis, which claims that (1) essentially intentional actions exist, and (2) that essentially intentional actions ground accidentally intentional actions. My paper has four parts. In the first part, I distinguish between essentially and accidentally intentional actions, and unpack the relevant principles of naive action theory. Second, I present the grounding thesis that accidentally intentional actions are grounded in essentially intentional actions. Next, I provide an argument for the existence of essentially intentional actions. Lastly, I briefly respond to a possible objection to my argument. The upshot of my arguments is that essentially intentional actions form the metaphysical and explanatory bedrock in a naive ontology of action, and that there are good reasons for accepting a key premise in Piñeros Glasscock’s anti-luminosity argument. (shrink)

Ambiguity is a property of syntactic expressions which is ubiquitous in all informal languages–natural, scientific and mathematical; the efficient use of language depends to an exceptional extent on this feature. Disambiguation is the process of separating out the possible meanings of ambiguous expressions. Ambiguity is typical if the process of disambiguation can be carried out in some systematic way. Russell made use of typical ambiguity in the theory of types in order to combine the assurance of its (apparent) consistency (...) (“having the cake”) with the freedom of the informal untyped theory of classes and relations (“eating it too”). The paper begins with a brief tour of Russell’s uses of typical ambiguity, including his treatment of the statement Cls ∈ Cls. This is generalized to a treatment in simple type theory of statements of the form A ∈ B where A and B are class expressions for which A is prima facie of the same or higher type than B. In order to treat mathematically more interesting statements of self membership we then formulate a version of typical ambiguity for such statements in an extension of Zermelo-Fraenkel set theory. Specific attention is given to how the“naive” theory of categories can thereby be accounted for. (shrink)

Neil Tennant’s core logic is a type of bilateralist natural deduction system based on proofs and refutations. We present a proof system for propositional core logic, explain its connections to bilateralism, and explore the possibility of using it as a type theory, in the same kind of way intuitionistic logic is often used as a type theory. Our proof system is not Tennant’s own, but it is very closely related, and determines the same consequence relation. (...) The difference, however, matters for our purposes, and we discuss this. We then turn to the question of strong normalization, showing that although Tennant’s proof system for core logic is not strongly normalizing, our modified system is. (shrink)

Abstract The problem of the existence of the objects of knowledge is the main problem in the controversy between realism and anti?realism. This controversy appears on three levels: (i) perceptions, (ii) concepts, (iii) scientific theories. According to perception?realism, things exist objectively; according to subjective idealism, they are only bundles of impressions. According to conceptual realism, genera (classes) exist objectively; according to nominalism, they do not exist (there are only general names). According to scientific realism, the objects of confirmed theories, including (...) unobservable entities, exist objectively; according to phenomenalism, only observable bodies exist. On each level a naive realism and a critical realism is distinguished. On the level of scientific theories direct objects (ideal models) are distinguished from ultimate objects (real entities). (shrink)

Two distinct and apparently "dual" traditions of non-classical logic, three-valued logic and paraconsistent logic, are considered here and a unified presentation of "easy-to-handle" versions of these logics is given, in which full naive set theory, i.e. Frege's comprehension principle + extensionality, is not absurd.

In a recent series of papers, I and others have advanced new logical approaches to familiar paradoxes. The key to these approaches is to accept full classical logic, and to accept the principles that cause paradox, while preventing trouble by allowing a certain sort ofnontransitivity. Earlier papers have treated paradoxes of truth and vagueness. The present paper will begin to extend the approach to deal with the familiar paradoxes arising in naive set theory, pointing out some of the (...) promises and pitfalls of such an approach. (shrink)

Prolegomena It is fitting to begin this book on intuitionistic type theory by putting the subject matter into perspective. The purpose of this chapter is to ...

The purpose of this informal survey article is to introduce the reader to a new and surprising connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Per Martin-Löf into homotopy theory and higher-dimensional category theory.

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.

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)

The main aim is to extend the range of logics which solve the set-theoretic paradoxes, over and above what was achieved by earlier work in the area. In doing this, the paper also provides a link between metacomplete logics and those that solve the paradoxes, by finally establishing that all M1-metacomplete logics can be used as a basis for naive set theory. In doing so, we manage to reach logics that are very close in their axiomatization to that (...) of the logic R of relevant implication. A further aim is the use of metavaluations in a new context, expanding the range of application of this novel technique, already used in the context of negation and arithmetic, thus providing an alternative to traditional model theoretic approaches. (shrink)

The article deals with an approach to the analysis of propositional attitudes based on the type-theoretical semantics proposed by A. Ranta and originating from the type theory of P. Martin-Löf. Type-theoretical semantics contains the notion of context and tools of extracting information from it in an explicit form. This allows us to correctly formalize the dependence on contexts typical of propositional attitudes. In the article the context is presented as a dependent sum type (Record (...) class='Hi'>type in the proof assistant Coq). Ranta’s approach is refined and applied to the analysis of Quine’s phrase “Ralph believes that someone is a spy”. Three variants of formalization for this phrase are described which differ in the content of contextual knowledge and the way the truth values of the phrase are derived. Contexts are connected through the function of conversion, making it possible to relate truth values. As a result, it is shown that the instruments for working with contexts provided by type-theoretical semantics allow us to avoid the problem of opacity described by Quine. Provided formalization along with proofs is coded in Coq and made freely available. (shrink)

The question "Why?" that is deployed in these exchanges evidently bears the "special sense" Elizabeth Anscombe has linked to the concepts of intention and of a reason for action; it is the sort of question "Why?" that asks for what Donald Davidson later called a "rationalization".2 The special character of what is given, in each response, as formulating a reason ── a description, namely, of the agent as actually doing something, and, moreover, as..

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)

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)

This paper describes a modal conception of sets, according to which sets are 'potential' with respect to their members. A modal theory is developed, which invokes a naive comprehension axiom schema, modified by adding `forward looking' and `backward looking' modal operators. We show that this `bi-modal' naive set theory can prove modalized interpretations of several ZFC axioms, including the axiom of infinity. We also show that the theory is consistent by providing an S5 Kripke model. (...) The paper concludes with some discussion of the nature of the modalities involved, drawing comparisons with noneism, the view that there are some non-existent objects. (shrink)

We suggest a way of bringing together type theory and unification-based grammar formalisms by using records in type theory. The work is part of a broader project whose aim is to present a coherent unified approach to natural language dialogue semantics using tools from type theory.

In this paper I propose a fundamental modification of standard type theory, produce a new kind of type theoretic language, and couch in this language a comprehensive theory of abstract individuals and abstract properties and relations of every type. I then suggest how to employ the theory to solve the four following philosophical problems: the identification and ontological status of Frege's Senses; the deviant behavior of terms in propositional attitude contexts; the non-identity of necessarily (...) equivalent propositions, and the paradox of analysis. We can roughly describe these solutions as follows: the senses of English names and descriptions which denote individuals will be modelled as abstract individuals; the senses of English relation denoting expressions of a given type will be modelled as abstract relations of that type. Inside de dicto attitude contexts, these English expressions denote their senses. Relations and propositions will not be identified with their extensions, nor with functions or sets of any kind. They will be taken as primitive, and precise being and identity conditions will be proposed consistent with the view that necessarily equivalent relations and propositions may be distinct. With the modelling described in, the expressions being a brother and being a male sibling may both denote the same property, though their senses may differ. Just as Frege predicts, being a brother just is being a male sibling is an informative identity statement because the terms flanking the identity sign have the same denotation, though distinct senses. (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)

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)

Higher-order logic, with its type-theoretic apparatus known as the simple theory of types (STT), has increasingly come to be employed in theorizing about properties, relations, and states of affairs—or ‘intensional entities’ for short. This paper argues against this employment of STT and offers an alternative: ordinal type theory (OTT). Very roughly, STT and OTT can be regarded as complementary simplifications of the ‘ramified theory of types’ outlined in the Introduction to Principia Mathematica (on a realist (...) reading). While STT, understood as a theory of intensional entities, retains the Fregean division of properties and relations into a multiplicity of categories according to their adicities and ‘input types’ and discards the division of intensional entities into different ‘orders’, OTT takes the opposite approach: it retains the hierarchy of orders (though with some modifications) and discards the categorisation of properties and relations according to their adicities and input types. In contrast to STT, this latter approach avoids intensional counterparts of the Epimenides and related paradoxes. Fundamental intensional entities lie at the base of the proposed hierarchy and are also given a prominent part to play in the individuation of non-fundamental intensional entities. (shrink)

Many philosophers believe in things, propositions, which are the things that we believe, assert etc., and which are the contents of sentences. The act-type theory of propositions is an attempt to say what propositions are, to explain how we stand in relations to them, and to explain why they are true or false. The core idea of the act-type theory is that propositions are types of acts of predication. The theory is developed in various ways (...) to offer explanations of the important properties of propositions. I present the core idea of the theory, and some developments of it. I discuss the relationship between the theory and the content–force distinction. I also present an important type of objection that has been raised to the explanations offered by the act-type theory. (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.

In light of the close connection between the ontological hierarchy of set theory and the ideological hierarchy of type theory, Øystein Linnebo and Agustín Rayo have recently offered an argument in favour of the view that the set-theoretic universe is open-ended. In this paper, we argue that, since the connection between the two hierarchies is indeed tight, any philosophical conclusions cut both ways. One should either hold that both the ontological hierarchy and the ideological hierarchy are open-ended, (...) or that neither is. If there is reason to accept the view that the set-theoretic universe is open-ended, that will be because such a view is the most compelling one to adopt on the purely ontological front. (shrink)

The paradox of propositions, presented in Appendix B of Russell's The Principles of Mathematics (1903), is usually taken as Russell's principal motive, at the time, for moving from a simple to a ramified theory of types. I argue that this view is mistaken. A closer study of Russell's correspondence with Frege reveals that Russell carne to adopt a very different resolution of the paradox, calling into question not the simplicity of his early type theory but the simplicity (...) of his early theory of propositions. (shrink)