In [2], Bar-Hillel, Gaifman, and Shamir prove that the simple phrase structure grammars (SPGs) defined by Chomsky are equivalent in a certain sense to Bar-Hillel's bidirectional categorial grammars (BCGs). On the other hand, Cohen [3] proves the equivalence of the latter ones to what the calls free categorial grammars (FCGs). They are closely related to Lambek's syntactic calculus which, in turn, is based on the idea due to Ajdukiewicz [1]. For the reasons which will be discussed in the last section, (...) Cohen's proof seems to be at least incomplete. This paper yields a direct proof of the equivalence ofFCGs andSPGs. (shrink)

Schwichtenberg showed that the System T definable functionals are closed under a rule-like version Spector’s bar recursion of lowest type levels 0 and 1. More precisely, if the functional Y which controls the stopping condition of Spector’s bar recursor is T-definable, then the corresponding bar recursion of type levels 0 and 1 is already T-definable. Schwichtenberg’s original proof, however, relies on a detour through Tait’s infinitary terms and the correspondence between ordinal recursion for α < ε₀ and primitive recursion (...) over finite types. This detour makes it hard to calculate on given concrete system T input, what the corresponding system T output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into T-definitions under the conditions of Schwichtenberg’s theorem. Finally, with the explicit construction we can also easily state a sharper result: if Y is in the fragment Tᵢ then terms built from BR^ℕ,σ for this particular Y are definable in the fragment T_i+max{1,level(σ)}+2. (shrink)

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

We discuss the problem raised by Miller to re-prove the well-known equivalences of some Lindenbaum theorems for deductive systems without an application of the Axiom of Choice. We present five special constructions of deductive systems, each of them providing some partial solutions to the mathematical problem. We conclude with a short discussion of the underlying philosophical problem of deciding, whether a given proof satisfies our demand that the Axiom of Choice is not applied.

We present a direct proof of the consistency of the existence of a five element basis for the uncountable linear orders. Our argument is based on the approach of König, Larson, Moore and Veličković and simplifies the original proof of Moore.

Shelah has shown that the number d, the smallest cardinality of a dominating family, is less than or equal to the number i, the smallest cardinality of a maximal independent family on ω. This was done using a downward Löwenheim-Skolem argument. Thus it is interesting to find a direct “elementary” proof. Here we show that this can be done.

We give a simplified proof of the main lemma in “Ramsey filters and the reaping number—Con” by Goldstern and Shelah.

In this paper, we present the outline for a goal-directed proof procedure for abductive reasoning and compare this procedure with Aliseda’s approach.

Classically, weak König's lemma and Brouwer's fan theorem for detachable bars are equivalent. We give a direct constructive proof that the former implies the latter.

We shall give a direct proof of the independence result of a Buchholz style-Hydra Game on labeled finite trees. We shall show that Takeuti-Arai's cut-elimination procedure of $(\Pi^{1}_{1}-CA) + BI$ and of the iterated inductive definition systems can be directly expressed by the reduction rules of Buchholz's Hydra Game. As a direct corollary the independence result of the Hydra Game follows.

In [BAT 00b], the flat Rescher–Manor consequence relations — the Free, Strong, Argued, C-Based, andWeak consequence relation—were shown to be characterized by inconsistency-adaptive logics defined from the paraconsistent logic CLuN. This provided these consequence relations with a dynamic proof theory. In the present paper we show that the detour via an inconsistency-adaptive logic is not necessary. We present a direct dynamic proof theory, formulated in the language of Classical Logic, and prove its adequacy. The present paper contains (...) the first direct dynamic proof theory for consequence relations that are characterized by an adaptive logic. (shrink)

Peter van Inwagen's influential Direct Argument (DA) for the incompatibility of moral responsibility and causal determinism makes use of an inference rule he calls "Rule B." Michael McKenna has argued that van Inwagen's defense of this rule is dialectically inappropriate because it is based entirely on alleged “confirming” cases that are not of the right kind to justify the use of Rule B in DA. Here I argue that McKenna’s objection is on the right track but more must be (...) said if we are to see why. To fill in the gaps I consider a recent attempt by Ira M. Schnall and David Widerker to defend DA against McKenna’s objection. I argue that neither prong of their attack is successful against a variation on McKenna’s basic argument. In the course of responding to Schnall and Widerker’s objections to McKenna, I identify what is, as I argue, the real reason DA fails in its purpose to shift the burden of proof. (shrink)

Different natural deduction proof systems for intuitionistic and classical logic —and related logical systems—differ in fundamental properties while sharing significant family resemblances. These differences become quite stark when it comes to the structural rules of contraction and weakening. In this paper, I show how Gentzen and Jaśkowski’s natural deduction systems differ in fine structure. I also motivate directed proof nets as another natural deduction system which shares some of the design features of Genzen and Jaśkowski’s systems, but which (...) differs again in its treatment of the structural rules, and has a range of virtues absent from traditional natural deduction systems. (shrink)

Peter van Inwagen's Direct Argument (DA) for incompatibilism purports to establish incompatibilism with respect to moral responsibility and determinism without appealing to assumptions that compatibilists usually consider controversial. Recently, Michael McKenna has presented a novel critique of DA. McKenna's critique raises important issues about philosophical dialectics. In this article, we address those issues and contend that his argument does not succeed.

We develop a combinatorial model to study the evolution of graphs underlying proofs during the process of cut elimination. Proofs are two-dimensional objects and differences in the behavior of their cut elimination can often be accounted for by differences in their two-dimensional structure. Our purpose is to determine geometrical conditions on the graphs of proofs to explain the expansion of the size of proofs after cut elimination. We will be concerned with exponential expansion and we give upper and lower bounds (...) which depend on the geometry of the graphs. The lower bound is computed passing through the notion of universal covering for directed graphs. In this paper we present ground material for the study of cut elimination and structure of proofs in purely combinatorial terms. We develop a theory of duplication for directed graphs and derive results on graphs of proofs as corollaries. (shrink)

While direct proof is widely considered the paradigm of the acquisition of knowledge by deductive means, indirect proof has traditionally been criticized as showing merely ‘that’ its conclusion is true and not ‘why’ it is true. This paper accounts for the traditional objection by emphasizing the argumentative role in indirect proof of logical principles such as excluded middle and non-contradiction.

We give a proof of Hechler's theorem that any \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\aleph_1$\end{document}-directed partial order can be embedded via a ccc forcing notion cofinally into \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\omega^\omega$\end{document} ordered by eventual dominance. The proof relies on the standard forcing relation rather than the variant introduced by Hechler.

In this paper it is shown that addition of certain reductions to the standard cut removing reductions of deductions in prepositional logic makes prepositional logic non-normalizable. From this follows that some provable propositions in prepositional logic has no direct proof.

This thesis is concerned with extending the underlying logical approach as well as the breadth of applications of the proof mining program to various (mostly previously untreated) areas of nonlinear analysis and optimization, with a particular focus being placed on topics which involve set-valued operators.For this, we extend the current logical methodology of proof mining by new systems and corresponding so-called logical metatheorems that cover these more involved areas of nonlinear analysis. Most of these systems crucially rely on (...) the use of intensional methods, treating sets with potentially high quantifier complexity in the defining matrix via characteristic functions and axioms that describe only their properties and do not completely characterize the elements of the sets.The applicability of all of these metatheorems is then substantiated by a range of case studies for the respective areas which in particular also highlight the naturalness of the use of intensional methods in the design of the corresponding systems.The first new area covered thereby is the theory of nonlinear semigroups induced by corresponding evolution equations for accretive operators. In that context, we present (besides an initial foray into the area from 2015) essentially the first applications of proof mining to the theory of partial differential equations. Concretely, we provide quantitative versions of four central results on the asymptotic behavior of solutions to such equations.The second new area unlocked in this thesis is that of the continuous dual of a Banach space and its norm (which are also approached via intensional methods). This in particular relies on a proof-theoretically tame treatment of suprema over (certain) bounded sets in this intensional context which is further exploited later on. These systems, which give access to this until now untreated fundamental notion from functional analysis, are then used to provide further substantial extensions to treat various notions from convex analysis like the Fréchet derivative of a convex function, Fenchel conjugates, Bregman distances, and monotone operators on Banach spaces in the sense of Browder.These systems are then utilized to provide applications in the context of Picard- and Halpern-style iterations of so-called Bregman strongly nonexpansive mappings where we provide both new quantitative and qualitative results.Lastly, we discuss the key notion of extensionality of a set-valued operator and its relation to set-theoretic maximality principles in more depth (which was already singled out—to some degree—in previous work). We thereby exhibit an issue arising with treating full extensionality in the context of these intensional approaches to set-valued operators and present useful fragments of the full extensionality statement where these issues are avoided.Corresponding to these fragments, we discuss a range of uniform continuity statements for set-valued operators beyond the usual notion involving the Hausdorff-metric. In particular, in that context, we utilize the previous tame treatment of suprema over bounded sets to also provide the first proof-theoretic treatment of that Hausdorff-metric in the context of systems for proof mining.The applicability of this treatment of the Hausdorff-metric is then in particular substantiated by a last case study where we provide quantitative information for a Mann-type iteration of set-valued mappings which are nonexpansive w.r.t. the Hausdorff-metric.The abstract was taken directly from the thesis.Abstract prepared by Nicholas Pischke, Technische Universität Darmstadt, Darmstadt, GermanyE-mail: [email protected]: https://doi.org/10.26083/tuprints-00026584. (shrink)

In this work we develop goal-directed deduction methods for the implicational fragment of several modal logics. We give sound and complete procedures for strict implication of K, T, K4, S4, K5, K45, KB, KTB, S5, G and for some intuitionistic variants. In order to achieve a uniform and concise presentation, we first develop our methods in the framework of Labelled Deductive Systems [Gabbay 96]. The proof systems we present are strongly analytical and satisfy a basic property of cut admissibility. (...) We then show that for most of the systems under consideration the labelling mechanism can be avoided by choosing an appropriate way of structuring theories. One peculiar feature of our proof systems is the use of restart rules which allow to re-ask the original goal of a deduction. In case of K, K4, S4 and G, we can eliminate such a rule, without loosing completeness. In all the other cases, by dropping such a rule, we get an intuitionistic variant of each system. The present results are part of a larger project of a goal directed proof theory for non-classical logics; the purpose of this project is to show that most implicational logics stem from slight variations of a unique deduction method, and from different ways of structuring theories. Moreover, the proof systems we present follow the logic programming style of deduction and seem promising for proof search [Gabbay and Reyle 84, Miller et al. 91]. (shrink)

A famous theorem by van der Waerden states the following: Given any finite coloring of the integers, one color contains arbitrarily long arithmetic progressions. Equivalently, for every q,k, there is an N = N(q,k) such that for every q-coloring of an interval of length N one color contains a progression of length k. An obvious question is what is the growth rate of N = N(q,k). Some proofs, like van der Waerden's combinatorial argument, answer this question directly, while the topological (...) proof by Furstenberg and Weiss does not. We present an analysis of (Girard's variant of) Furstenberg and Weiss's proof based on monotone functional interpretation, both yielding bounds and providing a general illustration of proof mining in topological dynamics. The bounds do not improve previous results by Girard, but only—as is also revealed by the analysis—because the combinatorial proof and the topological dynamics proof in principle are identical. (shrink)

We prove a theorem (1.7) about partial orders which can be viewed as a version of the Barwise compactness theorem which does not mention logic. The Barwise compactness theorem is easily equivalent to 1.7 + "Every Henkin set has a model". We then make the observation that 1.7 gives us the definability of forcing for quantifier-free sentences in the forcing language and use this to give a direct proof of the truth and definability lemmas of forcing.

Proof complexity is a rich subject drawing on methods from logic, combinatorics, algebra and computer science. This self-contained book presents the basic concepts, classical results, current state of the art and possible future directions in the field. It stresses a view of proof complexity as a whole entity rather than a collection of various topics held together loosely by a few notions, and it favors more generalizable statements. Lower bounds for lengths of proofs, often regarded as the key (...) issue in proof complexity, are of course covered in detail. However, upper bounds are not neglected: this book also explores the relations between bounded arithmetic theories and proof systems and how they can be used to prove upper bounds on lengths of proofs and simulations among proof systems. It goes on to discuss topics that transcend specific proof systems, allowing for deeper understanding of the fundamental problems of the subject. (shrink)

The notion of proof is central to mathematics yet it is one of the most difficult aspects of the subject to teach and master. In particular, undergraduate mathematics students often experience difficulties in understanding and constructing proofs. Understanding Mathematical Proof describes the nature of mathematical proof, explores the various techniques that mathematicians adopt to prove their results, and offers advice and strategies for constructing proofs. It will improve students’ ability to understand proofs and construct correct proofs of (...) their own. The first chapter of the text introduces the kind of reasoning that mathematicians use when writing their proofs and gives some example proofs to set the scene. The book then describes basic logic to enable an understanding of the structure of both individual mathematical statements and whole mathematical proofs. It also explains the notions of sets and functions and dissects several proofs with a view to exposing some of the underlying features common to most mathematical proofs. The remainder of the book delves further into different types of proof, including direct proof, proof using contrapositive, proof by contradiction, and mathematical induction. The authors also discuss existence and uniqueness proofs and the role of counter examples. (shrink)

Gentzen writes in the published version of his doctoral thesis Untersuchungen über das logische Schliessen that he was able to prove the normalization theorem only for intuitionistic natural deduction, but not for classical. To cover the latter, he developed classical sequent calculus and proved a corresponding theorem, the famous cut elimination result. Its proof was organized so that a cut elimination result for an intuitionistic sequent calculus came out as a special case, namely the one in which the sequents (...) have at most one formula in the right, succedent part. Thus, there was no need for a direct proof of normalization for intuitionistic natural deduction. The only traces of such a proof in the published thesis are some convertibilities, such as when an implication introduction is followed by an implication elimination [1934–35, II.5.13]. It remained to Dag Prawitz in 1965 to work out a proof of normalization. Another, less known proof was given also in 1965 by Andres Raggio.We found in February 2005 an early handwritten version of Gentzen's thesis, with exactly the above title, but with rather different contents: Most remarkably, it contains a detailed proof of normalization for what became the standard system of natural deduction. The manuscript is located in the Paul Bernays collection at the ETH-Zurichwith the signum Hs. 974: 271. Bernays must have gotten it well before the time of his being expelled from Göttingen on the basis of the racial laws in April 1933. (shrink)

Mathematicians judge proofs to possess, or lack, a variety of different qualities, including, for example, explanatory power, depth, purity, beauty and fit. Philosophers of mathematical practice have begun to investigate the nature of such qualities. However, mathematicians frequently draw attention to another desirable proof quality: being motivated. Intuitively, motivated proofs contain no "puzzling" steps, but they have received little further analysis. In this paper, I begin a philosophical investigation into motivated proofs. I suggest that a proof is motivated (...) if and only if mathematicians can identify (i) the tasks each step is intended to perform; and (ii) where each step could have reasonably come from. I argue that motivated proofs promote understanding, convey new mathematical resources and stimulate new discoveries. They thus have significant epistemic benefits and directly contribute to the efficient dissemination and advancement of mathematical knowledge. Given their benefits, I also discuss the more practical matter of how we can produce motivated proofs. Finally I consider the relationship between motivated proofs and proofs which are explanatory, beautiful and fitting. (shrink)

We examine 'weak-distributivity' as a rewriting rule $??$ defined on multiplicative proof-structures (so, in particular, on multiplicative proof-nets: MLL). This rewriting does not preserve the type of proof-nets, but does nevertheless preserve their correctness. The specific contribution of this paper, is to give a direct proof of completeness for $??$: starting from a set of simple generators (proof-nets which are a n-ary ⊗ of &-ized axioms), any mono-conclusion MLL proof-net can be reached by (...) $??$ rewriting (up to ⊗ and & associativity and commutativity). (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.

The paper explores the potential of Byzantine diagrams in syllogistic logic. Byzantine diagrams are originated by Byzantine scholars in the early modern period to use as tools for teaching and studying Aristotelian logic. This paper presents pioneering work on employing Byzantine diagrams for checking syllogistic validity through reduction.

A sequent calculus methodology for systems of agency based on branching-time frames with agents and choices is proposed, starting with a complete and cut-free system for multi-agent deliberative STIT; the methodology allows a transparent justification of the rules, good structural properties, analyticity, direct completeness and decidability proofs.

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)

By rephrasing quantifier-free axioms as rules of derivation in sequent calculus, we show that the generalized Steiner–Lehmus theorem admits a direct proof in classical logic. This provides a partial answer to a question raised by Sylvester in 1852. We also present some comments on possible intuitionistic approaches.

The paper explores the potential of Byzantine diagrams in syllogistic logic. Byzantine diagrams are originated by Byzantine scholars in the early modern period to use as tools for teaching and studying Aristotelian logic. This paper presents pioneering work on employing Byzantine diagrams for checking syllogistic validity through reduction.

The meaning of a formula built out of proof-functional connectives depends in an essential way upon the intensional aspect of the proofs of the component subformulas. We study three such connectives, strong equivalence (where the two directions of the equivalence are established by mutually inverse maps), strong conjunction (where the two components of the conjunction are established by the same proof) and relevant implication (where the implication is established by an identity map). For each of these connectives we (...) give a type assignment system, a realizability semantics, and a completeness theorem. This form of completeness implies the semantic completeness of the type assignment system. (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.

This mathematics textbook covers the fundamental ideas used in writing proofs. Proof techniques covered include direct proofs, proofs by contrapositive, proofs by contradiction, proofs in set theory, proofs of existentially or universally quantified predicates, proofs by cases, and mathematical induction. Inductive and deductive reasoning are explored. A straightforward approach is taken throughout. Plenty of examples are included and lots of exercises are provided after each brief exposition on the topics at hand. The text begins with a study of (...) symbolic logic, deductive reasoning, and quantifiers. Inductive reasoning and making conjectures are examined next, and once there are some statements to prove, techniques for proving conditional statements, disjunctions, biconditional statements, and quantified predicates are investigated. Terminology and proof techniques in set theory follow with discussions of the pick-a-point method and the algebra of sets. Cartesian products, equivalence relations, orders, and functions are all incorporated. Particular attention is given to injectivity, surjectivity, and cardinality. The text includes an introduction to topology and abstract algebra, with a comparison of topological properties to algebraic properties. This book can be used by itself for an introduction to proofs course or as a supplemental text for students in proof-based mathematics classes. The contents have been rigorously reviewed and tested by instructors and students in classroom settings. (shrink)

The traditional view of evidence in mathematics is that evidence is just proof and proof is just derivation. There are good reasons for thinking that this view should be rejected: it misrepresents both historical and current mathematical practice. Nonetheless, evidence, proof, and derivation are closely intertwined. This paper seeks to tease these concepts apart. It emphasizes the role of argumentation as a context shared by evidence, proofs, and derivations. The utility of argumentation theory, in general, and argumentation (...) schemes, in particular, as a methodology for the study of mathematical practice is thereby demonstrated. Argumentation schemes represent an almost untapped resource for mathematics education. Notably, they provide a consistent treatment of rigorous and non-rigorous argumentation, thereby working to exhibit the continuity of reasoning in mathematics with reasoning in other areas. Moreover, since argumentation schemes are a comparatively mature methodology, there is a substantial body of existing work to draw upon, including some increasingly sophisticated software tools. Such tools have significant potential for the analysis and evaluation of mathematical argumentation. The first four sections of the paper address the relationships of evidence to proof, proof to derivation, argument to proof, and argument to evidence, respectively. The final section directly addresses some of the educational implications of an argumentation scheme account of mathematical reasoning. (shrink)

Quantum theory predicts that, e.g., in a Stern-Gerlach experiment with electrons the measured spin component $S_Z = \pm \frac{1}{2}$ does not come about by an adjustment at the last moment, a forced “flipping” or “tilting” of the spin (vector), which would imply z-angular momentum exchange between particle and instrument, but will afterward appear to have had the value $\frac{1}{2} or - \frac{1}{2}$ already before the measurement. Because an electron spin cannot have components $ \pm \frac{1}{2}$ in all directions at the (...) same time, the measuring direction has a “privileged” status before the measurement, however we choose that direction, which implies a retroactive effect. A second proof of retroactivity is derived from a special case of the paradox of Einstein, Podolsky, and Rosen. It is strongly suggested by our result that, in essential respects, both Bohr and Einstein were right in their famous controversy about determinism and considering microprocesses “as a whole.”. (shrink)

The central debate of natural theology among medieval Muslims and Jews concerned whether or not the world was eternal. Opinions divided sharply on this issue because the outcome bore directly on God's relationship with the world: eternity implies a deity bereft of will, while a world with a beginning leads to the contrasting picture of a deity possessed of will. In this exhaustive study of medieval Islamic and Jewish arguments for eternity, creation, and the existence of God, Herbert Davidson provides (...) a systematic classification of the proofs, analyzes and explains them, and traces their sources in Greek philosophy. Throughout the study, Davidson tries to take into account every argument of a philosophical character, disregarding only those arguments that rest entirely on religious faith or which fall below a minimal level of plausibility. (shrink)

Miller, D., G. Nadathur, F. Pfenning and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51 125–157. A proof-theoretic characterization of logical languages that form suitable bases for Prolog-like programming languages is provided. This characterization is based on the principle that the declarative meaning of a logic program, provided by provability in a logical system, should coincide with its operational meaning, provided by interpreting logical connectives as simple and fixed search instructions. (...) The operational semantics is formalized by the identification of a class of cut-free sequent proofs called uniform proofs. A uniform proof is one that can be found by a goal-directed search that respects the interpretation of the logical connectives as search instructions. The concept of a uniform proof is used to define the notion of an abstract logic programming language, and it is shown that first-order and higher-order Horn clauses with classical provability are examples of such a language. Horn clauses are then generalized to hereditary Harrop formulas and it is shown that first-order and higher-order versions of this new class of formulas are also abstract logic programming languages if the inference rules are those of either intuitionistic or minimal logic. The programming language significance of the various generalizations to first-order Horn clauses is briefly discussed. (shrink)