Gentzen’s sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut elimination and consistency for classical and intuitionistic logics. Among the undesirable features of those sequent calculi is that their inferences rules are low-level and frequently permute over each other. As a result, large-scale structures within sequent calculus proofs are hard to identify. In this (...) paper, we present a different approach to designing a sequent calculus for classical logic. Starting with Gentzen’s LK proof system, we examine the proof search meaning of his inference rules and classify those rules as involving either don’t care nondeterminism or don’t know nondeterminism. Based on that classification, we design the focused proof system LKF in which inference rules belong to one of two phases of proof construction depending on which flavor of nondeterminism they involve. We then prove that the cut rule and the general form of the initial rule are admissible in LKF. Finally, by showing that the inference rules for LK are all admissible in LKF, we can give a relative completeness proof for LKF provability with respect to LK provability. We shall also apply these properties of the LKF proof system to establish other meta-theoretic properties of classical logic, including Herbrand’s theorem. (shrink)

Is truth in the law just plain truth - or something sui generis? Is a trial a search for truth? Do adversarial procedures and exclusionary rules of evidence enable, or impede, the accurate determination of factual issues? Can degrees of proof be identified with mathematical probabilities? What role can statistical evidence properly play? How can courts best handle the scientific testimony on which cases sometimes turn? How are they to distinguish reliable scientific testimony from unreliable hokum? These interdisciplinary essays (...) explore such questions about science, proof, and truth in the law. With her characteristic clarity and verve, Haack brings her original and distinctive work in theory of knowledge and philosophy of science to bear on real-life legal issues. She includes detailed analyses of a wide variety of cases and lucid summaries of relevant scientific work, of the many roles of the scientific peer-review system, and of relevant legal developments. (shrink)

The standard approach to what I call “proof-theoretic semantics”, which is mainly due to Dummett and Prawitz, attempts to give a semantics of proofs by defining what counts as a valid proof. After a discussion of the general aims of proof-theoretic semantics, this paper investigates in detail various notions of proof-theoretic validity and offers certain improvements of the definitions given by Prawitz. Particular emphasis is placed on the relationship between semantic validity concepts and validity concepts used (...) in normalization theory. It is argued that these two sorts of concepts must be kept strictly apart. (shrink)

We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus \(\mathtt{SC2Int}\) for the bi-intuitionistic logic \(\mathtt{2Int}\). A distinctive feature of \(\mathtt{SC2Int}\) is that it makes use of two kind of sequents, one representing proofs, the other representing refutations. The structural rules of \(\mathtt{SC2Int}\), in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, mediated (...) through two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of \(\mathtt{2Int}\). By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in \(\mathtt{SC2Int}\) is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously. (shrink)

I explore, from a proof-theoretic perspective, the hierarchy of classical and paraconsistent logics introduced by Barrio, Pailos and Szmuc in (Journal o f Philosophical Logic,49, 93-120, 2021). First, I provide sequent rules and axioms for all the logics in the hierarchy, for all inferential levels, and establish soundness and completeness results. Second, I show how to extend those systems with a corresponding hierarchy of validity predicates, each one of which is meant to capture “validity” at a different inferential level. (...) Then, I point out two potential philosophical implications of these results. (i) Since the logics in the hierarchy differ from one another on the rules, I argue that each such logic maintains its own distinct identity (contrary to arguments like the one given by Dicher and Paoli in 2019). (ii) Each validity predicate need not capture “validity” at more than one metainferential level. Hence, there are reasons to deny the thesis (put forward in Barrio, E., Rosenblatt, L. & Tajer, D. (Synthese, 2016)) that the validity predicate introduced in by Beall and Murzi in (Journal o f Philosophy,110(3), 143–165, 2013) has to express facts not only about what follows from what, but also about the metarules, etc. (shrink)

This paper uses some modest claims about knowledge to identify a significant problem for contemporary American trial procedure. First, suppose that legal proof requires knowledge. In particular, suppose that the defendant in a jury trial is proven guilty only if the jury knows that the defendant is guilty. Second, suppose that knowledge is subject to pragmatic encroachment. In particular, whether the jury knows the defendant is guilty depends on what’s at stake in their decision to convict, including the consequences (...) that the defendant may face if convicted. Then in order to know whether a defendant has been proven guilty, jurors may need to know something about the potential consequences of conviction. But in nearly every American criminal trial, this information is withheld from jurors. -/- In §1, I lay out the philosophical premises of my argument. In §2, I say more about why these premises present a problem for American trial procedure, and I identify social and political structures that exacerbate the problem. I describe the reasoning that has led courts to withhold sentencing information from jurors, and I diagnose the flaw in this reasoning. In §3, I expand my initial argument, strengthening its conclusions and offering alternative sets of premises that still entail them. I argue that the legal ramifications of pragmatic encroachment depend on highly controversial questions in epistemology, questions about the precise nature of practical stakes. In §4, I propose strategies for legal reform. (shrink)

Explores how to identify future-proof science. Peter Vickers takes a transdisciplinary approach in his analysis of 'scientific fact' in order to defend science against potentially dangerous scepticism.

The role of audiences in mathematical proof has largely been neglected, in part due to misconceptions like those in Perelman and Olbrechts-Tyteca which bar mathematical proofs from bearing reflections of audience consideration. In this paper, I argue that mathematical proof is typically argumentation and that a mathematician develops a proof with his universal audience in mind. In so doing, he creates a proof which reflects the standards of reasonableness embodied in his universal audience. Given this framework, (...) we can better understand the introduction of proof methods based on the mathematician’s likely universal audience. I examine a case study from Alexander and Briggs’s work on knot invariants to show that we can fruitfully reconstruct mathematical methods in terms of audiences. (shrink)

We suggest an algebraic approach to proof-theoretic analysis based on the notion of graded provability algebra, that is, Lindenbaum boolean algebra of a theory enriched by additional operators which allow for the structure to capture proof-theoretic information. We use this method to analyze Peano arithmetic and show how an ordinal notation system up to 0 can be recovered from the corresponding algebra in a canonical way. This method also establishes links between proof-theoretic ordinal analysis and the work (...) which has been done in the last two decades on provability logic and reflection principles. Because of its abstract algebraic nature, we hope that it will also be of interest for non-prooftheorists. (shrink)

We give a proof of Gödel's first incompleteness theorem based on Berry's paradox, and from it we also derive the second incompleteness theorem model-theoretically.

The core idea of the ontological proof is to show that the concept of existence is somehow contained in the concept of God, and that therefore God’s existence can be logically derived—without any further assumptions about the external world—from the very idea, or definition, of God. Now, G.W. Leibniz has argued repeatedly that the traditional versions of the ontological proof are not fully conclusive, because they rest on the tacit assumption that the concept of God is possible, i.e. (...) free from contradiction. A complete proof will rather have to consist of two parts. First, a proof of premiseGod is possible. Second, a demonstration of the “remarkable proposition”If God is possible, then God exists. The present contribution investigates an interesting paper in which Leibniz tries to prove proposition. It will be argued that the underlying idea of God as a necessary being has to be interpreted with the help of a distinguished predicate letter ‘E’ as follows:\\). Proposition which Leibniz considered as “the best fruit of the entire logic” can then be formalized as follows:\) \rightarrow \, E)\). At first sight, Leibniz’s proof appears to be formally correct; but a closer examination reveals an ambiguity in his use of the modal notions. According to, the possibility of the necessary being has to be understood in the sense of something which possibly exists. However, in other places of his proof, Leibniz interprets the assumption that the necessary being is impossible in the diverging sense of something which involves a contradiction. Furthermore, Leibniz believes that an »impossible thing«, y, is such that contradictory propositions like \\) and \\) might both be true of y. It will be argued that the latter assumption is incompatible with Leibniz’s general views about logic and that the crucial proof is better reinterpreted as dealing with the necessity, possibility, and impossibility of concepts rather than of objects. In this case, the counterpart of turns out to be a theorem of Leibniz’s second order logic of concepts; but in order to obtain a full demonstration of the existence of God, the counterpart of, i.e. the self-consistency of the concept of a necessary being, remains to be proven. (shrink)

A proof by Allan Gibbard (Ifs: Conditionals, beliefs, decision, chance, time. Reidel, Dordrecht, 1981) seems to demonstrate that if indicative conditionals have truth conditions, they cannot be stronger than material implication. Angelika Kratzer's theory that conditionals do not denote two-place operators purports to escape this result [see Kratzer (Chic Linguist Soc 22(2):1–15, 1986, 2012)]. In this note, I raise some trouble for Kratzer’s proposed method of escape and then show that her semantics avoids this consequence of Gibbard’s proof (...) by denying modus ponens. I also show that the same holds for Anthony Gillies’ semantics (Philos Rev 118(3):325–349, 2009) and argue that this consequence of these theories is not obviously prohibitive—hence, both remain viable theories of indicative conditionals. (shrink)

We give a simplified proof of elimination of imaginaries in ACVF, based on ideas of Hrushovski. This proof manages to avoid many of the technical issues which arose in the original proof by Haskell, Hrushovski, and Macpherson.

How is the burden of proof to be distributed among individuals who are involved in resolving a particular issue? Under what conditions should the burden of proof be distributed unevenly? We distinguish attitudinal from dialectical burdens and argue that these questions should be answered differently, depending on which is in play. One has an attitudinal burden with respect to some proposition when one is required to possess sufficient evidence for it. One has a dialectical burden with respect to (...) some proposition when one is required to provide supporting arguments for it as part of a deliberative process. We show that the attitudinal burden with respect to certain propositions is unevenly distributed in some deliberative contexts, but in all of these contexts, establishing the degree of support for the proposition is merely a means to some other deliberative end, such as action guidance, or persuasion. By contrast, uneven distributions of the dialectical burden regularly further the aims of deliberation, even in contexts where the quest for truth is the sole deliberative aim, rather than merely a means to some different deliberative end. We argue that our distinction between these two burdens resolves puzzles about unevenness that have been raised in the literature. (shrink)

Deductive proof checking programs are the most popular form of logic CAI. Whatever the reason for their widespread use, the proliferation and continuous development of these programs is evident. Contemporary proof checkers cover a wider variety of texts and rule sets, and offer more helpful editing, diagnostic, and remedial features than were once provided. These programs appear to be prime candidates for developing in the direction of "intelligent" CAI (ICAI). The primary thrust of ICAI is to build programs (...) that make use of information about learner strengths and weaknesses, the content of the subject matter being taught, and techniques for teaching various kinds of subject matter. This is a tall order by any standard, but there are signs that some initial progress is being made in the area of logic CAI. In particular, the expert system approach for offering strategic advice during proof construction is being explored by some projects. (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)

In the present note we make use of some information given in [2]. Also, the terminology and notation do not dier from those accepted in [2]; in particular this concerns the formalism for the predicate calculus. Let A be a model of a rst-order language L. We say that A realizes a set of formulas Fla i A j= [a] for some valuation a in A and all 2 . We say that A omits i A does not realize . (...) A formula 2 Fla is consistent with a theory T in i there is a model of T which realizes fg. (shrink)

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

Public and professional debates have come to rely heavily on a special type of reasoning: the argument-from-ignorance, in which conclusions depend on the _lack_ of compelling information. "I win my argument," says the skillful advocate, "unless you can prove that I am wrong." This extraordinary gambit has been largely ignored in modern rhetorical and philosophical studies. Yet its broad force can be demonstrated by analogy with the modern legal system, where courts have long manipulated burdens of proof with skill (...) and subtlety. This legal, philosophical, and rhetorical study by Richard H. Gaskins provides the first systematic treatment of arguments-from-ignorance across a wide range of modern discourse—from constitutional law, scientific inquiry, and moral philosophy to organizational behavior, computer operation, and personal interaction. Gaskins reviews the historic shifts in constitutional proof burdens that have shaped public debate on fundamental rights and, by analogy, on the fundamental status of intellectual and cultural authority. He shows how similar shifts have dominated polemical battles between scientific and ethical modes of authority, affecting both academic and popular discussion. Finally, he discovers the philosophical roots of default reasoning strategies in the arguments of Kant and nineteenth-century Kantian schools. Concluding that shifting proof burdens are inescapable in a world of scientific and moral uncertainty, Gaskins emphasizes the common strategic ground shared by dogmatic and skeptical reasoning. Using Hegelian strategies, he describes a more pluralistic temper that can move critical thinking beyond polemics and strengthen our capacities for common discourse. (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)

In the last few years there has been a resurgence of interest in Moore’s Proof of the existence of an external world, which is now often rendered as follows:1 (I) Here’s a hand (II) If there is a hand here, there is an external world Therefore (III) There is an external world The contemporary debate has been mostly triggered by Crispin Wright’s influential—conservative —“Facts and certainty” and further fostered by Jim Pryor’s recent—liberal—“What’s wrong with Moore’s argument?”.2 This debate is (...) worth surveying with care because—so I shall contend—it will help us see that, in fact, it allows for an important view that, so far, hasn’t been explicitly considered. The critical survey will be the task of the next two sections, while, in the remaining.. (shrink)

In this note, we review paradoxes like Russell’s, the Liar, and Curry’s in the context of intuitionistic logic. One may observe that one cannot blame the underlying logic for the paradoxes, but has to take into account the particular concept formations. For proof-theoretic semantics, however, this comes with the challenge to block some forms of direct axiomatizations of the Liar. A proper answer to this challenge might be given by Schroeder-Heister’s definitional freedom.

The notion of “the burden of proof” plays an important role in real-world argumentation contexts, in particular in law. It has also been given a central role in normative accounts of argumentation, and has been used to explain a range of classic argumentation fallacies. We argue that in law the goal is to make practical decisions whereas in critical discussion the goal is frequently simply to increase or decrease degree of belief in a proposition. In the latter case, it (...) is not necessarily important whether that degree of belief exceeds a particular threshold (e.g., ‘reasonable doubt’). We explore the consequences of this distinction for the role that the “burden of proof” has played in argumentation and in theories of fallacy. (shrink)

The aim of this essay is to develop a coherence theory for the justification of evidentiary judgments in law. The main claim of the coherence theory proposed in this article is that a belief about the events being litigated is justified if and only if it is a belief that an epistemically responsible fact finder might hold by virtue of its coherence in like circumstances. The article argues that this coherentist approach to evidence and legal proof has the resources (...) to meet some of the main objections that may be addressed against attempts to analyze the justification of evidentiary judgments in law in coherentist terms. It concludes by exploring some implications of the proposed version of legal coherentism for a jurisprudence of evidence. (shrink)

Open texture is a kind of semantic indeterminacy first systematically studied by Waismann. In this paper, extant definitions of open texture will be compared and contrasted, with a view towards the consequences of open-textured concepts in mathematics. It has been suggested that these would threaten the traditional virtues of proof, primarily the certainty bestowed by proof-possession, and this suggestion will be critically investigated using recent work on informal proof. It will be argued that informal proofs have virtues (...) that mitigate the danger posed by open texture. Moreover, it will be argued that while rigor in the guise of formalisation and axiomatisation might banish open texture from mathematical theories through implicit definition, it can do so only at the cost of restricting the tamed concepts in certain ways. (shrink)

We present our calculus of higher-level rules, extended with propositional quantification within rules. This makes it possible to present general schemas for introduction and elimination rules for arbitrary propositional operators and to define what it means that introductions and eliminations are in harmony with each other. This definition does not presuppose any logical system, but is formulated in terms of rules themselves. We therefore speak of a foundational account of proof-theoretic harmony. With every set of introduction rules a canonical (...) elimination rule, and with every set of elimination rules a canonical introduction rule is associated in such a way that the canonical rule is in harmony with the set of rules it is associated with. An example given by Hazen and Pelletier is used to demonstrate that there are significant connectives, which are characterized by their elimination rules, and whose introduction rule is the canonical introduction rule associated with these elimination rules. Due to the availabiliy of higher-level rules and propositional quantification, the means of expression of the framework developed are sufficient to ensure that the construction of canonical elimination or introduction rules is always possible and does not lead out of this framework. (shrink)

In this paper, we report results from experiments in which people read conversational arguments and then judge the convincingness of each claim and the individual speakers' burden of proof. The results showed an "anti-primacy" effect: People judge the speaker who makes the first claim as having greater burden of proof. This effect persists even when each speaker's claims are rated equally convincing. We also find that people rate claims less convincing when they appear in the first part of (...) an argument than when they appear in isolation. (shrink)

On a traditional view, the primary role of a mathematical proof is to warrant the truth of the resulting theorem. This view fails to explain why it is very often the case that a new proof of a theorem is deemed important. Three case studies from elementary arithmetic show, informally, that there are many criteria by which ordinary proofs are valued. I argue that at least some of these criteria depend on the methods of inference the proofs employ, (...) and that standard models of formal deduction are not well-equipped to support such evaluations. I discuss a model of proof that is used in the automated deduction community, and show that this model does better in that respect. (shrink)

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