Peirce’s triadic logic has been under discussion since its discovery in the 1960s by Fisch and Turquette. The experiments with matrices of three-valued logic are recorded in a few pages of unpublished manuscripts dated 1909, a decade before similar systems have been developed by logicians. The purposes of Peirce’s work on such logic, as well as semantical aspects of his system, are disputable. In the most extensive work about it, Turquette suggested that the matrices are related in dual pairs of (...) axiomatic Hilbert-style systems. In this paper, we present a simple tableau proof for a fragment of Peirce three-valued logic, called P3, based on similar approaches in many-valued literature. We demonstrated that this proof is sound and complete. Besides that, taking the false as the only undesignated value and adding non-classical negations to the calculus, we can explore paraconsistent and paracompleteness theories into P3. Keywords: Charles S. Peirce, many-valued logics, theory of proof, tableau method. (shrink)

The paper is an attempt to interpret Imre Lakatos's methodology of scientific research programmes (MSRP) on the basis of his mathematical methodology, the method of proofs and refutations (MPR). After sketching MSRP and MPR and analysing their relationship to Popper's and Poly a's work, I argue that MSRP was originally conceived as a methodology in the same sense as MPR. The most conspicuous difference between the two, namely that MSRP is fundamentally backward‐looking, whereas MPR is primarily forward‐looking, is due to (...) the fact that Lakatos could not carry out his project in the full sense. I also explain why he could not. (shrink)

In an erudite and wide-ranging contribution to this Revista, Jacopo Della Torre leverages the analytical power of comparative legal history to illuminate contemporary debates surrounding the standard of proof for criminal convictions. At the invitation of the Editors, I am pleased to have this opportunity to comment on Della Torre’s thought-provoking article.1 The following remarks are of two broad kinds. The first section of this Comment addresses methodological issues in comparative legal scholarship, largely expressing agreement with Della Torre’s general (...) approach, but with a few caveats and clarifications for further consideration. In the second section, I turn to practical questions of procedural jurisprudence and institutional practice in criminal adjudication. With the disciplinary agenda and biases of an English lawyer, my thoughts on these issues will embroider upon, and diverge somewhat, from Della Torre’s exposition. I will also suggest some minor exegetical corrections and refinements. (shrink)

This paper is a logical study of valid uses of symmetry in deductive reasoning, of what underlying principles make some appeals to symmetry legitimate but others illegitimate. The issue is first motivated informally. A framework is then given covering a fairly broad range of symmetry arguments, and the formulation of symmetry provided is shown to be a valid principle of reasoning, as is a slightly stronger principle of reasoning, one that is shown to be in some sense as strong as (...) possible. The relationship between symmetry and isomorphism is discussed, and finally the framework is extended to a more general model-theoretic setting. (shrink)

The aim of this paper is to present the method of Socratic proofs for seven modal propositional logics: K5, S4.2, S4.3, S4M, S4F, S4R and G. This work is an extension of [10] where the method was presented for the most common modal propositional logics: K, D, T, KB, K4, S4 and S5.

The goal of this paper is to propose correspondence analysis as a technique for generating the so-called erotetic calculi which constitute the method of Socratic proofs by Andrzej Wiśniewski. As we explain in the paper, in order to successfully design an erotetic calculus one needs invertible sequent-calculus-style rules. For this reason, the proposed correspondence analysis resulting in invertible rules can constitute a new foundation for the method of Socratic proofs. Correspondence analysis is Kooi and Tamminga's technique for designing proof (...) systems. In this paper it is used to consider sequent calculi with non-branching, invertible rules for the negation fragment of classical propositional logic and its extensions by binary Boolean functions. (shrink)

Until not too many years ago, all logics except classical logic (and, perhaps, intuitionistic logic too) were considered to be things esoteric. Today this state of a airs seems to have completely been changed. There is a growing interest in many types of nonclassical logics: modal and temporal logics, substructural logics, paraconsistent logics, non-monotonic logics { the list is long. The diversity of systems that have been proposed and studied is so great that a need is felt by many researchers (...) to try to put some order in the present logical jungle. Thus Cl91], Ep90] and Wo88] are three recent books in which an attempt is made to develop a general theoretical framework for the study of logics. On the more pragmatic side, several systems have been developed with the goal of providing a computerized logical framework in which many di erent logical systems can be implemented in a uniform way. An example is the Edinburgh LF( HHP91]). (shrink)

This book contains a systematic and formal attempt to model solutions to problems such as: Is it possible to prove a question? Is it possible to prove something by the use of questions? Do the existing paradigms in the logic of questions allow one to combine questions and proofs? What are the results in this field? In developing answers, the book focuses on the applications of the method of Socratic proofs, and goes beyond that. It starts out with an overview (...) of the leading paradigms, issues, problems and ready solutions in the logic of questions, and places Inferential Erotetic Logic and the method of Socratic proofs against a wider background. It then introduces these two methods in more detail and explains how they can be used for classical logic, intuitionistic propositional logic and for basic modal logics. Next, the book deals with issues specific to the field of the logic of questions, introducing the tools of Minimal Erotetic Semantics (MiES). The final chapters describe the translations between proof systems: from a Socratic transformation, derived in an erotetic calculus, into a sequent system. (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)

In Prior Analytics 1. 15, Aristotle states the following rule of modal logic, which we may call the possibility rule: given the premiss that A is possible, and given a derivation of B from A, it can be inferred that B is possible. Aristotle is the first philosopher known to state this rule, and it stands among his most significant contributions to philosophical thought about modality. He applies the possibility rule in arguments that are central to his physical and metaphysical (...) views, in works such as the _Physics, De caelo, De generationeetcorruptione_, and the _Metaphysics_. These arguments have proved difficult to understand, largely because the exact nature of the possibility rule and its role in each argument is often unclear. The chapter offers a comprehensive treatment of the arguments throughout Aristotle's works, resulting in a better understanding both of the possibility rule and of the individual arguments in which it appears. (shrink)

Who carries the burden of proof in analytic philosophical debates, and how can this burden be satisfied? As it turns out, the answer to this joint question yields a fundamental challenge to the very conduct of metaphysics in analytic philosophy. Empirical research presented in this book indicates that the vastly predominant goal pursued in analytic philosophical dialogues lies not in discovering truths or generating knowledge, but merely in prevailing over one’s opponents. Given this goal, the book examines how most (...) effectively to allocate and discharge the burden of proof. It focuses on premises that must prudently be avoided because a burden of proof on them could never be satisfied, and in particular discusses unsupportable bridge premises across inference barriers, like Hume’s barrier between ‘is’ and ‘ought’, or the barrier between the content of our talk or thought, and the world beyond such content. Employing this content/world barrier for a critical assessment of mainstream analytic philosophical methods, this book argues that we must prudently avoid invoking intuitions or other content of thought or talk in support of claims about the world beyond content, that is, metaphysically significant claims. Yet as content-located evidence is practically indispensable to metaphysical debates throughout analytic philosophy, from ethics to the philosophy of mathematics, this book reaches the startling conclusion that all such metaphysical debates must, prudently, be terminated. (shrink)

I consider two cognitive phenomena: inquiring and justifying, as complementary processes running in opposite directions. I explain on an example that the former process is driven by questions and the latter is a codification of the results of the first one. Traditionally, proof theory focuses on the latter process, and thus describes the former, at best, as an example of a backward proof search. I argue that this is not the best way to analyze cognitive processes driven by (...) questions, and that proof-theoretical analysis of questions can bring mutual benefits for both proof theory and erotetic logic. In the second part of my paper (sect. 6.3) I introduce the structural rules of weakening and contraction. Results concerning their admissibility are discussed. I also sketch an erotetic interpretation of the rule of weakening as reducing information noise, and that of contraction as securing information. (shrink)

In this paper we present an approach to automated learning within mathematical reasoning systems. In particular, the approach enables proof planning systems to automatically learn new proof methods from well-chosen examples of proofs which use a similar reasoning pattern to prove related theorems. Our approach consists of an abstract representation for methods and a machine learning technique which can learn methods using this representation formalism. We present an implementation of the approach within the ΩMEGA (...) class='Hi'>proof planning system, which we call LEARNΩMATIC. We also present the results of the experiments that we ran on this implementation in order to evaluate if and how it improves the power of proof planning systems. (shrink)

In view of an enhancement of our implementation on the computer, we explore the possibility of an algorithmic optimization of the various proof-theoretic techniques employed by Kohlenbach for the synthesis of new effective uniform bounds out of established qualitative proofs in Numerical Functional Analysis. Concretely, we prove that the method of “colouring” some of the quantifiers as “non-computational” extends well to ε-arithmetization, elimination-of-extensionality and model-interpretation.

The ancient Greek method of analysis has a rational reconstruction in the form of the tableau method of logical proof. This reconstruction shows that the format of analysis was largely determined by the requirement that proofs could be formulated by reference to geometrical figures. In problematic analysis, it has to be assumed not only that the theorem to be proved is true, but also that it is known. This means using epistemic logic, where instantiations of variables are typically allowed (...) only with respect to known objects. This requirement explains the preoccupation of Greek geometers with questions as to which geometrical objects are ?given?, that is, known or ?data?, as in the title of Euclid's eponymous book. In problematic analysis, constructions had to rely on objects that are known only hypothetically. This seems strange unless one relies on a robust idea of ?unknown? objects in the same sense as the unknowns of algebra. The Greeks did not have such a concept, which made their grasp of the analytic method shaky. (shrink)

The purpose of this paper may be found in the following quotation. “Whenever an argument can be made to lead to a descending infinitude of natural numbers the hypothesis upon which the argument rests becomes untenable. This method of proof is called the method of infinite descent;.... It would be interesting and valuable to compare this method with the method of mathematical induction.”.

In this paper, we first briefly survey the main responses to the challenge that experimental philosophy poses to the method of cases, given the common assumption that the latter is crucially based on intuitive judgments about cases. Second, we discuss two of the most popular responses in more detail: the expertise defense and the mischaracterization objection. Our take on the expertise defense is that the available empirical data do not support the claim that professional philosophers enjoy relevant expertise in their (...) intuitive judgments about cases. In contrast, the mischaracterization objection seems considerably more promising than its largely negative reception has suggested. We argue that the burden of proof is thus on philosophers who still hold that the method of cases crucially relies on intuitive judgments about cases. Finally, we discuss whether conceptual engineering provides an alternative to the method of cases in light of the challenge from experimental philosophy. We argue that this is not clearly the case, because conceptual engineering also requires descriptive information about the concepts it aims to improve. However, its primarily normative perspective on our concepts makes it largely orthogonal to the challenge from experimental philosophy, and it can also benefit from the empirical methods of the latter. (shrink)

This study of Plato's Phaedo promotes better understanding of its arguments for the soul's immortality by showing how Plato intended them, not as proofs, but as properly dialectical arguments functioning in accordance with the method of hypothesis. Unlike the argument for the soul's immortality in the Phaedrus, which does seem intended as a proof, the Phaedo arguments are proceeding toward the first principles that could serve as the basis for a proof - the most important being an account (...) of the soul's own essential nature. This study attends to the substantial progress the Phaedo makes toward such an account. It also considers Socrates' epistemic situation in the dialogue and the problem of whether his confidence in the face of death is misplaced if his arguments have not been proofs before considering how the concluding myth draws together several of the dialogue's main themes. (shrink)

The method of mathematical induction: The method of mathematical induction -- Examples and exercises -- The proof of induction of some theorems of elemetary algebra -- Solutions.

In the period 1893–1897 Charles Dodgson, writing as Lewis Carroll, published two books and two articles on logic topics. Manuscript material first published in 1977 together with letters and diary entries provide evidence that he was working toward a visual proof system for complex syllogistic propositional logic based on a mechanical tree method that he devised.

The Fraenkel-Mostowski method has been widely used to prove independence results among weak versions of the axiom of choice. In this paper it is shown that certain statements cannot be proved by this method. More specifically it is shown that in all Fraenkel-Mostowski models the following hold: 1. The axiom of choice for sets of finite sets implies the axiom of choice for sets of well-orderable sets. 2. The Boolean prime ideal theorem implies a weakened form of Sikorski's theorem.

Abstrack In this study, the subject of preference, its conceptual field and its historical process, as well as the methods of determining and choosing different readings of mutawatir recitation imâms are discussed. The different phrasing of the Qur'an began from the revelation period of the revelation. It is seen that there were some discussions about the different readings of the Qur'an among the Companions in the early period, albeit a little. These different recitations of some of the Companions, who (...) see their own reading better or who are not aware of their friends' readings, are the Prophet's. The fact that they took them to the Prophet indicates this. As a matter of fact, Allah's command to "read whatever is easy from the Qur'an" (Muzzammil, 73/20) and the hadith of the Messenger of Allah "read whatever is easy from it", together with the different reading license, also implicate his preference. Arab tribes who used different dialects from the Quraysh dialect during the Medina period and those who converted to Islam from other non-Arab nations faced some difficulties in pronouncing and understanding the Qur'an, which was revealed in the Quraysh dialect. Wanting to solve this serious problem, Hz. Prophet was given the permission to read with seven letters, the differences in recitation began to be seen. The concepts of preference and elder refer to the practices of the imams of recitation in the process of creating their own recitations together with their proofs, which they chose from among the recitations of their predecessors. In the science of hujjat, the most used concepts, along with other concepts, are the concepts of old age, preference and need. Ihticaj is a concept that expresses choosing one among different recitations by citing evidences and proofs. As a matter of fact, when the works of the recitation scholars on this subject are examined, it is seen that the imâms made their choices by citing evidence from the Qur'an, Sunnah, Mushafs and language rules regarding the differences in recitation. In the science of recitation, some other concepts such as ulema, especially proof, and illet and evidence were also used. Whether it is the Qurra that stands out in the field of natural recitation, or the imams of mutawatir recitation, they have formed their preferences by bringing evidence from verses, sunnah, mushaf, saned and language in line with the criteria of sound recitation. (shrink)

Most historians and philosophers of philosophy and history of mathematics hold one interpretation or the other of the nature of method of analysis and synthesis in itself and in its historical development. In this paper, I am trying to prove – through three points – that, in fact, there were two understandings of that method in Greek mathematics and philosophy, and which were reflected in Arabic mathematical science and philosophy; this reflection is considered as proof also of this double (...) nature of that method. Thus, we have to rethink the nature of Arabic philosophy systems. (shrink)

Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle (...) and I apologize for not displaying these results as well.Moreover the audience should be aware that in some points I have to oversimplify matters. Those who complain about that are invited to consult the original papers.1.1. General. Proof theory startedwithHilbert's Programme which aimed at a finitistic consistency proof for mathematics.By Gödel's Theorems, however, we know that we can neither formalize all mathematics nor even prove the consistency of formalized fragments by finitistic means. Inspite of this fact I want to give some reasons why I consider proof theory in the style of Gentzen's work still as an important and exciting field of Mathematical Logic. I will not go into applications of Gentzen's cut-elimination technique to computer science problems—this may be considered as applied proof theory—but want to concentrate on metamathematical problems and results. In this sense I am talking about Pure Proof Theory.Mathematicians are interested in structures. There is only one way to find the theorems of a structure. Start with an axiom system for the structure and deduce the theorems logically. These axiom systems are the objects of proof-theoretical research. Studying axiom systems there is a series of more or less obvious questions. (shrink)

his paper presents a unified treatment of the propositional and first-order many-valued logics through the method of tableaux. It is shown that several important results on the proof theory and model theory of those logics can be obtained in a general way. We obtain, in this direction, abstract versions of the completeness theorem, model existence theorem (using a generalization of the classical analytic consistency properties), compactness theorem and Lowenheim-Skolem theorem. The paper is completely self-contained and includes examples of application (...) to particular many-valued formal systems. (shrink)

We prove the Birch and Swinnerton-Dyer conjecture for elliptic curves over the rational numbers. Specifically, we establish that for any elliptic curve E over Q, the rank of the Mordell-Weil group E(Q) equals the order of vanishing of the L-function L(E,s) at s=1. The proof proceeds in three main steps. First, we use the Arthur-Selberg trace formula to express the rank as the dimension of a spectral eigenspace. Second, we apply the Satake isomorphism and strong multiplicity one theorem to (...) isolate the automorphic representation π_E associated to E via modularity. Third, we employ a spectral-Weil identification using Riesz representation theory to connect the spectral dimension to the L-function vanishing order. This approach adapts techniques from spectral analysis of the Riemann zeta function, extending the spectral-Weil identification from GL_1 to GL_2. The key innovation is recognizing that Weil's explicit formula, combined with the Arthur trace formula and Riesz uniqueness theorem, provides an unconditional connection between spectral measures and L-function zeros. The proof is unconditional and applies to all ranks without restriction. (shrink)

In [4], I proved that the product-free fragment L of Lambek's syntactic calculus (cf. Lambek [2]) is not finitely axiomatizable if the only rule of inference admitted is Lambek's cut-rule. The proof (which is rather complicated and roundabout) was subsequently adapted by Kandulski [1] to the non-associative variant NL of L (cf. Lambek [3]). It turns out, however, that there exists an extremely simple method of non-finite-axiomatizability proofs which works uniformly for different subsystems of L (in particular, for NL). (...) We present it below to the use of those who refer to the results of [1] and [4]. (shrink)

The value of knowledge and deeds of the methodology of the reasoning defined such as “due to they have a common effective cause (ʿilla), the provision of principle (aṣl) is given to the branch (farʿ)” has been the subject of debate from the first period. That is, on the one hand there are some who reject the method of analogical reasoning by saying that although the authority of legislation belongs to Shāri’only, this method is to make legislation in the religion (...) and that its value in knowledge is condemned as conjecture by the injunction (naṣṣ). They also put forward some arguments as well. However, on the other hand the majority accepts the method of reasoning as an essential and sharʿī (religious) argument. This study will not compare the opinions of those who reject qiyās and that of those who approve it. By means of religious and rational evidences this study will deal with that the method of analogical reasoning is not a rational effort simply, that the knowledge gained by it is not a conjecture criticised by the injunctions, that it is the highest ranking conjecture based on the proof, and that it is sufficient to practice in the field of law. After a general frame is drawn about qiyās, this article has been limited with the place of qiyās in the hierarchy of evidence and its value concerning knowledge and practice. This article wants to clarify the discussions related to the value of knowledge and deeds of the methodology of the reasoning. (shrink)

A few years ago, a manuscript by Jost Bürgi (1552–1632) was brought to scholarly attention, which included an ingenious sine calculation method. The purpose of this paper is to discuss two aspects of this manuscript. First, we wish to improve the current understanding of Bürgi’s method of sine calculation, especially with respect to the calculation of sines at a resolution of 1 min. Second, we wish to suggest a possible transfer of knowledge between India’s Kerala School of mathematical astronomy and (...) Bürgi. The evidence for the latter seems to be stronger than the evidence for other available case studies, but still revolves mainly around analogies, and can therefore not be considered as conclusive proof of transmission. We also append a translation of the relevant chapter of Bürgi’s treatise. (shrink)

How the concept of proof has enabled the creation of mathematical knowledge. The Story of Proof investigates the evolution of the concept of proof--one of the most significant and defining features of mathematical thought--through critical episodes in its history. From the Pythagorean theorem to modern times, and across all major mathematical disciplines, John Stillwell demonstrates that proof is a mathematically vital concept, inspiring innovation and playing a critical role in generating knowledge. Stillwell begins with Euclid and (...) his influence on the development of geometry and its methods of proof, followed by algebra, which began as a self-contained discipline but later came to rival geometry in its mathematical impact. In particular, the infinite processes of calculus were at first viewed as "infinitesimal algebra," and calculus became an arena for algebraic, computational proofs rather than axiomatic proofs in the style of Euclid. Stillwell proceeds to the areas of number theory, non-Euclidean geometry, topology, and logic, and peers into the deep chasm between natural number arithmetic and the real numbers. In its depths, Cantor, Gödel, Turing, and others found that the concept of proof is ultimately part of arithmetic. This startling fact imposes fundamental limits on what theorems can be proved and what problems can be solved. Shedding light on the workings of mathematics at its most fundamental levels, The Story of Proof offers a compelling new perspective on the field's power and progress. (shrink)

Pierre de Fermat is known as the inventor of modern number theory. He invented–improved many methods useful in this discipline. Fermat often claimed to have proved his most difficult theorems thanks to a method of his own invention: the infinite descent. He wrote of numerous applications of this procedure. Unfortunately, he left only one almost complete demonstration and an outline of another demonstration. The outline concerns the theorem that every prime number of the form 4n + 1 is the (...) sum of two squares. In this paper, we analyse a recent proof of this theorem. It is interesting because: it follows all the elements of which Fermat wrote in his outline; it represents a good introduction to all logical nuances and mathematical variants concerning this method of which Fermat spoke. The assertions by Fermat will also be framed inside their historical context. Therefore, the aims of this paper are related to the history of mathematics and to the logic of proof-methods. (shrink)

A common description of a mathematical proof is as a logically structured sequence of assertions, beginning from accepted premises and proceeding by standard inference rules to a conclusion. Does this description match the language of proofs as mathematicians write them in their research articles? In this chapter, we use methods from corpus linguistics to look at the prevalence of imperatives and instructions in mathematical preprints from the arXiv repository. We find thirteen verbs that are used most often to (...) form imperatives in proofs, and that these show up significantly more often within proofs than in the surrounding mathematical writing. We also show that there are many more verbs used to form a diverse selection of instructions in proofs. These findings are at odds with the view of proofs as sequences of assertions. Instead, we argue in favour of the recipe model of proofs: that proofs are like recipes, giving instructions for mathematical actions to be carried out. (shrink)