Online research in philosophy

When Archimedes, while bathing, suddenly hit upon the principle of buoyancy, he ran wildly through the streets of Syracuse, stark naked, crying "eureka!" In The Moment of Proof, Donald Benson attempts to convey to general readers the feeling of eureka--the joy of discovery--that mathematicians feel when they first encounter an elegant proof. This is not an introduction to mathematics so much as an introduction to the pleasures of mathematical thinking. And indeed the delights of this book are many (...) and varied. The book is packed with intriguing conundrums--Loyd's Fifteen Puzzle, the Petersburg Paradox, the Chaos Game, the Monty Hall Problem, the Prisoners' Dilemma--as well as many mathematical curiosities. We learn how to perform the arithmetical proof called "casting out nines" and are introduced to Russian peasant multiplication, a bizarre way to multiply numbers that actually works. The book shows us how to calculate the number of ways a chef can combine ten or fewer spices to flavor his soup (1,024) and how many people we would have to gather in a room to have a 50-50 chance of two having the same birthday (23 people). But most important, Benson takes us step by step through these many mathematical wonders, so that we arrive at the solution much the way a working scientist would--and with much the same feeling of surprise. Every fan of mathematical puzzles will be enthralled by The Moment of Proof. Indeed, anyone interested in mathematics or in scientific discovery in general will want to own this book. (shrink)

This work is derived from the SERC "Logic for IT" Summer School Conference on Proof Theory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to proof theory aimed at both mathematicians and computer scientists.

Jean van Heijenoort was best known for his editorial work in the history of mathematical logic. I survey his contributions to model-theoretic proof theory, and in particular to the falsifiability tree method. This work of van Heijenoort’s is not widely known, and much of it remains unpublished. A complete list of van Heijenoort’s unpublished writings on tableaux methods and related work in proof theory is appended.

This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply (...) them elsewhere in much more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)

Proof Theory of Modal Logic is devoted to a thorough study of proof systems for modal logics, that is, logics of necessity, possibility, knowledge, belief, time, computations etc. It contains many new technical results and presentations of novel proof procedures. The volume is of immense importance for the interdisciplinary fields of logic, knowledge representation, and automated deduction.

Proof-theoretical notions and techniques, developed on the basis of sentential/symbolic representations of formal proofs, are applied to Euler diagrams. A translation of an Euler diagrammatic system into a natural deduction system is given, and the soundness and faithfulness of the translation are proved. Some consequences of the translation are discussed in view of the notion of free ride, which is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. The translation enables us (...) to formalize and analyze free ride in terms of proof theory. The notion of normal form of Euler diagrammatic proofs is investigated, and a normalization theorem is proved. Some consequences of the theorem are further discussed: in particular, an analysis of the structure of normal diagrammatic proofs; a diagrammatic counterpart of the usual subformula property; and a characterization of diagrammatic proofs compared with natural deduction proofs. (shrink)

This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth. The chapters are arranged so that (...) the two introductory articles come first; these are then followed by articles from core classical areas of proof theory; the handbook concludes with articles that deal with topics closely related to computer science. (shrink)

Goal Directed Proof Theory presents a uniform and coherent methodology for automated deduction in non-classical logics, the relevance of which to computer science is now widely acknowledged. The methodology is based on goal-directed provability. It is a generalization of the logic programming style of deduction, and it is particularly favourable for proof search. The methodology is applied for the first time in a uniform way to a wide range of non-classical systems, covering intuitionistic, intermediate, modal and substructural (...) logics. The book can also be used as an introduction to these logical systems form a procedural perspective. Readership: Computer scientists, mathematicians and philosophers, and anyone interested in the automation of reasoning based on non-classical logics. The book is suitable for self study, its only prerequisite being some elementary knowledge of logic and proof theory. (shrink)

This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search including proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences.

Different proofs may be distinguished in terms of complexity. This paper reviews the inefficiency of current logical systems.

The main aim of Schonfinkel's paper was methodological: to reduce the primitive logical notions to as few and definite notions as possible. ...

"I know what you're thinking," we say, but how do we know what others are thinking or feeling? Because evolution has granted us what has come to be known as "Theory of Mind," the ability not only to be self-aware but aware of others' consciousness. Theory of Mind develops slowly-and in some cases, such as autism, develops little or not at all. Theory of Mind allows us to interact socially, to care about others, to manage our behavior (...) in groups, to fall in love, and--less admirably--it allows us to lie. Some of the subject matter covered in Mindreading: You are less likely to detect lies told to you by your longterm partner than by a new acquaintance.Female babies react more strongly and more often to another baby's cries than male babies. In other words, female children are more predisposed to become personally distressed by emotion in others and to cry in sympathy.In general, the female brain is superior to the male brain when it comes to social relationships; the male brain is better at spatial skills. People with autism follow the male trend, but to a much greater extreme.Autistics, like many normal men, collect things, focus on what seems to others to be trivial detail, and have a narrow range of interests. Could autism be an extreme form of the male brain?For evolutionary reasons, you should take very good care to detect eye gaze, because when another animal is looking at you it can mean one of the three 'F's. Either the animal wants to fight you, feed on you, or mate with you. (shrink)

1. Pohlers and The Problem. I first met Wolfram Pohlers at a workshop on proof theory organized by Walter Felscher that was held in Tübingen in early April, 1973. Among others at that workshop relevant to the work surveyed here were Kurt Schütte, Wolfram’s teacher in Munich, and Wolfram’s fellow student Wilfried Buchholz. This is not meant to slight in the least the many other fine logicians who participated there.2 In Tübingen I gave a couple of survey (...) lectures on results and problems in proof theory that had been occupying much of my attention during the previous decade. The following was the central problem that I emphasized there: The need for an ordinally informative, conceptually clear, proof-theoretic reduction of classical theories of iterated arithmetical inductive definitions to corresponding constructive systems. As will be explained below, meeting that need would be significant for the then ongoing efforts at establishing the constructive foundation for and proof-theoretic ordinal analysis of certain impredicative subsystems of classical analysis. I also spoke in Tübingen about.. (shrink)

At the turn of the nineteenth century, mathematics exhibited a style of argumentation that was more explicitly computational than is common today. Over the course of the century, the introduction of abstract algebraic methods helped unify developments in analysis, number theory, geometry, and the theory of equations; and work by mathematicians like Dedekind, Cantor, and Hilbert towards the end of the century introduced set-theoretic language and infinitary methods that served to downplay or suppress computational content. This shift in (...) emphasis away from calculation gave rise to concerns as to whether such methods were meaningful, or appropriate to mathematics. The discovery of paradoxes stemming from overly naive use of set-theoretic language and methods led to even more pressing concerns as to whether the modern methods were even consistent. This led to heated debates in the early twentieth century and what is sometimes called the “crisis of foundations.” In lectures presented in 1922, David Hilbert launched his Beweistheorie, or Proof Theory, which aimed to justify the use of modern methods and settle the problem of foundations once and for all. This, Hilbert argued, could be achieved as follows. (shrink)

We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the (...) West or the original presentation can be improved using notions or results which appeared later. This includes such topics as Novikov's cut-elimination method (regular formulas) and Maslov's inverse method for the predicate logic. (shrink)

In the 1970s, Robin Giles introduced a game combining Lorenzen-style dialogue rules with a simple scheme for betting on the truth of atomic statements, and showed that the existence of winning strategies for the game corresponds to the validity of formulas in Łukasiewicz logic. In this paper, it is shown that ‘disjunctive strategies’ for Giles’s game, combining ordinary strategies for all instances of the game played on the same formula, may be interpreted as derivations in a corresponding proof system. (...) In particular, such strategies mirror derivations in a hypersequent calculus developed in recent work on the proof theory of Łukasiewicz logic. (shrink)

The goals of reduction andreductionism in the natural sciences are mainly explanatoryin character, while those inmathematics are primarily foundational.In contrast to global reductionistprograms which aim to reduce all ofmathematics to one supposedly ``universal'' system or foundational scheme, reductive proof theory pursues local reductions of one formal system to another which is more justified in some sense. In this direction, two specific rationales have been proposed as aims for reductive proof theory, the constructive consistency-proof rationale and (...) the foundational reduction rationale. However, recent advances in proof theory force one to consider the viability of these rationales. Despite the genuine problems of foundational significance raised by that work, the paper concludes with a defense of reductive proof theory at a minimum as one of the principal means to lay out what rests on what in mathematics. In an extensive appendix to the paper,various reduction relations betweensystems are explained and compared, and arguments against proof-theoretic reduction as a ``good'' reducibilityrelation are taken up and rebutted. (shrink)

A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.

The ability to reason and think in a logical manner forms the basis of learning for most mathematics, computer science, philosophy and logic students. Based on the author's teaching notes at the University of Maryland and aimed at a broad audience, this text covers the fundamental topics in classical logic in an extremely clear, thorough and accurate style that is accessible to all the above. Covering propositional logic, first-order logic, and second-order logic, as well as proof theory, computability (...) theory, and model theory, the text also contains numerous carefully graded exercises and is ideal for a first or refresher course. (shrink)

I present an account of truth values for classical logic, intuitionistic logic, and the modal logic S5, in which truth values are not a fundamental category from which the logic is defined, but rather, an idealisation of more fundamental logical features in the proof theory for each system. The result is not a new set of semantic structures, but a new understanding of how the existing semantic structures may be understood in terms of a more fundamental notion of (...) logical consequence. (shrink)

We discuss the development of metamathematics in the Hilbert school, and Hilbert’s proof-theoretic program in particular. We place this program in a broader historical and philosophical context, especially with respect to nineteenth century developments in mathematics and logic. Finally, we show how these considerations help frame our understanding of metamathematics and proof theory today.

Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I (...) will discuss the aspects of forcing that are useful in this respect, and some sample applications. The latter include ways of obtaining conservation results for classical and intuitionistic theories, interpreting classical theories in constructive ones, and constructivizing model-theoretic arguments. (shrink)

We give an overview of recent results in ordinal analysis. Therefore,we discuss the different frameworks used in mathematical proof-theory, namely subsystem of analysis including reversemathematics, Kripke–Platek set theory, explicitmathematics, theories of inductive definitions,constructive set theory, and Martin-Löfs typetheory.

We introduce a Gentzen-style modal predicate logic and prove the cut-elimination theorem for it. This sequent calculus of cut-free proofs is chosen as a proxy to develop the proof-theory of the logics introduced in [14, 15, 4]. We present syntactic proofs for all the metatheoretical results that were proved model-theoretically in loc. cit. and moreover prove that the form of weak reflection proved in these papers is as strong as possible.

In this 4th edition of his successful Cultural Theory and Popular Culture: An Introduction, John Storey has extensively revised the text throughout.

Our first aim is to make the study of informal notions of proof plausible. Put differently, since the raison d'étre of anything like existing proof theory seems to rest on such notions, the aim is nothing else but to make a case for proof theory; ...

A concise introduction to structural proof theory, a branch of logic studying the general structure of logical and mathematical proofs.

The II-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the II-calculus and prove the cut-elimination theorem.The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting (...) considered here elegantly illustrates the distinction between the processes of normalization in a natural deduction system and cut-elimination in a Gentzen-style sequent calculus. (shrink)

A general definition theory should serve as a foundation for the mathematical study of definitional structures. The central notion of such a theory is a precise explication of the intuitively given notion of a definitional structure. The purpose of this paper is to discuss the proof theory of partial inductive definitions as a foundation for this kind of a more general definition theory. Among the examples discussed is a suggestion for a more abstract definition of (...) lambda-terms (derivations in natural deduction) that could provide a basis for a more systematic definitional approach to general proof theory. (shrink)

This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation facilitates (...) proofs of the classical incompleteness and undecidability theorems which are very elegant and easy to understand. The discussion of semantics makes clear the important distinction between standard and nonstandard models which is so important in understanding puzzling phenomena such as the incompleteness theorems and Skolem's Paradox about countable models of set theory. Some of the numerous exercises require giving formal proofs. A computer program called ETPS which is available from the web facilitates doing and checking such exercises. Audience: This volume will be of interest to mathematicians, computer scientists, and philosophers in universities, as well as to computer scientists in industry who wish to use higher-order logic for hardware and software specification and verification. (shrink)

In this paper we first briefly review Bell's (1964, 1966) Theorem to see how it invalidates any deterministic "hidden variable" account of the apparent indeterminacy of quantum mechanics (QM). Then we show that quantum uncertainty, at the level of DNA mutations, can "percolate" up to have major populational effects. Interesting as this point may be it does not show any autonomous indeterminism of the evolutionary process. In the next two sections we investigate drift and natural selection as the locus of (...) autonomous biological indeterminacy. Here we conclude that the population-level indeterminacy of natural selection and drift are ultimately based on the assumption of a fundamental indeterminacy at the level of the lives and deaths of individual organisms. The following section examines this assumption and defends it from the determinists' attack. Then we show that, even if one rejects the assumption, there is still an important reason why one might think evolutionary theory (ET) is autonomously indeterministic. In the concluding section we contrast the arguments we have mounted against a deterministic hidden variable account of ET with the proof of the impossibility of such an account of QM. (shrink)

Machine generated contents note: Prologue: Hilbert's Last Problem; 1. Introduction; Part I. Proof Systems Based on Natural Deduction: 2. Rules of proof: natural deduction; 3. Axiomatic systems; 4. Order and lattice theory; 5. Theories with existence axioms; Part II. Proof Systems Based on Sequent Calculus: 6. Rules of proof: sequent calculus; 7. Linear order; Part III. Proof Systems for Geometric Theories: 8. Geometric theories; 9. Classical and intuitionistic axiomatics; 10. Proof analysis in elementary (...) geometry; Part IV. Proof Systems for Nonclassical Logics: 11. Modal logic; 12. Quantified modal logic, provability logic, and so on; Bibliography; Index of names; Index of subjects. (shrink)

In the constructive theory of uniform spaces there occurs a technique of proof in which the application of a weak form of the law of excluded middle is circumvented by purely analytic means. The essence of this proof-technique is extracted and then applied in several different situations.

Q.E.D. presents some of the most famous mathematical proofs in a charming book that will appeal to nonmathematicians and math experts alike. Grasp in an instant why Pythagoras’s theorem must be correct. Follow the ancient Chinese proof of the volume formula for the frustrating frustum, and Archimedes’ method for finding the volume of a sphere. Discover the secrets of pi and why, contrary to popular belief, squaring the circle really is possible. Study the subtle art of mathematical domino (...) tumbling, and find out how slicing cones helped save a city and put a man on the moon. (shrink)

Nyāya, which is one of the orthodox Brahmanical schools in India, accepts the authority of both the Vedic scriptures and God as its composer. Nyāya has specialized in logic and argumentation from ancient times while at the same time gradually strengthening its theistic tendency. Nyāya polemicist, Udayana, is famous for his contribution to the rational proof of the existence of God. In this paper, I will consider a tiny part of his proof of the existence of God given (...) in his theistic monograph, the Nyāyakusumāñjali, and in particular a topic called prāmāṇyavāda, or the Theory of Validity, from the viewpoint of the historical development of this argument. In this topic, it is argued how we justify our cognition and undertake actions. Nyāya polemicists preceding Udayana argued this topic in order to justify the Vedic scriptures and to encourage people to perform the Vedic rituals. And this topic has had little relationship with theological context. However, Udayana seems to link this argument to his theory of theology in an implicit way. I will suppose in his argument the implicit linkage between the prāmāṇyavāda and the assumption of an omniscient being. (shrink)

Linear logic is a new logic which was recently developed by Girard in order to provide a logical basis for the study of parallelism. It is described and investigated in Gi]. Girard's presentation of his logic is not so standard. In this paper we shall provide more standard proof systems and semantics. We shall also extend part of Girard's results by investigating the consequence relations associated with Linear Logic and by proving corresponding str ong completeness theorems. Finally, we shall (...) investigate the relation between Linear Logic and previously known systems, especially Relevance logics. (shrink)

We study the proof-theoretic relationship between two deductive systems for the modal mu-calculus. First we recall an infinitary system which contains an omega rule allowing to derive the truth of a greatest fixed point from the truth of each of its (infinitely many) approximations. Then we recall a second infinitary calculus which is based on non-well-founded trees. In this system proofs are finitely branching but may contain infinite branches as long as some greatest fixed point is unfolded infinitely often (...) along every branch. The main contribution of our paper is a translation from proofs in the first system to proofs in the second system. Completeness of the second system then follows from completeness of the first, and a new proof of the finite model property also follows as a corollary. (shrink)

How do ordinals measure the strength and computational power of formal theories? This paper is concerned with the connection between ordinal representation systems and theories established in ordinal analyses. It focusses on results which explain the nature of this connection in terms of semantical and computational notions from model theory, set theory, and generalized recursion theory.

We confirm a conjecture, about neat embeddings of cylindric algebras, made in 1969 by J. D. Monk, and a later conjecture by Maddux about relation algebras obtained from cylindric algebras. These results in algebraic logic have the following consequence for predicate logic: for every finite cardinal α ≥ 3 there is a logically valid sentence X, in a first-order language L with equality and exactly one nonlogical binary relation symbol E, such that X contains only 3 variables (each of which (...) may occur arbitrarily many times), X has a proof containing exactly α + 1 variables, but X has no proof containing only α variables. This solves a problem posed by Tarski and Givant in 1987. (shrink)

A natural deduction formulation is given for the intermediate logic called MH by Gabbay in [4]. Proof-theoretic methods are used to show that every deduction can be normalized, that MH is the weakest intermediate logic for which the Glivenko theorem holds, and that the Craig-Lyndon interpolation theorem holds for it.

Este trabajo tiene por objetivo examinar la idea de deducción metamatemática en el programa de Hilbert, mostrando su dependencia de conceptos gnoseológicos, tales como el de conocimiento intuitivo. También se comparará esta concepcion de la deducción con la fundamentación intuicionista de la logica. Sostendré que esta deducción metamatemática lleva a una caracterización de la logica como una teoría de las deducciones formales en un sentido particular.This paper aims to examine the idea of metamathematical deduction in Hilbert’s program showing its dependence (...) of epistemological notions, such as intuitive knowledge. This conception of deduction will be also compared with the intuitionistic foundation of logic. I will argue that this metamathematical deduction leads to a characterization of logic as a theory of formal deductions in a particular sense. (shrink)

In the last decade the concept of context has been extensivelyexploited in many research areas, e.g., distributed artificialintelligence, multi agent systems, distributed databases, informationintegration, cognitive science, and epistemology. Three alternative approaches to the formalization of the notion ofcontext have been proposed: Giunchiglia and Serafini's Multi LanguageSystems (ML systems), McCarthy's modal logics of contexts, andGabbay's Labelled Deductive Systems.Previous papers have argued in favor of ML systems with respect to theother approaches. Our aim in this paper is to support these arguments froma (...) theoretical perspective. We provide a very general definition of ML systems, which covers allthe ML systems used in the literature, and we develop a proof theoryfor an important subclass of them: the MR systems. We prove variousimportant results; among other things, we prove a normal form theorem,the sub-formula property, and the decidability of an importantinstance of the class of the MR systems. The paper concludes with a detailed comparison among the alternativeapproaches. (shrink)

New to this edition: 4 new readings Stuart Hall The rediscovery of 'ideology': return of the repressed in media studies Ernesto Laclau and Chantal Mouffe Post ...

A critical discussion of selected chapters of the first volume of Scott Soames’s Philosophical Analysis in the Twentieth Century. It is argued that this volume falls short of the minimal standards of scholarship appropriate to a work that advertises itself as a history, and, further, that Soames’s frequent heuristic simplifications and distortions, since they are only sporadically identified as such, are more likely confuse than to enlighten the student. These points are illustrated by reference to Soames’s discussions of Russell’s logical (...) system and the place of the theory of descriptions in his ontological development. It is then argued that Soames’s interpretation of the point of G.E. Moore’s famous “proof” of an external world, while not straightforwardly undermined by the textual evidence, is nonetheless questionable, and plausibly overlooks what is novel in Moore’s discussion. This, it is argued, in his attempt to offer a common sense “refutation of idealism”, rather than (as is more commonly supposed) an anti-skeptical argument “from differential certainty”. (shrink)

Anti-realist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality $${\diamondsuit}$$ and an epistemic modality $${\mathcal{K}}$$ , by the axiom scheme $${A \supset \diamondsuit \mathcal{K} A}$$ ( KP ). The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, $${A \supset \mathcal{K} A}$$ ( OP ). A Gentzen-style (...) reconstruction of the Church–Fitch paradox is presented following a labelled approach to sequent calculi. First, a cut-free system for classical (resp. intuitionistic) bimodal logic is introduced as the logical basis for the Church–Fitch paradox and the relationships between $${\mathcal {K}}$$ and $${\diamondsuit}$$ are taken into account. Afterwards, by exploiting the structural properties of the system, in particular cut elimination, the semantic frame conditions that correspond to KP are determined and added in the form of a block of nonlogical inference rules. Within this new system for classical and intuitionistic “knowability logic”, it is possible to give a satisfactory cut-free reconstruction of the Church–Fitch derivation and to confirm that OP is only classically derivable, but neither intuitionistically derivable nor intuitionistically admissible. Finally, it is shown that in classical knowability logic, the Church–Fitch derivation is nothing else but a fallacy and does not represent a real threat for anti-realism. (shrink)

The volumes of G¨ odel’s collected papers under review consist almost entirely of a rich selection of his philosophical/scientific correspondence, including English translations face-to-face with the originals when the latter are in German. The residue consists of correspondence with editors (more amusing than of any scientific value) and five letters from G¨ odel to his mother, in which explains to her his religious views. The term “selection” is strongly operative here: The editors state the total number of items of personal (...) and scientific correspondence in G¨ odel’s Nachlass to be around thirty-five hundred. The correspondence selected involves fifty correspondents, and the editors list the most prominent of these: Paul Bernays, William Boone, Rudolph Carnap. Paul Cohen, Burton Dreben, Jacques Herbrand, Arend Heyting, Karl Menger, Ernest Nagel, Emil Post, Abraham Robinson, Alfred Tarski, Stanislaw Ulam, John von Neumann, Hao Wang, and Ernest Zermelo. The correspondence is arranged alphebetically, with A-G in Volume IV. The imbalance results from the disproportionate size of the Bernays correrspondence: 85 letters are included (almost all of them), spanning 234 pages) including the face-to-face originals and translations). Each volume contains a calendar of all the items included in the volume together with separate calendars listing all known correspondence (whether included or not) with the major correspondents (seven in Volume IV and ten in Volume V). Let me recommend to the reader the review of these same volumes by Paolo Mancosu in the Notre Dame Journal of Formal Logic 45 (2004):109- 125. This essay very nicely describes much of the correspondence in terms of broad themes relating, especially, to the incompleteness theorems—their origins in G¨ odel’s thought, their reception, their impact on Hilbert’s program. (shrink)

Semantics plays a role in grammar in at least three guises. (A) Linguists seek to account for speakers‘ knowledge of what linguistic expressions mean. This goal is typically achieved by assigning a model theoretic interpretation2 in a compositional fashion. For example, No whale flies is true if and only if the intersection of the sets of whales and fliers is empty in the model. (B) Linguists seek to account for the ability of speakers to make various inferences based on semantic (...) knowledge. For example, No whale flies entails No blue whale flies and No whale flies high. (C) The wellformedness of a variety of syntactic constructions depends on morpho-syntactic features with a semantic flavor. For example, Under no circumstances would a whale fly is grammatical, whereas Under some circumstances would a whale fly is not, corresponding to the downward vs. upward monotonic features of the preposed phrases. (shrink)

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, (...) class='Hi'>proof normalization corresponds to term reduction, etc. But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq). This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic. Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme. · Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics. · Elaborate study of classical logics and control operators. · Account of dialogue games for classical and intuitionistic logic. · Theoretical foundations of computer-assisted reasoning. (shrink)

Proof-theory has traditionally been developed based on linguistic (symbolic) representations of logical proofs. Recently, however, logical reasoning based on diagrammatic or graphical representations has been investigated by logicians. Euler diagrams were introduced in the eighteenth century. But it is quite recent (more precisely, in the 1990s) that logicians started to study them from a formal logical viewpoint. We propose a novel approach to the formalization of Euler diagrammatic reasoning, in which diagrams are defined not in terms of regions (...) as in the standard approach, but in terms of topological relations between diagrammatic objects. We formalize the unification rule, which plays a central role in Euler diagrammatic reasoning, in a style of natural deduction. We prove the soundness and completeness theorems with respect to a formal set-theoretical semantics. We also investigate structure of diagrammatic proofs and prove a normal form theorem. (shrink)

Until not too many years ago, all logics except classical logic (and, perhaps, intuitionistic logic too) were considered to be things esoteric. Today this state of a airs seems to have completely been changed. There is a growing interest in many types of nonclassical logics: modal and temporal logics, substructural logics, paraconsistent logics, non-monotonic logics { the list is long. The diversity of systems that have been proposed and studied is so great that a need is felt by many researchers (...) to try to put some order in the present logical jungle. Thus Cl91], Ep90] and Wo88] are three recent books in which an attempt is made to develop a general theoretical framework for the study of logics. On the more pragmatic side, several systems have been developed with the goal of providing a computerized logical framework in which many di erent logical systems can be implemented in a uniform way. An example is the Edinburgh LF( HHP91]). (shrink)

This is a summary of developments analysed in my (1997A). A first version of that paper was presented at the workshop Modern Mathematical Thought in Pittsburgh (September 21-24, 1995).

Linear Logic is a branch of proof theory which provides refined tools for the study of the computational aspects of proofs. These tools include a duality-based categorical semantics, an intrinsic graphical representation of proofs, the introduction of well-behaved non-commutative logical connectives, and the concepts of polarity and focalisation. These various aspects are illustrated here through introductory tutorials as well as more specialised contributions, with a particular emphasis on applications to computer science: denotational semantics, lambda-calculus, logic programming and concurrency (...) theory. The volume is rounded-off by two invited contributions on new topics rooted in recent developments of linear logic. The book derives from a summer school that was the climax of the EU Training and Mobility of Researchers project 'Linear Logic in Computer Science'. It is an excellent introduction to some of the most active research topics in the area. (shrink)

In this paper, constructions of free ordered algebras on one generator are given that correspond to some one-variable fragments of affine propositional classical logic and their extensions with n-contraction (n ≥ 2). Moreover, embeddings of the already known infinite free structures into the algebras introduced below are furnished with; thus, solving along the respective cardinality problems.

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)

The Unprovability of Consistency is concerned with connections between two branches of logic: proof theory and modal logic. Modal logic is the study of the principles that govern the concepts of necessity and possibility; proof theory is, in part, the study of those that govern provability and consistency. In this book, George Boolos looks at the principles of provability from the standpoint of modal logic. In doing so, he provides two perspectives on a debate in modal (...) logic that has persisted for at least thirty years between the followers of C. I. Lewis and W. V. O. Quine. The author employs semantic methods developed by Saul Kripke in his analysis of modal logical systems. The book will be of interest to advanced undergraduate and graduate students in logic, mathematics and philosophy, as well as to specialists in those fields. (shrink)

A proof is given that there does not exist an event, that is not already in the past for some possible distant observer at the (our) moment that the latter is "now" for us. Such event is as "legally" past for that distant observer as is the moment five minutes ago on the sun for us (irrespective of the circumstance that the light of the sun cannot reach us in a period of five minutes). Only an extreme positivism: "that (...) which cannot yet be observed does not yet exist", can possibly withstand the conclusion concerned. Therefore, there is determinism, also in micro-physics. (shrink)

Proof, Logic and Formalization addresses the various problems associated with finding a philosophically satisfying account of mathematical proof. It brings together many of the most notable figures currently writing on this issue in an attempt to explain why it is that mathematical proof is given prominence over other forms of mathematical justification. The difficulties that arise in accounts of proof range from the rightful role of logical inference and formalization to questions concerning the place of experience (...) in proof and the possibility of eliminating impredictive reasoning from proof. Students and lecturers of philosophy, philosophy of logic, and philosophy of mathematics will find this to be essential reading. A companion volume entitled Proof and Logic in Mathematics is also available from Routledge. (shrink)

The paper is devoted to the contributions of Helena Rasiowa to the theory of non-classical negation. The main results of Rasiowa in this area concerns–constructive logic with strong (Nelson) negation.

The requirement of proof-theoretic harmony has played a pivotal role in a number of debates in the philosophy of logic. Different authors have attempted to precisify the notion in different ways. Among these, three proposals have been prominent in the literature: harmony–as–conservative extension, harmony–as–leveling procedure, and Tennant’s harmony–as–deductive equilibrium. In this paper I propose to clarify the logical relationships between these accounts. In particular, I demonstrate that what I call the equivalence conjecture —that these three notions essentially come to (...) the same thing—is erroneous. (shrink)

Collectively these essays inform educators and researchers at different grade levels about the teaching and learning of proof at each level and, thus, help ...