We propose a novel, ontological approach to studying mathematical propositions and proofs. By “ontological approach” we refer to the study of the categories of beings or concepts that, in their practice, mathematicians isolate as fruitful for the advancement of their scientific activity (like discovering and proving theorems, formulating conjectures, and providing explanations). We do so by developing what we call a “formal ontology” of proofs using semantic modeling tools (like RDF and OWL) developed by the computer science community. In (...) this article, (i) we describe this new approach and, (ii) to provide an example, we apply it to the problem of the identity of proofs. We also describe open issues and further applications of this approach (for example, the study of purity of methods). We lay some foundations to investigate rigorously and at large scale intellectual moves and attitudes that underpin the advancement of mathematics through cognitive means (carving out investigationally valuable concepts and techniques) and social means (like communication, collaboration, revision, and criticism of specific categories, inferential patterns, and levels of analysis). Our approach complements other types of analysis of proofs such as reconstruction in a deductive system and examination through a proof-assistant. (shrink)

Rigorous formal proof is one of the key techniques in the natural sciences, engineering, and of course also in the formal sciences. Progress in automated reasoning increasingly enables computer systems to support, and even teach, users to conduct formal a.

In this textbook on elementary logic the authors present a rigorous treatment of first the propositional, and then the predicate calculi. The first two chapters deal with the former topic exclusively: there is much emphasis on translation of ordinary-language sentences into logic and testing their validity; also a proof notation consisting of nested boxes, similar to the Fitch subproof technique, is introduced and used. The third and fourth chapters are concerned with quantification theory in application to language analysis; the (...) next chapter discusses more theoretical topics including a proof procedure for formulae in prenex normal form and decision procedures for restricted classes of such formulae. Identity is treated next, with the following chapter on definite descriptions. The eighth chapter is more formal in approach and has as its subject the abstract approach to logical systems: the notion of the extension of a theory is introduced at this stage; two examples of formal theories—the theory of commutative ordered fields, and that of real numbers—are presented and come under extensive elaboration. The last chapter discusses variable-binding operations and presents the theory of convergence of series as an example of such a theory with these operations. Each chapter has numerous exercises, and most have historical remarks and lists of theorems of that chapter.—P. J. M. (shrink)

Designed to make logic interesting and accessible -- without sacrificing content or rigor -- this classic introduction to contemporary propositional logic explains the symbolization of English sentences and develops formal-proof, truth-table, and truth-tree techniques for evaluating arguments. Organizes content around natural-deduction formal-proof procedures, truth tables, and truth trees. Also presents logical statement connectives gradually, one per chapter, and finally, increases readers' awareness of the arguments they read and hear every day by providing examples of actual (...) arguments to which they can readily relate. (shrink)

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)

"Proof" has been and remains one of the concepts which characterises mathematics. Covering basic propositional and predicate logic as well as discussing axiom systems and formal proofs, the book seeks to explain what mathematicians understand by proofs and how they are communicated. The authors explore the principle techniques of direct and indirect proof including induction, existence and uniqueness proofs, proof by contradiction, constructive and non-constructive proofs, etc. Many examples from analysis and modern algebra are included. (...) The exceptionally clear style and presentation ensures that the book will be useful and enjoyable to those studying and interested in the notion of mathematical "proof.". (shrink)

We are used to the idea that computers operate on numbers, yet another kind of data is equally important: the syntax of formal languages, with variables, binding, and alpha-equivalence. The original application of nominal techniques, and the one with greatest prominence in this paper, is to reasoning on formal syntax with variables and binding. Variables can be modelled in many ways: for instance as numbers (since we usually take countably many of them); as links (since they may (...) `point' to a binding site in the term, where they are bound); or as functions (since they often, though not always, represent `an unknown'). None of these models is perfect. In every case for the models above, problems arise when trying to use them as a basis for a fully formal mechanical treatment of formal language. The problems are practical—but their underlying cause may be mathematical. The issue is not whether formal syntax exists, since clearly it does, so much as what kind of mathematical structure it is. To illustrate this point by a parody, logical derivations can be modelled using a Gödel encoding (i.e., injected into the natural numbers). It would be false to conclude from this that proof-theory is a branch of number theory and can be understood in terms of, say, Peano's axioms. Similarly, as it turns out, it is false to conclude from the fact that variables can be encoded e.g., as numbers, that the theory of syntax-with-binding can be understood in terms of the theory of syntax-without-binding, plus the theory of numbers (or, taking this to a logical extreme, purely in terms of the theory of numbers). It cannot; something else is going on. What that something else is, has not yet been fully understood. In nominal techniques, variables are an instance of names, and names are data. We model names using urelemente with properties that, pleasingly enough, turn out to have been investigated by Fraenkel and Mostowski in the first half of the 20th century for a completely different purpose than modelling formal language. What makes this model really interesting is that it gives names distinctive properties which can be related to useful logic and programming principles for formal syntax. Since the initial publications, advances in the mathematics and presentation have been introduced piecemeal in the literature. This paper provides in a single accessible document an updated development of the foundations of nominal techniques. This gives the reader easy access to updated results and new proofs which they would otherwise have to search across two or more papers to find, and full proofs that in other publications may have been elided. We also include some new material not appearing elsewhere. (shrink)

In order to develop efficient tools for automated reasoning with inconsistency (theorem provers), eventually making Logics of Formal inconsistency (_LFI_) a more appealing formalism for reasoning under uncertainty, it is important to develop the proof theory of the first-order versions of such _LFI_s. Here, we intend to make a first step in this direction. On the other hand, the logic _Ciore_ was developed to provide new logical systems in the study of inconsistent databases from the point of view (...) of _LFI_s. An interesting fact about _Ciore_ is that it has a _strong_ consistency operator, that is, a consistency operator which (forward/backward) propagates inconsistency. Also, it turns out to be an algebraizable logic (in the sense of Blok and Pigozzi) that can be characterized by means of a 3-valued logical matrix. Recently, a first-order version of _Ciore_, namely _QCiore_, was defined preserving the spirit of _Ciore_, that is, without introducing unexpected relationships between the quantifiers. Besides, some important model-theoretic results were obtained for this logic. In this paper we study some proof–theoretic aspects of both _Ciore_ and _QCiore_ respectively. In first place, we introduce a two-sided sequent system for _Ciore_. Later, we prove that this system enjoys the cut-elimination property and apply it to derive some interesting properties. Later, we extend the above-mentioned system to first-order languages and prove completeness and cut-elimination property using the well-known Shütte’s technique. (shrink)

Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle and (...) I apologize for not displaying these results as well.Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.By Gödel's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems—this may be considered as applied proof theory—but want to concentrate on metamathematical problems and results. In this sense I am talking about Pure Proof Theory.Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions. (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)

The author considers the model-theoretic character of proofs and disproofs by means of attempted counterexample constructions, distinguishes this proof format from formal derivations, then contrasts two approaches to semantic tableaux proposed by Beth and Lambert-van Fraassen. It is noted that Beth's original approach has not as yet been provided with a precisely formulated rule of closure for detecting tableau sequences terminating in contradiction. To remedy this deficiency, a technique is proposed to clarify tableau operations.

Preferential structures are probably the best examined semantics for nonmonotonic and deontic logics; in a wider sense, they also provide semantical approaches to theory revision and update, and other fields where a preference relation between models is a natural approach. They have been widely used to differentiate the various systems of such logics, and their construction is one of the main subjects in the formal investigation of these logics. We introduce new techniques to construct preferential structures for completeness (...) proofs. Since our main interest is to provide general techniques, which can be applied in various situations and for various base logics (propositional and other), we take a purely algebraic approach, which can be translated into logics by easy lemmata. In particular, we give a clean construction via indexing by trees for transitive structures, this allows us to simplify the proofs of earlier work by the author, and to extend the results given there. (shrink)

Originally published in 1965. This is a textbook of modern deductive logic, designed for beginners but leading further into the heart of the subject than most other books of the kind. The fields covered are the Propositional Calculus, the more elementary parts of the Predicate Calculus, and Syllogistic Logic treated from a modern point of view. In each of the systems discussed the main emphases are on Decision Procedures and Axiomatisation, and the material is presented with as much formal (...) rigour as is compatible with clarity of exposition. The techniques used are not only described but given a theoretical justification. Proofs of Consistency, Completeness and Independence are set out in detail. The fundamental characteristics of the various systems studies, and their relations to each other are established by meta-logical proofs, which are used freely in all sections of the book. Exercises are appended to most of the chapters, and answers are provided. (shrink)

Complex frameworks for defining programming languages aim to generate various tools (e.g. interpreters, symbolic execution engines, deductive verifiers, etc.) using only the formal definition of a language. When used at an industrial scale, these tools are constantly updated, and at the same time, it is required to be trustworthy. Ensuring the correctness of such a framework is practically impossible. A solution is to generate proof objects as correctness artefacts that can be checked by an external trusted checker. A (...) logic suitable for developing such frameworks is matching logic. K framework is a canonical example having matching logic-based foundation. Since the (symbolic) configurations of the programs are represented by matching logic patterns, the algorithms computing the dynamics of these configurations can be seen as pattern transformers and a proof object should be generated for the relationship between these patterns. In this paper, we show that conjunctions and disjunctions of patterns, produced by semantics or analysis rules, can be safely normalized using unification and antiunification algorithms. We also provide a prototype implementation of our proof object generation technique and a checker for certifying the generated objects. (shrink)

Originally published in 1965. This is a textbook of modern deductive logic, designed for beginners but leading further into the heart of the subject than most other books of the kind. The fields covered are the Propositional Calculus, the more elementary parts of the Predicate Calculus, and Syllogistic Logic treated from a modern point of view. In each of the systems discussed the main emphases are on Decision Procedures and Axiomatisation, and the material is presented with as much formal (...) rigour as is compatible with clarity of exposition. The techniques used are not only described but given a theoretical justification. Proofs of Consistency, Completeness and Independence are set out in detail. The fundamental characteristics of the various systems studies, and their relations to each other are established by meta-logical proofs, which are used freely in all sections of the book. Exercises are appended to most of the chapters, and answers are provided. (shrink)

Logic and Computation is concerned with techniques for formal theorem-proving, with particular reference to Cambridge LCF (Logic for Computable Functions). Cambridge LCF is a computer program for reasoning about computation. It combines methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of statements in a programming language. This book consists of two parts. Part I outlines the mathematical preliminaries: elementary logic and domain theory. They are explained at an intuitive level, (...) giving references to more advanced reading. Part II provides enough detail to serve as a reference manual for Cambridge LCF. It will also be a useful guide for implementors of other programs based on the LCF approach. (shrink)

We show that when certain statements are provable in subsystems of constructive analysis using intuitionistic predicate calculus, related sequential statements are provable in weak classical subsystems. In particular, if a $\Pi^1_2$ sentence of a certain form is provable using E-HA ${}^\omega$ along with the axiom of choice and an independence of premise principle, the sequential form of the statement is provable in the classical system RCA. We obtain this and similar results using applications of modified realizability and the Dialectica interpretation. (...) These results allow us to use techniques of classical reverse mathematics to demonstrate the unprovability of several mathematical principles in subsystems of constructive analysis. (shrink)

Despite the skepticism of many mathematicians and logicians as to the possibility of any test which will show conclusively the consistency or independence of the members of a postulate set, several methods have nevertheless been devised and employed, e.g., the empirical methods of Russell and Huntington, the internal method of Hilbert, and the reflective method of Royce. However, with the possible exception of Hilbert's method, these techniques require us to forsake the purely formal or abstract mode of analysis, (...) and instead to rely in some sense on “concrete representations” or “interpretations” or “modes of action” which are said to “satisfy” the postulates in question. In short, they are all interpretational methods—and here is the crux of the problem. “Is it possible,” queries Weiss, “that the only way we can determine whether a set is consistent is by seeing all the postulates actually exemplified in some object? If so, we must arbitrarily assume that the object is self-consistent, so that the proof of consistency must ultimately rest on a dogma. As independence rests on consistency there are therefore no satisfactory proofs as yet of either independence or consistency.” The question “is thus answered,” according to Young, “only by reference to a concrete representation of the abstract ideas involved, and it is such concrete representations that we wished especially to avoid. At the present time, however, no absolute test for consistency is known.” Moreover, “suppose,” says the late Dr. Eaton, “that the system has no interpretation: how can the consistency independence … of the postulates be shown? There should be some analytic way—purely in the realm of the abstract, without interpretation—of establishing these properties of a set of postulates. This is an important problem that awaits solution.”. (shrink)

The main objective of this paper is to sketch unifying conceptual and formal framework for inference that is able to explain various proof techniques without implicitly changing the underlying notion of inference rules. We base this framework upon the so-called two-dimensional, i.e., deduction to deduction, account of inference introduced by Tichý in his seminal work The Foundation’s of Frege’s Logic (1988). Consequently, it will be argued that sequent calculus provides suitable basis for such general concept of inference (...) and therefore should not be seen just as technical tool, but philosophically well-founded system that can rival natural deduction in terms of its “naturalness”. (shrink)

This lecture, given at Beijing University in 1984, presents a remarkable (previously unpublished) proof of the Gödel Incompleteness Theorem due to Kripke. Today we know purely algebraic techniques that can be used to give direct proofs of the existence of nonstandard models in a style with which ordinary mathematicians feel perfectly comfortable--techniques that do not even require knowledge of the Completeness Theorem or even require that logic itself be axiomatized. Kripke used these techniques to establish incompleteness (...) by means that could, in principle, have been understood by nineteenth-century mathematicians. The proof exhibits a statement of number theory--one which is not at all "self referring"--and constructs two models, in one of which it is true and in the other of which it is false, thereby establishing "undecidability" (independence). (shrink)

This article presents a simplified proof of the result that bounded depth propositional proofs of the pigeonhole principle are exponentially large. The proof uses the new techniques for proving switching lemmas developed by Razborov and Beame. A similar result is also proved for some examples based on graphs.

Deductive Logic is designed as an intermediate-level text directed at upper-division students from philosophy and the humanities. Its focus is exclusively on deductive logic, avoiding altogether topics such as informal reasoning and scientific method normally included in introductory logic courses. Its exposition of logical topics is informal, with emphasis on explaining the basic concepts and procedures of modern symbolic logic in the simplest and most intuitive manner possible rather than on developing a rigorous formal system and providing proofs of (...) its properties. The fact that the text presupposes a course offered to philosophy students and serves to introduce them to logic as the "language of philosophy" has strongly influenced the selection of topics. The topics here are controversial, and the problems not easily resolved, but this text strives to relate the formal logical structures introduced to issues of philosophic interest. (shrink)

Diagonalization is a proof technique that formal learning theorists use to show that inductive problems are unsolvable. The technique intuitively requires the construction of the mathematical equivalent of a "Cartesian demon" that fools the scientist no matter how he proceeds. A natural question that arises is whether diagonalization is complete. That is, given an arbitrary unsolvable inductive problem, does an invincible demon exist? The answer to that question turns out to depend upon what axioms of set theory we (...) adopt. The two main results of the paper show that if we assume ZermeloFraenkel set theory plus AC and CH, there exist undetermined inductive games. The existence of such games entails that diagonalization is incomplete. On the other hand, if we assume the Axiom of Determinacy, or even a weaker axiom known as Wadge Determinacy, then diagonalization is complete. In order to prove the results, inductive inquiry is viewed as an infinitary game played between the scientist and nature. Such games have been studied extensively by descriptive set theorists. Analogues to the results above are mentioned, in which both the scientist and the demon are restricted to computable strategies. The results exhibit a surprising connection between inductive methodology and the foundations of set theory. (shrink)

Compositional verification aims at managing the complexity of theverification process by exploiting compositionality of the systemarchitecture. In this paper we explore the use of a temporal epistemiclogic to formalize the process of verification of compositionalmulti-agent systems. The specification of a system, its properties andtheir proofs are of a compositional nature, and are formalized within acompositional temporal logic: Temporal Multi-Epistemic Logic. It isshown that compositional proofs are valid under certain conditions.Moreover, the possibility of incorporating default persistence ofinformation in a system, is (...) explored. A completion operation on aspecific type of temporal theories, temporal completion, is introducedto be able to use classical proof techniques in verification withrespect to non-classical semantics covering default persistence. (shrink)

This two-volume work bridges the gap between introductory expositions of logic or set theory on one hand, and the research literature on the other. It can be used as a text in an advanced undergraduate or beginning graduate course in mathematics, computer science, or philosophy. The volumes are written in a user-friendly conversational lecture style that makes them equally effective for self-study or class use. Volume II, on formal (ZFC) set theory, incorporates a self-contained 'chapter 0' on proof (...) techniques so that it is based on formal logic, in the style of Bourbaki. The emphasis on basic techniques will provide the reader with a solid foundation in set theory and provides a context for the presentation of advanced topics such as absoluteness, relative consistency results, two expositions of Godel's constructible universe, numerous ways of viewing recursion, and a chapter on Cohen forcing. (shrink)

We present a construction of a truth class (an interpretation of a compositional truth predicate) in an arbitrary countable recursively saturated model of first-order arithmetic. The construction is fully classical in that it employs nothing more than the classical techniques of formal proof theory.

Over the past half-century, formal, machine-executable proofs have been developed for an impressive range of mathematical theorems. Formalists argue that such proofs should be seen as providing the fully worked out proofs of which mathematicians’ proofs are sketches. Nonformalists argue that this conception of the relationship of formal to informal proofs cannot explain the fact that formal proofs lack essential virtues enjoyed by mathematicians’ proofs, the fact, for example, that formal proofs are not convincing and lack (...) the explanatory power of their informal counterparts. Formal proofs do not yield mathematical insight or understanding, and they are not fruitful in the way that informal proofs can be, for instance, in suggesting novel approaches to old problems. And yet, there is a clear sense in which the formalist is right: Formal proofs do seem to make explicit what is otherwise taken for granted in the mathematician’s reasoning. Very recent work uncovers the source of the dilemma by showing that rigor does not entail formalism insofar as rigor, unlike formalism, is compatible with contentfulness. Mathematical proofs, were they to be recast in a Leibnizian language, at once a characteristica and a calculus, would be, or could be made to be, completely gap-free and hence machine checkable. Because as so recast they would be grounded in mathematical ideas, they would not be machine executable. It is on just this basis that a compelling account can be given of the fact that formal proofs are mostly irrelevant to mathematicians in their practice. (shrink)

I develop the decision-theoretic approach to quantum probability, originally proposed by David Deutsch, into a mathematically rigorous proof of the Born rule in (Everett-interpreted) quantum mechanics. I sketch the argument informally, then prove it formally, and lastly consider a number of proposed ``counter-examples'' to show exactly which premises of the argument they violate. (This is a preliminary version of a chapter to appear --- under the title ``How to prove the Born Rule'' --- in Saunders, Barrett, Kent and Wallace, (...) "Many worlds? Everett, quantum theory and reality", forthcoming from Oxford University Press.). (shrink)

In a recent article, “Wayward Modeling: Population Genetics and Natural Selection,” Bruce Glymour claims that population genetics is burdened by serious predictive and explanatory inadequacies and that the theory itself is to blame. Because Glymour overlooks a variety of formal modeling techniques in population genetics, his arguments do not quite undermine a major scientific theory. However, his arguments are extremely valuable as they provide definitive proof that those who would deploy classical population genetics over natural systems must (...) do so with careful attention to interactions between individual population members and environmental causes. Glymour’s arguments have deep implications for causation in classical population genetics. (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.

Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion (...) subservient to proper propositions. The Curry–Howard correspondence is typically viewed as a formal counterpart of this conception. I will argue against this position and show that even though the Curry–Howard correspondence typically accommodates the placeholder view of assumptions, it is rather a matter of choice, not a necessity, and that another more assumption-friendly view can be adopted. (shrink)

Wilfred Sieg. “Church's Thesis”, “Consistency”, “Formalization”, “Proof Theory”: Dictionary Entries.

In this paper, we define a first-order logic CFʹ with strong negation and bounded static quantifiers, which is a variant of Thomason's logic CF. For the logic CFʹ, the usual Kripke formal semantics is defined based on situations, and a sound and complete axiomatic system is established based on the axiomatic systems of constructive logics with strong negation and Thomason's completeness proof techniques. With the use of bounded quantifiers, CFʹ allows the domain of quantification to be empty (...) and allows for nondenoting constants. CFʹ is intended as a fragment of a logic for situation theory. Thus the connection between CFʹ and infon logic is discussed. (shrink)

Here is a deft and new introduction to Gentzen proof techniques in axiom systems and to the analysis of formal axiom systems; in short, axiomatics inside and out. Treating of deduction in propositional and predicate logic, metatheoretical problems about both set theory and its paradoxes, the book is flexibly structured for selective use as a text. Yet the discussion is unified and motivated by the concept of the axiomatic system--the history of its use and analysis, and its (...) present practical and theoretical status. Well-chosen illustrations convey an historical overview of Euclid, non-Euclidean geometers, Peano, Boole, Hilbert and Gödel.--P. D. J. (shrink)

This is easily the most systematic survey of the foundations of logic and mathematics available today. Although Beth does not cover the development of set theory in great detail, all other aspects of logic are well represented. There are nine chapters which cover, though not in this order, the following: historical background and introduction to the philosophy of mathematics; the existence of mathematical objects as expressed by Logicism, Cantorism, Intuitionism, and Nominalism; informal elementary axiomatics; formalized axiomatics with reference to finitary (...) theory of proof; non-elementary metamathematics, embracing formal syntax and semantics; applications of set theory and topology in metamathematics—especially in the theory of models; recursive function theory; the logical paradoxes; the relation of philosophy of mathematics to general philosophy. This is a mere skeleton of the whole, but it indicates the broad sweep of the work. One unifying feature is the author's use of his "semantic tableau" method of examining the truth or falsity of sentences. Although the author is an Intuitionist, classical metamathematical proof techniques are by no means slighted; they are used throughout much of the book, and are indispensable, of course, when dealing with classical logic. Exercises are scattered throughout and at the end; few of them are trivial. There is a very extensive bibliography, brought up to date from the first edition. This extraordinary book will be of use to logicians as a reference tool and to philosophers trying to survey the field of modern formal logic; its appearance in a fine paper edition is therefore doubly welcome—P. J. M. (shrink)

By formalizing recent syntactic theories for natural languages Stabler shows how their complexity can be handled without guesswork or oversimplification. By formalizing recent syntactic theories for natural languages in the tradition of Chomsky's Barriers, Stabler shows how their complexity can be handled without guesswork or oversimplification. He introduces logical representations of these theories together with special deductive techniques for exploring their consequences that will provide linguists with a valuable tool for deriving and testing theoretical predictions and for experimenting with (...) alternative formulations of grammatical principles. Stabler's novel approach allows results to be deduced with straightforward calculations and provides a systematic framework for tackling the problem of how speakers can infer the properties of an utterance from principles of the grammar. The special treatment of equality, induction principles, and inclusion of a general method for collecting structures from proofs means that sophisticated linguistic arguments can be carried out in detail, giving a rich perspective to issues in linguistic theory and parsing. (shrink)

This introduction to formal logic is one of the few paperbacks available that provides a broad survey of the field. In addition to a clear presentation of sentential and first order quantificational logic, there is a discussion of the philosophical significance of recent work by Church, Gödel, and Tarski. The proof technique employed throughout is the indirect argument. Since proofs of this sort can be converted into mechanical tests of validity, it is easier than most for a beginning (...) student to grasp. Furthermore, this style of argument has long been recognized as the most obvious method of showing arguments in ordinary language to be invalid. Interesting treatments of the construction of decision machines, the nature of formal systems, and the application of logic to mathematics are included in the last section. Numerous exercises are included for which some answers are provided.--R. P. M. (shrink)

Purity is known as an ideal of proof that restricts a proof to notions belonging to the ‘content’ of the theorem. In this paper, our main interest is to develop a conception of purity for formal (natural deduction) proofs. We develop two new notions of purity: one based on an ontological notion of the content of a theorem, and one based on the notions of surrogate ontological content and structural content. From there, we characterize which (classical) first-order (...) natural deduction proofs of a mathematical theorem are pure. Formal proofs that refer to the ontological content of a theorem will be called ‘fully ontologically pure’. Formal proofs that refer to a surrogate ontological content of a theorem will be called ‘secondarily ontologically pure’, because they preserve the structural content of a theorem. We will use interpretations between theories to develop a proof-theoretic criterion that guarantees secondary ontological purity for formal proofs. (shrink)

The article presents a formalization of Thomas Aquinas proof for the indestructibility of the human soul. The author of the formalization—the first of its kind in the history of philosophy—is Father Joseph Maria Bocheński. The presentation involves no more than updating the logical symbolism used and accompanies the logical formulae with ordinary language paraphrases in order to ease the reader’s understanding of the formulae. “The fundamental idea of the Thomist proof is of utmost simplicity: things which are destructible (...) are destructible either per se or per accidens; but the human soul is destructible neither per se nor per accidens: therefore the human soul is not destructible”. Bochenski’s words required him to devote considerable effort for the sake of precision of the symbolic language that would be maximally adequate to Thomas’ discourse. Moreover, I have thought it necessary to provide an ample commentary to the traditional and contemporary semantical presuppositions of Aquinas philosophical anthropology in light of Bocheński’s interpretation thereof. (shrink)

What seem to be Kurt Gödel’s first notes on logic, an exercise notebook of 84 pages, contains formal proofs in higher-order arithmetic and set theory. The choice of these topics is clearly suggested by their inclusion in Hilbert and Ackermann’s logic book of 1928, the Grundzüge der theoretischen Logik. Such proofs are notoriously hard to construct within axiomatic logic. Gödel takes without further ado into use a linear system of natural deduction for the full language of higher-order logic, with (...) formal derivations closer to one hundred steps in length and up to four nested temporary assumptions with their scope indicated by vertical intermittent lines. (shrink)

Derivationists, those wishing to explain the correctness and rigour of informal proofs in terms of associated formal proofs, are generally held to be supported by the success of the project of translating informal proofs into computer-checkable formal counterparts. I argue, however, that this project is a false friend for the derivationists because there are too many different associated formal proofs for each informal proof, leading to a serious worry of overgeneration. I press this worry primarily against (...) Azzouni's derivation-indicator account, but conclude that overgeneration is a major obstacle to a successful account of informal proofs in this direction. (shrink)

Model checking, a prominent formal method used to predict and explain the behaviour of software and hardware systems, is examined on the basis of reflective work in the philosophy of science concerning the ontology of scientific theories and model-based reasoning. The empirical theories of computational systems that model checking techniques enable one to build are identified, in the light of the semantic conception of scientific theories, with families of models that are interconnected by simulation relations. And the mappings (...) between these scientific theories and computational systems in their scope are analyzed in terms of suitable specializations of the notions of model of experiment and model of data. Furthermore, the extensively mechanized character of model-based reasoning in model checking is highlighted by a comparison with proof procedures adopted by other formal methods in computer science. Finally, potential epistemic benefits flowing from the application of model checking in other areas of scientific inquiry are emphasized in the context of computer simulation studies of biological information processing. (shrink)