Several authors have suggested that a more parsimonious and conceptually elegant treatment of everyday mereological and topological reasoning can be obtained by adopting a spatial ontology in which regions, not points, are the primitive entities. This paper challenges this suggestion for mereotopological reasoning in two-dimensional space. Our strategy is to define a mereotopological language together with a familiar, point-based interpretation. It is proposed that, to be practically useful, any alternative region-based spatial ontology must support the same sentences in our language (...) as this familiar interpretation. This proposal has the merit of transforming a vague, open-ended question about ontologies for practical mereotopological reasoning into a precise question in model theory. We show that (a version of) the familiar interpretation is countable and atomic, and therefore prime. We conclude that useful alternative ontologies of the plane are, if anything, less parsimonious than the one which they are supposed to replace. (shrink)

In this paper a solution of Whitehead’s problem is presented: Starting with a purely mereological system of regions a topological space is constructed such that the class of regions is isomorphic to the Boolean lattice of regular open sets of that space. This construction may be considered as a generalized completion in analogy to the well-known Dedekind completion of the rational numbers yielding the real numbers . The argument of the paper relies on the theories of continuous lattices and “pointless” (...) topology.

. (shrink)

I ON THE PRIMITIVE TERM OF LOGISTICf IN this article I propose to establish a theorem belonging to logistic concerning some connexions, not widely known, ...

This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

Although the relationship of part to whole is one of the most fundamental there is, this is the first full-length study of this key concept. Showing that mereology, or the formal theory of part and whole, is essential to ontology, Simons surveys and critiques previous theories--especially the standard extensional view--and proposes a new account that encompasses both temporal and modal considerations. Simons's revised theory not only allows him to offer fresh solutions to long-standing problems, but also has far-reaching consequences for (...) our understanding of a host of classical philosophical concepts. (shrink)

This paper presents a calculus for mereotopological reasoning in which two-dimensional spatial regions are treated as primitive entities. A first order predicate language ℒ with a distinguished unary predicate c(x), function-symbols +, · and - and constants 0 and 1 is defined. An interpretation ℜ for ℒ is provided in which polygonal open subsets of the real plane serve as elements of the domain. Under this interpretation the predicate c(x) is read as 'region x is connected' and the function-symbols and (...) constants are given their meaning in terms of a Boolean algebra of polygons. We give an alternative interpretation ������ base on the real closed plane which turns out to be isomorphic to ℜ. A set of axioms and a rule of inference are introduced. We prove the soundness and completeness of the calculus with respect to the given interpretation. (shrink)

We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...) all formulas ψ not involving $p, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions. An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra. (shrink)

We define a propositionally quantified intuitionistic logic Hπ + by a natural extension of Kripke's semantics for propositional intutionistic logic. We then show that Hπ+ is recursively isomorphic to full second order classical logic. Hπ+ is the intuitionistic analogue of the modal systems S5π +, S4π +, S4.2π +, K4π +, Tπ +, Kπ + and Bπ +, studied by Fine.

Although Aristotle (Metaphysics, Book IV, Chapter 2) was perhaps the first person to consider the part-whole relationship to be a proper subject matter for philosophic inquiry, the Polish logician Stanislow Lesniewski [15] is generally given credit for the first formal treatment of the subject matter in his Mereology.1 Woodger [30] and Tarski [24] made use of a specific adaptation of Lesniewski's work as a basis for a formal theory of physical things and their parts. The term 'calculus of individuals' was (...) introduced by Leonard and Goodman [14] in their presentation of a system very similar to Tarski's adaptation of Lesniewski's Mereology. Contemporaneously with Lesniewski's development of his Mereology, Whitehead [27] and [28] was developing a theory of extensive abstraction based on the two-place predicate, 'x extends over y\ which is the converse of 'x is a part of y\ This system, according to Russell [22], was to have been the fourth volume of their Pήncipia Mathematica, the never-published volume on geometry. Both Lesniewski [15] and Tarski [25] have recognized the similarities between Whitehead's early work and Lesniewski's Mereology. Between the publication of Whitehead's early work and the publication of Process and Reality [29], Theodore de Laguna [7] published a suggestive alternative basis for Whitehead's theory. This led Whitehead, in Process and Reality, to publish a revised form of his theory based on the two-place predicate, 'x is extensionally connected with y\ It is the purpose of this paper to present a calculus of individuals based on this new Whiteheadian primitive predicate. (shrink)

Spatial reasoning is essential for many AI applications. In most existing systems the representation is primarily numerical, so the information that can be handled is limited to precise quantitative data. However, for many purposes the ability to manipulate high-level qualitative spatial information in a flexible way would be extremely useful. Such capabilities can be proveded by logical calculi; and indeed 1st-order theories of certain spatial relations have been given [20]. But computing inferences in 1st-order logic is generally intractable unless special (...) methods are known.0-order modal logics provide an alternative representation which is more expressive than classical 0-order logic and yet often more amenable to automated deduction than 1st-order formalisms. These calculi are usually interpreted as propositional logics: non-logical constants are taken as denoting propositions. However, they can also be given a nominal interpretation in which the constants stand for some kind of object. I show how 0-order logics can be given a spatial interpretation: constants denote regions and logical operators correspond to operations on regions which are important for characterising spatial situations.Representing certain spatial concepts requires the introduction of modal operators, interpreted as functions generating regions related in specific ways to those denoted by their arguments. A significant example is the convex-hull operator whose value is the smallest convex region containing its argument. I investigate how this this operator can be captured in a multi-medal logic. (shrink)

We define a propositionally quantified intuitionistic logic $\mathbf{H}\pi +$ by a natural extension of Kripke's semantics for propositional intutionistic logic. We then show that $\mathbf{H}\pi+$ is recursively isomorphic to full second order classical logic. $\mathbf{H}\pi+$ is the intuitionistic analogue of the modal systems $\mathbf{S}5\pi +, \mathbf{S}4\pi +, \mathbf{S}4.2\pi +, \mathbf{K}4\pi +, \mathbf{T}\pi +, \mathbf{K}\pi +$ and $\mathbf{B}\pi +$, studied by Fine.

Reviewed Works:Gaisi Takeuti, Proof Theory.Georg Kreisel, Proof Theory: Some Personal Recollections.Wolfram Pohlers, Contributions of the Schutte School in Munich to Proof Theory.Stephen G. Simpson, Subsystems of $\mathbf{Z}_2$ and Reverse Mathematics.Solomon Feferman, Proof Theory: A Personal Report.

ABSTRACT The paper studies propositional logics in a bimodal language, in which the first modality is interpreted as the local truth, and the second as the universal truth. The logic S4UC is introduced, which is finitely axiomatizable, has the f.m.p. and is determined by every connected separable metric space.

The second order intuitionistic propositional logic characterized by the class of all “principal” Kripke frames is non-recursively axiomatizable, as well as any logic of a class of principal Kripke frames containing every finite frame.