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.

The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory (...) of finite-valued first order logics in a general way, and to present some of the more important results in this area. In Systems covered are the resolution calculus, sequent calculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)

A modified Young double-slit experiment proposed by Wootters and Zurek is considered in which a system P of parallel plates covered with a photographic emulsion has been set up in the region where we would normally expect the central interference fringes. Because under certain conditions P makes it possible to conclude with much more than50% certainty through which of the two slits each particular photon passed, the relevant interference pattern becomes blurred. It is proved that this implies a retroactive effect (...) because the setup of P and the interaction of photons with P appear to influence the momentum transferred to the photons by the edges of the slits at an earlier stage of the experiment. (shrink)

In this paper we describe a novel approach to defining an ontologically fundamental notion of co-presentness that does not go against the tenets of relativity theory. We survey the possible reactions to the problem of the present in relativity theory, introducing a terminological distinction between a static role of the present, which is served by the relation of simultaneity, and a dynamic role of the present, with the corresponding relation of co-presentness. We argue that both of these relations need to (...) be equivalence relations, but they need not coincide. Simultaneity, the sharing of a temporal coordinate, need not have fundamental ontological import, so that a relativizing strategy with respect to simultaneity seems promising. The notion of co-presentness, on the other hand, does have ontological import, and can therefore not be relativized to an observer or to an arbitrarily chosen frame. We argue that a formal representation of indeterminism can provide the structure needed to anchor the relation of co-presentness, and that this addition is in fact congenial to the notion of dynamic time as requiring real change. The resulting picture is one of an extended dynamic present, implying a formal distinction between static simultaneity and dynamic co-presentness. After working out the basics of our approach in the simpler framework of branching time, we provide our full analysis in the framework of branching space-times, which allows for a formal definition of modal correlations. The spatial extension of the dynamic present can reach as far as the modal correlations do. In the limit, the dynamic present could extend across a maximal space-like hypersurface. (shrink)

This comprehensive monograph is a cornerstone in the area of mathematical logic and related fields. Focusing on Gentzen-type proof theory, the book presents a detailed overview of creative works by the author and other 20th-century logicians that includes applications of proof theory to logic as well as other areas of mathematics. 1975 edition.

Now in so far as it is recognized that the constituents of the environment are not present inside the body in the same way as they are present outside it, to that extent they are bound, the moment they are inside it, to become something essentially different from the environment.

Though pictures are often used to present mathematical arguments, they are not typically thought to be an acceptable means for presenting mathematical arguments rigorously. With respect to the proofs in the Elements in particular, the received view is that Euclid's reliance on geometric diagrams undermines his efforts to develop a gap-free deductive theory. The central difficulty concerns the generality of the theory. How can inferences made from a particular diagrams license general mathematical results? After surveying the history behind the received (...) view, this essay provides a contrary analysis by introducing a formal account of Euclid's proofs, termed Eu. Eu solves the puzzle of generality surrounding Euclid's arguments. It specifies what diagrams Euclid's diagrams are, in a precise formal sense, and defines generality-preserving proof rules in terms of them. After the central principles behind the formalization are laid out, its implications with respect to the question of what does and does not constitute a genuine picture proof are explored. (shrink)

We argue that Wittgenstein’s philosophical perspective on Gödel’s most famous theorem is even more radical than has commonly been assumed. Wittgenstein shows in detail that there is no way that the Gödelian construct of a string of signs could be assigned a useful function within (ordinary) mathematics. — The focus is on Appendix III to Part I of Remarks on the Foundations of Mathematics. The present reading highlights the exceptional importance of this particular set of remarks and, more specifically, emphasises (...) its refined composition and rigorous internal structure. (shrink)

An introduction to writing proofs, presented through compelling mathematical statements with interesting elementary proofs. This book offers an introduction to the art and craft of proof-writing. The author, a leading research mathematician, presents a series of engaging and compelling mathematical statements with interesting elementary proofs. These proofs capture a wide range of topics, including number theory, combinatorics, graph theory, the theory of games, geometry, infinity, order theory, and real analysis. The goal is to show students and aspiring mathematicians how (...) to write proofs with elegance and precision. (shrink)

This book continues from where the authors' previous book, Structural Proof Theory, ended. It presents an extension of the methods of analysis of proofs in pure logic to elementary axiomatic systems and to what is known as philosophical logic. A self-contained brief introduction to the proof theory of pure logic is included that serves both the mathematically and philosophically oriented reader. The method is built up gradually, with examples drawn from theories of order, lattice theory and elementary geometry. (...) The aim is, in each of the examples, to help the reader grasp the combinatorial behaviour of an axiom system, which typically leads to decidability results. The last part presents, as an application and extension of all that precedes it, a proof-theoretical approach to the Kripke semantics of modal and related logics, with a great number of new results, providing essential reading for mathematical and philosophical logicians. (shrink)

The paper presents a proof-theoretic semantics (PTS) for a fragment of natural language, providing an alternative to the traditional model-theoretic (Montagovian) semantics (MTS), whereby meanings are truth-condition (in arbitrary models). Instead, meanings are taken as derivability-conditions in a dedicated natural-deduction (ND) proof-system. This semantics is effective (algorithmically decidable), adhering to the meaning as use paradigm, not suffering from several of the criticisms formulated by philosophers of language against MTS as a theory of meaning. In particular, Dummett’s manifestation argument (...) does not obtain, and assertions are always warranted, having grounds of assertion. The proof system is shown to satisfy Dummett’s harmony property, justifying the ND rules as meaning conferring. The semantics is suitable for incorporation into computational linguistics grammars, formulated in type-logical grammar. (shrink)

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame (...) class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope. (shrink)

We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class (...) of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations. (shrink)

The idea of proof-theoretic validity originated in the work of Gentzen, when he suggested that the meaning of each logical expression was encapsulated in its introduction-rules. The idea was developed by Prawitz and Dummett, but came under attack by Prior under the soubriquet 'analytic validity'. Logical truths and logical consequences are deemed analytically valid by virtue of following, in a way which the present chapter clarifies, from the meaning of the logical constants. But different logics are based on different (...) rules, confer different meanings and so validate different theorems and consequences, some of which are arguably not true or valid at all. It seems to follow that some analytic statements are in fact false. The moral is that we must be careful what rules we adopt and what meanings we use our rules to determine. (shrink)

Sequent calculi constitute an interesting and important category of proof systems. They are much less known than axiomatic systems or natural deduction systems are, and they are much less known than they should be. Sequent calculi were designed as a theoretical framework for investigations of logical consequence, and they live up to the expectations completely as an abundant source of meta-logical results. The goal of this book is to provide a fairly comprehensive view of sequent calculi -- including a (...) wide range of variations. The focus is on sequent calculi for various non-classical logics, from intuitionistic logic to relevance logic, through linear and modal logics. A particular version of sequent calculi, the so-called consecution calculi, have seen important new developments in the last decade or so. The invention of new consecution calculi for various relevance logics allowed the last major open problem in the area of relevance logic to be solved positively: pure ticket entailment is decidable. An exposition of this result is included in chapter 9 together with further new decidability results (for less famous systems). A series of other results that were obtained by J. M. Dunn and me, or by me in the last decade or so, are also presented in various places in the book. Some of these results are slightly improved in their current presentation. Obviously, many calculi and several important theorems are not new. They are included here to ensure the completeness of the picture; their original formulations may be found in the referenced publications. This book contains very little about semantics, in general, and about the semantics of non-classical logic in particular. (shrink)

The article presents a full proof‐theoretic semantics for natural deduction based on an extended inversion principle: the elimination rule for an operator q may invert the introduction rule for q, but also vice versa, the introduction rule for a connective q may invert the elimination rule for q. Such an inversion—extending Prawitz' concept of inversion—gives the following theorem: Inversion for two rules of operator q (intro rule, elim rule) exists iff a reduction of a maximum formula for q exists. (...) The inversion theorem is specified to two logics, Lambek calculus (LC) and intuitionistic linear logic (ILL), with four propositional connectives: two multiplicatives (implication and conjunction) and two additives (conjunction and disjunction), with two quantifiers and two modals. LC is defined by using elimination rules by composition. ILL is defined by using usual general elimination rules. Elimination rules by composition are an exciting alternative to general elimination rules; in some cases, they do not need permutations. (shrink)

In a series of papers, Don Fallis points out that although mathematicians are generally unwilling to accept merely probabilistic proofs, they do accept proofs that are incomplete, long and complicated, or partly carried out by computers. He argues that there are no epistemic grounds on which probabilistic proofs can be rejected while these other proofs are accepted. I defend the practice by presenting a property I call ‘transferability’, which probabilistic proofs lack and acceptable proofs have. I also consider what this (...) says about the similarities between mathematics and, on the one hand natural sciences, and on the other hand philosophy. (shrink)

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than (...) in the explanation of the rules. (shrink)

A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.

The completeness of the modal logic S4 for all topological spaces as well as for the real line , the n-dimensional Euclidean space and the segment etc. was proved by McKinsey and Tarski in 1944. Several simplified proofs contain gaps. A new proof presented here combines the ideas published later by G. Mints and M. Aiello, J. van Benthem, G. Bezhanishvili with a further simplification. The proof strategy is to embed a finite rooted Kripke structure for S4 into (...) a subspace of the Cantor space which in turn encodes . This provides an open and continuous map from onto the topological space corresponding to . The completeness follows as S4 is complete with respect to the class of all finite rooted Kripke structures. (shrink)

The Four-Colour Theorem (4CT) proof, presented to the mathematical community in a pair of papers by Appel and Haken in the late 1970's, provoked a series of philosophical debates. Many conceptual points of these disputes still require some elucidation. After a brief presentation of the main ideas of Appel and Haken’s procedure for the proof and a reconstruction of Thomas Tymoczko’s argument for the novelty of 4CT’s proof, we shall formulate some questions regarding the connections between (...) the points raised by Tymoczko and some Wittgensteinian topics in the philosophy of mathematics such as the importance of the surveyability as a criterion for distinguishing mathematical proofs from empirical experiments. Our aim is to show that the “characteristic Wittgensteinian invention” (Mühlhölzer 2006) – the strong distinction between proofs and experiments – can shed some light in the conceptual confusions surrounding the Four-Colour Theorem. (shrink)

Tetravalent modal logic (TML) was introduced by Font and Rius in 2000. It is an expansion of the Belnap-Dunn four-valued logic FOUR, a logical system that is well-known for the many applications found in several fields. Besides, TML is the logic that preserves degrees of truth with respect to Monteiro’s tetravalent modal algebras. Among other things, Font and Rius showed that TML has a strongly adequate sequent system, but unfortunately this system does not enjoy the cut-elimination property. However, in a (...) previous work we presented a sequent system for TML with the cut-elimination property. Besides, in this same work, it was also presented a sound and complete natural deduction system for this logic. In the present article we continue with the study of TML under a proof-theoretic perspective. In the first place, we show that the natural deduction system that we introduced before admits a normalization theorem. In the second place, taking advantage of the contrapositive implication for the tetravalent modal algebras introduced by A. V. Figallo and P. Landini, we define a decidable tableau system adequate to check validity in the logic TML. Finally, we provide a sound and complete tableau system for TML in the original language. These two tableau systems constitute new (proof-theoretic) decision procedures for checking validity in the variety of tetravalent modal algebras. (shrink)

The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

This paper presents proof that Buss's S22 can prove the consistency of a fragment of Cook and Urquhart's PV from which induction has been removed but substitution has been retained. This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic S12. Our proof relies on the notion of "computation" of the terms of PV. In our work, we first prove that, in the system under consideration, if an equation is proved (...) and either its left- or right-hand side is computed, then there is a corresponding computation for its right- or left-hand side, respectively. By carefully computing the bound of the size of the computation, the proof of this theorem inside a bounded arithmetic is obtained, from which the consistency of the system is readily proven. This result apparently implies the separation of bounded arithmetic because Buss and Ignjatović stated that it is not possible to prove the consistency of a fragment of PV without induction but with substitution in Buss's S12. However, their proof actually shows that it is not possible to prove the consistency of the system, which is obtained by the addition of propositional logic and other axioms to a system such as ours. On the other hand, the system that we have considered is strictly equational, which is a property on which our proof relies. (shrink)

We present some proof-theoretic results for the normal modal logic whose characteristic axiom is \. We present a sequent system for this logic and a hypersequent system for its first-order form and show that these are equivalent to Hilbert-style axiomatizations. We show that the question of validity for these logics reduces to that of classical tautologyhood and first-order logical truth, respectively. We close by proving equivalences with a Fitch-style proof system for revision theory.

Kurt Gödel wrote (1964, p. 272), after he had read Husserl, that the notion of objectivity raises a question: “the question of the objective existence of the objects of mathematical intuition (which, incidentally, is an exact replica of the question of the objective existence of the outer world)”. This “exact replica” brings to mind the close analogy Husserl saw between our intuition of essences in Wesensschau and of physical objects in perception. What is it like to experience a mathematical proving (...) process? What is the ontological status of a mathematical proof? Can computer assisted provers output a proof? Taking a naturalized world account, I will assess the relationship between mathematics, the physical world and consciousness by introducing a significant conceptual distinction between proving and proof. I will propose that proving is a phenomenological conscious experience. This experience involves a combination of what Kurt Gödel called intuition, and what Husserl called intentionality. In contrast, proof is a function of that process — the mathematical phenomenon — that objectively self-presents a property in the world, and that results from a spatiotemporal unity being subject to the exact laws of nature. In this essay, I apply phenomenology to mathematical proving as a performance of consciousness, that is, a lived experience expressed and formalized in language, in which there is the possibility of formulating intersubjectively shareable meanings. (shrink)

We present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing and Odintsov & Wansing, as well as the modal logic KN4 with strong implication introduced in Goble. In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an FDE-style axiom (...) system and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown. (shrink)

This article investigates the proof theory of the Quantified Argument Calculus as developed and systematically studied by Hanoch Ben-Yami [3, 4]. Ben-Yami makes use of natural deduction, we, however, have chosen a sequent calculus presentation, which allows for the proofs of a multitude of significant meta-theoretic results with minor modifications to the Gentzen’s original framework, i.e., LK. As will be made clear in course of the article LK-Quarc will enjoy cut elimination and its corollaries.

In the present paper, the Fregean conception of proof-theoretic semantics that I developed elsewhere will be revised so as to better reflect the different roles played by open and closed derivations. I will argue that such a conception can deliver a semantic analysis of languages containing paradoxical expressions provided some of its basic tenets are liberalized. In particular, the notion of function underlying the Brouwer–Heyting–Kolmogorov explanation of implication should be understood as admitting functions to be partial. As argued in (...) previous work, the correctness of an inference rule should not be defined in terms of transmission of provability, but rather should be grounded on weaker principles, which I show that are motivated by consideration about the content of the inversion principle. In the conclusion, I briefly address the issue of compositionality, arguing that the violation of compositionality induced by paradoxes are no worse than others that are regarded, at least by Dummett, as wholly unproblematic. (shrink)

Hence, there is still controversy over which of the two versions of the deduction deserves priority and whether indeed any distinction between them can be maintained that would go beyond questions of presentation and involve the structure of the proof itself. Schopenhauer and Heidegger held that the first edition alone fully expresses Kant's unique philosophy, while Kant himself, as well as many other Kantians, have only seen a difference in the method of presentation.

Mathematical proofs generally allow for various levels of detail and conciseness, such that they can be adapted for a particular audience or purpose. Using automated reasoning approaches for teaching proof construction in mathematics presupposes that the step size of proofs in such a system is appropriate within the teaching context. This work proposes a framework that supports the granularity analysis of mathematical proofs, to be used in the automated assessment of students' proof attempts and for the presentation (...) of hints and solutions at a suitable pace. Models for granularity are represented by classifiers, which can be generated by hand or inferred from a corpus of sample judgments via machine-learning techniques. This latter procedure is studied by modeling granularity judgments from four experts. The results provide support for the granularity of assertion-level proofs but also illustrate a degree of subjectivity in assessing step size. (shrink)

The paper briefly surveys the sentential proof-theoretic semantics for fragment of English. Then, appealing to a version of Frege’s context-principle (specified to fit type-logical grammar), a method is presented for deriving proof-theoretic meanings for sub-sentential phrases, down to lexical units (words). The sentential meaning is decomposed according to the function-argument structure as determined by the type-logical grammar. In doing so, the paper presents a novel proof-theoretic interpretation of simple type, replacing Montague’s model-theoretic type interpretation (in arbitrary Henkin (...) models). The domains of derivations are collections of derivations in the associated “dedicated” natural-deduction proof-system, and functions therein (with no appeal to models, truth-values and elements of a domain). The compositionality of the semantics is analyzed. (shrink)

This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories $\widehat{ID}_\alpha and \widehat{ID}_{ the exact proof-theoretic ordinals of these systems are presented.

Many philosophers are sceptical about the power of philosophy to refute commonsensical claims. They look at the famous attempts and judge them inconclusive. I prove that, even if those famous attempts are failures, there are alternative successful philosophical proofs against commonsensical claims. After presenting the proofs I briefly comment on their significance.

In this dissertation, we shall investigate whether Tennant's criterion for paradoxicality(TCP) can be a correct criterion for genuine paradoxes and whether the requirement of a normal derivation(RND) can be a proof-theoretic solution to the paradoxes. Tennant’s criterion has two types of counterexamples. The one is a case which raises the problem of overgeneration that TCP makes a paradoxical derivation non-paradoxical. The other is one which generates the problem of undergeneration that TCP renders a non-paradoxical derivation paradoxical. Chapter 2 deals (...) with the problem of undergeneration and Chapter 3 concerns the problem of overgeneration. Chapter 2 discusses that Tenant’s diagnosis of the counterexample which applies CR−rule and causes the undergeneration problem is not correct and presents a solution to the problem of undergeneration. Chapter 3 argues that Tennant’s diagnosis of the counterexample raising the overgeneration problem is wrong and provides a solution to the problem. Finally, Chapter 4 addresses what should be explicated in order for RND to be a proof-theoretic solution to the paradoxes. (shrink)

In this paper I shall present a method for proving determinacy from large cardinals which, in many cases, seems to yield optimal results. One of the main applications extends theorems of Martin, Steel and Woodin about determinacy within the projective hierarchy. The method can also be used to give a new proof of Woodin's theorem about determinacy in L.The reason we look for optimal determinacy proofs is not only vanity. Such proofs serve to tighten the connection between large cardinals (...) and descriptive set theory, letting us bring our knowledge of one subject to bear on the other, and thus increasing our understanding of both. A classic example of this is the Harrington-Martin proof that -determinacy implies -determinacy. This is an example of a transfer theorem, which assumes a certain determinacy hypothesis and proves a stronger one. While the statement of the theorem makes no mention of large cardinals, its proof goes through 0#, first proving that-determinacy ⇒ 0# exists,and then that0# exists ⇒ -determinacyMore recent examples of the connection between large cardinals and descriptive set theory include Steel's proof thatADL ⇒ HODL ⊨ GCH,see [9], and several results of Woodin about models of AD+, a strengthening of the axiom of determinacy AD which Woodin has introduced. These proofs not only use large cardinals, but also reveal a deep, structural connection between descriptive set theoretic notions and notions related to large cardinals. (shrink)

Leading theologian Matthew Levering presents a thoroughgoing critical survey of the proofs of God's existence for readers interested in traditional Christian responses to the problem of atheism. Beginning with Tertullian and ending with Karl Barth, Levering covers twenty-one theologians and philosophers from the early church to the modern period, examining how they answered the critics of their day. He also shows the relevance of the classical arguments to contemporary debates and challenges to Christianity. In addition to students, this book will (...) appeal to readers of apologetics. (shrink)

We present a setting in which the search for a proof of B or a refutation of B can be carried out simultaneously: in contrast, the usual approach in automated deduction views proving B or proving ¬B as two, possibly unrelated, activities. Our approach to proof and refutation is described as a two-player game in which each player follows the same rules. A winning strategy translates to a proof of the formula and a counter-winning strategy translates to (...) a refutation of the formula. The game is described for multiplicative and additive linear logic . A game theoretic treatment of the multiplicative connectives is intricate and our approach to it involves two important ingredients. First, labeled graph structures are used to represent positions in a game and, second, the game playing must deal with the failure of a given player and with an appropriate resumption of play. This latter ingredient accounts for the fact that neither player might win. (shrink)

The present paper aims to show that the reconstruction of the formal framework of the proofs in Pr. An. 1.15, as proposed by Malink and Rosen 2013 (‘Proof by Assumption of the Possible in Prior Analytics 1.15’, Mind, 122, 953-85) is due to affront a double impasse. Malink and Rosen argue convincingly that Aristotle operates with two different modal frameworks, one as found in the system of modal logic presented in Prior Analytics 1.3 and 8-22, and one occurring in (...) many of Aristotle’s works, such as the Physics, De Caelo and the Metaphysics. However, they misconstrue the latter framework. More precisely, they misconstrue the domain of significance of what they call the ‘Principle of Necessitation’. As a consequence, bringing the two frameworks into one results into a contradictory modal logic. On the other hand, if the Principle of Necessitation is rectified, the proofs put forward by Malink and Rosen in the same paper are no longer available. (shrink)

Fuzzy logics are many-valued logics that are well suited to reasoning in the context of vagueness. They provide the basis for the wider field of Fuzzy Logic, encompassing diverse areas such as fuzzy control, fuzzy databases, and fuzzy mathematics. This book provides an accessible and up-to-date introduction to this fast-growing and increasingly popular area. It focuses in particular on the development and applications of "proof-theoretic" presentations of fuzzy logics; the result of more than ten years of intensive work by (...) researchers in the area, including the authors. In addition to providing alternative elegant presentations of fuzzy logics, proof-theoretic methods are useful for addressing theoretical problems and developing efficient deduction and decision algorithms. Proof-theoretic presentations also place fuzzy logics in the broader landscape of non-classical logics, revealing deep relations with other logics studied in Computer Science, Mathematics, and Philosophy. The book builds methodically from the semantic origins of fuzzy logics to proof-theoretic presentations such as Hilbert and Gentzen systems, introducing both theoretical and practical applications of these presentations. (shrink)

We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.

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

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)

We present a novel way of using proof nets for the multimodal Lambek calculus, which provides a general treatment of both the unary and binary connectives. We also introduce a correctness criterion which is valid for a large class of structural rules and prove basic soundness, completeness and cut elimination results. Finally, we will present a correctness criterion for the original Lambek calculus Las an instance of our general correctness criterion.

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)

Classical proof forests are a proof formalism for first-order classical logic based on Herbrand’s Theorem and backtracking games in the style of Coquand. First described by Miller in a cut-free setting as an economical representation of first-order and higher-order classical proof, defining features of the forests are a strict focus on witnessing terms for quantifiers and the absence of inessential structure, or ‘bureaucracy’.This paper presents classical proof forests as a graphical proof formalism and investigates the (...) possibility of composing forests by cut-elimination. Cut-reduction steps take the form of a local rewrite relation that arises from the structure of the forests in a natural way. Yet reductions, which are significantly different from those of the sequent calculus, are combinatorially intricate and do not exclude the possibility of infinite reduction traces, of which an example is given.Cut-elimination, in the form of a weak normalisation theorem, is obtained using a modified version of the rewrite relation inspired by the game-theoretic interpretation of the forests. It is conjectured that the modified reduction relation is, in fact, strongly normalising. (shrink)

First-order logic is formalized by means of tools taken from the logic of questions. A calculus of questions which is a counterpart of the Pure Calculus of Quantifiers is presented. A direct proof of completeness of the calculus is given.