Online research in philosophy

We give a simple and direct proof that super-consistency implies the cut-elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with the cut-elimination theorems in higher-order logic that involve V-complexes.

The antireductionist arguments of many philosophers (e.g., Baker, Fodor and Davidson) are motivated by a worry that successful reduction would eliminate rather than conserve the mental. This worry derives from a misunderstanding of the empiricist account of reduction, which, although it does not underwrite "cognitive suicide", should be rejected for its positivist baggage. Philosophy of psychology needs more detailed attention to issues in natural science which serve as analogies for reduction of the mental. I consider a range of central cases, (...) including water and H 2 O, genes and DNA, and common sense and scientific solidity. The last case is illuminated by Eddington's Two Tables paradox, a resolution which suggests the plasticity of the mental under reduction. If reduction of the mental is like any of these cases, it is neither empiricist nor eliminative. (shrink)

Do we conduct our conscious propositional thinking in natural language? Or is such language only peripherally related to human conscious thought-processes? In this paper I shall present a partial defence of the former view, by arguing that the only real alternative is eliminativism about conscious propositional thinking. Following some introductory remarks, I shall state the argument for this conclusion, and show how that conclusion can be true. Thereafter I shall defend each of the three main premises in turn.

Inferentialism claims that expressions are meaningful by virtue of rules governing their use. In particular, logical expressions are autonomous if given meaning by their introduction-rules, rules specifying the grounds for assertion of propositions containing them. If the elimination-rules do no more, and no less, than is justified by the introduction-rules, the rules satisfy what Prawitz, following Lorenzen, called an inversion principle. This connection between rules leads to a general form of elimination-rule, and when the rules have this form, (...) they may be said to exhibit “general-elimination” harmony. Ge-harmony ensures that the meaning of a logical expression is clearly visible in its I-rule, and that the I- and E-rules are coherent, in encapsulating the same meaning. However, it does not ensure that the resulting logical system is normalizable, nor that it satisfies the conservative extension property, nor that it is consistent. Thus harmony should not be identified with any of these notions. (shrink)

Aside from brute force, there are several philosophically respectable ways of eliminating the mental. In recent years the most popular elimination strategy has been directed against our common sense or folk psychological understanding of the mental. The strategy goes by the name of eliminative materialism (or eliminativism, in short). The motivation behind this strategy seems to be the following. If common sense psychology can be construed as the principled theory of the mental, whose vocabulary and principles implicitly define what (...) counts as mental, then eliminating the theory is eliminating its subject matter. If the theory is shown to be false, then its subject matter does not exist. If, in other words, common sense psychology can be shown to describe and explain nothing real in human cognition, then the mental itself is a fiction. (shrink)

Two central and well-known philosophical goals of the logical empiricists are the unification of science and the elimination of metaphysics. I argue, via textual analysis, that these two apparently distinct planks of the logical empiricist party platform are actually intimately related. From the 1920’s through 1950, one abiding criterion for judging whether an apparently declarative assertion or descriptive term is metaphysical is that that assertion or term cannot be incorporated into a language of unified science. I explore various versions (...) of this criterion throughout the works of Carnap and Neurath. (shrink)

The Elimination of Morality poses a fundamental challenge to the dominant conception of medical ethics. In this controversial and timely study, Anne Maclean addresses the question of what kind of contribution philosophers can make to the discussion of medico-moral issues and the work of health care professionals. She establishes the futility of bioethics by challenging the conception of reason in ethics which is integral to the utilitarian tradition. She argues that a philosophical training confers no special authority to make (...) pronouncements about moral issues, and proposes that pure utilitarianism eliminates the essential ingredients of moral thinking. Maclean also exposes the inadequacy of a utilitarian account of moral reasoning and moral life, dismissing the claim that reason demands the rejection of special obligations. She argues that the utilitarian drive to reduce rational moral judgment to a single form is ultimately destructive of moral judgment as such. This vital discussion of the nature of medical ethics and moral philosophy will be important reading for anyone interested in the fields of health care ethics and philosophy. (shrink)

In his paper “Generalised Ortho Negation” [2] J. Michael Dunn mentions a claim of mine to the effect that there is no condition on ‘perp frames’ equivalent to the holding of double negation elimination ∼∼A A. That claim is wrong. In this paper I correct my error and analyse the behaviour of conditions on frames for negations which verify a number of different theses.1..

Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cut-elimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations of the systems considered can be presented as (...) encodings of Kripke-style formulations. (shrink)

Second-order quantifier elimination in the context of classical logic emerged as a powerful technique in many applications, including the correspondence theory, relational databases, deductive and knowledge databases, knowledge representation, commonsense reasoning and approximate reasoning. In the current paper we first generalize the result of Nonnengart and Szałas [17] by allowing second-order variables to appear within higher-order contexts. Then we focus on a semantical analysis of conditionals, using the introduced technique and Gabbay’s semantics provided in [10] and substantially using a (...) third-order accessibility relation. The analysis is done via finding correspondences between axioms involving conditionals and properties of the underlying third-order relation. (shrink)

Animalism is the view that we are animals: living, breathing, wholly material beings. Despite its considerable appeal, animalism has come under fire. Other philosophers have had much to say about objections to animalism that stem from reflection on personal identity over time. But one promising objection (the `Elimination Argument') has been overlooked. In this paper, I remedy this situation and examine the Elimination Argument in some detail. I contend that the Elimination Argument is both unsound and unmotivated.

S4C is a logic of continuous transformations of a topological space. Cut elimination for it requires new kind of rules and new kinds of reductions.

Schwartz (1991) argues that the worry that successful reduction would eliminate rather than conserve the mental is a needless worry. He examines cases of reduction from the natural sciences and claims that if reduction of the mental is like any of those cases then it would not be a case of elimination. I discuss other cases of scientific reduction which do involve elimination. Schwartz has not shown that reduction of the mental could not be like such cases, so (...) his argument is not sufficient to dispel the worry of elimination. (shrink)

We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present (...) a proof search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search. (shrink)

We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.

Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed (...) as special cases of the cut-elimination theorems for intuitionistic logic. (shrink)

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.

According to Wimsatt, a proper treatment of reduction must distinguish between two types of reductionist activities scientists engage in. One of the benefits of better understanding the nature of reduction, he believes, is that it shows that eliminativism, that is, the elimination of concepts and theories from science, is a rather circumscribed and limited affair, especially in the case of inter-level reductionist activities. While I agree with Wimsatt that it is important to distinguish the two types of reductionisms, I (...) show that elimination in inter-level reductionist activities can be a powerful heuristic in science, driving both inter-level and successional reduction. (shrink)

Abstract Evolutionary epistemologists from Popper to Campbell have appropriated the Darwinian principle to explain the apparent fit between the world and our knowledge of it. I argue that this strategy suffers from the lack of any principled distinction among various types of elimination. I offer such a distinction and show that there is a species of elimination that is really corrective, that is, which violates the Darwinian principle as Popper understands it.

A common aim of elimination problems for languages of logic is to express the entire content of a set of formulas of the language, or a certain part of it, in a way that is more elementary or more informative. We want to bring out that as the languages for logic grew in expressive power and, at the same time, our knowledge of their expressive limitations also grew, elimination problems in logic underwent some change. For languages other than (...) that for monadic second-order logic, there remain important open problems. (shrink)

The importance of the connotation theory in Ockham’s semantics and metaphysics can hardly be overstated---it is the main mechanism that brings forth Ockham’s famous ontological elimination. Yet none of the extant interpretations can satisfactorily accommodate three widely accepted theses: (1) there is no synonym in mental language; (2) a connotative term has a semantically equivalent nominal definition; and (3) there are simple connotative terms in Ockham’s mental language. In this paper I offer an interpretation that I argue can accommodate (...) all. (shrink)

In 1983, Valentini presented a syntactic proof of cut elimination for a sequent calculus GLSV for the provability logic GL where we have added the subscript V for “Valentini”. The sequents in GLSV were built from sets, as opposed to multisets, thus avoiding an explicit contraction rule. From a syntactic point of view, it is more satisfying and formal to explicitly identify the applications of the contraction rule that are ‘hidden’ in these set based proofs of cut elimination. (...) There is often an underly ing assumption that the move to a proof of cut elimination for sequents built from multisets is easy. Recently, however, it has been claimed that Valentini’s arguments to eliminate cut do not terminate when applied to a multiset formulation of GLSV with an explicit rule of contraction. The claim has led to much confusion and various authors have sought new proofs of cut elimination for GL in a multiset setting. Here we refute this claim by placing Valentini’s arguments in a formal setting and proving cut elimination for sequents built from multisets. The formal setting is particularly important for sequents built from multisets, in order to accurately account for the interplay between the weakening and contraction rules. Furthermore, Valentini’s original proof relies on a novel induction parameter called “width” which is computed ‘globally’. It is diffi cult to verify the correctness of his induction argument based on “width”. In our formulation however, verification of the induction argument is straight forward. Finally, the multiset setting also introduces a new complication in the the case of contractions above cut when the cut formula is boxed. We deal with this using a new transformation based on Valentini’s original arguments. Finally, we show that the algorithm purporting to show the non termi nation of Valentini’s arguments is not a faithful representation of the original arguments, but is instead a transformation already known to be insufficient. (shrink)

A non-effective cut-elimination proof for modal mu-calculus has been given by G. Jäger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M 1 with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M 1 without restriction to positive sequents.

Behind this question are two fundamentally different approaches about how to reason with chance hypotheses. One approach, due to Ronald Fisher, rejects a chance hypothesis provided sample data appear in a prespecified rejection region. The other, due to Thomas Bayes, rejects a chance hypothesis provided an alternative hypothesis confers a bigger probability on the data in question than the original hypothesis. In the Fisherian approach, chance hypotheses are rejected in isolation for rendering data too improbable. In the Bayesian approach, chance (...) hypotheses are eliminated provided some other hypotheses render the data more probable. Whereas in the Fisherian approach the emphasis is on elimination, in the Bayesian approach the emphasis is on comparison. These approaches are incompatible, and the statistical community itself is deeply riven over which of these approaches to adopt as the right canon for statistical rationality. The difference reflects a deep divergence in fundamental intuitions about the nature of statistical rationality and in particular about what counts as statistical evidence. (shrink)

We consider T -round elimination tournaments where players have fixed resources instead of cost functions. We show that players always spend a higher share of their resources in early than in later rounds in a symmetric equilibrium. Equal resource allocation across T rounds takes place only in the winner-take-all case. Applications for career paths, elections, and sports are discussed.

We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille (...) completion. Moreover, the finite model property is obtained for many cases, by modifying our completeness proof. This is an algebraic presentation of the proof of the finite model property discussed by Lafont [12] and Okada-Terui [17]. (shrink)

We give an answer to the question as to whether quantifier elimination is possible in some infinite algebraic extensions of Qp (‘infinite p-adic fields’) using a natural language extension. The present paper deals with those infinite p-adic fields which admit only tamely ramified algebraic extensions (so-called tame fields). In the case of tame fields whose residue fields satisfy Kaplansky’s condition of having no extension of p-divisible degree quantifier elimination is possible when the language of valued fields is extended (...) by the power predicates Pn introduced by Macintyre and, for the residue field, further predicates and constants. For tame infinite p-adic fields with algebraically closed residue fields an extension by Pn predicates is sufficient. (shrink)

Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it (...) is harder to design cut elimination procedures. In this paper we see a cut elimination procedure for a deep inference system for classical predicate logic. As a consequence we derive Herbrand's Theorem, which we express as a factorisation of derivations. (shrink)

Via the formulas-as-types embedding certain extensions of Heyting Arithmetic can be represented in intuitionistic type theories. In this paper we discuss the embedding of ω-sorted Heyting Arithmetic HA ω into a type theory WL, that can be described as Troelstra's system ML 1 0 with so-called weak Σ-elimination rules. By syntactical means it is proved that a formula is derivable in HA ω if and only if its corresponding type in WL is inhabited. Analogous results are proved for Diller's (...) so-called restricted system and for a type theory based on predicate logic instead of arithmetic. (shrink)

An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence (...) to characterize strong cutelimination in such systems. We show that the following properties of a canonical system G with arbitrary (n, k)-ary quantifiers are equivalent: (i) G is coherent, (ii) G admits strong cut-elimination, and (iii) G has a strongly characteristic two-valued generalized non-deterministic matrix. In addition, we define simple calculi, an important subclass of canonical calculi, for which coherence is equivalent to the weaker, standard cut-elimination property. (shrink)

We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.

This work presents a model-theoretic approach to the study of first-order theories of classes of BL-chains. Among other facts, we present several classes of BL-algebras, generating the whole variety of BL-algebras, whose first-order theory has quantifier elimination. Model-completeness and decision problems are also investigated. Then we investigate classes of BL-algebras having (or not having) the amalgamation property or the joint embedding property and we relate the above properties to the existence of ultrahomogeneous models.

The Joint Non-Trivialization Theorem, two Definability Theorems and the generalized Quantifier Elimination Theorem are proved for J 3-theories. These theories are three-valued with more than one distinguished truth-value, reflect certain aspects of model type logics and can. be paraconsistent. J 3-theories were introduced in the author's doctoral dissertation.

In this paper we investigate the connections between quantifier elimination, decidability and Uniform Craig Interpolation in Δ-core fuzzy logics added with propositional quantifiers. As a consequence, we are able to prove that several propositional fuzzy logics have a conservative extension which is a Δ-core fuzzy logic and has Uniform Craig Interpolation.

Let TP be the theory obtained by adding a generic predicate to an o-minimal theory T. We prove that if T admits elimination of imaginaries, then TP also admits elimination of imaginaries.

We develop an elimination theory for addition and the Frobenius map over rings of polynomials. As a consequence we show that if F is a countable. recursive and perfect field of positive characteristic p, with decidable theory, then the structure of addition, the Frobenius map x $\rightarrow$ $x^{p}$ and the property 'x $\epsilon$ F', over the ring of polynomials F[T]. has a decidable theory.

An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence (...) to characterize strong cutelimination in such systems. We show that the following properties of a canonical system G with arbitrary (n, k)-ary quantifiers are equivalent: (i) G is coherent, (ii) G admits strong cut-elimination, and (iii) G has a strongly characteristic two-valued generalized non-deterministic matrix. (shrink)

In order to reach a better understanding of brain function, conceptual synergies linking empirical neurobiological studies and neurocomputational studies should be pursued. I describe an example of a potential synergy based on studies of neural network pruning. Simulations demonstrate that selective elimination of connections enhances the computational capacity of networks capable of temporal processing. These findings may shed light on the functional significance of postnatal neuro-developmental pruning of cortical connections that occurs in mammals.

We shall prove quantifier elimination theorems for neocompact formulas, which define neocompact sets and are built from atomic formulas using finite disjunctions, infinite conjunctions, existential quantifiers, and bounded universal quantifiers. The neocompact sets were first introduced to provide an easy alternative to nonstandard methods of proving existence theorems in probability theory, where they behave like compact sets. The quantifier elimination theorems in this paper can be applied in a general setting to show that the family of neocompact sets (...) is countably compact. To provide the necessary setting we introduce the notion of a law structure. This notion was motivated by the probability law of a random variable. However, in this paper we discuss a variety of model theoretic examples of the notion in the light of our quantifier elimination results. (shrink)

We say that a ring admits elimination of quantifiers, if in the language of rings, {0, 1, +, ·}, the complete theory of R admits elimination of quantifiers. Theorem 1. Let D be a division ring. Then D admits elimination of quantifiers if and only if D is an algebraically closed or finite field. A ring is prime if it satisfies the sentence: ∀ x ∀ y ∃ z (x = 0 ∨ y = 0 ∨ xzy (...) ≠ 0). Theorem 2. If R is a prime ring with an infinite center and R admits elimination of quantifiers, then R is an algebraically closed field. Let A be the class of finite fields. Let B be the class of 2 × 2 matrix rings over a field with a prime number of elements. Let C be the class of rings of the form $GF(p^n) \bigoplus GF(p^k)$ such that either n = k or g.c.d. (n, k) = 1. Let D be the set of ordered pairs (f, Q) where Q is a finite set of primes and f: Q → A ∪ B ∪ C such that the characteristic of the ring f(q) is q. Finally, let E be the class of rings of the form $\bigoplus_{q \in Q}f(q)$ for some (f, Q) in D. Theorem 3. Let R be a finite ring without nonzero trivial ideals. Then R admits elimination of quantifiers if and only if R belongs to E. Theorem 4. Let R be a ring with the descending chain condition of left ideals and without nonzero trivial ideals. Then R admits elimination of quantifiers if and only if R is an algebraically closed field or R belongs to E. In contrast to Theorems 2 and 4, we have Theorem 5. If R is an atomless p-ring, then R is finite, commutative, has no nonzero trivial ideals and admits elimination of quantifiers, but is not prime and does not have the descending chain condition. We also generalize Theorems 1, 2 and 4 to alternative rings. (shrink)

In 1985, van den Dries showed that the theory of the reals with a predicate for the integer powers of two admits quantifier elimination in an expanded language, and is hence decidable. He gave a model-theoretical argument, which provides no apparent bounds on the complexity of a decision procedure. We provide a syntactical argument that yields a procedure that is primitive recursive, although not elementary.

The aim of this paper is to provide an addendum to a paper by Rose with the same title which has appeared in an earlier issue of this Journal [2]. Our new result is: Theorem. A ring of characteristic zero which admits elimination of quantifiers in the language {0, 1, +, ·} is an algebraically closed field.

Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with (...) unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix. (shrink)

The importance of downward causation lies in showing that it shows that functional properties such as mental properties are real, although they cannot be reduced to physical properties. Kim rejects nonreductive physicalism, which includes leading functionalism, by eliminating downward causation, and thereby returns to reductionism. In this paper, I make a distinction between two aspects of function—functional meaning and functional structure and argue that functional meaning cannot be reduced to the physical level whereas functional structure can. On this basis, I (...) further distinguish between the integer of the function, which includes the functional meaning and the functional structure, and the whole of the functional realization, and also among the strong, medial, and weak supervenience relations. So-called downward causation is indeed the relationship between the whole of the functional realization and its physical realizer, which is a whole-part relation instead of a relation between levels. As a result of understanding downward causation in this way and abandoning the principle of the causal closure of the physical world, Kim’s argument becomes invalid and nonreductive functionalism, justified. (shrink)

Although it was traditionally thought that self-reference is a crucial ingredient of semantic paradoxes, Yablo (1993, 2004) showed that this was not so by displaying an infinite series of sentences none of which is self-referential but which, taken together, are paradoxical. Yablo’s paradox consists of a countable series of linearly ordered sentences s(0), s(1), s(2),... , where each s(i) says: For each k (...) class='Hi'>> i, s(k) is false (or equivalently: For no k > i is s(k) true). We generalize Yablo’s results along two dimensions. First, we study the behavior of generalized Yablo-series in which each sentence s(i) has the form: For Q k > i, s(k) is true, where Q is a generalized quantifier (e.g., no, every, infinitely many, etc). We show that under broad conditions all the sentences in the series must have the same truth value, and we derive a characterization of those values of Q for which the series is paradoxical. Second, we show that in the Strong Kleene trivalent logic Yablo’s results are a special case of a more general fact: under certain conditions, any semantic phenomenon that involves self-reference can be emulated without self-reference. Various translation procedures that eliminate self-reference from a non-quantificational language are defined and characterized. An Appendix sketches an extension to quantificational languages, as well as a new argument that Yablo’s paradox and the translations we offer do not involve self-reference. (shrink)

The article rebutts Michael Kremer’s contention that Russell’s contextual definition of set-theoretic language in Principia Mathematica constituted the ontological achievement of eliminating commitment to classes. Although Russell’s higher-order quantifiers, used in the definition, need not range over classes, none of the plausible substitutes provide a solid basis for eliminating them. This point is used to defend the presentation, in The Dawn of Analysis, of Russell’s logicist reduction, using a first-order version of naive set theory.

The claim that theoretical entities are not real, that they are merely convenient fictions, has been defended and attacked in diverse ways. This paper is concerned with only one defense of the fictionalist thesis and with a certain realist attack on it. The defense in question is that theories which prima facie make reference to theoretical entities can be revised in such a way that no such apparent reference is made by eliminating all occurrences of theoretical expressions. It will be (...) argued here that there is a procedure for revising theories which meets certain minimal criteria of adequacy, contrary to arguments in the literature. Further, it will be argued that the existence of this procedure provides neither sufficient nor necessary support for the fictionalist thesis, that this procedure is not of significance in the dispute between the fictionalist and the realist. Whether or not the theoretical-nontheoretical distinction is viable is another story which will not be told here. It will be assumed for the sake of argument that such a distinction can be drawn. (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)

A way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate logic (...) with equality in which also cuts on the equality axioms are eliminated. (shrink)

It is shown that de re formulas are eliminable in the modal logic S5 extended with the axiom scheme x x.

We propose that the primary cause of schizophrenia is a pathological extension of synaptic pruning involving local connectivity that unfolds ordinarily during adolescence. Computer simulations suggest that this pathology provides reasonable accounts of a range of symptoms in schizophrenia, and is consistent with recent postmortem and genetic studies. NMDA-receptors play a regulatory role in maintaining and/or eliminating cortical synapses, and therefore may play a pathophysiological role.

This paper refutes two important and influential views in one fell stroke. The first is G.E. Moore’s view that assertions of the form ‘Q but I don’t believe that Q’ are inherently “absurd.” The second is Gareth Evans’s view that justification to assert Q entails justification to assert that you believe Q. Both views run aground the possibility of being justified in accepting eliminativism about belief. A corollary is that a principle recently defended by John Williams is also false, namely, (...) that justification to believe Q entails justification to believe that you believe Q. (shrink)

We provide a constructive, direct, and simple proof of the completeness of the cut-free part of the hypersequential calculus for G¨odel logic (thereby proving both completeness of the calculus for its standard semantics, and the admissibility of the cut rule in the full calculus). We then extend the results and proofs to derivations from assumptions, showing that such derivations can be confined to those in which cuts are made only on formulas which occur in the assumptions.

An efficient algorithm, HALO, is given to compute As computer aided design (CAD) deals with more com- haloed line drawings of wire frame objects. (Haloed..

We argue in this paper that so-called new wave reductionism fails to capture the nature of the interlevel relations between psychology and neuroscience. Bickle (1995, Psychoneural reduction of the genuinely cognitive: some accomplished facts, Philosophical Psychology, 8, 265-285; 1998, Psychoneural reduction: the new wave, Cambridge, MA: MIT Press) has claimed that a (bottom-up) reduction of the psychological concepts of learning and memory to the concepts of neuroscience has in fact already been accomplished. An investigation of current research on the phenomenon (...) of long-term potentiation reveals that this claim overstates the facts. Both the psychological and the neural concepts involved have not yet stabilized and face further correction under the influence of both bottom-up and top-down selection pressures. In addition, psychological concepts often refer to functions, and functions are indispensable and irreducible. Function ascriptions pick out objective patterns involving historical factors and distal goals. This view of functions implies that psychological facts cannot be simply read off from the neurophysiological facts. Although psychological theorizing is constrained by neurophysiology (and vice versa), psychology remains distinct at least to some degree. (shrink)

This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the formn(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence (...) of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program Otter played an indispensable role in this study. (shrink)

For any extension $T$ of $I\Sigma_{1}$ having a cut-elimination property extending that of $I\Sigma_{1}$ , the number of different proofs that can be obtained by cut elimination from a single $T$ -proof cannot be bound by a function which is provably total in $T$.

We show that the ordered field of real numbers with restricted $\mathbb{R}_{\mathscr{H}}$-definable analytic functions admits quantifier elimination if we add a function symbol $^{-1}$ for the function $x\mapsto \frac{1}{x}$ (with $0^{-1}=0$ by convention), where $\mathbb{R}_{\mathscr{H}}$ is the real field augmented by the functions in the family $\mathscr{H}$ of restricted parts (real and imaginary) of holomorphic functions which satisfies certain conditions. Further, with another condition on $\mathscr{H}$ we show that the structure ($\mathbb{R}_{\mathscr{H}}$, constants) is strongly model complete.

I consider the error-statistical account as both a theory of evidence and as a theory of inference. I seek to show how inferences regarding the truth of hypotheses can be upheld by avoiding a certain kind of alternative hypothesis problem. In addition to the testing of assumptions behind the experimental model, I discuss the role of judgments of implausibility. A benefit of my analysis is that it reveals a continuity in the application of error-statistical assessment to low-level empirical hypotheses and (...) highly general theoretical principles. This last point is illustrated with a brief sketch of the issues involved in the parametric framework analysis of tests of physical theories such as General Relativity and of fundamental physical principles such as the Einstein Equivalence Principle. (shrink)

The American Journal of Bioethics, Volume 11, Issue 6, Page 45-46, June 2011.

By the theory TT is meant the higher order predicate logic with the following recursively defined types: (1) 1 is the type of individuals and [] is the type of the truth values: (2) [τ l ,..., τ n ] is the type of the predicates with arguments of the types τ l ,..., τ n . The theory ITT described in this paper is an intensional version of TT. The types of ITT are the same as the types of (...) TT, but the membership of the type 1 of individuals in ITT is an extension of the membership in TT. The extension consists of allowing any higher order term, in which only variables of type 1 have a free occurrence, to be a term of type 1. This feature of ITT is motivated by a nominalist interpretation of higher order predication. In ITT both well-founded and non-well-founded recursive predicates can be defined as abstraction terms from which all the properties of the predicates can be derived without the use of non-logical axioms. The elementary syntax, semantics, and proof theory for ITT are defined. A semantic consistency proof for ITT is provided and the completeness proof of Takahashi and Prawitz for a version of TT without cut is adapted for ITT: a consequence is the redundancy of cut. (shrink)

We formulate a unified display calculus proof theory for the four principal varieties of bunched logic by combining display calculi for their component logics. Our calculi satisfy cut-elimination, and are sound and complete with respect to their standard presentations. We show how to constrain applications of display-equivalence in our calculi in such a way that an exhaustive proof search need be only finitely branching, and establish a full deduction theorem for the bunched logics with classical additives, BBI and CBI. (...) We also show that the standard sequent calculus for BI can be seen as a reformulation of its display calculus, and argue that analogous sequent calculi for the other varieties of bunched logic are very unlikely to exist. (shrink)

In this paper we present a sequent calculus for the multi-agent system S5 m . First, we introduce a particularly simple alternative Kripke semantics for the system S5 m . Then, we construct a hypersequent calculus for S5 m that reflects at the syntactic level this alternative interpretation. We prove that this hypersequent calculus is theoremwise equivalent to the Hilbert-style system S5 m , that it is contraction-free and cut-free, and finally that it is decidable. All results are proved in (...) a purely syntactic way and the cut-elimination procedure yields an upper bound of ip 2 (n, 0) where ip 2 is an hyperexponential function of base 2. (shrink)