We present an approach in which ancient Greek mathematical proofs by Hippocrates of Chios and Euclid are addressed as a form of (guided) intentional reasoning. Schematically, in a proof, we start with a sentence that works as a premise; this sentence is followed by another, the conclusion of what we might take to be an inferential step. That goes on until the last conclusion is reached. Guided by the text, we go through small inferential steps; in each one, we (...) go through an autonomous reasoning process linking the premise to the conclusion. The reasoning process is accompanied by a metareasoning process. Metareasoning gives rise to a feeling-knowing of correctness. In each step/cycle of the proof, we have a feeling-knowing of correctness. Overall, we reach a feeling of correctness for the whole proof. We suggest that this approach allows us to address the issues of how a proof functions, for us, as an enabler to ascertain the correctness of its argument and how we ascertain this correctness. (shrink)

My purpose in this paper is to argue for two separate, but related theses. The first is that contemporary analytic philosophy is incoherent. This is so, I argue, because its methods contain as an essential constituent a conception of intuition that cannot be rendered consistent with a key tenet of analytic philosophy unless we allow a Bayesian-subjectivist epistemology. I argue for this within a discussion of two theories of intuition: a classical account as proposed by Descartes and a modern reliabilist (...) account as proposed by Kornblith, maintaining that reliabilist accounts require a commitment to Bayesian subjectivism about probability. However, and this is the second thesis, Bayesian subjectivism is itself logically incoherent given two simple assumptions: (1) that some empirical propositions are known and (2) any proposition that is known is assigned a degree of subjective credence of 1. I establish this using a formal reductio proof. I argue for the first thesis in section 2 and for the second in section 3. The final section contains a summary and conclusion. (shrink)

This paper targets a series of potential issues for the discussion of, and modal resolution to, the alethic paradoxes advanced by Scharp (2013). I proffer four novel extensions of the theory, and detail six issues that the theory faces. I provide a counter-example to epistemic closure for reductio proofs.

Bilateralists hold that the meanings of the connectives are determined by rules of inference for their use in deductive reasoning with asserted and denied formulas. This paper presents two bilateral connectives comparable to Prior's tonk, for which, unlike for tonk, there are reduction steps for the removal of maximal formulas arising from introducing and eliminating formulas with those connectives as main operators. Adding either of them to bilateral classical logic results in an incoherent system. One way around this problem is (...) to count formulas as maximal that are the conclusion of reductio and major premise of an elimination rule and to require their removability from deductions. The main part of the paper consists in a proof of a normalisation theorem for bilateral logic. The closing sections address philosophical concerns whether the proof provides a satisfactory solution to the problem at hand and confronts bilateralists with the dilemma that a bilateral notion of stability sits uneasily with the core bilateral thesis. (shrink)

In the literature on supervaluationism, a central source of concern has been the acceptability, or otherwise, of its alleged logical revisionism. I attack the presupposition of this debate: arguing that when properly construed, there is no sense in which supervaluational consequence is revisionary. I provide new considerations supporting the claim that the supervaluational consequence should be characterized in a ‘global’ way. But pace Williamson (1994) and Keefe (2000), I argue that supervaluationism does not give rise to counterexamples to familiar inference-patterns (...) such as reductio and conditional proof. (shrink)

Brogaard and Salerno (2005, Nous, 39, 123–139) have argued that antirealism resting on a counterfactual analysis of truth is flawed because it commits a conditional fallacy by entailing the absurdity that there is necessarily an epistemic agent. Brogaard and Salerno's argument relies on a formal proof built upon the criticism of two parallel proofs given by Plantinga (1982, "Proceedings and Addresses of the American Philosophical Association", 56, 47–70) and Rea (2000, "Nous," 34, 291–301). If this argument were conclusive, antirealism (...) resting on a counterfactual analysis of truth should probably be abandoned. I argue however that the antirealist is not committed to a controversial reading of counterfactuals presupposed in Brogaard and Salerno's proof, and that the antirealist can in principle adopt an alternative reading that makes this proof invalid. My conclusion is that no reductio of antirealism resting on a counterfactual analysis of truth has yet been provided. (shrink)

We advance a theory of the representational role of Euclidean diagrams according to which they are samples of co-exact features. We contrast our theory with two other conceptions, the instantial conception and Macbeth’s iconic view, with respect to how well they accommodate three fundamental constraints on theories of the Euclidean diagrammatic practice— that Euclidean diagrams are used in proofs whose results are wholly general, that Euclidean diagrams indicate the co-exact features that the geometer is allowed to infer from them and (...) that Euclidean diagrams play the same role in both direct proofs and indirect proofs by reductio—and argue that our view is the one best suited to account for them. We conclude by illustrating the virtues of our conception of Euclidean diagrams as samples by means of an analysis of Saccheri’s quadrilateral. (shrink)

It has been noticed that self-referential, ambiguous definitional formulas are accompanied by complementary self-referential antinomy formulas, which gives rise to contradictions. This made it possible to re-examine ancient antinomies and Cantor’s Diagonal Argument (CDA), as well as the method of nested intervals, which is the basis for evaluating the existence of uncountable sets. Using Georg Cantor’s remark that every real number can be represented as an infinite digital expansion (usually decimal or binary), a simplified system for verifying the definitions of (...) real numbers, subsets, and strings was created - the Cantor Criterion, which allows faulty definitions to be pointed out. For the CDA, the connection of formulas defining objects (real numbers, subsets, strings) from outside the list with supplementary formulas was demonstrated - their indirect and indispensable nature testifies to the lack of unambiguity and gives rise to contradictions for Cantor’s antinomic formulas. Thus, Cantor’s theorem about the higher power of the set of all subsets, using the reductio ad absurdum proof, lost its power and it was indicated that it is necessary to correct the scheme of the Axiom of Specification, which was introduced precisely to exclude antinomies from set theory by excluding from the use of self-referential antinomies and ambiguous supplementary formulas coupled with them identified by the H hypothesis. The method of nested intervals was investigated and it was shown that every real number can be defined by the limit of nested intervals and a countable list of real numbers obtained from a countable pool of all Jules Richard’s texts. (shrink)

According to the “paradox of knowability”, the moderate thesis that all truths are knowable – ... – implies the seemingly preposterous claim that all truths are actually known – ... –, i.e. that we are omniscient. If Fitch’s argument were successful, it would amount to a knockdown rebuttal of anti-realism by reductio. In the paper I defend the nowadays rather neglected strategy of intuitionistic revisionism. Employing only intuitionistically acceptable rules of inference, the conclusion of the argument is, firstly, not (...) ..., but .... Secondly, even if there were an intuitionistically acceptable proof of ..., i.e. an argument based on a different set of premises, the conclusion would have to be interpreted in accordance with Heyting semantics, and read in this way, the apparently preposterous conclusion would be true on conceptual grounds and acceptable even from a realist point of view. Fitch’s argument, understood as an immanent critique of verificationism, fails because in a debate dealing with the justification of deduction there can be no interpreted formal language on which realists and anti-realists could agree. Thus, the underlying problem is that a satisfactory solution to the “problem of shared content” is not available. I conclude with some remarks on the proposals by J. Salerno and N. Tennant to reconstruct certain arguments in the debate on anti-realism by establishing aporias. (shrink)

St. Thomas’s Third Way to prove the existence of God, “Of Possibility and Necessity” (ST 1, q.2, art. 3, response) is one of the most controverted passages in the entire Thomistic corpus. The central point of dispute is that if there were only possible beings, each at some time would cease to exist and, therefore, at some point in time nothing would exist, and because something cannot come from nothing, in such an eventuality, nothing would exist now—a reductio ad (...) absurdum conclusion. Therefore, at least one necessary being must exist. Generations of critics and defenders have contended over St. Thomas’s proof. This article argues that the principle of pros hen analogy is implicit in the Third Way and that once identified explains the ontological dependency of possible beings, as secondary analogates, on the first necessary being, as primary analogate. Thus, without the necessary being as primary analogate, possible beings simply could not exist. The fact that they do exist is evidence for the existence of the necessary being. St. Thomas makes synthesizes the principle of pros hen analogy, as found in Aristotle’s Metaphysics, with the Neoplatonic principle of participation. Aristotle develops pros hen analogy in contradistinction to univocal and equivocal predication as well as to genus in Metaphysics 4.2, 11.3, 12.3-5. Since Scotus and re-enforced by modern analytic logic, philosophers have almost universally regarded any kind of analogical predication as a sub-category of equivocal predication and, thus, implicitly occlude the possibility of considering pros hen analogy in their readings of the Third Way. Distinction of per se and per accidens infinite regress and of radical and natural contingency are also central to understanding the Third Way. While resolving apparent problems in the Third Way, the article also seeks to rehabilitate the doctrine of pros hen analogy as a basic principle in Thomistic and, indeed, Aristotelian metaphysics. (shrink)

There are two aspects to Wittgenstein’s method of deconstructing pseudo-philosophical problems that need to be distinguished: (1) describing actual linguistic practice, and (2) constructing hypothetical ‘language-games’. Both methods were, for Wittgenstein, indispensable means of clarifying the ‘grammar’ of expressions of our language -- i.e., the appropriate contexts for using those expressions – and thereby dissolving pseudo-philosophical problems. Though (2) is often conflated with (1), it is important to recognize that it differs from it in important respects. (1) can be seen (...) as functioning as a direct method of ‘proof’ (i.e., attempt to convince the reader of some thesis), and (2) as an indirect method of ‘proof’ -- proof by reductio ad absurdum. This essay will be devoted to clarifying (2) by forging an analogy with surrealism in art. (shrink)

Can the so-ca\led first incompleteness theorem refer to itself? Many or maybe even all the paradoxes in mathematics are connected with some kind of self-reference. Gбdel built his proof on the ground of self-reference: а statement which claims its unprovabllity. So, he demonstrated that undecidaЬle propositions exist in any enough rich axiomatics (i.e. such one which contains Peano arithmetic in some sense). What about the decidabllity of the very first incompleteness theorem? We can display that it fulfills its conditions. (...) That's why it can Ье applied to itself, proving that it is an undecidaЬle statement. It seems to Ье а too strange kind of proposition: its validity implies its undecidabllity. If the validity of а statement implies its untruth, then it is either untruth (reductio ad absurdum) or an antinomy (if also its negation implies its validity). А theory that contains а contradiction implies any statement. Appearing of а proposition, whose validity implies its undecidabllity, is due to the statement that claims its unprovability. Obviously, it is а proposition of self-referential type. Ву Gбdel's words, it is correlative with Richard's or liar paradox, or even with any other semantic or mathematical one. What is the cost, if а proposition of that special kind is used in а proof? ln our opinion, the price is analogous to «applying» of а contradictory in а theory: any statement turns out to Ье undecidaЬ!e. Ifthe first incompleteness theorem is an undecidaЬ!e theorem, then it is impossiЬle to prove that the very completeness of Peano arithmetic is also an tmdecidaЬle statement (the second incompleteness theorem). Hilbert's program for ап arithmetical self-foundation of matheшatics is partly rehabllitated: only partly, because it is not decidaЬ!e and true, but undecidaЬle; that's wby both it and its negation шау Ье accepted as true, however not siшultaneously true. The first incompleteness theoreш gains the statute of axiom of а very special, semi-philosophical kind: it divides mathematics as whole into two parts: either Godel шathematics or Нilbert matheшatics. Нilbert's program of self-foundation ofmatheшatic is valid only as to the latter. (shrink)

Should we use the same standard of proof to adjudicate guilt for murder and petty theft? Why not tailor the standard of proof to the crime? These relatively neglected questions cut to the heart of central issues in the philosophy of law. This paper scrutinises whether we ought to use the same standard for all criminal cases, in contrast with a flexible approach that uses different standards for different crimes. I reject consequentialist arguments for a radically flexible standard (...) of proof, instead defending a modestly flexible approach on non-consequentialist grounds. The system I defend is one on which we should impose a higher standard of proof for crimes that attract more severe punishments. This proposal, although apparently revisionary, accords with a plausible theory concerning the epistemology of legal judgments and the role they play in society. (shrink)

Thomas Polger and Laurence Shapiro argue that Carl Gillett's much publicized dimensioned theory of realization is incoherent, being subject to a reductio. Their argument turns on the fact that Gillett's definition of realization makes property instances the exclusive relata of the realization relation, while his belief in multiple realization implies its denial, namely, that properties are the relata of the realization relation on occasions of multiple realization. Others like Sydney Shoemaker have also expressed their view of realization in terms (...) of property instances, yet they too have accepted the multiple realizability of properties. Thus I am interested in the more general issue raised by Polger and Shapiro's argument. Specifically, I show how to supplement a theory of realization with a category-inclusive auxiliary assumption, which avoids the stated reductio. I then offer a few reasons to justify the proposed category-inclusive view of realization, making some comparisons to supervenience and causation along the way. (shrink)

Prawitz conjectured that proof-theoretic validity offers a semantics for intuitionistic logic. This conjecture has recently been proven false by Piecha and Schroeder-Heister. This article resolves one of the questions left open by this recent result by showing the extensional alignment of proof-theoretic validity and general inquisitive logic. General inquisitive logic is a generalisation of inquisitive semantics, a uniform semantics for questions and assertions. The paper further defines a notion of quasi-proof-theoretic validity by restricting proof-theoretic validity to (...) allow double negation elimination for atomic formulas and proves the extensional alignment of quasi-proof-theoretic validity and inquisitive logic. (shrink)

By means of a reductio argument, Wittgenstein’s Tractatus calls into question the very idea that we can represent logical form. My paper addresses three interrelated questions: first, what conception of logical form is at issue in this argument? Second, whose conception of logic is this argument intended to undermine? And third, what could count as an adequate response to it? I show that the argument construes logical form as the universal, underlying correlation of any representation and the reality it (...) represents. I further show that the argument seeks to undermine core commitments of Frege’s and Russell’s. But the reductio, as I read it, is not intended to establish the falsity of any of their specific assumptions. Rather, its aim is to make manifest the indeterminacies that underlie the language in which these assumptions are framed, and establish the need for a transformation of that language. So understood, Wittgenstein’s argument exemplifies his idea that philosophy is not a theory, but an activity of elucidation. The interpretation I propose bears on one of the central debates in the literature, namely how we should understand Wittgenstein’s contention that his elucidations succeed despite being nonsensical. (shrink)

Smith argues that, unlike other forms of evidence, naked statistical evidence fails to satisfy normic support. This is his solution to the puzzles of statistical evidence in legal proof. This paper focuses on Smith’s claim that DNA evidence in cold-hit cases does not satisfy normic support. I argue that if this claim is correct, virtually no other form of evidence used at trial can satisfy normic support. This is troublesome. I discuss a few ways in which Smith can respond.

This paper discusses proof-theoretic semantics, the project of specifying the meanings of the logical constants in terms of rules of inference governing them. I concentrate on Michael Dummett’s and Dag Prawitz’ philosophical motivations and give precise characterisations of the crucial notions of harmony and stability, placed in the context of proving normalisation results in systems of natural deduction. I point out a problem for defining the meaning of negation in this framework and prospects for an account of the meanings (...) of modal operators in terms of rules of inference. (shrink)

The standard of proof in criminal trials in many liberal democracies is proof beyond a reasonable doubt, the BARD standard. It is customary to describe it, when putting a number on it, as requiring that the fact finder be at least 90% certain, after considering the evidence, that the defendant is guilty. Strikingly, no good reason has yet been offered in defense of using that standard. A number of non-consequentialist justifications that aim to support an even higher standard (...) have been offered; all are morally unsound. Meanwhile, consequentialist arguments plausibly support a substantially lower standard — in some cases so low as to undermine the idea that punishment is what is at stake. In this paper, I offer a new retributive justification that supports excluding the instrumental benefits of punishment from the balance that sets the standard. The resulting balance supports a standard arguably in the ballpark of the customary understanding of BARD: a standard requiring that the fact finder have a high, though not maximally high, degree of confidence that the defendant is guilty. (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)

In “A Reliabilist Solution to the Problem of Promiscuous Bootstrapping”, Hilary Kornblith (2009) proposes a reliabilist solution to the bootstrapping problem. I’m going to argue that Kornblith’s proposal, far from solving the bootstrapping problem, in fact makes the problem much harder for the reliabilist to solve. Indeed, I’m going to argue that Kornblith’s considerations give us a way to develop a quick reductio of a certain kind of reliabilism. Let’s start with a crude statement of the problem. The bootstrapper, (...) call them S, looks at a device D1 that happens to be reliable, though at this stage S doesn’t know this. We assume that S is a reliable reader of devices. S then draws the following conclusions. (shrink)

Don Marquis’ future-like-ours account argues that abortion is seriously immoral because itdeprives the embryo or fetus of a valuable future much like our own. Marquis was mindful ofcontraception being reductio ad absurdum of his reasoning, and argued that prior tofertilisation, there is not an identifiable subject of harm. Contra Marquis, Tomer Chaffercontends that the ovum is a plausible subject of harm, and therefore contraception deprives theovum of a future-like-ours. In response, I argue that being an identifiable subject of harm (...) is notsufficient for Marquis’ argument to succeed. In addition, we must also share our identity withan ovum. I show that on the account of personal identity utilised by Marquis’ defenders, weare not identical with an ovum. As a result, Chaffer’s reductio fails. (shrink)

In mathematics, any form of probabilistic proof obtained through the application of a probabilistic method is not considered as a legitimate way of gaining mathematical knowledge. In a series of papers, Don Fallis has defended the thesis that there are no epistemic reasons justifying mathematicians’ rejection of probabilistic proofs. This paper identifies such an epistemic reason. More specifically, it is argued here that if one adopts a conception of mathematical knowledge in which an epistemic subject can know a mathematical (...) proposition based solely on a probabilistic proof, one is then forced to admit that such an epistemic subject can know several lottery propositions based solely on probabilistic evidence. Insofar as knowledge of lottery propositions on the basis of probabilistic evidence alone is denied by the vast majority of epistemologists, it is concluded that this constitutes an epistemic reason for rejecting probabilistic proofs as a means of acquiring mathematical knowledge. (shrink)

In this paper, we argue that formal ontological relations avoid Bradley's reductio of relations, including his famous relation regress.

Which rules for aggregating judgments on logically connected propositions are manipulable and which not? In this paper, we introduce a preference-free concept of non-manipulability and contrast it with a preference-theoretic concept of strategy-proofness. We characterize all non-manipulable and all strategy-proof judgment aggregation rules and prove an impossibility theorem similar to the Gibbard--Satterthwaite theorem. We also discuss weaker forms of non-manipulability and strategy-proofness. Comparing two frequently discussed aggregation rules, we show that “conclusion-based voting” is less vulnerable to manipulation than “premise-based (...) voting”, which is strategy-proof only for “reason-oriented” individuals. Surprisingly, for “outcome-oriented” individuals, the two rules are strategically equivalent, generating identical judgments in equilibrium. Our results introduce game-theoretic considerations into judgment aggregation and have implications for debates on deliberative democracy. (shrink)

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

The relation of normic support offers a novel solution to the proof paradox: a paradox in evidence law arising from legal cases involving merely statistical evidence (Smith 2018). Central to the normic support solution has been the thesis that merely statistical evidence cannot confer normic support. However, it has been observed that there are exceptions to this: there exist cases where merely statistical evidence can give rise to normic support (Blome-Tillmann 2020). If correct, this fact seems to undermine the (...) normic support solution to the proof paradox. This paper explores a resolution: normic support can resolve the proof paradox even though merely statistical evidence sometimes gives rise to normic support. The key to understanding this resolution lies with a source of evidential support that arises out of bodies of evidence that involve *character evidence* (Colyvan, et al. 2001). It turns out that character evidence can provide normic support when it is grounded in our knowledge of a certain kind of disposition individuals can have: *goal-directed dispositions*. The upshot is the recovery of the normic support solution to the puzzle of whether statistical evidence can meet legal standards of proof. (shrink)

There is a long tradition of logic, from Aristotle to Gödel, of understanding a proof from the concepts of necessity and causality. Gödel's attempts to define provability in terms of necessity led him to the distinction of formal and absolute (abstract) provability. Turing's definition of mechanical procedure by means of a Turing machine (TM) and Gödel's definition of a formal system as a mechanical procedure for producing formulas prompt us to understand formal provability as a mechanical causality. We propose (...) a formalism which makes explicit the mechanical causal nature of a TM's work. We claim that Gödel's axiomatised ontotheology and his ontological proof give a clue for the understanding of the concept of absolute provability and the pattern of the corresponding absolute completeness proof, respectively. (shrink)

Pierre Bayle is perhaps most well-known for arguing in his Dictionary (1697) that the problem of evil cannot be solved by reason alone. This skepticism about theodicy is usually credited to a religious crisis suffered by Bayle in 1685 following the unjust imprisonment and death of his brother, the death of his father, and the revocation of the Edict of Nantes. But in this paper I argue that Bayle was skeptical about theodicy a decade earlier than these events, from at (...) least the time of his Sedan philosophy course (1675–77). I then argue that both the Various Thoughts on the Comet (1683) and Philosophical Commentary on Luke 4:23 (1686–88), which are usually read as treatments of superstition and toleration respectively, are works that also closely engage the problem of evil and demonstratethe skepticism of Bayle toward theodicy. (shrink)

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)

Despite recent controversies surrounding the principle that knowledge entails truth (KT), this paper aims to prove that the principle is true. It offers a proof of (KT) in the following sense. It advances a deductively valid argument for (KT), whose premises are, by most lights, obviously true. Moreover, each premise is buttressed by at least two supporting arguments. And finally, all premises and supporting arguments can be rationally accepted by people who don’t already accept (KT).

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

This essay addresses one of the open questions of proof-theoretic semantics: how to understand the semantic values of atomic sentences. I embed a revised version of the explanatory proof system of Millson and Straßer (2019) into the proof-theoretic semantics of Francez (2015) and show how to specify (part of) the intended interpretation of atomic sentences on the basis of their occurrences in the premises and conclusions of inferences to and from best explanations.

Computational tools might tempt us to renounce complete cer- tainty. By forgoing of rigorous proof, we could get (very) probable results for a fraction of the cost. But is it really true that proofs (as we know and love them) can lead us to certainty? Maybe not. Proofs do not wear their correct- ness on their sleeve, and we are not infallible in checking them. This suggests that we need help to check our results. When our fellow mathematicians will (...) be too tired or too busy to scrutinize our putative proofs, computer proof assistants could help. But feeding a mathematical argument to a computer is hard. Still, we might be willing to undertake the endeavor in view of the extra perks that formalization may bring—chiefly among them, an enhanced mathematical understanding. (shrink)

Proofs of God in Early Modern Europe offers a fascinating window into early modern efforts to prove God’s existence. Assembled here are twenty-two key texts, many translated into English for the first time, which illustrate the variety of arguments that philosophers of the seventeenth and eighteenth centuries offered for God. These selections feature traditional proofs—such as various ontological, cosmological, and design arguments—but also introduce more exotic proofs, such as the argument from eternal truths, the argument from universal aseity, and the (...) argument ex consensu gentium. Drawn from the work of eighteen philosophers, this book includes both canonical figures (such as Descartes, Spinoza, Newton, Leibniz, Locke, and Berkeley) and noncanonical thinkers (such as Norris, Fontenelle, Voltaire, Wolff, Du Châtelet, and Maupertuis). -/- Lloyd Strickland provides fresh translations of all selections not originally written in English and updates the spelling and grammar of those that were. Each selection is prefaced by a lengthy headnote, giving a biographical account of its author, an analysis of the main argument(s), and important details about the historical context. Strickland’s introductory essay provides further context, focusing on the various reasons that led so many thinkers of early modernity to develop proofs of God’s existence. -/- Proofs of God is perfect for both students and scholars of early modern philosophy and philosophy of religion. (shrink)

The proof paradox results from conflicting intuitions concerning different types of fallible evidence in a court of law. We accept fallible individual evidence but reject fallible statistical evidence even when the conditional probability that the defendant is guilty given the evidence is the same, a seeming inconsistency. This paper defends a solution to the proof paradox, building on a sensitivity account of checking and settling a question. The proposed sensitivity account of legal proof not only requires sensitivity (...) simpliciter but sensitivity of each relevant step of the proof procedure and/or sensitivity concerning all relevant alternatives. This account avoids problems that have been identified for other sensitivity views of legal proof. Moreover, it is argued that sensitivity, rather than safety, is the crucial modal condition for legal proof. It is, finally, shown that the provided account can fruitfully support very different existing views on the relationship between knowledge and legal proof. (shrink)

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

Philosophical Issues, Volume 31, Issue 1, Page 355-373, October 2021.

Researchers often pursue proof of concept research, but criteria for evaluating such research remain poorly specified. This article proposes a general framework for proof of concept research that k...

It is shown how the schema of equivalence can be used to obtain short proofs of tautologies A , where the depth of proofs is linear in the number of variables in A .

Mathematicians distinguish between proofs that explain their results and those that merely prove. This paper explores the nature of explanatory proofs, their role in mathematical practice, and some of the reasons why philosophers should care about them. Among the questions addressed are the following: what kinds of proofs are generally explanatory (or not)? What makes a proof explanatory? Do all mathematical explanations involve proof in an essential way? Are there really such things as explanatory proofs, and if so, (...) how do they relate to the sorts of explanation encountered in philosophy of science and metaphysics? (shrink)

“Proof of concept” is a phrase frequently used in descriptions of research sought in program announcements, in experimental studies, and in the marketing of new technologies. It is often coupled with either a short definition or none at all, its meaning assumed to be fully understood. This is problematic. As a phrase with potential implications for research and technology, its assumed meaning requires some analysis to avoid it becoming a descriptive category that refers to all things scientifically exciting. I (...) provide a short analysis of proof of concept research and offer an example of it within synthetic biology. I suggest that not only are there activities that circumscribe new epistemological categories but there are also associated normative ethical categories or principles linked to the research. I examine these and provide an outline for an alternative ethical account to describe these activities that I refer to as “extended agency ethics”. This view is used to explain how the type of research described as proof of concept also provides an attendant proof of principle that is the result of decision-making that extends across practitioners, their tools, techniques, and the problem solving activities of other research groups. (shrink)

In this paper, I propose that applying the methods of data science to “the problem of whether mathematical explanations occur within mathematics itself” (Mancosu 2018) might be a fruitful way to shed new light on the problem. By carefully selecting indicator words for explanation and justification, and then systematically searching for these indicators in databases of scholarly works in mathematics, we can get an idea of how mathematicians use these terms in mathematical practice and with what frequency. The results of (...) this empirical study suggest that mathematical explanations do occur in research articles published in mathematics journals, as indicated by the occurrence of explanation indicators. When compared with the use of justification indicators, however, the data suggest that justifications occur much more frequently than explanations in scholarly mathematical practice. The results also suggest that justificatory proofs occur much more frequently than explanatory proofs, thus suggesting that proof may be playing a larger justificatory role than an explanatory role in scholarly mathematical practice. (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)

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

Gottfried Leibniz embarked on a research program to prove all the Aristotelic categorical syllogisms by diagrammatic and algebraic methods. He succeeded in proving them by means of Euler diagrams, but didn’t produce a manuscript with their algebraic proofs. We demonstrate how key excerpts scattered across various Leibniz’s drafts on logic contained sufficient ingredients to prove them by an algebraic method –which we call the Leibniz-Cayley (LC) system– without having to make use of the more expressive and complex machinery of first-order (...) quantificational logic. In addition, we prove the classic categorical syllogisms again by a relational method –which we call the McColl-Ladd (ML) system– employing categorical relations studied by Hugh McColl and Christine Ladd. Finally, we show the connection of ML and LC with Boolean algebra, proving that ML is a consequence of LC, and that LC is a consequence of the Boolean lattice axioms, thus establishing Leibniz’s historical priority over George Boole in characterizing and applying (a sufficient fragment of) Boolean algebra to effectively tackle categorical syllogistic. (shrink)

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

A textbook on proof in mathematics, inspired by an Aristotelian point of view on mathematics and proof. The book expounds the traditional view of proof as deduction of theorems from evident premises via obviously valid steps. It deals with the proof of "all" statements, "some" statements, multiple quantifiers and mathematical induction.

We explore depth substitution invariance, or hyperformalism, and extend known results in this realm to justification logics extending weak relevant logics. We then examine the surprising invariance of justifications over formulas and restrict our attention to the substitution of proofs in the original relevant logic. The results of this paper indicate that depth invariance is a recalcitrant feature of the logic and that proof structures in hyperformal logics are quite inflexible.

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to (...) a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics. (shrink)