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

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

Grouping research participants by culture or language proficiency may no longer suffice to investigate cognitive universals and differences cross-culturally, due to the interconnectedness of our multicultural world. Based on immigration psychology research, we provide a ‘proof of principle’ for three culture screening tools. Across five online experiments (total N = 440), we developed (1) The Cultural Traditions Questionnaire (CTQ), (2) the Arts Engagement in Childhood Questionnaire (AECQ), and (3) the Enculturation and Acculturation Quiz (EAQ). While these screening tools are (...) tailored to Iranian and English cultures, the procedures provided here are expandable to other cultures. The screening scores predicted emotional attachment to a culture better than traditional variables used in cross-cultural research (self-ascribed culture group, country of residence during formative years, mother tongue). Continuous measures of enculturation and acculturation are potentially better predictors for downstream variables of interest, due to their finer granularity and capability to capture multifaceted cultural identities. (shrink)

This is the first comprehensive textbook on higher order logic that is written specifically to introduce the subject matter to graduate students in philosophy. The book covers both the formal aspects of higher-order languages -- their model theory and proof theory, the theory of λ-abstraction and its generalizations -- and their philosophical applications, especially to the topics of modality and propositional granularity. The book has a strong focus on non-extensional higher-order logics, making it more appropriate for foundational metaphysics (...) than other introductions to the subject from computer science, mathematics, and linguistics. A Philosophical Introduction to Higher Order Logics assumes only that readers have a basic knowledge of first-order logic. With an emphasis on exercises, it can be used as a textbook though is also ideal for self-study. Author Andrew Bacon organizes the book's 18 chapters around four main parts: I. Typed Language II. Higher Order Languages III. General Higher-Order Languages IV. Higher-Order Model Theory In addition, two appendices cover the Curry-Howard isomorphism and its applications for modeling propositional structure. Each chapter includes exercises that move from easier to more difficult, strategically placed throughout the chapter, and concludes with an annotated suggested reading list providing graduate students with most valuable additional resources. Key Features Is the first comprehensive introduction to higher-order logic as a grounding for addressing problems in metaphysics Introduces the basic formal tools that are needed to theorize in, and model, higher order languages Offers an abundance of: - Simple exercises throughout the book, serving as comprehension checks on basic concepts and definitions - More difficult exercises designed to facilitate long-term learning Contains annotated sections on further reading, pointing the reader to related literature, learning resources, and historical context. (shrink)

Covers first-order language in method appropriate for first and second courses in logic. CD-ROM consists of a new book, 3 programs,and an Internet-based grading service.

This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

In order to perform certain actions – such as incarcerating a person or revoking parental rights – the state must establish certain facts to a particular standard of proof. These standards – such as preponderance of evidence and beyond reasonable doubt – are often interpreted as likelihoods or epistemic confidences. Many theorists construe them numerically; beyond reasonable doubt, for example, is often construed as 90 to 95% confidence in the guilt of the defendant. -/- A family of influential cases (...) suggests standards of proof should not be interpreted numerically. These ‘proof paradoxes’ illustrate that purely statistical evidence can warrant high credence in a disputed fact without satisfying the relevant legal standard. In this essay I evaluate three influential attempts to explain why merely statistical evidence cannot satisfy legal standards. (shrink)

Why can testimony alone be enough for findings of liability? Why statistical evidence alone can’t? These questions underpin the “Proof Paradox” (Redmayne 2008, Enoch et al. 2012). Many epistemologists have attempted to explain this paradox from a purely epistemic perspective. I call it the “Epistemic Project”. In this paper, I take a step back from this recent trend. Stemming from considerations about the nature and role of standards of proof, I define three requirements that any successful account in (...) line with the Epistemic Project should meet. I then consider three recent epistemic accounts on which the standard is met when the evidence rules out modal risk (Pritchard 2018), normic risk (Ebert et al. 2020), or relevant alternatives (Gardiner 2019 2020). I argue that none of these accounts meets all the requirements. Finally, I offer reasons to be pessimistic about the prospects of having a successful epistemic explanation of the paradox. I suggest the discussion on the proof paradox would benefit from undergoing a ‘value-turn’. (shrink)

The notion of burden of proof and its companion notion of presumption are central to argumentation studies. This book argues that we can learn a lot from how the courts have developed procedures over the years for allocating and reasoning with presumptions and burdens of proof, and from how artificial intelligence has built precise formal and computational systems to represent this kind of reasoning. The book provides a model of reasoning with burden of proof and presumption, based (...) on analyses of many clearly explained legal and non-legal examples. The model is shown to fit cases of everyday conversational argumentation as well as argumentation in legal cases. Burden of proof determines under what conditions an arguer is obliged to support a claim with an argument that backs it up and how strong that argument needs to be to prove the claim in question. (shrink)

Is science getting at the truth? The sceptics – those who spread doubt about science – often employ a simple argument: scientists were sure in the past, and then they ended up being wrong. Such sceptics draw on dramatic quotes from eminent scientists such as Lord Kelvin, who reportedly stated at the turn of the 20th century “There is nothing new to be discovered in physics now,” shortly before physics was dramatically transformed. They ask: given the history of science, wouldn’t (...) it be naïve to think that current scientific theories reveal ‘the truth’, and will never be discarded in favour of other theories? Through a combination of historical investigation and philosophical-sociological analysis, Identifying Future-Proof Science defends science against such potentially dangerous scepticism. It is argued that we can confidently identify many scientific claims that are future-proof: they will last forever, so long as science continues. How do we identify future-proof claims? This appears to be a new question for science scholars, and not an unimportant one. It is argued that the best way to identify future-proof science is to avoid any attempt to analyse the relevant first-order scientific evidence, instead focusing purely on second-order evidence. Specifically, a scientific claim is future-proof when the relevant scientific community is large, international, and diverse, and at least 95% of that community would describe the claim as a ‘scientific fact’. In the entire history of science, no claim meeting these criteria has ever been overturned, despite enormous opportunity. (shrink)

Existing discussions of legal proof address a host of apparently disparate questions: What does it take to prove a fact beyond a reasonable doubt? Why is the reasonable doubt standard notoriously elusive, sometimes considered by courts to be impossible to define? Can the standard of proof by a preponderance of the evidence be defined in terms of probability thresholds? Why is statistical evidence often insufficient to meet the burden of proof? -/- This paper defends an account of (...) proof that addresses each of these questions. Where existing theories take a piecemeal approach to these puzzles, my theory develops an insight that unifies them—namely, the thesis that legal proof requires knowledge. Although this thesis may seem radical at first, I answer several common objections to it, and I argue that it does better than several competing accounts when it comes to making sense of our intuitions about what legal proof requires. (shrink)

Recent years have seen fresh impetus brought to debates about the proper role of statistical evidence in the law. Recent work largely centres on a set of puzzles known as the ‘proof paradox’. While these puzzles may initially seem academic, they have important ramifications for the law: raising key conceptual questions about legal proof, and practical questions about DNA evidence. This article introduces the proof paradox, why we should care about it, and new work attempting to resolve (...) it. (shrink)

I have argued that without an adequate solution to the knower paradox Fitch's Proof is- or at least ought to be-ineffective against verificationism. Of course, in order to follow my suggestion verificationists must maintain that there is currently no adequate solution to the knower paradox, and that the paradox continues to provide prima facie evidence of inconsistent knowledge. By my lights, any glimpse at the literature on paradoxes offers strong support for the first thesis, and any honest, non-dogmatic reflection (...) on the knower paradox provides strong support for the second. Whether verificationists want to go the route I've suggested is not for me todecide. As in the previous section my aim has been that of defending the mere viability of verificationism in the face of what many, many philosophers have taken to be its death-knell, namely Fitch's Proof. But, as the final objection makes clear, showing that verificationism can live in the face of Fitch's Proof is one thing; showing that it should live is another project. If nothing else, I hope that this papershows that verificationists still have a project to pursue; Fitch's Proof, contrary to popular opinion, need not bury verificationism.13. (shrink)

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

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

This 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)

I present a novel interpretation of Frege’s attempt at Grundgesetze I §§29-31 to prove that every expression of his language has a unique reference. I argue that Frege’s proof is based on a contextual account of reference, similar to but more sophisticated than that enshrined in his famous Context Principle. Although Frege’s proof is incorrect, I argue that the account of reference on which it is based is of potential philosophical value, and I analyze the class of cases (...) to which it may successfully be applied. (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)

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)

The current paper studies the formal properties of the Global Reflection Principle, to wit the assertion “All theorems of$\mathrm {Th}$are true,” where$\mathrm {Th}$is a theory in the language of arithmetic and the truth predicate satisfies the usual Tarskian inductive conditions for formulae in the language of arithmetic. We fix the gap in Kotlarski’s proof from [15], showing that the Global Reflection Principle for Peano Arithmetic is provable in the theory of compositional truth with bounded induction only ($\mathrm {CT}_0$). Furthermore, (...) we extend the above result showing that$\Sigma _1$-uniform reflection over a theory of uniform Tarski biconditionals ($\mathrm {UTB}^-$) is provable in$\mathrm {CT}_0$, thus answering the question of Beklemishev and Pakhomov [2]. Finally, we introduce the notion of a prolongable satisfaction class and use it to study the structure of models of$\mathrm {CT}_0$. In particular, we provide a new model-theoretical characterization of theories of finite iterations of uniform reflection and present a new proof characterizing the arithmetical consequences of$\mathrm {CT}_0$. (shrink)

In this paper we calibrate the exact proof-theoretic strength of Kruskal's theorem, thereby giving, in some sense, the most elementary proof of Kruskal's theorem. Furthermore, these investigations give rise to ordinal analyses of restricted bar induction.

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

In discussions of standards of proof, a familiar perspective often emerges. According to what we call specificationism, standards of proof are legal rules that specify the quantum of evidence required to determine that a litigant’s claim has been proven. In so doing, they allocate the risk of error among litigants (and potential litigants), minimizing the risk of certain types of error. Specificationism is meant as a description of the way the rules actually function. We argue, however, that its (...) claims are either mistaken or at a minimum deeply misleading, especially when it comes to standard of proof rules (SPRs) that contain indeterminate formulas, as is typical. As against specificationism, we argue that SPRs are best understood as rules that confer competence to decide whether a given standard has been met—according to whatever vague or inchoate interpretation (if any) of the rule in question triers of fact implicitly or explicitly employ. We call this the competence-norm approach. (shrink)

A question, long discussed by legal scholars, has recently provoked a considerable amount of philosophical attention: ‘Is it ever appropriate to base a legal verdict on statistical evidence alone?’ Many philosophers who have considered this question reject legal reliance on bare statistics, even when the odds of error are extremely low. This paper develops a puzzle for the dominant theories concerning why we should eschew bare statistics. Namely, there seem to be compelling scenarios in which there are multiple sources of (...) incriminating statistical evidence. As we conjoin together different types of statistical evidence, it becomes increasingly incredible to suppose that a positive verdict would be impermissible. I suggest that none of the dominant views in the literature can easily accommodate such cases, and close by offering a diagnosis of my own. (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)

Crispin Wright; IV*—On Putnam's Proof that We are not Brains-in-a-Vat1, Proceedings of the Aristotelian Society, Volume 92, Issue 1, 1 June 1992, Pages 67–94, h.

In this paper we argue that an account of proof-theoretic harmony based on reductions and expansions delivers an inferentialist picture of meaning which should be regarded as intensional, as opposed to other approaches to harmony that will be dubbed extensional. We show how the intensional account applies to any connective whose rules obey the inversion principle first proposed by Prawitz and Schroeder-Heister. In particular, by improving previous formulations of expansions, we solve a problem with quantum-disjunction first posed by Dummett. (...) As recently observed by Schroeder-Heister, however, the specification of an inversion principle cannot yield an exhaustive account of harmony. The reason is that there are more collections of elimination rules than just the one obtained by inversion which we are willing to acknowledge as being in harmony with a given collection of introduction rules. Several authors more or less implicitly suggest that what is common to all alternative harmonious collection of rules is their being interderivable with each other. On the basis of considerations about identity of proofs and formula isomorphism, we show that this is too weak a condition for a given collection of elimination rules to be in harmony with a collection of introduction rules, at least if the intensional picture of meaning we advocate is not to collapse on an extensional one. (shrink)

Mathematical investigation, when done well, can confer understanding. This bare observation shouldn’t be controversial; where obstacles appear is rather in the effort to engage this observation with epistemology. The complexity of the issue of course precludes addressing it tout court in one paper, and I’ll just be laying some early foundations here. To this end I’ll narrow the field in two ways. First, I’ll address a specific account of explanation and understanding that applies naturally to mathematical reasoning: the view proposed (...) by Philip Kitcher and Michael Friedman of explanation or understanding as involving the unification of theories that had antecedently appeared heterogeneous. For the second narrowing, I’ll take up one specific feature (among many) of theories and their basic concepts that is sometimes taken to make the theories and concepts preferred: in some fields, for some problems, what is counted as understanding a problem may involve finding a way to represent the problem so that it (or some aspect of it) can be visualized. The final section develops a case study which exemplifies the way that this consideration – the potential for visualizability – can rationally inform decisions as to what the proper framework and axioms should be. The discussion of unification (in sections 3 and 4) leads to a mathematical analogue of Goodman’s problem of identifying a principled basis for distinguishing grue and green. Just as there is a philosophical issue about how we arrive at the predicates we should use when making empirical predictions, so too there is an issue about what properties best support many kinds of mathematical reasoning that are especially valuable to us. The issue becomes pressing via an examination of some physical and mathematical cases that make it seem unlikely that treatments of unification can be as straightforward as the philosophical literature has hoped. Though unification accounts have a grain of truth (since a phenomenon (or cluster of phenomena) called “unification” is in fact important in many cases) we are far from an analysis of what “unification” is.. (shrink)

One of the most fundamental questions in the philosophy of mathematics concerns the relation between truth and formal proof. The position according to which the two concepts are the same is called deflationism, and the opposing viewpoint substantialism. In an important result of mathematical logic, Kurt Gödel proved in his first incompleteness theorem that all consistent formal systems containing arithmetic include sentences that can neither be proved nor disproved within that system. However, such undecidable Gödel sentences can be established (...) to be true once we expand the formal system with Alfred Tarski s semantical theory of truth, as shown by Stewart Shapiro and Jeffrey Ketland in their semantical arguments for the substantiality of truth. According to them, in Gödel sentences we have an explicit case of true but unprovable sentences, and hence deflationism is refuted. -/- Against that, Neil Tennant has shown that instead of Tarskian truth we can expand the formal system with a soundness principle, according to which all provable sentences are assertable, and the assertability of Gödel sentences follows. This way, the relevant question is not whether we can establish the truth of Gödel sentences, but whether Tarskian truth is a more plausible expansion than a soundness principle. In this work I will argue that this problem is best approached once we think of mathematics as the full human phenomenon, and not just consisting of formal systems. When pre-formal mathematical thinking is included in our account, we see that Tarskian truth is in fact not an expansion at all. I claim that what proof is to formal mathematics, truth is to pre-formal thinking, and the Tarskian account of semantical truth mirrors this relation accurately. -/- However, the introduction of pre-formal mathematics is vulnerable to the deflationist counterargument that while existing in practice, pre-formal thinking could still be philosophically superfluous if it does not refer to anything objective. Against this, I argue that all truly deflationist philosophical theories lead to arbitrariness of mathematics. In all other philosophical accounts of mathematics there is room for a reference of the pre-formal mathematics, and the expansion of Tarkian truth can be made naturally. Hence, if we reject the arbitrariness of mathematics, I argue in this work, we must accept the substantiality of truth. Related subjects such as neo-Fregeanism will also be covered, and shown not to change the need for Tarskian truth. -/- The only remaining route for the deflationist is to change the underlying logic so that our formal languages can include their own truth predicates, which Tarski showed to be impossible for classical first-order languages. With such logics we would have no need to expand the formal systems, and the above argument would fail. From the alternative approaches, in this work I focus mostly on the Independence Friendly (IF) logic of Jaakko Hintikka and Gabriel Sandu. Hintikka has claimed that an IF language can include its own adequate truth predicate. I argue that while this is indeed the case, we cannot recognize the truth predicate as such within the same IF language, and the need for Tarskian truth remains. In addition to IF logic, also second-order logic and Saul Kripke s approach using Kleenean logic will be shown to fail in a similar fashion. (shrink)

In Baghdad in the mid twelfth century Abū al-Barakāt proposes a radical new procedure for finding the conclusions of premise-pairs in syllogistic logic, and for identifying those premise-pairs that have no conclusions. The procedure makes no use of features of the standard Aristotelian apparatus, such as conversions or syllogistic figures. In place of these al-Barakāt writes out pages of diagrams consisting of labelled horizontal lines. He gives no instructions and no proof that the procedure will yield correct results. So (...) the reader has to work out what his procedure is and whether it is correct. The procedure turns out to be insightful and entirely correct, but this paper may be the first study to give a full description of the procedure and a rigorous proof of its correctness. (shrink)

In the first part we show why ordinals and ordinal notations are naturally connected with proof theoretical research. We introduce the program of ordinal analysis. The second part gives examples of applications of ordinal analysis.

We consider the problem about the length of proofs of the sentences $\operatorname{Con}_S(\underline{n})$ saying that there is no proof of contradiction in S whose length is ≤ n. We show the relation of this problem to some problems about propositional proof systems.

This paper proposes an account of why proof is the only way to acquire knowledge of some mathematical proposition’s truth. Admittedly, non-deductive arguments for mathematical propositions can be strong and play important roles in mathematics. But this paper proposes a necessary condition for knowledge that can be satisfied by putative proofs (and proof sketches), as well as by non-deductive arguments in science, but not by non-deductive arguments from mathematical evidence. The necessary condition concerns whether we can justly expect (...) that if the mathematical proposition is actually false, despite the evidence for its truth, then this fact has an explanation. (shrink)

This volume is the first ever collection devoted to the field of proof-theoretic semantics. Contributions address topics including the systematics of introduction and elimination rules and proofs of normalization, the categorial characterization of deductions, the relation between Heyting's and Gentzen's approaches to meaning, knowability paradoxes, proof-theoretic foundations of set theory, Dummett's justification of logical laws, Kreisel's theory of constructions, paradoxical reasoning, and the defence of model theory. The field of proof-theoretic semantics has existed for almost 50 years, (...) but the term itself was proposed by Schroeder-Heister in the 1980s. Proof-theoretic semantics explains the meaning of linguistic expressions in general and of logical constants in particular in terms of the notion of proof. This volume emerges from presentations at the Second International Conference on Proof-Theoretic Semantics in Tübingen in 2013, where contributing authors were asked to provide a self-contained description and analysis of a significant research question in this area. The contributions are representative of the field and should be of interest to logicians, philosophers, and mathematicians alike. (shrink)

This paper contends that Stoic logic (i.e. Stoic analysis) deserves more attention from contemporary logicians. It sets out how, compared with contemporary propositional calculi, Stoic analysis is closest to methods of backward proof search for Gentzen-inspired substructural sequent logics, as they have been developed in logic programming and structural proof theory, and produces its proof search calculus in tree form. It shows how multiple similarities to Gentzen sequent systems combine with intriguing dissimilarities that may enrich contemporary discussion. (...) Much of Stoic logic appears surprisingly modern: a recursively formulated syntax with some truth-functional propositional operators; analogues to cut rules, axiom schemata and Gentzen’s negation-introduction rules; an implicit variable-sharing principle and deliberate rejection of Thinning and avoidance of paradoxes of implication. These latter features mark the system out as a relevance logic, where the absence of duals for its left and right introduction rules puts it in the vicinity of McCall’s connexive logic. Methodologically, the choice of meticulously formulated meta-logical rules in lieu of axiom and inference schemata absorbs some structural rules and results in an economical, precise and elegant system that values decidability over completeness. (shrink)

Restall :279–291, 2014) proposes a new, proof-theoretic, logical pluralism. This is in contrast to the model-theoretic pluralism he and Beall proposed in Beall and Restall :475–493, 2000) and in Beall and Restall. What I will show is that Restall has not described the conditions on being admissible to the proof-theoretic logical pluralism in such a way that relevance logic is one of the admissible logics. Though relevance logic is not hard to add formally, one critical component of Restall’s (...) pluralism is that the relevance logic that gets added must have connectives which mean the same thing as the connectives in the already admitted logic. This is what I will show is not possible. (shrink)

Inquiry into the metaphysics of essence tends to be pursued in a realist and model-theoretic spirit, in the sense that metaphysical vocabulary is used in a metalanguage to model truth conditions for the object-language use of essentialist vocabulary. This essay adapts recent developments in proof-theoretic semantics to provide a nominalist analysis for a variety of essentialist vocabularies. A metalanguage employing explanatory inferences is used to individuate introduction and elimination rules for atomic sentences. The object-language assertions of sentences concerning essences (...) are then interpreted as devices for marking off structural features of the explanatory inferences that, under a given interpretation, constitute the contents of the atoms of the language. On this proposal, object-language essentialist vocabulary is mentioned in a proof-theoretic metalanguage that uses a vocabulary of explanation. The result is a nominalist interpretation of essence as a modality, understood in the grammatical sense as a modification of the copula, and a view of metaphysical inquiry that is closely connected to the explanatory commitments present in first-order inquiry into things like sets, chemicals, and organisms. This result illustrates that some of the presuppositions that have animated analytic metaphysics over the last few decades can be profitably substituted with more practice-oriented conceptions of the forms of reasoning at work in different domains of human knowledge. (shrink)

This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, (...) we show that the refined calculi Ldm^m_nL derive theorems within a restricted class of (forestlike) sequents, allowing us to provide proof-search algorithms that decide single-agent STIT logics. We prove that the proof-search algorithms are correct and terminate. (shrink)

In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language (a decidable system with the same complexity as orthodox propositional modal logic) to the strong Priorean language (which offers full first-order expressivity).We show that hybrid logic offers a genuinely first-order perspective on Kripke semantics: it is possible to define base logics which extend automatically to a (...) wide variety of frame classes and to prove completeness using the Henkin method. In the weaker languages, this requires the use of non-orthodox rules. We discuss these rules in detail and prove non-eliminability and eliminability results. We also show how another type of rule, which reflects the structure of the strong Priorean language, can be employed to give an even wider coverage of frame classes. We show that this deductive apparatus gets progressively simpler as we work our way up the expressivity hierarchy, and conclude the paper by showing that the approach transfers to first-order hybrid logic. (shrink)

The prime number theorem, established by Hadamard and de la Vallée Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1/ln x. Whereas their proofs made serious use of the methods of complex analysis, elementary proofs were provided by Selberg and Erdos in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.

In this paper, we discuss the prevailing view amongst philosophers and many mathematicians concerning mathematical proof. Following Cellucci, we call the prevailing view the “axiomatic conception” of proof. The conception includes the ideas that: a proof is finite, it proceeds from axioms and it is the final word on the matter of the conclusion. This received view can be traced back to Frege, Hilbert and Gentzen, amongst others, and is prevalent in both mathematical text books and logic (...) text books. (shrink)

Let KP- be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let G: V → V (V:= universe of sets) be a ▵0-definable set function, i.e. there is a ▵0-formula φ(x, y) such that φ(x, G(x)) is true for all sets x, and $V \models \forall x \exists!y\varphi (x, y)$ . In this paper we shall verify (by elementary proof-theoretic methods) that the collection of set functions primitive recursive in G coincides with the collection (...) of those functions which are Σ1-definable in KP- + Σ1-Foundation + ∀ x ∃!yφ (x, y). Moreover, we show that this is still true if one adds Π1-Foundation or a weak version of ▵0-Dependent Choices to the latter theory. (shrink)