We identify complete fragments of the simple theory of types with infinity and Quine’s new foundations set theory. We show that TSTI decides every sentence ϕ in the language of type theory that is in one of the following forms: ϕ=∀x1r1⋯∀xkrk∃y1s1⋯∃ylslθ where the superscripts denote the types of the variables, s1>⋯>sl, and θ is quantifier-free, ϕ=∀x1r1⋯∀xkrk∃y1s⋯∃ylsθ where the superscripts denote the types of the variables and θ is quantifier-free. This shows that NF decides (...) every stratified sentence ϕ in the language of set theory that is in one of the following forms: ϕ=∀x1⋯∀xk∃y1⋯∃ylθ where θ is quantifier-free and ϕ admits a stratification that assigns distinct values to all of the variables y1,…,yl, ϕ=∀x1⋯∀xk∃y1⋯∃ylθ where θ is quantifier-free and ϕ admits a stratification that assigns the same value to all of the variables y1,…,yl. (shrink)

Church's simple theory of types is a system of higher-order logic in which functions are assumed to be total. We present in this paper a version of Church's system called PF in which functions may be partial. The semantics of PF, which is based on Henkin's general-models semantics, allows terms to be nondenoting but requires formulas to always denote a standard truth value. We prove that PF is complete with respect to its semantics. The reasoning mechanism in (...) PF for partial functions corresponds closely to mathematical practice, and the formulation of PF adheres tightly to the framework of Church's system. (shrink)

In this paper we define intensional models for the classical theory of types, thus arriving at an intensional type logic ITL. Intensional models generalize Henkin's general models and have a natural definition. As a class they do not validate the axiom of Extensionality. We give a cut-free sequent calculus for type theory and show completeness of this calculus with respect to the class of intensional models via a model existence theorem. After this we turn our attention to (...) applications. Firstly, it is argued that, since ITL is truly intensional, it can be used to model ascriptions of propositional attitude without predicting logical omniscience. In order to illustrate this a small fragment of English is defined and provided with an ITL semantics. Secondly, it is shown that ITL models contain certain objects that can be identified with possible worlds. Essential elements of modal logic become available within classical type theory once the axiom of Extensionality is given up. (shrink)

It is often claimed that the theory of function levels proposed by Frege in Grundgesetze der Arithmetik anticipates the hierarchy of types that underlies Church’s simple theory of types. This claim roughly states that Frege presupposes a type of functions in the sense of simple type theory in the expository language of Grundgesetze. However, this view makes it hard to accommodate function names of two arguments and view functions as incomplete entities. I propose (...) and defend an alternative interpretation of first-level function names in Grundgesetze into simple type-theoretic open terms rather than into closed terms of a function type. This interpretation offers a still unhistorical but more faithful type-theoretic approximation of Frege’s theory of levels and can be naturally extended to accommodate second-level functions. It is made possible by two key observations that Frege’s Roman markers behave essentially like open terms and that Frege lacks a clear criterion for distinguishing between Roman markers and function names. (shrink)

In this work Ockham proposes a theory of simple predication, which he uses in explicating the truth conditions of progressively more complicated kinds of propositions. His discussion includes what he takes to be the correct semantic treatment of quantified propositions, past tense and future tense propositions, and modal propositions, all of which are receiving much attention from contemporary philosophers. He also illustrates the use of exponential analysis to deal with propositions that prove troublesome in both semantic theory (...) and other disciplines, such as metaphysics, physics, and theology. This type of analysis plays an essential role in his substantive philosophical and theological works, and in many cases then can hardly be understood without a prior acquaintance with this section of the Summa. An introduction by Alfred J. Freddoso clarifies and summarizes Ockham's theory, discusses certain philosophical problems which it engenders, and proposes new interpretations for parts of it. The essay will be helpful both to those interested in Ockham as a historical figure and to those interested in his substantive systematic contributions to logical theory. (shrink)

This article investigates a theory of type assignment (assigning types to lambda terms) called ETA which is intermediate in strength between the simple theory of type assignment and strong polymorphic theories like Girard’s F (Proofs and types. Cambridge University Press, Cambridge, 1989). It is like the simple theory and unlike F in that the typability and type-checking problems are solvable with respect to ETA. This is proved in the article along with three other (...) main results: (1) all primitive recursive functionals of finite type are representable in ETA; (2) every term typable in ETA has a unique normal form; (3) there is a function defined by ${{\varepsilon}_0}$ -recursion which takes every typable term to a natural number which is an upper bound to the lengths of all βη-reduction sequences starting with that term. (shrink)

We continue work of Shelah on the cardinality of families of pairwise incompatible types in simple theories obtaining characterizations of simple and supersimple theories. We develop a local analysis of the number of types in simple theories and we find a new example of a simple unstable theory.

We investigate stationarity of types over models in simple theories. In particular, we show that in simple theories with finite SU-rank, any complete type over a model having Cantor-Bendixson rank is stationary.

In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have (...) a strong correlation with predicativity, predicative logic still plays an influential role in Computer Science.An important example is the proof checker Nuprl, which is basedon Martin-Löf''s Type Theory which uses type universes. Those type universes,and also degrees of expressions in AUTOMATH, are closely related toorders. In this paper, we show that orders have not disappeared from modern logic and computer science, rather, orders play a crucial role in understanding the hierarchy of modern systems. In order to achieve our goal, we concentrate on a subsystem of Nuprl.The novelty of our paper lies in: (1) a modest revival of Russell's orders, (2) the placing of the historical system RTT underlying the famous Principia Mathematica in a context with a modern system of computer mathematics (Nuprl) and modern type theories (Martin-Löf''s type theory and PTSs), and (3) the presentation of acomplex type system (Nuprl) as a simple and compact PTS. (shrink)

This reissue, first published in 1971, provides a brief historical account of the Theory of Logical Types; and describes the problems that gave rise to it, its various different formulations (Simple and Ramified), the difficulties connected with each, and the criticisms that have been directed against it. Professor Copi seeks to make the subject accessible to the non-specialist and yet provide a sufficiently rigorous exposition for the serious student to see exactly what the theory is and (...) how it works. (shrink)

ABSTRACT One of the most important developments in twentieth-century rhetorical theory is Perelman and Olbrechts-Tyteca's insight that concepts, when under strain, can be split or dissociated into two separate terms. Not a simple binary, these terms remain interconnected in a value hierarchy with one term serving as the normative frame for the other. Perelman and Olbrechts-Tyteca theorize that either term can be dissociated further, producing a fan-type dissociation. Unlike ordinary dissociations, fan-types place three or more terms in (...) hierarchical relationship, resulting in unique rhetorical features. Fanning a dissociation can serve three basic rhetorical functions: purging undesirable elements, preserving less undesirable elements from total devaluation, and purifying desirable elements. Building on these basic functions, rhetors can perform complex rhetorical actions, from intensifying a dissociation's values to completely undoing a dissociation. Long ignored by theorists and critics, fan-types complicate our understanding of dissociation, argumentation, and value-based reasoning, and therefore deserve more scholarly attention. (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)

Let T be simple, work in Ceq over a boundedly closed set. Let p ∈ S(θ) be internal in a quasi-stably-embedded type-definable set Q (e.g., Q is definable or stably-embedded) and suppose (p, Q) is ACL-embedded in Q (see definitions below). Then Aut(p/Q) with its action on pC is type-definable in Ceq over θ. In particular, if p ∈ S(θ) is internal in a stably-embedded type-definable set Q, and pC υ Q is stably-embedded, then Aut(p/Q) is type-definable with its (...) action on pC. (shrink)

[I] Divine Simplicity: God and His Existence Types of Divine Simplicity Of the properties ascribed to God in Aquinas' natural theology, we may call one sort ...

In this paper a class of simple theories, called the low theories is developed, and the following is proved. Theorem. Let T be a low theory. A set and a, b elements realizing the same strong type over A. Then, a and b realized the same Lascar strong type over A.

Let T be a countable, small simple theory. In this paper, we prove that for such T, the notion of Lascar strong type coincides with the notion of strong type, over an arbitrary set.

Let T be a simple L-theory and let \ be a reduct of T to a sublanguage \ of L. For variables x, we call an \-invariant set \\) in \ a universal transducer if for every formula \\in L^-\) and every a, $$\begin{aligned} \phi ^-\ L^-\text{-forks } \text{ over }\ \emptyset \ \text{ iff } \Gamma \wedge \phi ^-\ L\text{-forks } \text{ over }\ \emptyset. \end{aligned}$$We show that there is a greatest universal transducer \ and it is (...) type-definable. In particular, the forking topology on \\) refines the forking topology on \\) for all y. Moreover, we describe the set of universal transducers in terms of certain topology on the Stone space and show that \ is the unique universal transducer that is \-type-definable with parameters. If \ is a theory with the wnfcp and T is the theory of its lovely pairs of models we show that \\) and give a more precise description of the set of universal transducers for the special case where \ has the nfcp. (shrink)

We reconstruct the group action in the group configuration theorem. We apply it to show that in an ω-categorical theory a finitely based pseudolinear regular type is locally modular, and the geometry associated to a finitely based locally modular regular type is projective geometry over a finite field.

As emphasized by Alonzo Church and David Kaplan (Church 1974, Kaplan 1975), the philosophies of language of Frege and Russell incorporate quite different methods of semantic analysis with different basic concepts and different ontologies. Accordingly we distinguish between a Fregean and a Russellian tradition in intensional semantics. The purpose of this paper is to pursue the Russellian alternative and to provide a language of intensional logic with a model-theoretic semantics. We also discuss the so-called Russell-Myhill paradox that threatens simple (...) Russellian type theory if propositions satisfies very strict principles of individuation. One way of avoiding the paradox is to adopt a ramified rather than a simple theory of types. (shrink)

Since their introduction by Partee and Rooth (1983) into linguistic theory, type shifting principles have been extensively employed in various linguistic domains, including nominal predicates (Partee 1987), kind denoting NPs (Chierchia 1998), interrogatives (Groenendijk and Stokhof 1989), scrambled definites (De Hoop and Van der Does 1998) and plurals (Winter 2001,2002). Most of the accounts that use type shifting principles employ them as ``last resort'' mechanisms, which apply only when other compositional mechanisms fail. This failure is often sloppily referred to (...) as type mismatch . The motivation for introducing type mismatch into the compositional mechanism is twofold: on the one hand it allows lexical items to be assigned the minimal types that are needed for describing their denotation; on the other hand, it has been argued that the ``last resort'' strategy of type shifting prevents derivation of undesired meanings. The first goal of this paper is to define a simple notion of type mismatch, which will rather closely follow Partee and Rooth's original proposal but will be expressed within more familiar terms of categorial semantics. After introducing this implementation of traditional type mismatch, it will be argued that in fact, it covers only one possible kind of trigger for type shifting principles. Partee and Rooth's notion of mismatch is ``external'' in that the type of an expression is changed only when it combines with another type to which it cannot compose using the ``normal'' compositional mechanism. It will be argued that, within an appropriate type system, another notion of mismatch is also useful. This is the kind of mismatch in which the semantic type of an expression does not match its syntactic category. Two such cases will be explored: mismatch between morpho-syntactic number (singular or plural) and semantic number (a denotation ranging over atoms or sets), and mismatch between syntactic category (noun, DP, adjective etc.) and semantic role (predicate, quantifier, predicate modifier etc.).. (shrink)

Let T be a complete O-minimal theory in a language L. We first give an elementary proof of the result (due to Marker and Steinhorn) that all types over Dedekind complete models of T are definable. Let L * be L together with a unary predicate P. Let T * be the L * -theory of all pairs (N, M), where M is a Dedekind complete model of T and N is an |M| + -saturated elementary extension (...) of N (and M is the interpretation of P). Using the definability of types result, we show that T * is complete and we give a simple set of axioms for T * . We also show that for every L * -formula φ(x) there is an L-formula ψ(x) such that $T^\ast \models (\forall \mathbf{x})(P(\mathbf{x}) \rightarrow (\phi(\mathbf{x}) \mapsto \psi (\mathbf{x}))$ . This yields the following result: Let M be a Dedekind complete model of T. Let φ(x, y) be an L-formula where l(y) = k. Let $\mathbf{X} = \{X \subset M^k$ : for some a in an elementary extension N of M, X = φ (a,y N ∩ M k }. Then there is a formula ψ(y, z) of L such that X = {ψ (y, b) M : b in M}. (shrink)

The basic idea of counterfactual theories of causation is that the meaning of causal claims can be explained in terms of counterfactual conditionals of the form “If A had not occurred, C would not have occurred”. While counterfactual analyses have been given of type-causal concepts, most counterfactual analyses have focused on singular causal or token-causal claims of the form “event c caused event e”. Analyses of token-causation have become popular in the last thirty years, especially since the development in the (...) 1970's of possible world semantics for counterfactuals. The best known counterfactual analysis of causation is David Lewis's (1973b) theory. However, intense discussion over thirty years has cast doubt on the adequacy of any simple analysis of singular causation in terms of counterfactuals. Recent years have seen a proliferation of different refinements of the basic idea to achieve a closer match with commonsense judgements about causation. (shrink)

In recent work, the authors have established the group configuration theorem for simple theories, as well as some of its main applications from geometric stability theory, such as the binding group theorem, or in the $\omega$-categorical case, the characterization of the forking geometry of a finitely based non-trivial locally modular regular type as projective geometry over a finite field and the equivalence of pseudolinearity and local modularity. The proof necessitated an extension of the model-theoretic framework to include almost (...) hyperimaginaries, and the study of polygroups. (shrink)

1. We show that if p is a real type which is internal in a set $\sigma$ of partial types in a simple theory, then there is a type p' interbounded with p, which is finitely generated over $\sigma$ , and possesses a fundamental system of solutions relative to $\sigma$ . 2. If p is a possibly hyperimaginary Lascar strong type, almost \sigma-internal$ , but almost orthogonal to $\sigma^{\omega}$ , then there is a canonical non-trivial almost hyperdefinable (...) polygroup which multi-acts on p while fixing $\sigma$ generically. In case p is $\sigma-internal$ and T is stable, this is the binding group of p over \sigma$. (shrink)

In a simple theory with elimination of finitary hyperimaginaries if tp(a) is real and analysable over a definable set Q, then there exists a finite sequence ( $a_{i}|i \leq n^{*}$ ) $\subseteq dcl^{eq}$ (a) with $a_{n}*$ = a such that for every $i \leq n*$ , if $p_{i} = tp(a_{i}/{a_{i}|j < i}$ ) then $Aut(p_{i}/Q)$ is type-definable with its action on $p_{i}^{c}$ . A unidimensional simple theory eliminates the quantifier $\exists^{\infty}$ and either interprets (in $C^{eq}$ ) (...) an infinite type-definable group or has the property that ACL(Q) = C for every infinite definable set Q. (shrink)

Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define (...) a notion of an interpretation of one PF* theory in another. PF* is intended as a foundation for mechanized mathematics. It is the basis for the logic of , an Interactive Mathematical Proof System developed at The MITRE Corporation. (shrink)

Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define (...) a notion of an interpretation of one PF* theory in another. PF* is intended as a foundation for mechanized mathematics. It is the basis for the logic of, an Interactive Mathematical Proof System developed at The MITRE Corporation. (shrink)