The dissertation deals with problems in "logic", more precisely, it deals with particular formal systems aiming at capturing patterns of valid reasoning. Sequent calculi were proposed to characterize logical connectives via introduction rules. These systems customarily also have structural rules which allow one to rearrange the set of premises and conclusions. In the "structurally free logic" of Dunn and Meyer the structural rules are replaced by combinatory rules which allow the same reshuffling of formulae, and additionally introduce an explicit marker (...) for the application of the rule---the combinator. The dissertation gives syntactic extensions of such systems introducing conjunction and disjunction . Cut elimination is proved for these systems. ;Syntactic systems as a rule are accompanied by a semantics which interprets them. The extended systems are supplied with semantics using algebraic methods. First, the Lindenbaum algebras are formed, and then these algebras are represented in an algebra of sets. This gives a so called Kripke-style semantics for the systems. The representation for the distributive extension utilizes well-known techniques; it uses sets of prime filters and set theoretical operations on them to deal with conjunction and disjunction, plus a ternary accessibility relation to accommodate the intensional operators as fusion and implication. The representation theorem is proven generally, i.e., for arbitrary sets of combinators using the "squeeze lemma" of Routley and Meyer. ;The non-distributive calculi require a different representation since union and intersection are distributive. Two previous representations for lattices are overviewed, and a modification of the Hartonas-Dunn representation is successfully augmented with the intensional operations. Instead of sets of filters, sets of pairs of minimally inconsistent filters and ideals are used and the representation theorem is proven. The representation results provide soundness and completeness for the systems. The dissertation also investigates properties of dual combinators , proving a series of lemmas about dual combinatory systems not being Church-Rosser and being inconsistent. Combinatorially definable classes of lambda-terms are considered as well. (shrink)

In June 1888, Oliver Heaviside received by mail an officially unpublished pamphlet, which was written and printed by the American author Willard J. Gibbs around 1881–1884. This original document is preserved in the Dibner Library of the History of Science and Technology at the Smithsonian Institute in Washington DC. Heaviside studied Gibbs’s work very carefully and wrote some annotations in the margins of the booklet. He was a strong defender of Gibbs’s work on vector analysis against quaternionists, even if he (...) criticised Gibbs’s notation system. The aim of our paper is to analyse Heaviside’s annotations and to investigate the role played by the American physicist in the development of Heaviside’s work. (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)

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)

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)

The traditional distinction between ordinary, i.e., obligatory means to preserve life and extraordinary, non-obligatory means is an especially useful tool for HECs in today's secular pluralist health care system, because it gives factors that can override the prima facie good of preserving the patient's life. I first indicate the need for such a tool. I then demonstrate the present misunderstanding of the distinction and give its proper understanding. Finally, I show the applicability of the distinction for HEC deliberations about three (...) important types of cases: the conscious, irreversibly but not terminally ill patient who requests cessation of curative treatment; the provision of artificial nutrition and hydration to permanently vegetative patients; and the allotment of intensive care and other scarce medical resources. (shrink)

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)

After the publication of Begriffsschrift, a conflict erupted between Frege and Schröder regarding their respective logical systems which emerged around the Leibnizian notions of lingua characterica and calculus ratiocinator. Both of them claimed their own logic to be a better realisation of Leibniz’s ideal language and considered the rival system a mere calculus ratiocinator. Inspired by this polemic, van Heijenoort (1967b) distinguished two conceptions of logic—logic as language and logic as calculus—and presented them as opposing views, but (...) did not explain Frege’s and Schröder’s conceptions of the fulfilment of Leibniz’s scientific ideal. -/- In this paper I explain the reasons for Frege’s and Schröder’s mutual accusations of having created a mere calculus ratiocinator. On the one hand, Schröder’s construction of the algebra of relatives fits with a project for the reduction of any mathematical concept to the notion of relative. From this stance I argue that he deemed the formal system of Begriffsschrift incapable of such a reduction. On the other hand, first I argue that Frege took Boolean logic to be an abstract logical theory inadequate for the rendering of specific content; then I claim that the language of Begriffsschrift did not constitute a complete lingua characterica by itself, more being seen by Frege as a tool that could be applied to scientific disciplines. Accordingly, I argue that Frege’s project of constructing a lingua characterica was not tied to his later logicist programme. (shrink)

By way of a close reading of Boole and Frege’s solutions to the same logical problem, we highlight an underappreciated aspect of Boole’s work—and of its difference with Frege’s better-known approach—which we believe sheds light on the concepts of ‘calculus’ and ‘mechanization’ and on their history. Boole has a clear notion of a logical problem; for him, the whole point of a logical calculus is to enable systematic and goal-directed solution methods for such problems. Frege’s Begriffsschrift, on the (...) other hand, is a visual tool to scrutinize concepts and inferences, and is a calculus only in the thin sense that every possible transition between sentences is fully and unambiguously specified in advance. While Frege’s outlook has dominated much of philosophical thinking about logical symbolism, we believe there is value—particularly in light of recent interest in the role of notations in mathematics and logic—in reviving Boole’s idea of an intrinsic link between, as he put it, a ‘calculus’ and a ‘directive method’ to solve problems. (shrink)