This paper is a contribution to the study of the rôle of disjunction inAlgebraic Logic. Several kinds of (generalized) disjunctions, usually defined using a suitable variant of the proof by cases property, were introduced and extensively studied in the literature mainly in the context of finitary logics. The goals of this paper are to extend these results to all logics, to systematize the multitude of notions of disjunction (both those already considered in the literature and those introduced in (...) this paper), and to show several interesting applications allowed by the presence of a suitable disjunction in a given logic. (shrink)

This paper is a contribution to the general study of consequence relations which contain (definable) connective of “disjunction”. Our work is centered around the “proof by cases property”, we present several of its equivalent definitions, and show some interesting applications, namely in constructing axiomatic systems for intersections of logics and recognizing weakly implicative fuzzy logics among the weakly implicative ones.

This mathematics textbook covers the fundamental ideas used in writing proofs. Proof techniques covered include direct proofs, proofs by contrapositive, proofs by contradiction, proofs in set theory, proofs of existentially or universally quantified predicates, proofs by cases, and mathematical induction. Inductive and deductive reasoning are explored. A straightforward approach is taken throughout. Plenty of examples are included and lots of exercises are provided after each brief exposition on the topics at hand. The text begins with a study of (...) symbolic logic, deductive reasoning, and quantifiers. Inductive reasoning and making conjectures are examined next, and once there are some statements to prove, techniques for proving conditional statements, disjunctions, biconditional statements, and quantified predicates are investigated. Terminology and proof techniques in set theory follow with discussions of the pick-a-point method and the algebra of sets. Cartesian products, equivalence relations, orders, and functions are all incorporated. Particular attention is given to injectivity, surjectivity, and cardinality. The text includes an introduction to topology and abstract algebra, with a comparison of topological properties to algebraic properties. This book can be used by itself for an introduction to proofs course or as a supplemental text for students in proof-based mathematics classes. The contents have been rigorously reviewed and tested by instructors and students in classroom settings. (shrink)

This is the continuation of the paper :417–446, 2010). We continue the abstract study of non-classical logics based on the kind of generalized implication connectives they possess and we focus on semilinear logics, i.e. those that are complete with respect to the class of models where the implication defines a linear order. We obtain general characterizations of semilinearity in terms of the intersection-prime extension property, the syntactical semilinearity metarule and the class of finitely subdirectly irreducible models. Moreover, we consider extensions (...) of the language with lattice connectives and generalized disjunctions, study their interplay with implication and obtain axiomatizations and further descriptions of semilinear logics in terms of disjunctions and the proof by cases property. (shrink)

The axioms of projective and affine plane geometry are turned into rules of proof by which formal derivations are constructed. The rules act only on atomic formulas. It is shown that proof search for the derivability of atomic cases from atomic assumptions by these rules terminates . This decision method is based on the central result of the combinatorial analysis of derivations by the geometric rules: The geometric objects that occur in derivations by the rules can be (...) restricted to those known from the assumptions and cases. This “subterm property” is proved by permuting suitably the order of application of the geometric rules. As an example of the decision method, it is shown that there cannot exist a derivation of Euclid’s fifth postulate if the rule that corresponds to the uniqueness of the parallel line construction is taken away from the system of plane affine geometry. (shrink)

We present a proof for a conjecture previously formulated by Dzhafarov et al.. The conjecture specifies a measure for the degree of contextuality and a criterion for contextuality in a broad class of quantum systems. This class includes Leggett–Garg, EPR/Bell, and Klyachko–Can–Binicioglu–Shumovsky type systems as special cases. In a system of this class certain physical properties \ are measured in pairs \ \); every property enters in precisely two such pairs; and each measurement outcome is a binary (...) random variable. Denoting the measurement outcomes for a property \ in the two pairs it enters by \ and \, the pair of measurement outcomes for \ \) is \ \). Contextuality is defined as follows: one computes the minimal possible value \ for the sum of \ ) that is allowed by the individual distributions of \ and \; one computes the minimal possible value \ for the sum of \ across all possible couplings of the entire set of random variables \ in the system; and the system is considered contextual if \ ). This definition has its justification in the general approach dubbed Contextuality-by-Default, and it allows for measurement errors and signaling among the measured properties. The conjecture proved in this paper specifies the value of \ in terms of the distributions of the measurement outcomes \ \). (shrink)

In the recent literature on proof theory, there seems to be a new raising topic which consists in identifying those properties that characterise a good sequent calculus. The property that has received by far the most attention is the analyticity property. In this paper we propose a new argument in support of the analyticity property. We will do it by means of the example of the logic of proofs, a logic recently introduced by Artemov [1]. Indeed a detailed (...) proof analysis of this logic sheds new light on the logic itself and perfectly exemplifies our argument in favour of the analiticity. (shrink)

This thesis is concerned with extending the underlying logical approach as well as the breadth of applications of the proof mining program to various (mostly previously untreated) areas of nonlinear analysis and optimization, with a particular focus being placed on topics which involve set-valued operators.For this, we extend the current logical methodology of proof mining by new systems and corresponding so-called logical metatheorems that cover these more involved areas of nonlinear analysis. Most of these systems crucially rely on (...) the use of intensional methods, treating sets with potentially high quantifier complexity in the defining matrix via characteristic functions and axioms that describe only their properties and do not completely characterize the elements of the sets.The applicability of all of these metatheorems is then substantiated by a range of case studies for the respective areas which in particular also highlight the naturalness of the use of intensional methods in the design of the corresponding systems.The first new area covered thereby is the theory of nonlinear semigroups induced by corresponding evolution equations for accretive operators. In that context, we present (besides an initial foray into the area from 2015) essentially the first applications of proof mining to the theory of partial differential equations. Concretely, we provide quantitative versions of four central results on the asymptotic behavior of solutions to such equations.The second new area unlocked in this thesis is that of the continuous dual of a Banach space and its norm (which are also approached via intensional methods). This in particular relies on a proof-theoretically tame treatment of suprema over (certain) bounded sets in this intensional context which is further exploited later on. These systems, which give access to this until now untreated fundamental notion from functional analysis, are then used to provide further substantial extensions to treat various notions from convex analysis like the Fréchet derivative of a convex function, Fenchel conjugates, Bregman distances, and monotone operators on Banach spaces in the sense of Browder.These systems are then utilized to provide applications in the context of Picard- and Halpern-style iterations of so-called Bregman strongly nonexpansive mappings where we provide both new quantitative and qualitative results.Lastly, we discuss the key notion of extensionality of a set-valued operator and its relation to set-theoretic maximality principles in more depth (which was already singled out—to some degree—in previous work). We thereby exhibit an issue arising with treating full extensionality in the context of these intensional approaches to set-valued operators and present useful fragments of the full extensionality statement where these issues are avoided.Corresponding to these fragments, we discuss a range of uniform continuity statements for set-valued operators beyond the usual notion involving the Hausdorff-metric. In particular, in that context, we utilize the previous tame treatment of suprema over bounded sets to also provide the first proof-theoretic treatment of that Hausdorff-metric in the context of systems for proof mining.The applicability of this treatment of the Hausdorff-metric is then in particular substantiated by a last case study where we provide quantitative information for a Mann-type iteration of set-valued mappings which are nonexpansive w.r.t. the Hausdorff-metric.The abstract was taken directly from the thesis.Abstract prepared by Nicholas Pischke, Technische Universität Darmstadt, Darmstadt, GermanyE-mail: [email protected]: https://doi.org/10.26083/tuprints-00026584. (shrink)

We give a uniform proof of the theorems of Yao and Beigel–Tarui representing ACC predicates as constant depth circuits with MODm\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {MOD}_{m}$$\end{document} gates and a symmetric gate. The proof is based on a relativized, generalized form of Toda’s theorem expressed in terms of closure properties of formulas under bounded universal, existential and modular counting quantifiers. This allows the main proofs to be expressed in terms of formula classes instead (...) of Boolean circuits. The uniform version of the Beigel–Tarui theorem is then obtained automatically via the Furst–Saxe–Sipser and Paris–Wilkie translations. As a special case, we obtain a uniform version of Razborov and Smolensky’s representation of AC0[p]\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {AC}^{0}[p]$$\end{document} circuits. The paper is partly expository, but is also motivated by the desire to recast Toda’s theorem, the Beigel–Tarui theorem, and their proofs into the language of bounded arithmetic. However, no knowledge of bounded arithmetic is needed. (shrink)

The initial motivating question for this thesis is what the standard of rigour in modern mathematics amounts to: what makes a proof rigorous, or fail to be rigorous? How is this judged? A new account of rigour is put forward, aiming to go some way to answering these questions. Some benefits of the norm of rigour on this account are discussed. The account is contrasted with other remarks that have been made about mathematical proof and its workings, and (...) is tested and illustrated by considering a case study discussed in the literature. On the view put forward here one can obtain a manner of informal, rigorous mathematics founded on any of a variety of proof systems. The latter part of the thesis is concerned with the question of how we should decide which of these competing proof systems we should base our mathematics on: i.e., the question of which proof system we should take as a foundation for our mathematics. A novel answer to this question is proposed, in which the key property we should require of a proof system is that for as many different kinds of structures as possible, when the proof system allows a generalization about that kind of structure to be proved, the generalization actually holds of all real examples of that kind of structure which exist. This is the requirement of soundness of the proof system. It is argued that the best way to establish the soundness of a proof system may be by giving an interpretation of its axioms on which they are established as true. As preparation for this discussion, the thesis first investigates the logical and conceptual basis of various arithmetic concepts, with the results obtained used in the final discussion of soundness. (shrink)

Mathematical investigation, when done well, can confer understanding. This bare observation shouldn’t be controversial; where obstacles appear is rather in the effort to engage this observation with epistemology. The complexity of the issue of course precludes addressing it tout court in one paper, and I’ll just be laying some early foundations here. To this end I’ll narrow the field in two ways. First, I’ll address a specific account of explanation and understanding that applies naturally to mathematical reasoning: the view proposed (...) by Philip Kitcher and Michael Friedman of explanation or understanding as involving the unification of theories that had antecedently appeared heterogeneous. For the second narrowing, I’ll take up one specific feature (among many) of theories and their basic concepts that is sometimes taken to make the theories and concepts preferred: in some fields, for some problems, what is counted as understanding a problem may involve finding a way to represent the problem so that it (or some aspect of it) can be visualized. The final section develops a case study which exemplifies the way that this consideration – the potential for visualizability – can rationally inform decisions as to what the proper framework and axioms should be. The discussion of unification (in sections 3 and 4) leads to a mathematical analogue of Goodman’s problem of identifying a principled basis for distinguishing grue and green. Just as there is a philosophical issue about how we arrive at the predicates we should use when making empirical predictions, so too there is an issue about what properties best support many kinds of mathematical reasoning that are especially valuable to us. The issue becomes pressing via an examination of some physical and mathematical cases that make it seem unlikely that treatments of unification can be as straightforward as the philosophical literature has hoped. Though unification accounts have a grain of truth (since a phenomenon (or cluster of phenomena) called “unification” is in fact important in many cases) we are far from an analysis of what “unification” is.. (shrink)

The proofs of universally quantified statements, in mathematics, are given as “schemata” or as “prototypes” which may be applied to each specific instance of the quantified variable. Type Theory allows to turn into a rigorous notion this informal intuition described by many, including Herbrand. In this constructive approach where propositions are types, proofs are viewed as terms of λ-calculus and act as “proof-schemata”, as for universally quantified types. We examine here the critical case of Impredicative Type Theory, i. e. (...) Girard's system F, where type-quantification ranges over all types. Coherence and decidability properties are proved for prototype proofs in this impredicative context. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Proof and Persuasion in the Philosophical Debate about AbortionChris KaposyPhilosophers involved in debating the abortion issue often assume that the arguments they provide can offer decisive resolution.1 Arguments on the prolife side of the debate, for example, usually imply that it is rationally mandatory to view the fetus as having a right to life, or full moral standing.2 Such an account assumes that philosophical argument can compel the (...) reader to see the fetus in a certain way and that dissent risks irrationality.I wish to question this image of the use of philosophical argument in the abortion debate. I focus on the question of fetal moral standing, which is one of the subproblems in the debate. I am especially concerned with prolife arguments for fetal moral standing, since the prolife side must argue for a position that is compulsory. The prochoice side, in contrast, typically holds that people are entitled to believe what they want about the fetus’s moral standing.My position is that philosophical arguments should be understood as tools for persuasion in the abortion debate rather than as a method for discovering decisive proofs about the morality of abortion. I argue that because any one position on the moral standing of fetuses cannot be established decisively, law and policy should favour the prochoice position. In support of these conclusions, I present two common argumentative strategies used to suggest that the prolife view of the fetus is rationally [End Page 139] mandatory, and I illustrate why arguments involving these strategies do not compel us to view the fetus as having full moral standing.Framing the IssueIn order to show that abortion is wrong (in cases in which it is considered wrong), one must first establish that fetuses have full moral standing.3 It is a serious moral wrong to take the life of someone with full moral standing—this is part of what it means to have this status. The possessor of full moral standing is entitled to have his or her life protected. If abortion is wrong, then the fetus must have full moral standing, because without such standing, killing a fetus could be justified by the pregnant woman’s strong interest in ending an unwanted pregnancy. Those arguing against the moral permissibility of abortion must show that it is mandatory (in some way) to view the fetus as having full moral standing. There are a range of positions one could take with regard to the fetus’s status, from viewing the fetus as an incipient organism with no moral standing to seeing the fetus as gaining moral standing as the pregnancy progresses. But if it is mandatory to view the fetus as having full moral standing, all other positions must then be mistaken, incorrect, or somehow unjustified.This paper analyzes why philosophers opposed to abortion think it is mandatory to attribute full moral standing to fetuses. There are two popular argumentative strategies offering different accounts of the source of this obligation. The first strategy suggests that fetal full moral standing derives from morally relevant facts about the fetus. According to this line of argument, we are rationally obligated to view the fetus as having full moral standing because we cannot deny (without courting irrationality) that there are properties, characteristics, or attributes of the fetus that entitle it to this status.The second strategy is to claim that the fetus has full moral standing because this position is most consistent with our intuitions in cases unrelated to abortion. Philosophers taking this approach are fond of analogies comparing fetuses to comatose adults or to people at the end of life, for example. This strategy of appealing to your interlocutor’s sense of consistency I call the “shared-value” strategy.The two strategies map very well onto the distinction some have made between argumentum ad rem and argumentum ad hominem. The philosopher of rhetoric Henry Johnstone Jr. draws this distinction in very clear terms, and others in the history of philosophy make note of the difference [End Page 140] between these two types of arguments as well.4 The appeal to the facts (or argumentum ad rem) seeks to establish the truth of its... (shrink)

Elekes proved that any infinite-fold cover of a σ-finite measure space by a sequence of measurable sets has a subsequence with the same property such that the set of indices of this subsequence has density zero. Applying this theorem he gave a new proof for the random-indestructibility of the density zero ideal. He asked about other variants of this theorem concerning I-almost everywhere infinite-fold covers of Polish spaces where I is a σ-ideal on the space and the set of (...) indices of the required subsequence should be in a fixed ideal ${{\mathcal{J}}}$ on ω. We introduce the notion of the ${{\mathcal{J}}}$ -covering property of a pair ${({\mathcal{A}}, I)}$ where ${{\mathcal{A}}}$ is a σ-algebra on a set X and ${{I \subseteq \mathcal{P}(X)}}$ is an ideal. We present some counterexamples, discuss the category case and the Fubini product of the null ideal ${\mathcal{N}}$ and the meager ideal ${\mathcal{M}}$ . We investigate connections between this property and forcing-indestructibility of ideals. We show that the family of all Borel ideals ${{\mathcal{J}}}$ on ω such that ${\mathcal{M}}$ has the ${{\mathcal{J}}}$ -covering property consists exactly of non weak Q-ideals. We also study the existence of smallest elements, with respect to Katětov–Blass order, in the family of those ideals ${\mathcal{J}}$ on ω such that ${\mathcal{N}}$ or ${\mathcal{M}}$ has the ${\mathcal{J}}$ -covering property. Furthermore, we prove a general result about the cases when the covering property “strongly” fails. (shrink)

When is an ideal of a ring radical or prime? By examining its generators, one may in many cases definably and uniformly test the ideal’s properties. We seek to establish such definable formulas in rings of p-adic power series, such as $\mathbb Q_{p}\langle X\rangle $, $\mathbb Z_{p}\langle X\rangle $, and related rings of power series over more general valuation rings and their fraction fields. We obtain a definable, uniform test for radicality, and, in the one-dimensional case, for primality. (...) This builds upon the techniques stemming from the proof of the quantifier elimination results for the analytic theory of the p-adic integers by Denef and van den Dries, and the linear algebra methods of Hermann and Seidenberg.prepared by Madeline G. Barnicle.E-mail: [email protected]: https://escholarship.org/uc/item/6t02q9s4. (shrink)

In this work we develop goal-directed deduction methods for the implicational fragment of several modal logics. We give sound and complete procedures for strict implication of K, T, K4, S4, K5, K45, KB, KTB, S5, G and for some intuitionistic variants. In order to achieve a uniform and concise presentation, we first develop our methods in the framework of Labelled Deductive Systems [Gabbay 96]. The proof systems we present are strongly analytical and satisfy a basic property of cut admissibility. (...) We then show that for most of the systems under consideration the labelling mechanism can be avoided by choosing an appropriate way of structuring theories. One peculiar feature of our proof systems is the use of restart rules which allow to re-ask the original goal of a deduction. In case of K, K4, S4 and G, we can eliminate such a rule, without loosing completeness. In all the other cases, by dropping such a rule, we get an intuitionistic variant of each system. The present results are part of a larger project of a goal directed proof theory for non-classical logics; the purpose of this project is to show that most implicational logics stem from slight variations of a unique deduction method, and from different ways of structuring theories. Moreover, the proof systems we present follow the logic programming style of deduction and seem promising for proof search [Gabbay and Reyle 84, Miller et al. 91]. (shrink)

The article approaches cut elimination from a new angle. On the basis of an arbitrary inference relation among logically atomic formulae, an inference relation on a language possessing logical operators is defined by means of inductive clauses similar to the operator-introducing rules of a cut-free intuitionistic sequent calculus. The logical terminology of the richer language is not uniquely specified, but assumed to satisfy certain conditions of a general nature, allowing for, but not requiring, the existence of infinite conjunctions and disjunctions. (...) We investigate to what extent structural properties of the given atomic relation are preserved through the extension to the full language. While closure under the Cut rule narrowly construed is not in general thus preserved, two properties jointly amounting to closure under the ordinary structural rules, including Cut, are. -/- Attention is then narrowed down to the special case of a standard first-order language, where a similar result is obtained also for closure under substitution of terms for individual parameters. Taken together, the three preservation results imply the familiar cut-elimination theorem for pure first-order intuitionistic sequent calculus. -/- In the interest of conceptual economy, all deducibility relations are specified purely inductively, rather than in terms of the existence of formal proofs of any kind. (shrink)

Chapter 1 constitutes an introduction to Gentzen calculi from two perspectives, logical and philosophical. It introduces the notion of generalisations of Gentzen sequent calculus and the discussion on properties that characterize good inferential systems. Among the variety of Gentzen-style sequent calculi, I divide them in two groups: syntactic and semantic generalisations. In the context of such a discussion, the inferentialist philosophy of the meaning of logical constants is introduced, and some potential objections – mainly concerning the choice of working (...) with semantic generalizations – are addressed. Finally, I’ll introduce the case studies that I’ll be dealing with in part II. Chapter 2 is concerned with the origins and development of Jaśkowski’s discussive logic. The main idea of this chapter is to systematize the various stages of the development of discussive logic related researches from two different angles, i.e., its connections to modal logics and its proof theory, by highlighting virtues and vices. Chapter 3 focuses on the Gentzen-style proof theory of discussive logic, by providing a characterization of it in terms of labelled sequent calculi. Chapter 4 deals with the Gentzen-style proof theory of relevant logics, again by employing the methodology of labelled sequent calculi. This time, instead of working with a single logic, I’ll deal with a whole family of them. More precisely, I’ll study in terms of proof systems those relevant logics that can be characterised, at the semantic level, by reduced Routley-Meyer models, i.e., relational structures with a ternary relation between states and a unique base element. Chapter 5 investigates the proof theory of a modal expansion of intuitionistic propositional logic obtained by adding an ‘actuality’ operator to the connectives. This logic was introduced also using Gentzen sequents. Unfortunately, the original proof system is not cut-free. This chapter shows how to solve this problem by moving to hypersequents. Chapter 6 concludes the investigations and discusses the future of the research presented throughout the dissertation. (shrink)

This chapter focuses on one of the common fallacies in Western philosophy called ' proof by verbosity (PVB)'. PVB is a favorite device among conspiracy theorists who utilize it to obfuscate the weakness of their case. By supporting their theories with so much random information (and misinformation), it gives the impression that their position is superficially well researched and supported by an avalanche of evidence. Sometimes PVB takes the form of a proof by intimidation, especially when an argument (...) is made using sophisticated insider jargon, or when a complex and long‐winded argument is made by an eminent scholar in the field. In the spirit of overwhelming the opposition, a PVB can be committed by employing a litany of numbers and statistics. Articulating your arguments in a clear and concise fashion and substantiating the position with well‐founded and mutually intelligible premises is the key to avoiding a proof by verbosity. (shrink)

An old conjecture of modal logics states that every splitting of the major systems K4, S4, G and Grz has the finite model property. In this paper we will prove that all iterated splittings of G have fmp, whereas in the other cases we will give explicit counterexamples. We also introduce a proof technique which will give a positive answer for large classes of splitting frames. The proof works by establishing a rather strong property of these splitting (...) frames namely that they preserve the finite model property in the following sense. Whenever an extension Λ has fmp so does the splitting Λ/f of Λ by f. Although we will also see that this method has its limitations because there are frames lacking this property, it has several desirable side effects. For example, properties such as compactness, decidability and others can be shown to be preserved in a similar way and effective bounds for the size of models can be given. Moreover, all methods and proofs are constructive. (shrink)

A proof of Fermat’s last theorem is demonstrated. It is very brief, simple, elementary, and absolutely arithmetical. The necessary premises for the proof are only: the three definitive properties of the relation of equality (identity, symmetry, and transitivity), modus tollens, axiom of induction, the proof of Fermat’s last theorem in the case of n = 3 as well as the premises necessary for the formulation of the theorem itself. It involves a modification of Fermat’s approach of (...) infinite descent. The infinite descent is linked to induction starting from n = 3 by modus tollens. An inductive series of modus tollens is constructed. The proof of the series by induction is equivalent to Fermat’s last theorem. As far as Fermat had been proved the theorem for n = 4, one can suggest that the proof for n ≥ 4 was accessible to him. An idea for an elementary arithmetical proof of Fermat’s last theorem (FLT) by induction is suggested. It would be accessible to Fermat unlike Wiles’s proof (1995). (shrink)

Abstract The first fractal constructions appeared in mathematics in the second half of the 19th century. Their history is divided into two periods. The first period lasted 100 years and is a good example of the method of proofs and refutations discovered by Lakatos. The modern history of these objects started 20 years ago, when Mandelbrot decided to create fractal geometry, a general theory concentrated on specific properties of fractals. His approach has been surprisingly effective. The aim of this (...) paper is to examine the reasons for Mandelbrot's success and for the present popularity of fractals. They are now known not only in mathematics but also in many fields of natural, social and applied sciences, and even in the arts. (shrink)

Most metaphysicians deny that dispositions are among the fundamental constituents of the world. The solubility of salt, for example, is regarded as derivative from more basic features of reality, such as the molecular structure of salt and the laws of nature. This is an initially plausible view: a disposition seems to be essentially a characterization of what its bearer can do, which seems to be wholly dependent on what that bearer is like. ;Nonetheless, I think that the most attractive view (...) of dispositions is that they are fundamental constituents of reality---in fact, almost all real properties are irreducibly dispositional. Following D. M. Armstrong, I call this view dispositionalism. In my dissertation, I address several major difficulties for dispositionalism. For instance, it is often argued that dispositionalism makes causal relations necessary, and is thus committed to an unacceptable theory of causation. In response to this worry, I defend the thesis that causal relations are necessary. A second objection is based on C. B. Martin's "finkish" cases. It is widely accepted that some accounts of dispositions are able to escape this objection by adopting David Lewis's response to it. Contra Lewis, I argue that dispositionalism can follow in their footsteps. Finally, I consider the objection that dispositionalism, by implying that it is dispositions all the way down, leads to a vicious regress. I think that this is the most serious problem for dispositionalism, and although I do not fully lay it to rest, I make some headway. ;I also survey a wide range of competing theories of dispositions. I argue that the difficulties they face are both far greater than has been recognized, and more serious than the difficulties that beset dispositionalism. The result is not a conclusive proof of dispositionalism, but a demonstration that this underdog theory is preferable to its more popular competitors. (shrink)

This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax (...) that explicitly incorporates the semantics of the associated logic, and such systems typically violate the subformula property to a high degree. By contrast, nested sequent calculi employ a simpler syntax and adhere to a strict reading of the subformula property, making such systems useful in the design of automated reasoning algorithms. However, the downside of the nested sequent paradigm is that a general theory concerning the automated construction of such calculi (as in the labelled setting) is essentially absent, meaning that the construction of nested systems and the confirmation of their properties is usually done on a case-by-case basis. The refinement method connects both paradigms in a fruitful way, by transforming labelled systems into nested (or, refined labelled) systems with the properties of the former preserved throughout the transformation process. To demonstrate the method of refinement and some of its applications, we consider grammar logics, first-order intuitionistic logics, and deontic STIT logics. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics. Furthermore, we employ our refined labelled calculi for grammar logics to show that every logic in the class possesses the effective Lyndon interpolation property. (shrink)

The main purpose of this paper is to give alternative proofs of syntactical and semantical properties, i.e. the subformula property and the nite model property, of the sequent calculi for the modal logics K4.3, KD4.3, and S4.3. The application of the inference rules is said to be acceptable, if all the formulas in the upper sequents are subformula of the formulas in lower sequent. For some modal logics, Takano analyzed the relationships between the acceptable inference rules and semantical (...) class='Hi'>properties by constructing models. By using these relationships, he showed Kripke completeness and subformula property. However, his method is difficult to apply to inference rules for the sequent calculi for K4.3, KD4.3, and S4.3. Lookinglosely at Takano's proof, we nd that his method can be modied to construct nite models based on the sequent calculus for K4.3, if the calculus has and all the applications of the inference rules are acceptable. Similarly, we can apply our results to the calculi for KD4.3 and S4.3. This leads not only to Kripke completeness and subformula property, but also to finite model property of these logics simultaneously. (shrink)

As I have read the scholium, it divides into three main parts, not including the introductory paragraph. The first consists of paragraphs one to four in which Newton sets out his characterizations of absolute and relative time, space, place, and motion. Although some justificatory material is included here, notably in paragraph three, the second part is reserved for the business of justifying the characterizations he has presented. The main object is to adduce grounds for believing that the absolute quantities are (...) indeed distinct from their relative measures and are not reducible to them. Paragraph five takes this up for the case of time. Paragraphs eight to twelve endeavor to do this for rest and motion by appealing to their properties, causes and effects. In arguing that absolute motion is not reducible to any particular form of the relative motion of bodies with respect to one another, and thus, as is directly argued in the third argument, must be understood in terms of motionless places, Newton thereby constructs an indirect case that absolute space is indeed something distinct from any relative space. Paragraph thirteen functions as conclusion to this line of inquiry and comments on how, in the light of this, the names of these quantities are to be interpreted in the scriptures. The third and final part consists of paragraph fourteen alone, and addresses the question: given that true motion is motion with respect to absolute space, but the parts of the latter are not perceivable, is it possible for us to know the true motions of individual bodies? Newton illustrates how this may be done from the evidence provided by their apparent motions and the forces which are the causes and effects of true motion. This forms a bridge to the body of the work insofar as the purpose of the Principia, according to Newton, is to show how this, and the converse problem, of inferring true and apparent motions from the forces, can be dealt with.Part II of this paper will appear in the next issue of Studies in History and Philosophy of Science. (shrink)

The Löwenheim-Skolem theorem was published in Skolem's long paper of 1920, with the first section dedicated to the theorem. The second section of the paper contains a proof-theoretical analysis of derivations in lattice theory. The main result, otherwise believed to have been established in the late 1980s, was a polynomial-time decision algorithm for these derivations. Skolem did not develop any notation for the representation of derivations, which makes the proofs of his results hard to follow. Such a formal notation (...) is given here by which these proofs become transparent. A third section of Skolem's paper gives an analysis for derivations in plane projective geometry. To clear a gap in Skolem's result, a new conservativity property is shown for projective geometry, to the effect that a proper use of the axiom that gives the uniqueness of connecting lines and intersection points requires a conclusion with proper cases (logically, a disjunction in a positive part) to be proved. The forgotten parts of Skolem's first paper on the Löwenheim-Skolem theorem are the perhaps earliest combinatorial analyses of formal mathematical proofs, and at least the earliest analyses with profound results. (shrink)

The principle of publicity is one of the fundamental principles of property law: property rights should be made public in order to inform third parties about the existence of the property right and its holder and thereby to foster legal certainty and efficiency. The publicity of ownership in immovable property is achieved through registration of ownership in the public register. However, the problem arises because of the unavoidable discrepancies between the data contained in the public register and the factual situation. (...) Different states choose different models to solve the practical problems arising out of the aforementioned discrepancies. On the one hand, Lithuania belongs to the group of states that implement the so-called declaratory system of registration, i.e. the transfer of ownership is based on an agreement or other legal grounds and the registration is not mandatory but provides the transfer with a third-party effect. This can be seen as a proof of priority of a factual situation over the registered data. On the other hand, Lithuanian laws provide the data of the register with some positive reliance, i.e. third parties are not only protected from claims arising out of unregistered rights (negative reliance), but they can also rely on the transcripts in the register. This is especially true in the case of bona fide transferee of immovable property which with some minor exceptions acquires ownership even from a non-owner, if the latter honestly relied on the data of the register. This regulatory framework is further adopted and transformed by the case law of the Lithuanian courts. The analysis of the latter shows that courts are inclined to rely more on the factual situation and easily deny the meaning of the registered rights. In various ways, the concept of the bona fide transferee is restricted and there are instances of positive duties ascribed to them. Besides, the existing case law demonstrates equivocal attitude towards the legal effects of registered data. Such tendencies of case law may hinder the rule of positive reliance and cause greater legal uncertainty. (shrink)

We introduce the logic LRC, designed to describe and reason about agents’ abilities and capabilities in using resources. The proposed framework bridges two—up to now—mutually independent strands of literature: the one on logics of abilities and capabilities, developed within the theory of agency, and the one on logics of resources, motivated by program semantics. The logic LRC is suitable to describe and reason about key aspects of social behaviour in organizations. We prove a number of properties enjoyed by LRC (...) and its associated analytic calculus. These results lay at the intersection of the algebraic theory of unified correspondence and the theory of multitype calculi in structural proof theory. Case studies are discussed which showcase several ways in which this framework can be extended and enriched while retaining its basic properties, so as to model an array of issues, both practically and theoretically relevant, spanning from planning problems to the logical foundations of the theory of organizations. (shrink)

We present nested sequent systems for propositional Gödel-Dummett logic and its first-order extensions with non-constant and constant domains, built atop nested calculi for intuitionistic logics. To obtain nested systems for these Gödel-Dummett logics, we introduce a new structural rule, called the linearity rule, which (bottom-up) operates by linearising branching structure in a given nested sequent. In addition, an interesting feature of our calculi is the inclusion of reachability rules, which are special logical rules that operate by propagating data and/or checking (...) if data exists along certain paths within a nested sequent. Such rules require us to generalise our nested sequents to include signatures (i.e. finite collections of variables) in the first-order cases, thus giving rise to a generalisation of the usual nested sequent formalism. Our calculi exhibit favourable properties, admitting the height-preserving invertibility of every logical rule and the (height-preserving) admissibility of a large collection of structural and reachability rules. We prove all of our systems sound and cut-free complete, and show that syntactic cut-elimination obtains for the intuitionistic systems. We conclude the paper by discussing possible extensions and modifications, putting forth an array of structural rules that could be used to provide a sizable class of intermediate logics with cut-free nested sequent systems. (shrink)

A mahāvidyā inference is used for establishing another inference. Its Reason is normally an omnipresent property. Its Target is defined in terms of a general feature that is satisfied by different properties in different cases. It assumes that there is no case that has the absence of its Target. The main defect of a mahāvidyā inference μ is a counterbalancing inference that can be formed by a little modification of μ. The discovery of its counterbalancing inference can invalidate (...) such an inference. This paper will argue that Cantor’s diagonal argument too shares some features of the mahāvidyā inference. A diagonal argument has a counterbalanced statement. Its main defect is its counterbalancing inference. Apart from presenting an epistemological perspective that explains the disquiet over Cantor’s proof, this paper would show that both the mahāvidyā and diagonal argument formally contain their own invalidators. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Reviewed by:Does Judaism Condone Violence? Holiness and Ethics in the Jewish Tradition by Alan L. MittlemanMatthew LeveringDoes Judaism Condone Violence? Holiness and Ethics in the Jewish Tradition by Alan L. Mittleman (Princeton, NJ: Princeton University Press, 2018), v + 227 pp.Alan Mittleman has written a profoundly thought-provoking book. A main question of the book is whether a higher (revealed) law may in some cases require harm to be (...) done to the neighbor—harm that otherwise would be unjust. Mittleman offers some fascinating examples of cases in which Jews have appealed to God's Law in order to justify oppression of Gentiles. He cites a contemporary halakhic text, Torat ha-Melekh (The King's Torah), as particularly egregious. While Torat ha-Melekh was widely condemned by rabbis and the general public in Israel, it had an audience among the ultra-Orthodox. According to the Torat ha-Melekh, Gentiles' souls are not intrinsically holy in the way that Jews' souls are. This means that killing Gentile children in wartime may be acceptable due to the threat that otherwise these children may grow up to kill Jews. The Torat ha-Melekh observes that many Gentiles do not practice and obey the seven Noachide commandments. Since this is so, the Gentiles who do not obey the Noachide commandments live "in an inhuman state, where the brutish nature of their souls has free rein and their lives have lost value" (186).Another example given by Mittleman is the status of the Holy Land and the Holy People. Insofar as the holiness of the land and people is thought to be intrinsic—an inseparable property—problems can arise. According to a midrash in Bereshit Rabbah, the land is so intrinsically holy that only the dead who are buried in the land—or whose dead bodies somehow travel to the land—will rise from the dead and enjoy everlasting resurrected life. Likewise, the land's air is presented as uniquely making its inhabitants wise, and the divine presence or shekinah comes only in the land. For the medieval Jewish philosopher Yehuda Halevi, in his Kuzari: The Book of Refutation and Proof on Behalf of the Most Despised Religion (ca. 1140), the land of Israel is the most temperate climate and the most conducive to producing the ideal human beings. In addition, Halevi thinks that only certain descendants of Adam are "true Adamites" (66). A true Adamite is a son of God, just as Adam was. Specifically, only Seth and some of his descendants are fully human in accord with the Adamic model. It is only in the family of Jacob that "God's influence [finally] becomes the property of an entire people" (67). The true Adamites are Adam's (and Jacob's) seed; other humans are comparatively speaking mere husks. Although people can convert to Judaism, therefore, converts cannot be equal to those born of the Jewish nation. This does not mean that all who descend from Jacob are holy, since [End Page 745] it is possible for a Jew to distort his or her purity of soul. Nevertheless, for Halevi the Jewish people are a holy seed that is intrinsically superior to all other humans, so that it is possible to say that "Israel is an angelomorphic, even theomorphic race" (69).Moses Maimonides responded to Halevi, rejecting his viewpoint completely—on the grounds that holiness is not an intrinsic or biological (let alone racial) property. Yet, Halevi's viewpoint influenced Jewish Kabbalah in a major way. For the Kabbalist text the Zohar, the people of Israel derive from the emanations of the divine, whereas all other nations derive from the impure powers. The Zohar holds, "The other nations count for nothing in God's sight. They are the products of Eve's illicit union with the serpent," rather than coming forth from the theomorphic being who was Adam (70). Similarly, Moses de Leon—thought to be an author of the Zohar—argues that Gentiles ontologically possess impure souls that will carry them to spiritual damnation and will ensure that they have no participation in the resurrection of the dead. Another Kabbalist, Joseph of Hamadan, makes the same point that Gentiles... (shrink)

In lieu of an abstract, here is a brief excerpt of the content:176 BOOK REVIEWS tianity came into being. To take one example: God's involvement with and reaction to genuine novelties introduced into the world as a result of the initiatives of human freedom, rightly renders suspect the conception of God as immutable. But what immutability really claimed was not anything like inertia or unconcern, but only that God was not mutable in any of the ways characteristic of finite realities (...) striving to transcend their limitations. Immutability was predicated as a property of deity whose essence was Pure Actuality-the consummation of all mutation. What this meant to preclude from God was only change that amounted to some sort of further perfecting of his intrinsic being-leaving the way clear for the possibility at least of relational change vis-a-vis a world of creatures. There is no reason why contemporary experiences of God's saving activity in Christ must be articulated only in the conceptual and linguistic categories of the past. But seemingly there ought to be some means of showing that such newer articulations do not repudiate truths achieved in the past and handed on in authentic living tradition. The Catholic University of America Washington, D.C. WILLIAM J. HILL, 0.P. The Church: Communion, Sacrament, Communication. By ROBERT KRESS. New York: Paulist Press, 1985. Pp. iv + 217. $9.95. One of the results of the recent synod is certain to be more attention to deepening our understanding of the church as communion. Robert Kress's fine volume cannot help but be a useful contribution to that discussion. As he succinctly states, "the Church is the communion of believers who exist as the sacrament of Christ, who is the sacrament of God, who is the communion of Father, Son, and Holy Spirit" (p. 59). For Kress any ecclesiology that does not root the church in the triune, perichoretic (a favored word) life of God is a radically truncated one. As a theandric (another favored word) reality, the Church must mirror its ground or source. If that ground is a dynamic, joyous unity-in-diversity, this should be reflected in the life and structures of the ecclesial community. Such is the context in which the author reflects on a variety of themes that are reflective of the post-Vatican II agenda: the relationship among local, regional, and universal churches; the understanding of the church as sacrament; the tension between holiness and office; the meaning of leadership in a community best understood as a perichoretic communion of gifted members. To each of these topics Kress brings a grasp of the BOOK REVIEWS 177 tradition, a wide acquaintance with the relevant theological literature, and a willingness to make provocative judgments ("yes" to the ordination of women; " no " to the new egalitarianism-a church conceived without administrative, pastoral authority.) Kress particularly cherishes the church as "the memory and tradition of Christ." His commitment to this tradition has both rooted him and freed him. He draws knowledgeably on Aquinas and Augustine, Rahner and Heidegger, von Balthasar and the Shepherd of Hermas. Lawrence Cunningham is correct: this book is radically conservative. There is one area where I felt that there was a certain lack. Kress's treatment of the church as sacrament and of the seven sacraments contained much that was valuable: his stress on the sacramentality of ecclesial life as such, his historical analysis of "sacrament", his phenomenolog·y of the nature of Christian worship. Yet all of this seemed strangely abstracted from the liturgical praxis of the Christian community. This lack is especially visible in his admittedly tentative salvation-historical correlation of the sacraments with our sharing in the religious experience of Jesus (pp. 147-148). To make that correlation, especially in the case of Baptism, Confirmation, and Eucharist, without an exp1icit reference to the initiatory, communal dimension of these sacraments is certainly problematic. I would like to make a final comment, not on the substance of the book, but on its editing and proofing. There are a number of errors, the most obvious of which is the elimination of the umlaut from Heribert Miihlen's name. (There is a curious inconsistency, too, in the use of the umlaut. It is used in... (shrink)

In the course of his painstaking study of ancient verse, Ferdinand de Saussure came up with an intriguing theory about the phonetics of the poetry he scrutinised. He postulated that the “jeux phoniques” he detected in the texts he analysed was proof that their authors were attempting to “parasite” the surface level meaning of their verse with a “hypotexte.” This hypotexte consisted of “anagrams” of “mots thèmes” whose phonetic properties were “isosyllabically diffracted” throughout the rest of the host (...) text. Today it is generally accepted that Saussure was wrong about this. Few however maintain that what he discerned in the phonetic depths of the verse he auscultated was no more than the figment of a fertile imagination. But if this be so, what exactly had he detected? This paper maintains that what Saussure stumbled upon was the trace of a contribution made to ancient verse by melodically and metrically organised sounds. This was inevitable. Virtually all the texts he probed were “carmina sacra” that were composed to be sung and accompanied by music. This musical accompaniment had a decisive impact on the phonetics of the “lexemic” words in the Poetry that has survived. This is so because sung verse cannot “euphoniously” accommodate a musical accompaniment unless its phonetics constituents are selected, concatenated and intoned in such a way as to follow the melodic contours and rhythm patterns that modulate their articulation. In addition, the point of making verse consist both of melodically organised arrangements of sound and of organisations of sound in which one can recognise ordinary words was not simply ornamental. The real point was to bi-nature what one was hearing. In other words, the goal was to “over-signify” the usual meanings of the “logocentric” words in the verse with a separate but complementary meaning and narrative encoded in melodised tones and metered rhythms. Why qualify the accompanying music as “acousmatic voices”? Because the music in question was added to song to give a voice to whichever tutelary divinity the song was performed to honour. That’s what makes “acousmatic voices” an especially apt epithet for characterising the melodically and rhythmically structured bodies of sound Saussure so presciently discerned in the phonetic depths of the poésie phonisante he probed. The point of their being in poetry was to give a voice to the agencies to whom the object or occasion of verse is beholden for its Being-in-the-world. (shrink)

The role played by the symmetric structure of a group of finite Morley rank without involutions in the proof by contradiction of Frécon 2018 was put in evidence in Poizat 2018; indeed, this proof consists in the construction of a symmetric space of dimension two (“a plane”), and then in showing that such a plane cannot exist.To a definable symmetric subset of such a group are associated symmetries and transvections, that we undertake here to study in the abstract, (...) without mentioning a group envelopping them. This leads us to consider axiomatically defined structures that we callsymmetrons(preferably todyadic symmetric setsas was done in Lawson & Lim 2004).Glauberman's$Z^*$-Theorem allows to elucidate completely the structure of the finite symmetrons: each of them is isomorphic to the set of symmetries associated to a symmetric subspace of a finite group without involutions, which is far from being uniquely determined. In fact, there exist non-isomorphic finite groups which have the same symmetries, and also finite symmetrons which are not isomorphic to the symmetries of a group.The situation is not so clear in the case of symmetrons of finite Morley rank, or even algebraic, which are the main objects of study of this paper. But in spite of the fact that a symmetron be a structure much weaker that a group, we can extend to symmetrons some well-known results concerning groups of finite Morley rank: chain condition, decomposition into connected components, characterisation of the generic definable subsets, elliptic generation, etc. These properties are new even in the case of a symmetric subspace of a group, and allow to bypass the computations made by Frécon during the construction of his paradoxical plane.Moreover, assuming the Algebricity Conjecture, we generalize Glauberman's Theorem to the finite Morley rank context. (shrink)

In this paper we see that the answer of this question is affirmative. We prove this for Dco-algebras and as special case we obtain the result for Positive Implication algebras. First we give, without proof, the properties of Dco-algebras and S-algebras and their connection with Positive Implication algebras and Implication algebras. These results can be found in [T] and [IT].

Background: SNOMED CT is a large terminology system designed to represent all aspects of healthcare. Its current form and content result from decades of bottom-up evolution. Due to SNOMED CT’s formal descriptions, it can be considered an ontology. The Basic Formal Ontology (BFO) is a foundational ontology that proposes a small set of disjoint, hierarchically ordered classes, supported by relations and axioms. In contrast, as a typical top-down endeavor, BFO was designed as a foundational framework for domain ontologies in the (...) natural sciences and related disciplines. Whereas it is mostly assumed that domain ontologies should be created as extensions of foundational ontologies, a post-hoc harmonization of consolidated domain ontologies in use, such as SNOMED CT, is known to be challenging. Methods: We explored the feasibility of harmonizing SNOMED CT with BFO, with a focus on the SNOMED CT Clinical Finding hierarchy. With more than 100,000 classes, it accounts for about one third of SNOMED CT’s content. In particular, we represented typical SNOMED CT finding/disorder concepts using description logics under BFO. Three representational patterns were created and the logical entailments analyzed. Results: Under a first scrutiny, the clinical intuition that diseases, disorders, signs and symptoms form a homogeneous ontological upper-level class appeared incompatible with BFO’s upper-level distinction into continuants and occurrents. The Clinical finding class seemed to be an umbrella for all kinds of entities of clinical interest, such as material entities, processes, states, dispositions, and qualities. This suggests the conclusion that Clinical finding would not be a suitable upper-level class from an BFO perspective. On closer inspection of the taxonomic links within this hierarchy and the implicit meaning derived thereof, it became clear that Clinical finding classes do not characterize the entity (e.g. a fracture, allergy, tumor, pain, hemorrhage, seizure, fever) in a literal sense but rather the condition of a patient having that fracture, allergy, pain etc. This gives sense to the current characteristic of the Clinical Finding hierarchy, in which complex classes are modeled as subclasses of their constituents. Most of these taxonomic links are inferred, as the consequence of the ‘role group’ design pattern, which is ubiquitous in SNOMED CT and has often been subject of controversy regarding its semantics. Conclusion: Our analyses resulted in the proposal of (i) equating SNOMED CT’s ‘role group’ property with the reflexive and transitive BFO relation ‘has occurrent part’; and (ii) reinterpreting Clinical Findings as Clinical Occurrents, i.e. temporally extended entities in an organism, having one or more occurrents as temporal parts that occur in continuants. This re-interpretation was corroborated by a manual analysis of classes under Clinical Finding, as well as the identification of similar modeling patterns in other ontologies. As a result, SNOMED CT does not require any content redesign to establish compatibility with BFO, apart from this re-interpretation, and a suggested re-labeling. Regarding the feasibility of harmonizing terminologies with principled foundational ontologies post-hoc, our results provide support to the assumption that this does not necessarily require major redesign efforts, but rather a careful analysis of the implicit assumptions of terminology curators and users. (shrink)

This paper investigates some delicate tradeoffs between the generality of an algorithmic learning device and the quality of the programs it learns successfully. There are results to the effect that, thanks to small increases in generality of a learning device, the computational complexity of some successfully learned programs is provably unalterably suboptimal. There are also results in which the complexity of successfully learned programs is asymptotically optimal and the learning device is general, but, still thanks to the generality, some of (...) those optimal, learned programs are provably unalterably information deficient—in some cases, deficient as to safe, algorithmic extractability/provability of the fact that they are even approximately optimal. For these results, the safe, algorithmic methods of information extraction will be by proofs in arbitrary, true, computably axiomatizable extensions of Peano Arithmetic. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:BOOK REVIEWS 755 preaching. The question posed by Richard Kieckhefer whether the mystical birth of the Word in the soul can be considered to be a conscious event (discussed briefly on p. 191) may not be capable of satisfactory resolution in terms of modern psychology, especially pop psychology. But there is ample evidence in Eckhart's own words (cf. Sermons DW 10 and DW 68) that awareness must accompany such (...) a breakthrough to be fully human, even if the awareness itself is not the source of bliss. The preceding misgivings notwithstanding, I consider Frank Tobin's book to be a major contribution by a serious scholar in the field, a necessary adjunct in the rapidly growing number of vcolumes in the field of Eckhart studies. As a primer of scholastic thought and language, it.fa an excellent introductory text, especially for readers unfamiliar with the area. And, despite Tobin's modest reservations, even medieval Germanists and Eckhart specialists will find much in it of value. It is a book that can be consulted thoughtfully 1and 1 even freqently with pl'ofit. Loyola University of Chicago Chicago, Illinois RICHARD WooDs, O.P. The Virtue of Faith and Other Essays in Philosophical Theology. By ROBERT MERRIHEW ADAMS. New York and Oxford: Oxford University Press, 1987. Pp. 270. This impressive volume includes most of the material on the philosophy of religion that the author has published in the last fifteen years, together with some additional items. Philosophy of religion has close links with other areas of philosophy, for instance metaphysics, epistemology, ethics, and the philosophy of mind; and several papers argue that theistic belief consorts well with otherwise acceptable positions in these areas. The author roundly contests the view that has recently been in vogue, that there is no matter of fact about the existence and nature of God, and that as a consequence human religious phenomena are the only religious subject matter available for such studies as are to claim academic respectability. He is vehemently 'realist' in this matter. Whatever our beliefs about the issue, he insists, God exists or does not exist, is omnipotent or is not omnipotent, and so forth. The author's realism is combined with what he sees as a moderate scepticism. It is liable to be objected that scepticism naturally and inevitably leads to subjectivism and anti-realism, but this, according to 756 BOOK REVIEWS the author, is a mistake. After all, the assumption, made by persons of common sense and by most philosophers, that physical objects exist and have the properties that they do have independently of our perceiving and thinking about them, implies that there is a gap between objects and our apprehensions of them, which is such that we can never he totally certain of their reality by way of any possible experience. 'This gap inevitably introduces a greater or smaller degree of unprovability into our beliefs about the objectively real. Realism thus goes naturally with some kind of scepticism, and with a need for faith.' This consorts well with the author's view that in matters of religion, as in most matters of concern to philosophers, conclusive proof is impossible, for all that beliefs on these topics may he more or less reasonable, and firm convictions may be appropriate. Thus, while there are no knock-down proofs for the existense of God, the traditional arguments have, and deserve to have, some persausive force, especially when considered cumulatively. Most of the papers here are meant to contribute at least indirectly to such a cumulative case for the existence of God, clearing away some objection, or putting some aspect of theistic belief in a more favorable light than that in which it often appears. The hook is divided into four sections, on faith, the problem of evil, God and ethics, and the metaphysics of theism. While all of the papers display admirable learning and philosophical skill, I was particularly intrigued by the last one, 'Flavors, Colors and God'. Here it is argued, following Descartes and Locke, that the best explanation of the manner in which phenomenal qualia are apparently related to physical properties is a theological one. Elsewhere, Anselm's arguments are formalized with dazzling... (shrink)

It is argued that the truth status of emergent properties of complex adaptive systems models should be based on an epistemology of proof by constructive verification and therefore on the ontological axioms of a non-realist logical system such as constructivism or intuitionism. ‘Emergent’ properties of complex adaptive systems models create particular epistemological and ontological challenges. These challenges bear directly on current debates in the philosophy of mathematics and in theoretical computer science. CAS research, with its emphasis on (...) computer simulation, is heavily reliant on models which explore the entailments of Formal Axiomatic Systems. The incompleteness results of G¨odel, the incomputability results of Turing, and the Algorithmic Information Theory results of Chaitin, undermine a realist truth model of emergent properties. These same findings support the hegemony of epistemology over ontology and point to alternative truth models such as intuitionism, constructivism and quasi-empiricism. (shrink)

In recent years, new forms of transnational regulation have emerged, filling the void created by the failure of governments and international institutions to effectively regulate transnational corporations. Among the variety of initiatives addressing social and environmental problems, a growing number of certification systems have appeared in various sectors, particularly agrifood. Most initiatives rely on independent third-party certification to verify compliance with a standard, as it is seen as the most credible route for certification. The effects of third-party audits, however, still (...) need to be empirically investigated. This article provides a critical assessment of the notion of ‘evidence’ which is at the heart of auditing practices. It focuses on the case of the Roundtable on Sustainable Palm Oil (RSPO) and fieldwork carried out in Indonesia, the world’s largest producer of palm oil. In this country, some non-governmental organizations decided to participate in the RSPO in order to use this platform to tackle the issue of land conflicts. They managed to include important clauses regarding indigenous and land rights in the RSPO standard. In practice, however, auditors rarely recognize as valid evidence the forms of proof put forward by local communities. As a result, the whole process risks compounding local power imbalances. (shrink)

This essay discusses the instructional value of mathematical proofs using different interpretations of the analysis cum synthesis method in Apollonius’ Conics as a case study. My argument is informed by Descartes’ complaint about ancient geometers and William Thurston’s discussion on how mathematical understanding is communicated. Three historical frameworks of the analysis/synthesis distinction are used to understand the instructive function of the analysis cum synthesis method: the directional interpretation, the structuralist interpretation, and the phenomenological interpretation. I apply these interpretations to the (...) analysis cum synthesis method in order reveal how the same underlying mathematical activity occurs at different levels of scale: at the level of an individual proof, at the level of a collection of proofs, and at the level of a single line within a proof. On the basis of this investigation, I argue that the instructive value of mathematical proof lies in engendering in the reader the same mathematical activity experienced by the author themselves. (shrink)

A generator program for a computable function (by definition) generates an infinite sequence of programs all but finitely many of which compute that function. Machine learning of generator programs for computable functions is studied. To motivate these studies partially, it is shown that, in some cases, interesting global properties for computable functions can be proved from suitable generator programs which cannot be proved from any ordinary programs for them. The power (for variants of various learning criteria from the (...) literature) of learning generator programs is compared with the power of learning ordinary programs. The learning power in these cases is also compared to that of learning limiting programs, i.e., programs allowed finitely many mind changes about their correct outputs. (shrink)

This article is a methodological discussion of formal approaches to the question of identity of proofs from a philosophical standpoint. First, an introduction to the question of identity of proofs itself is given, followed by a brief reconstruction of the so-called normalisation thesis, proposed by Dag Prawitz in 1971, in which some of its core mathematical and conceptual traits are presented. After that, a comparison between the normalisation thesis and the more well-known Church-Turing thesis on computability is carried out in (...) three main parts: the first dedicated to highlighting some of the analogies between them; the second, their most remarkable differences; and the third, to the possible relations of dependence between the two. Based on these considerations, some concluding remarks concerning the potential of the normalisation thesis and similar approaches to the question of identity of proofs are made in the last section. (shrink)

ABSTRACT In our response Field's ‘Properties, Propositions and Conditionals’, we explore the methodology of Field's program. We begin by contrasting it with a proof-theoretic approach and then commenting on some of the particular choices made in the development of Field's theory. Then, we look at issues of property identity in connection with different notions of equivalence. We close with some comments relating our discussion to Field's response to Restall’s [2010] ‘What Are We to Accept, and What Are We (...) to Reject, While Saving Truth from Paradox?’. (shrink)

Full proofs of the Gödel incompleteness theorems are highly intricate affairs. Much of the intricacy lies in the details of setting up and checking the properties of a coding system representing the syntax of an object language (typically, that of arithmetic) within that same language. These details are seldom illuminating and tend to obscure the core of the argument. For this reason a number of efforts have been made to present the essentials of the proofs of Gödel’s theorems without (...) getting mired in syntactic or computational details. One of the most important of these efforts was made by Löb [8] in connection with his analysis of sentences asserting their own provability. Löb formulated three conditions (now known as the Hilbert-Bernays-Löb derivability conditions), on the provability predicate in a formal system which are jointly sufficient to yield the Gödel’s second incompleteness theorem for it. A key role in Löb’s analysis is played by (a special case of) what later became known as the diagonalization or fixed point property of formal systems, a property which had already, in essence, been exploited by Gödel in his original proofs of the incompleteness theorems. The fixed point property plays a central role in Lawvere’s [7] category-theoretic account of incompleteness phenomena (see also [10]). Incompleteness theorems have also been subjected to intensive investigation within the framework of modal logic (see, e.g.[4], [5]). In this formulation the modal operator takes up the role previously played by the provability predicate, and the derivability conditions on the latter are translated into algebraic conditions (the so-called GL, i.e., Gödel–Löb, conditions) on the former. My purpose here is to present a framework for incompleteness phenomena, fully compatible with intuitionistic or constructive principles, in which the idea of a coding system is retained, only in a 2 simple, but very general form, a form wholly free of syntactical notions. As codes we shall take the elements of an arbitrary given nonempty set, possibly, but not necessarily, the set of natural numbers.. (shrink)

The author has previously shown that for a certain class of structures $\mathcal {I}$, $\mathcal {I}$-indexed indiscernible sets have the modeling property just in case the age of $\mathcal {I}$ is a Ramsey class. We expand this known class of structures from ordered structures in a finite relational language to ordered, locally finite structures which isolate quantifier-free types by way of quantifier-free formulas. This result is applied to give new proofs that certain classes of trees are Ramsey. To aid this (...) project we develop the logic of EM-types. (shrink)

Definitionally: _strongly effectively immune_ sets are infinite and their c.e. subsets have _maximums_ effectively bounded in their c.e. indices; whereas, for _effectively immune_ sets, their c.e. subsets’ _cardinalities_ are what’re effectively bounded. This definitional difference between these two kinds of sets is very nicely paralleled by the following difference between their _complements_. McLaughlin: _strongly_ effectively immune sets can_not_ have _immune complements_; whereas, the main theorem herein: _effectively_ immune sets can_not_ have _hyperimmune complements_. Ullian: _effectively_ immune sets _can_ have _effectively_ immune (...) complements. The main theorem _improves_ Arslanov’s, effectively hyperimmune sets can_not_ have _effectively_ hyperimmune complements: the _improvement_ omits the second ‘_effectively_’. Two _natural_ examples of _strongly effectively immune_ sets are presented with new cases of the first proved herein. The first is the set of minimal-Blum-size programs for the partial computable functions; the second, the set of Kolmogorov-random strings. A proved, _natural_ example is presented of an _effectively dense simple_, _not_ strongly effectively simple set; its complement is a set of maximal run-times. Further motivations for this study are presented. _Kleene_ recursion theorem proofs herein emphasize how to conceptualize them. Finally, is suggested, future, related work—illustrated by a first, _natural_, _strongly effectively_ \(\Sigma _2^0\) -_immune set_—included: solution of an open problem from Rogers’ book. (shrink)

Progressions of iterated reflection principles can be used as a tool for the ordinal analysis of formal systems. We discuss various notions of proof-theoretic ordinals and compare the information obtained by means of the reflection principles with the results obtained by the more usual proof-theoretic techniques. In some cases we obtain sharper results, e.g., we define proof-theoretic ordinals relevant to logical complexity Π1 0 and, similarly, for any class Π n 0 . We provide a more (...) general version of the fine structure relationships for iterated reflection principles (due to U. Schmerl [25]). This allows us, in a uniform manner, to analyze main fragments of arithmetic axiomatized by restricted forms of induction, including IΣ n , IΣ n − , IΠ n − and their combinations. We also obtain new conservation results relating the hierarchies of uniform and local reflection principles. In particular, we show that (for a sufficiently broad class of theories T) the uniform Σ1-reflection principle for T is Σ2-conservative over the corresponding local reflection principle. This bears some corollaries on the hierarchies of restricted induction schemata in arithmetic and provides a key tool for our generalization of Schmerl's theorem. (shrink)