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)

We attempt to extend the nominalistic project initiated in Hartry Field's Science Without Numbers to modern physical theories based in differential geometry.

We present our calculus of higher-level rules, extended with propositional quantification within rules. This makes it possible to present general schemas for introduction and elimination rules for arbitrary propositional operators and to define what it means that introductions and eliminations are in harmony with each other. This definition does not presuppose any logical system, but is formulated in terms of rules themselves. We therefore speak of a foundational account of proof-theoretic harmony. With every set of introduction rules a canonical (...) elimination rule, and with every set of elimination rules a canonical introduction rule is associated in such a way that the canonical rule is in harmony with the set of rules it is associated with. An example given by Hazen and Pelletier is used to demonstrate that there are significant connectives, which are characterized by their elimination rules, and whose introduction rule is the canonical introduction rule associated with these elimination rules. Due to the availabiliy of higher-level rules and propositional quantification, the means of expression of the framework developed are sufficient to ensure that the construction of canonical elimination or introduction rules is always possible and does not lead out of this framework. (shrink)

This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.

Traces the development of the integral and the differential calculus and related theories since ancient times.

A mathematical model in science can be formulated as a counterfactual conditional, with the model’s assumptions in the antecedent and its predictions in the consequent. Interestingly, some of these models appear to have assumptions that are metaphysically impossible. Consider models in ecology that use differential equations to track the dynamics of some population of organisms. For the math to work, the model must assume that population size is a continuous quantity, despite that many organisms are necessarily discrete. This means our (...) counterfactual representation of the model can have an impossible antecedent, giving us a counterpossible. Analogous counterpossibles arise in other sciences, as we’ll see. According to a prominent view in counterfactual semantics, the vacuity thesis, all counterpossibles are vacuously true, that is, true merely because their antecedents are necessarily false. But some counterpossible formulations of differential equation models in science are not all vacuously true—some are non-vacuously true, and some are false. I go on to show how an alternative semantics, one that employs impossible worlds, can deliver this judgment. (shrink)

The calculus of Natural Calculation is introduced as an extension of Natural Deduction by proper term rules. Such term rules provide the capacity of dealing directly with terms in the calculus instead of the usual reasoning based on equations, and therefore the capacity of a natural representation of informal mathematical calculations. Basic proof theoretic results are communicated, in particular completeness and soundness of the calculus; normalisation is briefly investigated. The philosophical impact on a proof theoretic account of (...) the notion of meaning is considered. (shrink)

A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. (...) Therefore it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction. (shrink)

The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term εx A denotes some x satisfying A(x), if there is one. In Hilbert's Program, the epsilon terms play the role of ideal elements; the aim of Hilbert's finitistic consistency proofs is to give a procedure which removes (...) such terms from a formal proof. The procedures by which this is to be carried out are based on Hilbert's epsilon substitution method. The epsilon calculus, however, has applications in other contexts as well. The first general application of the epsilon calculus was in Hilbert's epsilon theorems, which in turn provide the basis for the first correct proof of Herbrand's theorem. More recently, variants of the epsilon operator have been applied in linguistics and linguistic philosophy to deal with anaphoric pronouns. (shrink)

In the year 1714, Johann Christian Lange published a baroque textbook about a logic machine, supposed to simulate human cognitive abilities such as perception, judgement, and reasoning. From today’s perspective, it can be argued that this blueprint is based on an inference engine applied to a strict ontology which serves as a knowledge base. In this paper, I will first introduce Lange’s approach in the period of baroque logic and then present a diagrammatic modernization of Lange’s principles, entitled Calculus (...) CL. Finally, I would like to discuss the possibilities of how to apply CL to modern cases of concern by using an example from epidemiology. (shrink)

Because of the “all-or-none” character of nervous activity, neural events and the relations among them can be treated by means of propositional logic. It is found that the behavior of every net can be described in these terms, with the addition of more complicated logical means for nets containing circles; and that for any logical expression satisfying certain conditions, one can find a net behaving in the fashion it describes. It is shown that many particular choices among possible neurophysiological assumptions (...) are equivalent, in the sense that for every net behaving under one assumption, there exists another net which behaves under the other and gives the same results, although perhaps not in the same time. Various applications of the calculus are discussed. (shrink)

In recent years CL diagrams inspired by Lange’s Cubus Logicus have been used in various contexts of diagrammatic reasoning. However, whether CL diagrams can also be used as a formal system seemed questionable. We present a CL diagram as a formal system, which is a fragment of propositional logic. Syntax and semantics are presented separately and a variant of bitstring semantics is applied to prove soundness and completeness of the system.

In recent years, the e ffort to formalize erotetic inferences (i.e., inferences to and from questions) has become a central concern for those working in erotetic logic. However, few have sought to formulate a proof theory for these inferences. To fill this lacuna, we construct a calculus for (classes of) sequents that are sound and complete for two species of erotetic inferences studied by Inferential Erotetic Logic (IEL): erotetic evocation and regular erotetic implication. While an attempt has been made (...) to axiomatize the former in a sequent system, there is currently no proof theory for the latter. Moreover, the extant axiomatization of erotetic evocation fails to capture its defeasible character and provides no rules for introducing or eliminating question-forming operators. In contrast, our calculus encodes defeasibility conditions on sequents and provides rules governing the introduction and elimination of erotetic formulas. We demonstrate that an elimination theorem holds for a version of the cut rule that applies to both declarative and erotetic formulas and that the rules for the axiomatic account of question evocation in IEL are admissible in our system. (shrink)

The $\lambda\mu$-calculus is an extension of the $\lambda$-calculus that has been introduced by M Parigot to give an algorithmic content to classical proofs. We show that Bohm's theorem fails in this calculus.

This book is a collection of essays published by the author in the long run of about 20 years and is centered on the reconstruction of Leibniz’s logical calculi. All the essays have been revised for the present edition and some of them constituted the background for Lenzen’s first monograph on Leibniz’s logic. A feature common to all these essays is the vindication of the relevance and originality of Leibniz’s logical achievements. Lenzen manifests strong dissatisfaction with the evaluations of Leibniz’s (...) logic previously offered by interpreters like Louis Couturat, Clarence I. Lewis, Karl Dürr, William and Martha Kneale, and states that till now Leibniz’s results in the field of logic have been widely underestimated. The book contains a careful and detailed examination of almost all Leibniz’s papers on the logical calculus and it is based on the knowledge of a wide range of texts unknown to previous interpreters. Lenzen’s acquaintance with the entire corpus of Leibniz’s logical texts is impressive. Some chapters of the book in particular contain very solid and useful logical analyses. Chapter 7, for instance, includes the most profound account of Leibniz’s theory of negation I ever read. Chapter 8 presents in a very clear way Leibniz’s attempt to reduce traditional syllogistic to a calculus based on logical inclusion between terms. Chapter 14 is devoted to Leibniz’s a priori proof of the existence of God and presents the first edition of an important manuscript on the proof. On chapters 3 and 5 a series of convincing reasons are given to argue that Leibniz’s concept of ens does not have to be considered a constant in the logical calculus. In brief: this work discusses a wide range of topics in such a clear and learned way that it will surely become a reference book for scholars interested in the study of Leibniz’s logical papers in the forthcoming years. (shrink)

This is a commentary on the use of squares in elementary statistics. One sees an ubiquitous use of squares in statistics, and the analogy of "distance in a statistical sense" is teased out. We conjecture that elementary statistical theory has its roots in classical Calculus, and preserves the notion of two senses described in this paper. We claim that the senses of the differentials dx/dy hold between classical and modern infinitesimal Calculus and show how this sense becomes cashed (...) out in both models. We suggest that the commonalities of both accounts can be used to find a informational realist account of Calculus. This account involves infinitesimal Calculus as acting as an epistemic mediator that expands our conceptual space and enables us to create new measures. (shrink)

This is the initial publication on Concept Calculus, which establishes mutual interpretability between formal systems based on informal commonsense concepts and formal systems for mathematics through abstract set theory. Here we work with axioms for "better than" and "much better than", and the Zermelo and Zermelo Frankel axioms for set theory.

Say that space is ‘gunky’ if every part of space has a proper part. Traditional theories of gunk, dating back to the work of Whitehead in the early part of last century, modeled space in the Boolean algebra of regular closed subsets of Euclidean space. More recently a complaint was brought against that tradition in Arntzenius and Russell : Lebesgue measure is not even finitely additive over the algebra, and there is no countably additive measure on the algebra. Arntzenius advocated (...) modeling gunk in measure algebras instead—in particular, in the algebra of Borel subsets of Euclidean space, modulo sets of Lebesgue measure zero. But while this algebra carries a natural, countably additive measure, it has some unattractive topological features. In this paper, we show how to construct a model of gunk that has both nice rudimentary measure-theoretic and topological properties. We then show that in modeling gunk in this way we can distinguish between finite dimensions, and that nothing in lost in terms of our ability to identify points as locations in space. (shrink)

The paper outlines the advantages and limits of the so-called ‘Calculus CL’ in the field of ontology engineering and automated theorem proving. CL is a diagram type that combines features of tree, Euler-type, Venn-type diagrams and squares of opposition. Due to the simple taxonomical structures and intuitive rules of CL, it is easy to edit ontologies and to prove inferences.

In this paper we introduce a Gentzen calculus for (a functionally complete variant of) Belnap's logic in which establishing the provability of a sequent in general requires \emph{two} proof trees, one establishing that whenever all premises are true some conclusion is true and one that guarantees the falsity of at least one premise if all conclusions are false. The calculus can also be put to use in proving that one statement \emph{necessarily approximates} another, where necessary approximation is a (...) natural dual of entailment. The calculus, and its tableau variant, not only capture the classical connectives, but also the `information' connectives of four-valued Belnap logics. This answers a question by Avron. (shrink)

Provides computer science students and researchers with a firm background in lambda-calculus and combinators.

The aim of this chapter is to develop a semantics for Calculus CL. CL is a diagrammatic calculus based on a logic machine presented by Johann Christian Lange in 1714, which combines features of Euler-, Venn-type, tree diagrams, squares of oppositions etc. In this chapter, it is argued that a Boolean account of formal ontology in CL helps to deal with logical oppositions and inferences of extended syllogistics. The result is a combination of Lange’s diagrams with an algebraic (...) semantics of terms: Bit-CL, in which any ordered objects are identified by characteristic bitstrings. Then, a number of objections to Bit-CL are answered to, and the process of inference is explained in this new logical framework. (shrink)

A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. (...) Therefore it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction. (shrink)

This paper aims to address the difficulties of high school students in bridging their computational understanding with their visualization skills in understanding the notion of the limits in their calculus class. This research used a pre-experimental one-group pretest-posttest design research on 62 grade 10 students enrolled in the Science, Technology, and Engineering Program (STEP) in one of the public high schools in Zamboanga del Sur, Philippines. A series of remedial sessions were given to help them understand the function values, (...) one-sided limits, limits of a function, and its discontinuities with the aid of the GeoGebra. Results revealed that there is a significant improvement in their mathematics performance before and after the remediation, t(61) = -19.99, p<.05. The real-time feedback provided by the drawing interface of GeoGebra has provided the students the insights into how objects behave in geometrical space, bridging their understanding in locating the values shown by the computational algebraic processes. Additionally, the significant difference in the achievement reveals a large effect size (Cohen’s =2.54) which could be accounted for by the remediation using interactive activities in the GeoGebra. (shrink)

The revised edition contains a new chapter which provides an elegant description of the semantics. The various classes of lambda calculus models are described in a uniform manner. Some didactical improvements have been made to this edition. An example of a simple model is given and then the general theory (of categorical models) is developed. Indications are given of those parts of the book which can be used to form a coherent course.

The purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int, which Wansing presents in [2016a]. There he also gives a natural deduction system for this logic, N2Int, to which SC2Int is equivalent in terms of what is derivable. What is important is that these calculi represent a kind of bilateralist (...) reasoning, since they do not only internalize processes of verifcation or provability but also the dual processes in terms of falsifcation or what is called dual provability. In [Wansing, 2017] a normal form theorem for N2Int is stated, here, I want to prove a cut-elimination theorem for SC2Int, i.e., if successful, this would extend the results existing so far. (shrink)

Traditionally, “the operator calculus of Born and Wiener” has been considered one of the four formulations of quantum mechanics that existed in 1926. The present paper reviews the operator calculus as applied by Max Born and Norbert Wiener during the last months of 1925 and the early months of 1926 and its connections with the rise of the new quantum theory. Despite the relevance of this operator calculus, Born–Wiener’s joint contribution to the topic is generally bypassed in (...) historical accounts of quantum mechanics. In this study, we analyse the paper that epitomises the contribution, and we explain the main reasons for the apparent lack of interest in Born and Wiener’s work. We argue that they did not solve the main problem for which the tool was intended, that of linear motion, because of their reluctance to use Dirac delta functions. (shrink)

If all dependent expressions were adjacent some variety of immediate constituent analysis would suffice for grammar, but syntactic and semantic mismatches are characteristic of natural language; indeed this is a, or the, central problem in grammar. Logical categorial grammar reduces grammar to logic: an expression is well-formed if and only if an associated sequent is a theorem of a categorial logic. The paradigmatic categorial logic is the Lambek calculus, but being a logic of concatenation the Lambek calculus can (...) only capture discontinuous dependencies when they are peripheral. In this paper we present the displacement calculus, which is a logic of intercalation as well as concatenation and which subsumes the Lambek calculus. On the empirical side, we apply the new calculus to discontinuous idioms, quantification, VP ellipsis, medial extraction, pied-piping, appositive relativisation, parentheticals, gapping, comparative subdeletion, cross-serial dependencies, reflexivization, anaphora, dative alternation, and particle shift. On the technical side, we prove that the calculus enjoys Cut-elimination. (shrink)

The derivative is a basic concept of differential calculus. However, if we calculate the derivative as change in distance over change in time, the result at any instant is 0/0, which seems meaningless. Hence, Newton and Leibniz used the limit to determine the derivative. Their method is valid in practice, but it is not easy to intuitively accept. Thus, this article describes the novel method of differential calculus based on the double contradiction, which is easier to accept intuitively. (...) Next, the geometrical meaning of the double contradiction is considered as follows. A tangent at a point on a convex curve is iterated. Then, the slope of the tangent at the point is sandwiched by two kinds of lines. The first kind of line crosses the curve at the original point and a point to the right of it. The second kind of line crosses the curve at the original point and a point to the left of it. Then, the double contradiction can be applied, and the slope of the tangent is determined as a single value. Finally, the meaning of this method for the foundation of mathematics is considered. We reflect on Dehaene’s notion that the foundation of mathematics is based on the intuitions, which evolve independently. Hence, there may be gaps between intuitions. In fact, the Ancient Greeks identified inconsistency between arithmetic and geometry. However, Eudoxus developed the theory of proportion, which is equivalent to the Dedekind Cut. This allows the iteration of an irrational number by rational numbers as precisely as desired. Simultaneously, we can define the irrational number by the double contradiction, although its existence is not guaranteed. Further, an area of a curved figure is iterated and defined by rectilinear figures using the double contradiction. (shrink)

We study an expansion of the Distributive Non-associative Lambek Calculus with conjugates of the Lambek product operator and residuals of those conjugates. The resulting logic is well-motivated, under-investigated and difficult to tackle. We prove completeness for some of its fragments and establish that it is decidable. Completeness of the logic is an open problem; some difficulties with applying the usual proof method are discussed.

Some formal properties of enriched systems of Lambek calculus with analogues of conjunction and disjunction are investigated. In particular, it is proved that the class of languages recognizable by the Lambek calculus with added intersective conjunction properly includes the class of finite intersections of context-free languages.

We consider substitutions in order sensitive situations, having in the back of our minds the case of dynamic predicate logic (DPL) with a stack semantics. We start from the semantic intuition that substitutions are move instructions on stacks: the syntactic operation [y/x] is matched by the instruction to move the value of the y-stack to the x-stack. We can describe these actions in the positive fragment of DPLE. Hence this fragment counts as a logic for DPL-substitutions. We give a (...) class='Hi'>calculus for the fragment and prove soundness and completeness. (shrink)

We present a sequent calculus of a paraconsistent logic QMPT0, which has the paraconsistent-type excluded middle law (PEML) as an initial sequent. Our system shows that the presence of PEML is essentially important for QMPT0. It also has special rules when the set of constant symbols is finite. We also discuss the cut-elimination property of our system.

In the present article, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic (...) logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag–Moss–Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination. (shrink)