In this article we define a logical system called Hybrid Partial Type Theory ( $\mathcal {HPTT}$ ). The system is obtained by combining William Farmer’s partial type theory with a strong form of hybrid logic. William Farmer’s system is a version of Church’s theory of types which allows terms to be non-denoting; hybrid logic is a version of modal logic in which it is possible to name worlds and evaluate expressions with respect to (...) particular worlds. We motivate this combination of ideas in the introduction, and devote the rest of the article to defining, axiomatising, and proving a completeness result for $\mathcal {HPTT}$. (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)

To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem (...) prover. Lean’s elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved. (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 refine the definition of II-computability of [12] so that oracles have a “consistent”, but natural, behaviour. We prove a Kleene Normal Form Theorem and closure of semi-recursive relations under ∃1. We also show that in this more inclusive computation theory Post's theorem in the arithmetical hierarchy still holds.

We investigate Hilbert’s varepsilon -calculus in the context of intuitionistic type theories, that is, within certain systems of intuitionistic higher-order logic. We determine the additional deductive strength conferred on an intuitionistic type theory by the adjunction of closed varepsilon -terms. We extend the usual topos semantics for type theories to the varepsilon -operator and prove a completeness theorem. The paper also contains a discussion of the concept of “partially defined‘ varepsilon -term. MSC: 03B15, 03B20, 03G30.

Fragments of extensional Martin-Löf type theory without universes,ML 0, are introduced that conservatively extend S.A. Cook and A. Urquhart'sIPV ω. A model for these restricted theories is obtained by interpretation in Feferman's theory APP of operators, a natural model of which is the class of partial recursive functions. In conclusion, some examples in group theory are considered.

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)

This is part two of a two-part paper in which we develop an axiomatic theory of the relation of partial ground. The main novelty of the paper is the of use of a binary ground predicate rather than an operator to formalize ground. In this part of the paper, we extend the base theory of the first part of the paper with hierarchically typed truth-predicates and principles about the interaction of partial ground and truth. We show (...) that our theory is a proof-theoretically conservative extension of the ramified theory of positive truth up to. (shrink)

Partial functions can be easily represented in set theory as certain sets of ordered pairs. However, classical set theory provides no special machinery for reasoning about partial functions. For instance, there is no direct way of handling the application of a function to an argument outside its domain as in partial logic. There is also no utilization of lambda-notation and sorts or types as in type theory. This paper introduces a version of von-Neumann-Bernays-Gödel (...) set theory for reasoning about sets, proper classes, and partial functions represented as classes of ordered pairs. The underlying logic of the system is a partial first-order logic, so class-valued terms may be nondenoting. Functions can be specified using lambda-notation, and reasoning about the application of functions to arguments is facilitated using sorts similar to those employed in the logic of the IMPS Interactive Mathematical Proof System. The set theory is intended to serve as a foundation for mechanized mathematics systems. (shrink)

The notion of empirical adequacy has received recent philosophical attention, especially within the framework of the semantic approach. Empirical adequacy, as explicated in the semantic approach, concerns the relationship between empirical substructures and some phenomena. The aim here is to differentiate this notion of empirical adequacy from one concerning the relationship between data and phenomena. Distinguishing each notion of empirical adequacy emphasizes different aspects of scientific practice—one concerning theory-development from the basis of an established theory, the other concerning (...) theory-development from the basis of data-fitting, where established theory may not foster further development. To illustrate this contrast, an example from financial economics is considered. (shrink)

A type-structure of partial effective functionals over the natural numbers, based on a canonical enumeration of the partial recursive functions, is developed. These partial functionals, defined by a direct elementary technique, turn out to be the computable elements of the hereditary continuous partial objects; moreover, there is a commutative system of enumerations of any given type by any type below (relative numberings). By this and by results in [1] and [2], the Kleene-Kreisel countable (...) functionals and the hereditary effective operations (HEO) are easily characterized. (shrink)

In this paper it is shown how a partial semantics for presuppositions can be given which is empirically more satisfactory than its predecessors, and how this semantics can be integrated with a technically sound, compositional grammar in the Montagovian fashion. Additionally, it is argued that the classical objection to partial accounts of presupposition projection, namely that they lack “flexibility,” is based on a misconception. Partial logics can give rise to flexible predictions without postulating any ad hoc ambiguities. (...) Finally, it is shown how the partial foundation can be combined with a dynamic system of common-ground maintenance to account for accommodation. (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)

The dispute over the viability of various theories of relativistic, dissipative fluids is analyzed. The focus of the dispute is identified as the question of determining what it means for a theory to be applicable to a given type of physical system under given conditions. The idea of a physical theory's regime of propriety is introduced, in an attempt to clarify the issue, along with the construction of a formal model trying to make the idea precise. This (...) construction involves a novel generalization of the idea of a field on spacetime, as well as a novel method of approximating the solutions to partial-differential equations on relativistic spacetimes in a way that tries to account for the peculiar needs of the interface between the exact structures of mathematical physics and the inexact data of experimental physics in a relativistically invariant way. It is argued, on the basis of these constructions, that the idea of a regime of propriety plays a central role in attempts to understand the semantical relations between theoretical and experimental knowledge of the physical world in general, and in particular in attempts to explain what it may mean to claim that a physical theory models or represents a kind of physical system. This discussion necessitates an examination of the initial-value formulation of the partial-differential equations of mathematical physics, which suggests a natural set of conditions---by no means meant to be canonical or exhaustive---one may require a mathematical structure, in conjunction with a set of physical postulates, satisfy in order to count as a physical theory. Based on the novel approximating methods developed for solving partial-differential equations on a relativistic spacetime by finite-difference methods, a technical result concerning a peculiar form of theoretical under-determination is proved, along with a technical result purporting to demonstrate a necessary condition for the self-consistency of a physical theory. (shrink)

We investigate a theory of Frege structures extended by the Myhill-Flagg hierarchy of implications. We study its relation to a property theory with an approximation operator and we give a proof theoretical analysis of the basic system involved. MSC: 03F35, 03D60.

This paper has four parts. In the first part, I present Leniewski's protothetics and the complete system provided for that logic by Henkin. The second part presents a generalized notion of partial functions in propositional type theory. In the third part, these partial functions are used to define partial interpretations for protothetics. Finally, I present in the fourth part a complete system for partial protothetics. Completeness is proved by Henkin's method [4] using saturated sets (...) instead of maximally saturated sets. This technique provides a canonical representation of a partial semantic space and it is suggested that this space can be interpreted as an epistemic state of a non-omniscient agent. (shrink)

We consider semi-isolation on the locus of a strongly non-isolated, RK-minimal type in a small theory, and we prove that its asymmetry (as a binary relation) is caused by a specific form of the strict order property: the partial definability of semi-isolation.

There is a duality in our everyday view of belief. On the one hand, we sometimes speak of credence as a matter of degree. We talk of having some level of confidence in a claim (that a certain course of action is safe, for example, or that a desired event will occur) and explain our actions by reference to these degrees of confidence – tacitly appealing, it seems, to a probabilistic calculus such as that formalized in Bayesian decision theory. (...) On the other hand, we also speak of belief as an unqualified, or flat-out, state (‘plain belief’ as it is sometimes called), which is either categorically present or categorically absent. We talk of simply believing or thinking that something is the case, and we cite these flat-out attitudes in explanation of our actions – appealing to classical practical reasoning of the sort formalized in the so-called ‘practical syllogism’.1 This tension in everyday discourse is reflected in the theoretical literature on belief. In formal epistemology there is a division between those in the Bayesian tradition, who treat credence as graded, and those who think of it as a categorical attitude of some kind. The Bayesian perspective also contrasts with the dominant view in philosophy of mind, where belief is widely regarded as a categorical state (a token sentence of a mental language, inscribed in a functionally defined ‘belief box’, according to one popular account). A parallel duality is present in our everyday view of desire. Sometimes we talk of having degrees of preference or desirability; sometimes we speak simply of wanting or desiring something tout court, and, again, this tension is reflected in the theoretical literature. What should we make of these dualities? Are there two different types of belief and desire – partial and flat-out, as they are sometimes called? If so, how are they related? And how could both have a role in guiding rational action, as the everyday view has it? The last question poses a particular challenge in relation to flat-out belief and desire.. (shrink)

Partial functions are ubiquitous in both mathematics and computer science. Therefore, it is imperative that the underlying logical formalism for a general-purpose mechanized mathematics system provide strong support for reasoning about partial functions. Unfortunately, the common logical formalisms — first-order logic, type theory, and set theory — are usually only adequate for reasoning about partial functionsin theory. However, the approach to partial functions traditionally employed by mathematicians is quite adequatein practice. This paper (...) shows how the traditional approach to partial functions can be formalized in a range of formalisms that includes first-order logic, simple type theory, and Von-Neumann—Bernays—Gödel set theory. It argues that these new formalisms allow one to directly reason about partial functions; are based on natural, well-understood, familiar principles; and can be effectively implemented in mechanized mathematics systems. (shrink)

Effect algebras (EAs), play a significant role in quantum logic, are featured in the theory of partially ordered Abelian groups, and generalize orthoalgebras, MV-algebras, orthomodular posets, orthomodular lattices, modular ortholattices, and boolean algebras.We study centrally orthocomplete effect algebras (COEAs), i.e., EAs satisfying the condition that every family of elements that is dominated by an orthogonal family of central elements has a supremum. For COEAs, we introduce a general notion of decomposition into types; prove that a COEA factors uniquely as (...) a direct sum of types I, II, and III; and obtain a generalization for COEAs of Ramsay’s fourfold decomposition of a complete orthomodular lattice. (shrink)

Many theories of fairness distinguish between compensation factors and responsibility factors. Whereas the distinction between both types of factors is a matter of definition in theory, empirical work usually requires a sharp cut. All determinants of the outcome of interest have to be classified as either a compensation factor or a responsibility factor. We argue that the determinants are often hard to classify. A pragmatic solution to the problem at hand is to introduce a more general soft cut: determinants (...) can be partly compensation, partly responsibility. Still, in a first-best income tax framework, such a soft cut is possible only if the gross income function is additively separable. In case separability fits the data, a simple partial sharing rule emerges as a natural candidate for partial redistribution. This rule can be characterized on the basis of two simple properties, equal treatment of equals and partial solidarity. In case additive separability is rejected by the data, we propose two alternative solutions. (shrink)

We show that the theory of the partial ordering of the computably enumerable degrees in any given nontrivial interval is undecidable and has uncountably many 1-types.

In recent years, semantical partiality has emerged as an important explanatory concept in philosophical logic as well as in the study of natural language semantics. Despite the many applications, however, a number of mathematically intriguing questions associated with this concept have received only very limited attention. ;The present dissertation aims to present a systematic study of certain types of partiality in the area of basic model theory. Two types of issues are given special attention: Introducing partially defined models, there (...) are many ways to generalize the classical truth definition for sentences of a simple first order language relative to standard, complete models. Different interpretations of the formal framework motivate conflicting truth definitions between language and partial models: A partial model can be taken to represent a part of the world, or a partial information set. The truth of a sentence can be supported directly by a part of the world, but can also follow indirectly from an information set. These notions are related, and the relation motivates a comparison between various weaker and stronger alternative truth definitions. Results are obtained about the extent to which these truth definitions differ, and a number of characterization results are deduced. ;Among other conditions that are not expressible in the framework of standard, complete model theory, a condition of monotonicity or persistence of truth relative to partial models is argued to follow under both the given interpretations of the formal framework. The final chapter investigates the relation between such conditions and expressibility properties in general. These discussions culminate with a combined Lindstrom and persistence characterization theorem. (shrink)

This article points out problems in current dynamic treatments of anaphora and provides a new account that solves these by grafting Muskens' Compositional Discourse Representation Theory onto a partial theory of types. Partiality is exploited to keep track of which discourse referents have been introduced in the text (thus avoiding the overwrite problem) and to account for cases of anaphoric failure. Another key assumption is that the set of discourse referents is well-ordered, so that we can keep (...) track of the order in which they have been introduced, allowing a semantic characterization of anaphoric accessibility across stretches of discourse. Unlike other dynamic approaches, the system defines semantic values for unresolved anaphors. This leads to a clear separation of monotonic and non-monotonic content (in this case anaphoric resolution) and arguably provides a sound basis for a non-monotonic theory of anaphoric resolution. (shrink)

Hume offers two ways of reconciling the partiality of people’s feelings with the generality of moral thinking. First, the general point of view in moral evaluation is not that of a disinterested observer, but of another person who has a close relationship with the person to be judged. Here I find something analogous to the idea of Nel Noddings, who attempts to build an ethical theory on the basis of caring relationships. Second, according to Hume, the generality of the (...) rules of justice is also compatible with partial feelings. Such rules allow everyone to pursue his or her goals without fear of violent intervention from others. My idea is that these rules are comparable to those of a competitive game. The idea of fair competition is not necessarily alien to Noddings’ type of ethical theory. As children, human beings normally learn to be fair in competitive games, along with caring for family members and friends. An ethical ideal of fairness may develop through competitions and help people get along with others beyond narrow circles. Taking into account of the competitive elements in relationship between people will be helpful in giving a fuller picture of a broadly Humean, sentimentalist ethical theory. (shrink)

The purpose of this paper is to look at some of the apparent characteristics of consciousness in theories in which consciousness is said to play a role in the collapse of the state vector. In particular, these reflections are based primarily on the work of three theorists: Amit Goswami, Henry Stapp, and Evan Harris Walker. Upon looking at such theories, three characteristics of consciousness become apparent. The first is a volitional aspect of the mind that needs to be distinguished from (...) awareness or observation. The second is the stratification of consciousness such that the experiential stream that goes on privately for a given person can be distinguished from a universal deep consciousness, akin to David Bohm’s implicate order, that might underlie ordinary consciousness. Having done so, a question arises regarding the manner in which deliberately intentional acts that occur within one’s experiential stream can apparently have their intended effects. An indirect mechanism consistent with the M5 model of Robert Jahn and Brenda Dunne is proposed. Third, in transferring the notion of the collapse of the state vector from the context of observation in experimental physics to manifestation of everyday life, the temporal discontinuity of collapses implies that the experiential stream of ordinary waking consciousness is also discontinuous. Furthermore, in some collapse-type quantum mind theories, the subject–object distinction is thought to emerge with the collapse, so that the physical universe itself, including its spatial features, could be arising from a pre-physical substrate at the rate of once per Planck time. This idea can be modelled using Jack Ng’s notion of a spacetime lattice with Planck time timelike separations and Planck length spacelike separations. Furthermore, such modelling can be partially cast in category-theoretic form by adapting a previous application of Grothendieck topoi to Edmund Husserl’s conceptualization of conscious mental acts. Thus, a volitional aspect of mind, the stratification of consciousness, and discontinuity of the ordinary waking state are some of the characteristics of consciousness implicit in some collapse-type quantum mind theories. (shrink)

We study relativized Lascar groups, which are formed by relativizing Lascar groups to the solution set of a partial type $$\Sigma $$. We introduce the notion of a Lascar tuple for $$\Sigma $$ and by considering the space of types over a Lascar tuple for $$\Sigma $$, the topology for a relativized Lascar group is (re-)defined and some fundamental facts about the Galois groups of first-order theories are generalized to the relativized context. In particular, we prove that any (...) closed subgroup of a relativized Lascar group corresponds to a stabilizer of a bounded hyperimaginary having at least one representative in the solution set of the given partial type $$\Sigma $$. Using this, we find the correspondence between subgroups of the relativized Lascar group and the relativized strong types. (shrink)

We investigate a model of becoming—classical sequential growth (CSG)—that has been proposed within the framework of causal sets (causets), with the latter defined as order types of certain partial orderings. To investigate how causets grow, we introduce special sequences of causets, which we call “csg-paths”. We prove a number of results concerning relations between csg-paths and causets. These results paint a highly non-trivial picture of csg-paths. There are uncountably many csg-paths, all of them sharing the same beginning, after which (...) they branch. Every infinite csg-path achieves in the limit an infinite causet, and vice versa, every infinite causet is achieved in the limit by an infinite csg-path. However, coalescing csg-paths, i.e., ones that achieve the same causet even after forking off at some point, are ubiquitous. (shrink)

This paper presents a new language for isomorphic representations of legalknowledge in feature structures. The language includes predefinedstructures based on situation theory for common-sense categories, andpredefined structures based on Van Kralingens frame-based conceptualmodelling language for legal rules. It is shown that the flexibility of thefeature-structure formalism can exploited to allow for structure-preservingrepresentations of non-primitive concepts, and to enable various types ofinteraction and cross- reference between language elements. A fragment of theDutch Opium Act is used to illustrate how modelling and (...) reasoning proceed in practice. (shrink)

Definitional and axiomatic theories of truth -- Objects of truth -- Tarski -- Truth and set theory -- Technical preliminaries -- Comparing axiomatic theories of truth -- Disquotation -- Classical compositional truth -- Hierarchies -- Typed and type-free theories of truth -- Reasons against typing -- Axioms and rules -- Axioms for type-free truth -- Classical symmetric truth -- Kripke-Feferman -- Axiomatizing Kripke's theory in partial logic -- Grounded truth -- Alternative evaluation schemata -- Disquotation (...) -- Classical logic -- Deflationism -- Reflection -- Ontological reduction -- Applying theories of truth. (shrink)

“Small” large cardinal notions in the language of ZFC are those large cardinal notions that are consistent with V = L. Besides their original formulation in classical set theory, we have a variety of analogue notions in systems of admissible set theory, admissible recursion theory, constructive set theory, constructive type theory, explicit mathematics and recursive ordinal notations (as used in proof theory). On the face of it, it is surprising that such distinctively set-theoretical (...) notions have analogues in such disaparate and relatively constructive contexts. There must be an underlying reason why that is possible (and, incidentally, why “large” large cardinal notions have not led to comparable analogues). My long term aim is to develop a common language in which such notions can be expressed and can be interpreted both in their original classical form and in their analogue form in each of these special constructive and semi-constructive cases. This is a program in progress. What is done here, to begin with, is to show how that can be done to a considerable extent in the settings of classical and admissible set theory (and thence, admissible recursion theory). The approach taken here is to expand the language of set theory to allow us to talk about (possibly partial) operations applicable both to sets and to operations and to formulate the large cardinal notions in question in terms of operational closure conditions; at the same time only minimal existence axioms are posited for sets. The resulting system, called Operational Set Theory, is a partial adaptation to the set-theoretical framework of the explicit mathematics framework Feferman (1975). The.. (shrink)

It is exhibited that mature scientific economical theory is a set of propositions that describe the relationship between theoretical objects of two types - basic objects and derivative ones. The set of basic objects makes up the aggregate of initial idealizations (the Fundamental Theoretical Scheme or FTS) with no direct reference to experimental data. The derivative theoretical objects are formed from the basic ones according to certain rules. The sets of derivative objects form partial theoretical schemes or PTS. (...) Any mature economics scientific theory grows due to transitions, in order to describe each new experimental situation, from FTS to PTS. Each PTS construction from the FTS represents a problem that cannot be reduced to a strict algorithm. (shrink)

In some situations, a decision is best represented by an incompletely analyzed act: conditionally on a given event A, the consequences of the decision on sub-events are perfectly known and uncertainty becomes probabilizable, whereas the plausibility of this event itself remains vague and the decision outcome on the complementary event ${\bar{A}}$ is imprecisely known. In this framework, we study an axiomatic decision model and prove a representation theorem. Resulting decision criteria aggregate partial evaluations consisting of (i) the conditional expected (...) utility associated with the analyzed part of the decision, and (ii) the best and worst consequences of its non-analyzed part. The representation theorem is consistent with a wide variety of decision criteria, which allows for expressing various degrees of knowledge on ( ${A, \bar{A}}$ ) and various types of attitude toward ambiguity and uncertainty. This diversity is taken into account by specific models already existing in the literature. We exploit this fact and propose some particular forms of our model incorporating these models as sub-models and moreover expressing various types of beliefs concerning the relative plausibility of the analyzed and the non-analyzed events ranging from probabilities to complete ignorance that include capacities. (shrink)

Universal theories with model completions are characterized. A new omitting types theorem is proved. These two results are used to prove the existence of a universal ℵ 0 -categorical partial order with an interesting embedding property. Other aspects of these results also are considered.

We continue the study of simple theories begun in [3] and [5]. We first find the right analogue of definability of types. We then develop the theory of generic types and stabilizers for groups definable in simple theories. The general ideology is that the role of formulas (or definability) in stable theories is replaced by partial types (or ∞-definability) in simple theories.

A persuasion dialogue is a dialogue in which a conflict between agents with respect to their points of view arises at the beginning of the talk and the agents have the shared, global goal of resolving the conflict and at least one agent has the persuasive aim to convince the other party to accept an opposing point of view. I argue that the persuasive force of argument may have not only extreme values but also intermediate strength. That is, I wish (...) to introduce two additional types of the effects of persuasion in addition to successful and unsuccessful ones (cf. Van Eemeren and Houtlosser in Argumentation 14(3):293–305, 2000; Advances in pragma-dialectics. Sic Sat, Amsterdam, 2002; Walton in A pragmatic theory of fallacy. University of Alabama Press, Tuscaloosa, 1995; Walton and Krabbe in Commitment in dialogue: basic concepts of interpersonal reasoning. State University of New York Press, Albany, New York, 1995). I propose a model which provides for modified versions of the standpoint of an agent needed in order to bring about two possible outcomes of a persuasion dialogue. These two outcomes I label partially-successful and over-successful. I call the potential, not yet verbalised, standpoint of an agent here the original topic t. Based on some aspects of relevance theory (Sperber and Wilson in Relevance: communication and cognition. Blackwell, Oxford, 1986; Wilson and Sperber in The handbook of pragmatics. Blackwell Publishing, Malden, 2006), I explain that the modified version of the original topic t is an implicature created from the original topic t and from a specific mental topic which belongs to, what I call the beneficial cognitive model (hence BCM). I define BCMi,t as a set of topics which are within the area of agent i’s interest of persuasion with respect to t. (shrink)

We present the model construction technique called Linear Realizability. It consists in building a category of Partial Equivalence Relations over a Linear Combinatory Algebra. We illustrate how it can be used to provide models, which are fully complete for various typed λ-calculi. In particular, we focus on special Linear Combinatory Algebras of partial involutions, and we present PER models over them which are fully complete, inter alia, w.r.t. the following languages and theories: the fragment of System F consisting (...) of ML-types, the maximal theory on the simply typed λ-calculus with finitely many ground constants, and the maximal theory on an infinitary version of this latter calculus. (shrink)

This paper studies the theories defended by John Buridan and Nicole Oresme on the presence of the soul in the body, with a special focus on the interpretation of the Augustinian principle – or ‘holenmeric’ principle – according to which the soul is in the whole body and is wholly present in every part of it. The first part of the paper introduces the different types of composition involved in the medieval discussions over the soul and its parts and shows (...) how different psychological theories prior to 1350 employed this typology of part/whole relations to clarify the soul’s presence in the body. The next part of the paper presents how the theories designed by John Buridan and Nicole Oresme were motivated by problems raised by these earlier accounts of the soul’s presence and undertook to solve them from the perspective of a reductionist conception of parthood. It is argued that, despite their common commitment to a reductionist stance, the solutions endorsed by Buridan and Oresme represent two opposite ways of applying a nominalist metaphysics of parts to psychological matters. (shrink)

§1. Introduction. A linear ordering embedsinto another linear ordering if it is isomorphic to a subset of it. Two linear orderings are said to beequimorphicif they can be embedded in each other. This is an equivalence relation, and we call the equivalence classesequimorphism types. We analyze the structure of equimorphism types of linear orderings, which is partially ordered by the embeddability relation. Our analysis is mainly fromthe viewpoints of Computability Theory and Reverse Mathematics. But we also obtain results, as (...) the definition of equimorphism invariants for linear orderings, which provide a better understanding of the shape of this structure in general.This study of linear orderings started by analyzing the proof-theoretic strength of a theorem due to Jullien [Jul69]. As is often the case in Reverse Mathematics, to solve this problem it was necessary to develop a deeper understanding of the objects involved. This led to a variety of results on the structure of linear orderings and the embeddability relation on them. These results can be divided into three groups. (shrink)

In this dissertation we study two-cardinal phenomena—both of the admitting cardinals variety and of the Chang’s Conjecture variety—under the assumption that all our models have stable theories. All our results involve two, relatively widely accepted generalizations of the traditional definitions in this area. First, we allow the relevant subsets of our models to be picked out by (perhaps infinitary) partial types; second we consider δ-cardinal problems as well as two-cardinal problems.

Ambos-Spies, K. and R.A. Shore, Undecidability and 1-types in the recursively enumerable degrees, Annals of Pure and Applied Logic 63 3–37. We show that the theory of the partial ordering of recursively enumerable Turing degrees is undecidable and has uncountably many 1-types. In contrast to the original proof of the former which used a very complicated O''' argument our proof proceeds by a much simpler infinite injury argument. Moreover, it combines with the permitting technique to get similar results (...) for any ideal of the r.e. degrees. (shrink)

One way to construct a contraction operator for a theory (belief set) is to assign to it a base (belief base) and an operator of partial meet contraction for that base. Axiomatic characterizations are given of the theory contractions that are generated in this way by (various types of) partial meet base contractions.

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)

The notion of a strongly determined type over A extending p is introduced, where p .S. A strongly determined extension of p over A assigns, for any model M )- A, a type q S extending p such that, if realises q, then any elementary partial map M → M which fixes acleq pointwise is elementary over . This gives a crude notion of independence which arises very frequently. Examples are provided of many different kinds of theories (...) with strongly determined types, and some without. We investigate a notion of multiplicity for strongly determined types with applications to ‘involved’ finite simple groups, and an analogue of the Finite Equivalence Relation Theorem. Lifting of strongly determined types to covers of a structure is discussed, and an application to finite covers is given. (shrink)

The implicit-explicit distinction is applied to knowledge representations. Knowledge is taken to be an attitude towards a proposition which is true. The proposition itself predicates a property to some entity. A number of ways in which knowledge can be implicit or explicit emerge. If a higher aspect is known explicitly then each lower one must also be known explicitly. This partial hierarchy reduces the number of ways in which knowledge can be explicit. In the most important type of (...) implicit knowledge, representations merely reflect the property of objects or events without predicating them of any particular entity The dearest cases of explicit knowledge of a fact are representations of one's own attitude of knowing that fact. These distinctions are discussed in their relationship to similar distinctions such as procedural-declarative, conscious unconscious, verbalizable-nonverbalizable, direct-indirect tests, and automatic voluntary control. This is followed by an outline of how these distinctions can be used to integrate and relate the often divergent uses of the implicit-explicit distinction in different research areas. We illustrate this for visual perception, memory, cognitive development, and artificial grammar learning. (shrink)