In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic raises some technical and conceptual issues. We relate Sandqvist’s (complete) base-extension semantics of intuitionistic propositional logic to categorical proof theory (...) in presheaves, reconstructing categorically the soundness and completeness arguments, thereby demonstrating the naturality of Sandqvist’s constructions. This naturality includes Sandqvist’s treatment of disjunction that is based on its second-order or elimination-rule presentation. These constructions embody not just validity, but certain forms of objects of justifications. This analysis is taken a step further by showing that from the perspective of validity, Sandqvist’s semantics can also be viewed as the natural disjunction in a category of sheaves. (shrink)

Categorical proof theory is an approach to understanding the structure of proofs. We illustrate the idea first by analyzing G0̈del's Dialectica interpretation and the Diller-Nahm variant in categorical terms. Then we consider the problematic question of the structure of classical proofs. We show how double negation translations apply in the case of the Dialectica interpretations. Finally we formulate a proposal as to how to give a more faithful analysis of proofs in the sequent calculus.

The foundations of mathematics are divided into proof theory and set theory. Proof theory tries to justify the world of infinite mind from the standpoint of finite mind. Set theory tries to know more and more of the world of the infinite mind. The development of two subjects are discussed including a new proof of the accessibility of ordinal diagrams. Finally the world of large cardinals appears when we go slightly beyond girard's (...) class='Hi'>categorical approach to proof theory. (shrink)

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 show that the categoricity of second-order Peano axioms can be proved from the comprehension axioms. We also show that the categoricity of second-order Zermelo–Fraenkel axioms, given the order type of the ordinals, can be proved from the comprehension axioms. Thus these well-known categoricity results do not need the so-called “full” second-order logic, the Henkin second-order logic is enough. We also address the question of “consistency” of these axiom systems in the second-order sense, that is, the question of existence of (...) models for these systems. In both cases we give a consistency proof, but naturally we have to assume more than the mere comprehension axioms. (shrink)

We explore the existence and the size of infinite models of categorical theories having cardinality less than the size of the associated Tarski-Lindenbaum algebra. Restricting to totally transcendental, categorical theories we show that “Every tiny model is countable” is independent of ZFC. IfT is trivial there is at most one tiny model, which must be the algebraic closure of the empty set. We give a new proof that there are no tiny models ifT is not totally transcendental (...) and is non-trivial. (shrink)

In bilateral systems for classical logic, assertion and denial occur as primitive signs on formulas. Such systems lend themselves to an inferentialist story about how truth-conditional content of connectives can be determined by inference rules. In particular, for classical logic there is a bilateral proof system which has a property that Carnap in 1943 called categoricity. We show that categorical systems can be given for any finite many-valued logic using $n$-sided sequent calculus. These systems are understood as a (...) further development of bilateralism—call it multilateralism. The overarching idea is that multilateral proof systems can incorporate the logic of a variety of denial speech acts. So against Frege we say that denial is not the negation of assertion and, with Mark Twain, that denial is more than a river in Egypt. (shrink)

A system of logic usually comprises a language for which a model-theory and a proof-theory are defined. The model-theory defines the semantic notion of model-theoretic logical consequence (⊨), while the proof-theory defines the proof- theoretic notion of logical consequence (or logical derivability, ⊢). If the system in question is sound and complete, then the two notions of logical consequence are extensionally equivalent. The concept of full formalization is a more restrictive one and requires (...) in addition the preservation of the standard meanings of the logical terms in all the admissible interpretations of the logical calculus, as it is proof-theoretically defined. Although classical first-order logic is sound and complete, its standard formalizations fall short to be full formalizations since they allow non-intended interpretations. This fact poses a challenge for the logical inferentialism program, whose main tenet is that the meanings of the logical terms are uniquely determined by the formal axioms or rules of inference that govern their use in a logical calculus, i.e., logical inferentialism requires a categorical calculus. This paper is the first part of a more elaborated study which will analyze the categoricity problem from its beginning until the most recent approaches. I will first start by describing the problem of a full formalization in the general framework in which Carnap (1934/1937, 1943) formulated it for classical logic. Then, in sections IV and V, I shall discuss the way in which the mathematicians B.A. Bernstein (1932) and E.V. Huntington (1933) have previously formulated and analyzed it in algebraic terms for propositional logic and, finally, I shall discuss some critical reactions Nagel (1943), Hempel (1943), Fitch (1944), and Church (1944) formulated to these approaches. (shrink)

The categoricity problem for a system of logic reveals an asymmetry between the model-theoretic and the proof-theoretic resources of that logic. In particular, it reveals prima facie that the proof-theoretic instruments are insufficient for matching the envisaged model-theory, when the latter is already available. Among the proposed solutions for solving this problem, some make use of new proof-theoretic instruments, some others introduce new model-theoretic constrains on the proof-systems, while others try to use instruments from both (...) sides. On the proof-theoretical side, two main approaches for solving the categoricity problem for propositional classical logic consist in the enforcement of the formal systems of this logic by introducing rules of inference of a new kind. A multiple-conclusions logic allows rules of inference with more than one conclusion, while a bilateralist system contains rules of inference formulated in terms of assertion and rejection. Both these approaches reveal interesting formal features of logical reasoning. This paper analyses some of the advantages and limitations of these two approaches as solutions for a full formalization of logic, i.e., for a categorical formalization. (shrink)

Here we suggest a formal using of N.A. Vasil’ev’s logical ideas in categorical logic: the idea of “accidental” assertion is formalized with topoi and the idea of the notion of nonclassical negation, that is not based on incompatibility, is formalized in special cases of monoidal categories. For these cases, the variant of the law of “excluded n-th” suggested by Vasil’ev instead of the tertium non datur is obtained in some special cases of these categories. The paraconsistent law suggested by (...) Vasil’ev is also demonstrated with linear and tensor logics but in a form weaker than he supposed. As we have, in fact, many truth-values in linear logic and topos logic, the admissibility of the traditional notion of inference in the categorical interpretation of linear and intuitionistic proof theory is discussed. (shrink)

Even though the strong relationship between proof-theoretic and model-theoretic notions in one’s logical theory can be shown by soundness and completeness proofs, whether we can define the model-theoretic notions by means of the inferences in a proof system is not at all trivial. For instance, provable inferences in a proof system of classical logic in the logical framework do not determine its intended models as shown by Carnap (Formalization of logic, Harvard University Press, Cambridge, 1943), i.e., (...) there are non-Boolean models that satisfy its provable inferences. In the literature, this is known as the Categoricity problem or Carnap’s problem. In this paper, we will discuss the Categoricity problem (or Carnap’s problem) for three-valued logics K3 and LP. We will provide three different restrictions on admissible models that will deliver us categoricity results, some of which draw from the solutions provided for the Categoricity problem for classical logic in Belnap and Massey (Stud Log 49(1):67–82, 1990) and Bonnay and Westerståhl (Erkenntis 81(4):721–739, 2016). We will then argue that two of those solutions are philosophically well-motivated: (1) restricting the admissible models where negation is interpreted as a Strong Kleene truth-function, and (2) restricting the admissible models where a complex formula is assigned the third value when its immediate subformulas are assigned the third value. (shrink)

A natural extension of Natural Deduction was defined by Schroder-Heister where not only formulas but also rules could be used as hypotheses and hence discharged. It was shown that this extension allows the definition of higher-level introduction and elimination schemes and that the set $\{ \vee, \wedge, \rightarrow, \bot \}$ of intuitionist sentential operators forms a {\it complete} set of operators modulo the higher level introduction and elimination schemes, i.e., that any operator whose introduction and elimination rules are instances of (...) the higher-level schemes can be defined in terms of $\{ \vee, \wedge, \rightarrow, \bot \}$.The aim of the present work is to extend the well-known connections between Proof Theory and Category Theory to higher-level Natural Deduction. To be precise, we will show how an adjointness between cartesian closed categories with finite coproducts can be associated, in a systematic way, with any operator $\phi$ defined by the higher-level schemes. The objects in the categories will be rules instead of formulas. (shrink)

We elaborate on the approach to syllogistic reasoning based on “case identification” (Stenning & Oberlander, 1995; Stenning & Yule, 1997). It is shown that this can be viewed as the formalisation of a method of proof that dates back to Aristotle, namely proof by exposition ( ecthesis ), and that there are traces of this method in the strategies described by a number of psychologists, from St rring (1908) to the present day. We hypothesised that by rendering individual (...) cases explicit in the premises, the chance that reasoners would engage in a proof by exposition would be enhanced, and thus performance improved. To do so, we used syllogisms with singular premises (e.g., this X is Y ). This resulted in a uniform increase in performance as compared to performance on the associated standard syllogisms. These results cannot be explained by the main theories of syllogistic reasoning in their current state. (shrink)

Inductively defined structures are ubiquitous in mathematics; their specification is unambiguous and their properties are powerful. All fields of mathematical logic feature these structures prominently: the formula of a language, the set of theorems, the natural numbers, the primitive recursive functions, the constructive number classes and segments of the cumulative hierarchy of sets. -/- This dissertation gives a mathematical characterization of a species of inductively defined structures, called accessible domains, which include all of the above examples except the set of (...) theorems. The concept of an accessible domain comes from Wilfried Sieg's analysis of proof-theoretic practices, starting with his dissertation. In particular, he noticed the special epistemological character of elements of an accessible domain: they can always be uniquely identified with their build-up. Generally, the unique build-up of elements justifies the principles of induction and recursion. -/- I use category theory to give an abstract characterization of accessible domains. I claim that accessible domains are all instances of initial algebras for endofunctors. Grounded in the historical roots of Sieg's discussions, this dissertation shows how the properties of initial algebras for endofunctors and accessible domains coincide in a satisfying and natural way. -/- Filling out this characterization, I show how important examples of accessible domains fit into this broad characterization. I first characterize some accessible domains by relatively simple functors (e.g. finite, polynomial, those that preserve certain colimits) where we can see how iterating the functor can produce the accessible domain. Then I describe accessible domains that result from more involved specifications (e.g. ordinals and segments of the cumulative hierarchies associated with CZF, IZF, and ZF) by relying heavily on algebraic set theory. I end with a discussion of some of the methodological features of category theory in particular that helped characterize accessible domains. (shrink)

We present the paradigm of categories-as-syntax. We briefly recall the even stronger paradigm categories-as-machine-language which led from -calculus to categorical combinators viewed as basic instructions of the Categorical Abstract Machine. We extend the categorical combinators so as to describe the proof theory of first order logic and higher order logic. We do not prove new results: the use of indexed categories and the description of quantifiers as adjoints goes back to Lawvere and has been developed (...) in detail in works of R. Seely. We rather propose a syntactic, equational presentation of those ideas. We sketch the (quasi-equational) categorical structures for dependent types, following ideas of J. Cartmell (contextual categories). All these theories of categorical combinators, together with the translations from -calculi into them, are introduced smoothly, thanks to the systematic use of– - an abstract variable-free notation for -calculus, going back to N. De Bruijn, – - a sequent formulation of the natural deduction. (shrink)

Babenyshev and Martins proved that two hidden multi-sorted deductive systems are deductively equivalent if and only if there exists an isomorphism between their corresponding lattices of theories that commutes with substitutions. We show that the π-institutions corresponding to the hidden multi-sorted deductive systems studied by Babenyshev and Martins satisfy the multi-term condition of Gil-F´erez. This provides a proof of the result of Babenyshev and Martins by appealing to the general result of Gil-F´erez pertaining to arbitrary multi-term π-institutions. The approach (...) places hidden multi-sorted deductive systems in a more general framework and bypasses the laborious reuse of well-known proof techniques from traditional abstract algebraic logic by using “off the shelf” tools. (shrink)

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)

Mathematical realists have long invoked the categoricity of axiomatizations of arithmetic and analysis to explain how we manage to fix the intended meaning of their respective vocabulary. Can this strategy be extended to set theory? Although traditional wisdom recommends a negative answer to this question, Vann McGee (1997) has offered a proof that purports to show otherwise. I argue that one of the two key assumptions on which the proof rests deprives McGee's result of the significance he (...) and the realist want to attribute to it. I consider two strategies to deal with the problem --- one of which is outlined by McGee himself (2000) --- and argue that both of them fail. I end with some remarks on the prospects for mathematical realism in the light of my discussion. (shrink)

A new case of Shelah's eventual categoricity conjecture is established: Let be an abstract elementary class with amalgamation. Write and. Assume that is H2‐tame and has primes over sets of the form. If is categorical in some, then is categorical in all. The result had previously been established when the stronger locality assumptions of full tameness and shortness are also required. An application of the method of proof of the mentioned result is that Shelah's categoricity conjecture holds (...) in the context of homogeneous model theory (this was known, but our proof gives new cases): If D be a homogeneous diagram in a first‐order theory T and D is categorical in a, then D is categorical in all. (shrink)

We consider a “polarized” version of bi-intuitionistic logic [5, 2, 6, 4] as a logic of assertions and hypotheses and show that it supports a “rich proof theory” and an interesting categorical interpretation, unlike the standard approach of C. Rauszer’s Heyting-Brouwer logic [28, 29], whose categorical models are all partial orders by Crolard’s theorem [8]. We show that P.A. Melliès notion of chirality [21, 22] appears as the right mathematical representation of the mirror symmetry between the (...) intuitionistic and co-intuitionistc sides of polarized bi-intuitionism. Philosophically, we extend Dalla Pozza and Garola’s pragmatic interpretation of intuitionism as a logic of assertions [10] to bi-intuitionism as a logic of assertions and hypotheses. We focus on the logical role of illocutionary forces and justification conditions in order to provide “intended interpretations” of logical systems that classify inferential uses in natural language and remain acceptable from an intuitionistic point of view. Although Dalla Pozza and Garola originally provide a constructive interpretation of intuitionism in a classical setting, we claim that some conceptual refinements suffice to make their “pragmatic interpretation” a bona fide representation of intuitionism. We sketch a meaning-asuse interpretation of co-intuitionism that seems to fulfil the requirements of Dummett and Prawitz’s justificationist approach. We extend the Brouwer-Heyting-Kolmogorov interpretation to bi-intuitionism by regarding co-intuitionistic formulas as types of the evidence for them: if conclusive evidence is needed to justify assertions, only a scintilla of evidence suffices to justify hypotheses. (shrink)

There are still on-going debates on what exactly is wrong with Prior’s pathological “tonk.” In this article I argue, on the basis of categorical inferentialism, that two notions of inconsistency ought to be distinguished in an appropriate account of tonk; logic with tonk is inconsistent as the theory of propositions, and it is due to the fallacy of equivocation; in contrast to this diagnosis of the Prior’s tonk problem, nothing is actually wrong with tonk if logic is viewed (...) as the theory of proofs rather than propositions, and tonk perfectly makes sense in terms of the identity of proofs. Indeed, there is fully complete semantics of proofs for tonk, which allows us to link the Prior’s old philosophical idea with contemporary issues at the interface of categorical logic, computer science, and quantum physics, and thereby to expose commonalities between the laws of Reason and the laws of Nature, which are what logic and physics are respectively about. I conclude the article by articulating the ideas of categorical logical positivism and pluralistic unified science as its goal, including the unification of realist and antirealist conceptions of meaning by virtue of the categorical logical basis of metaphysics. (shrink)

Gottfried Martin has recently reminded us of a useful distinction between two possible ways of doing metaphysics. We may proceed by framing a “theory of principles” or by proposing a “theory of being”. Aristotle explicitly formulates both possibilities as the task of metaphysics, formulating a theory of principles in his doctrine of the four types of causal explanation in the first book of the Metaphysics, while exploring the theory of being in a number of other passages, (...) such as Book I, chapters 6 and 9; Book X, chapter 2; and Book XIII. These passages do not elaborate principles whereby we can analyze the structure of certain entities, be they causes, substances or forms, but rather concern themselves with the ontological status of these entities—in what sense can they be said to be? In Plato this distinction is more implicit, but we may contrast the theory of forms developed in the Phaedo and the Republic with the subsequent probing investigation of the being of these forms in the Parmenides and the Sophist. Kant “explicitly claims to have discovered and presented a complete and necessary system of the basic concepts and principles. The proof of the completeness and necessity of this system is the aim of the middle part of the Critique of Pure Reason, the Transcendental Analytic.” Yet. (shrink)

Equivalences and translations between consequence relations abound in logic. The notion of equivalence can be defined syntactically, in terms of translations of formulas, and order-theoretically, in terms of the associated lattices of theories. W. Blok and D. Pigozzi proved in [4] that the two definitions coincide in the case of an algebraizable sentential deductive system. A refined treatment of this equivalence was provided by W. Blok and B. Jónsson in [3]. Other authors have extended this result to the cases of (...) k-deductive systems and of consequence relations on associative, commutative, multiple conclusion sequents. Our main result subsumes all existing results in the literature and reveals their common character. The proofs are of order-theoretic and categorical nature. (shrink)

Canonical extension has proven to be a powerful tool in algebraic study of propositional logics. In this paper we describe a generalisation of the theory of canonical extension to the setting of first order logic. We define a notion of canonical extension for coherent categories. These are the categorical analogues of distributive lattices and they provide categorical semantics for coherent logic, the fragment of first order logic in the connectives ∧, ∨, 0, 1 and ∃. We describe (...) a universal property of our construction and show that it generalises the existing notion of canonical extension for distributive lattices. Our new construction for coherent categories has led us to an alternative description of the topos of types, introduced by Makkai in [22]. This allows us to give new and transparent proofs of some properties of the action of the topos of types construction on morphisms. Furthermore, we prove a new result relating, for a coherent category C, its topos of types to its category of models. (shrink)

Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics and computer science. The book contains a wealth of results on proof-theoretical systems, including extensions (...) of such systems from logic to mathematics, and on the connection between the two main forms of structural proof theory - natural deduction and sequent calculus. The authors emphasize the computational content of logical results. A special feature of the volume is a computerized system for developing proofs interactively, downloadable from the web and regularly updated. (shrink)

This paper provides an analysis of contrary-to-duty reasoning from the proof-theoretical perspective of category theory. While Chisholm’s paradox hints at the need of dyadic deontic logic by showing that monadic deontic logics are not able to adequately model conditional obligations and contrary-to-duties, other arguments can be objected to dyadic approaches in favor of non-monotonic foundations. We show that all these objections can be answered at one fell swoop by modeling conditional obligations within a deductive system defined as an (...) instance of a symmetric monoidal closed category. Using category theory as a foundational framework for logic, we show that it is possible to model conditional normative reasoning and conflicting obligations within a monadic approach without adding further operators or considering deontic conditionals as primitive. (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)

Versions and extensions of intuitionistic and modal logic involving biHeyting and bimodal operators, the axiom of constant domains and Barcan's formula, are formulated as structured categories. Representation theorems for the resulting concepts are proved. Essentially stronger versions, requiring new methods of proof, of known completeness theorems are consequences. A new type of completeness result, with a topos theoretic character, is given for theories satisfying a condition considered by Lawvere . The completeness theorems are used to conclude results asserting that (...) certain logics are conservatively interpretable in others. (shrink)

This paper casts doubt on a recent criticism of Frege's theory of concepts and extensions by showing that it misses one of Frege's most important contributions: the derivation of the infinity of the natural numbers. We show how this result may be incorporated into the conceptual structure of Zermelo- Fraenkel Set Theory. The paper clarifies the bearing of the development of the notion of a real-valued function on Frege's theory of concepts; it concludes with a brief discussion (...) of the claim that the standard interpretation of second-order logic is necessary for the derivation of the Peano Postulates and the proof of their categoricity. (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.

On the basis of passages from John Buridan's Summula Suppositionibus and Sophismata, E. Karger has reconstructed what could be called the 'Buridanian theory of inferential relations between doubly quantified propositions', presented in her 1993 article 'A theory of immediate inference contained in Buridan's logic'. In the reconstruction, she focused on the syntactical elements of Buridan's theory of modes of personal supposition to extract patterns of formally valid inferences between members of a certain class of basic categorical (...) propositions. The present study aims at offering semantic corroboration 'a proof of soundness' to the inferential relations syntactically identified by E. Karger, by means of the analysis of Buridan's semantic definitions of the modes of personal supposition. The semantic analysis is done with the help of some modern logical concepts, in particular that of the model. In effect, the relations of inference syntactically established are shown to hold also from a semantic point of view, which means thus that this fragment of Buridan's logic can be said to be sound. (shrink)

Dividing chains have been used as conditions to isolate adequate subclasses of simple theories. In the first part of this paper we present an introduction to the area. We give an overview on fundamental notions and present proofs of some of the basic and well-known facts related to dividing chains in simple theories. In the second part we discuss various characterizations of the subclass of low theories. Our main theorem generalizes and slightly extends a well-known fact about the connection between (...) dividing chains and Morley sequences (in our case: independent sequences). Moreover, we are able to give a proof that is shorter than the original one. This result motivates us to introduce a special property of formulas concerning independent dividing chains: For any dividing chain there exists an independent dividing chain of the same length. We study this property in the context of low, short and ω -categorical simple theories, outline some examples and define subclasses of low and short theories, which imply this property. The results give rise to further studies of the relationships between some subclasses of simple theories. (shrink)

General theories are reductionist explications of apparently independent facts. Here, in reviewing the literature, I develop a GT to simplify the cluttered landscape of cancer therapy targets by revealing they cluster parsimoniously according to only a few underlying principles. The first principle is that targets can be only exploited by either or both of two fundamentally different approaches: causality-inhibition, and ‘acausal’ recognition of some marker or signature. Nonetheless, each approach must achieve both of two separate goals, efficacy and selectivity ; (...) if the mechanisms are known, this provides a definition of rational treatment. The second principle is target fragmentation, whereby the target may perform up to three categoric functions, potentially mediated by physically different target molecules, even on different cell types, or circulating freely. This GT remains incomplete until the minimal requirements for cure, or alternatively, proof that cure is impossible, become predictable. A reductionist General Theory of Cancer Targets is presented, proposing that all good targets are based either on causality-inhibition, or recognition; essential tasks emerge differently in each case. Sophisticated hybrids may provide additional benefit. General theory analysis, including target fragmentation concepts, provides deeper insights into therapeutic mechanisms. (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.

This paper deals with a proof theory for a theory T22 of recursively Mahlo ordinals in the form of Π2-reflecting on Π2-reflecting ordinals using a subsystem Od of the system O of ordinal diagrams in Arai 353). This paper is the first published one in which a proof-theoretic analysis à la Gentzen–Takeuti of recursively large ordinals is expounded.

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)

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)

This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O of ordinal diagrams in Arai 1375). This is a sequel to the previous one 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically.

This chapter focuses on the development of Gerhard Gentzen's structural proof theory and its connections with intuitionism. The latter is important in proof theory for several reasons. First, the methods of Hilbert's old proof theory were limited to the “finitistic” ones. These methods proved to be insufficient, and they were extended by infinitistic principles that were still intuitionistically meaningful. It is a general tendency in proof theory to try to use weak principles. (...) A second reason for the importance of intuitionism for proof theory is that the proof-theoretical study of intuitionistic logic has become a prominent part of logic, with applications in computer science. (shrink)

The paper contains proof-theoretic investigation on extensions of Kripke-Platek set theory, KP, which accommodate first-order reflection. Ordinal analyses for such theories are obtained by devising cut elimination procedures for infinitary calculi of ramified set theory with Пn reflection rules. This leads to consistency proofs for the theories KP+Пn reflection using a small amount of arithmetic and the well-foundedness of a certain ordinal system with respect to primitive decending sequences. Regarding future work, we intend to avail ourselves of (...) these new cut elimination techniques to attain an ordinal analysis of П12 comprehension by approaching П12 comprehension through transfinite levels of reflection. (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 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.

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)

Proof-theoretic methods are developed for subsystems of Johansson’s logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems. In particular, cut-free complete sequent calculi are introduced and used to provide a proof of the fact that the systems satisfy the Craig interpolation property. Alternative versions of the calculi are later obtained by means of an appropriate loop-checking history mechanism. Termination of the new calculi is (...) proved, and used to conclude that the considered logical systems are PSPACE-complete. (shrink)

We show that the existence of a weakly compact cardinal over the Zermelo–Fraenkel's set theory ZF is proof-theoretically reducible to iterations of Mostowski collapsings and Mahlo operations.