Computer assisted theorem proving is an increasingly important part of mathematical methodology, as well as a long-standing topic in artificial intelligence (AI) research. However, the current generation of theorem proving software have limited functioning in terms of providing new proofs. Importantly, they are not able to discriminate interesting theorems and proofs from trivial ones. In order for computers to develop further in theorem proving, there would need to be a radical change in how the software functions. Recently, (...) machine learning results in solving mathematical tasks have shown early promise that deep artificial neural networks could learn symbolic mathematical processing. In this paper, I analyze the theoretical prospects of such neural networks in proving mathematical theorems. In particular, I focus on the question how such AI systems could be incorporated in practice to theorem proving and what consequences that could have. In the most optimistic scenario, this includes the possibility of autonomous automated theorem provers (AATP). Here I discuss whether such AI systems could, or should, become accepted as active agents in mathematical communities. (shrink)

This chapter focuses on one of the common fallacies in Western philosophy called 'proving too much'. The proving too much fallacy has been committed when an argument can be used to also prove something false or leads to contradictory conclusions. An argument that proves too much demonstrates a lack of soundness, since sound arguments can only establish true conclusions, and thus when an argument can be used to prove false conclusions, it becomes evident that there is a flaw (...) in its reasoning. The fallacy of proving too much is not really a single fallacy so much as a great tool for detecting faulty reasoning, since any argument that leads to a contradiction cannot be sound. There are a few forms this fallacy can take on such as when an argument leads to multiple contradictory conclusions. (shrink)

In this paper we focus on theorem proving for conditional logics. First, we give a detailed description of CondLean, a theorem prover for some standard conditional logics. CondLean is a SICStus Prolog implementation of some labeled sequent calculi for conditional logics recently introduced. It is inspired to the so called “lean” methodology, even if it does not fit this style in a rigorous manner. CondLean also comprises a graphical interface written in Java. Furthermore, we introduce a goal-directed proof search (...) mechanism, derived from the above mentioned sequent calculi based on the notion of uniform proofs. Finally, we describe GOALDUCK, a simple SICStus Prolog implementation of the goal-directed calculus mentioned here above. Both the programs CondLean and GOALDUCK, together with their source code, are available for free download at. (shrink)

In this chapter we introduce concepts for analyzing proofs, and for analyzing undergraduate and beginning graduate mathematics students’ proving abilities. We discuss how coordination of these two analyses can be used to improve students’ ability to construct proofs. -/- For this purpose, we need a richer framework for keeping track of students’ progress than the everyday one used by mathematicians. We need to know more than that a particular student can, or cannot, prove theorems by induction or contradiction or (...) can, or cannot, prove certain theorems in beginning set theory or analysis. It is more useful to describe a student’s work in terms of a finer-grained framework that includes various smaller abilities that contribute to proving and that can be learned in differing ways and at differing periods of a student’s development. (shrink)

We consider equational theories based on axioms for recursively defining functions, with rules for equality and substitution, but no form of induction—we denote such equational theories as PETS for pure equational theories with substitution. An example is Cook’s system PV without its rule for induction. We show that the Bounded Arithmetic theory $\mathrm {S}^{1}_2$ proves the consistency of PETS. Our approach employs model-theoretic constructions for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be (...) of independent interest. (shrink)

(2013). Incompatibilism proved. Canadian Journal of Philosophy. ???aop.label???

We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S 1 2 . In particular this solves an open problem formulated by TAKEUTI (c.f. [5, p.5 problem 9.]).

Formal verification involves the use of logical and computational methods to establish claims that are expressed in precise mathematical terms. These can include ordinary mathematical theorems, as well as claims that pieces of hardware or software, network protocols, and mechanical and hybrid systems meet their specifications. In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point (...) establishing claims as to their correctness becomes a form of theorem proving. Conversely, the proof of a mathematical theorem may require a lengthy computation, in which case verifying the truth of the theorem requires verifying that the computation does what it is supposed to do. The gold standard for supporting a mathematical claim is to provide a proof, and twentieth-century developments in logic show most if not all conventional proof methods can be reduced to a small set of axioms and rules in any of a number of foundational systems. With this reduction, there are two ways that a computer can help establish a claim: it can help find a proof in the first place, and it can help verify that a purported proof is correct. Automated theorem proving focuses on the “finding” aspect. Resolution theorem provers, tableau theorem provers, fast satisfiability solvers, and so on provide means of establishing the validity of formulas in propositional and first-order logic. Other systems provide search procedures and decision procedures for specific languages and domains, such as linear or nonlinear expressions over the integers or the real numbers. Architectures like SMT combine domain-general search methods with domain-specific procedures. Computer algebra systems and specialized mathematical software packages provide means of carrying out mathematical computations, establishing mathematical bounds, or finding mathematical objects. A calculation can be viewed as a proof as well, and these systems, too, help establish mathematical claims. Automated reasoning systems strive for power and efficiency, often at the expense of guaranteed soundness. Such systems can have bugs, and it can be difficult to ensure that the results they deliver are correct. In contrast, interactive theorem proving focuses on the “verification” aspect of theorem proving, requiring that every claim is supported by a proof in a suitable axiomatic foundation. This sets a very high standard: every rule of inference and every step of a calculation has to be justified by appealing to prior definitions and theorems, all the way down to basic axioms and rules. In fact, most such systems provide fully elaborated “proof objects” that can be communicated to other systems and checked independently. Constructing such proofs typically requires much more input and interaction from users, but it allows us to obtain deeper and more complex proofs. The Lean Theorem Prover aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains. (shrink)

It is quite common to object to an argument by saying that it “proves too much.” In this paper, I argue that the “proving too much” charge can be understood in at least three different ways. I explain these three interpretations of the “proving too much” charge. I urge anyone who is inclined to level the “proving too much” charge against an argument to think about which interpretation of that charge one has in mind.

This paper addresses the question: given some theory T that we accept, is there some natural, generally applicable way of extending T to a theory S that can prove a range of things about what it itself (i.e. S) can prove, including a range of things about what it cannot prove, such as claims to the effect that it cannot prove certain particular sentences (e.g. 0 = 1), or the claim that it is consistent? Typical characterizations of Gödel’s second incompleteness (...) theorem, and its significance, would lead us to believe that the answer is ‘no’. But the present paper explores a positive answer. The general approach is to follow the lead of recent (and not so recent) approaches to truth and the Liar paradox. (shrink)

This piece continues the tradition of arguments by John Lucas, Roger Penrose and others to the effect that the human mind is not a machine. Kurt Gödel thought that the intensional paradoxes stand in the way of proving that the mind is not a machine. According to Gödel, a successful proof that the mind is not a machine would require a solution to the intensional paradoxes. We provide what might seem to be a partial vindication of Gödel and show (...) that if a particular solution to the intensional paradoxes is adopted, one can indeed give an argument to the effect that the mind is not a machine. (shrink)

Arguments to the effect that Church's thesis is intrinsically unprovable because proof cannot relate an informal, intuitive concept to a mathematically defined one are unconvincing, since other 'theses' of this kind have indeed been proved, and Church's thesis has been proved in one direction. However, though evidence for the truth of the thesis in the other direction is overwhelming, it does not yet amount to proof.

In many toxic-tort cases - notably in Oxendine v. Merrell Dow Pharmaceuticals, Inc, and in Joiner v. G.E., - plaintiffs argue that the expert testimony they wish to present, though no part of it is sufficient by itself to establish causation "by a preponderance of the evidence," is jointly sufficient to meet this standard of proof; and defendants sometimes argue in response that it is a mistake to imagine that a collection of pieces of weak evidence can be any stronger (...) than its individual components. This article draws on the epistemological theory I first presented in 1993 in Evidence and Inquiry, and then amplified and refined in 2003 in Defending Science - Within Reason. This theory of evidence shows that, under certain conditions, a combination of pieces of evidence none of which is sufficient by itself really can warrant a casual conclusion to a higher degree than any of its components alone. When my account is applied to the very complex congeries of evidence typically proffered to prove general causation in these toxic-tort cases, it improves on the influential "Bradford Hill criteria" for assessing causation; and it suggests answers to questions frequently raised in such cases: e.g., whether epidemiological evidence is essential for proof of causation, and whether such evidence should be excluded if it is not statistically significant. Moreover, the argument of this paper reveals that by obliging courts to screen each item of expert testimony individually for reliability, the atomism implicit in Daubert will sometimes stand in the way of an accurate assessment of the worth of complex causation evidence. (shrink)

Bertand's Postulate is proved in Peano Arithmetic minus the Successor Axiom.

Justification of theorems plays a vital role in any rational human activity. It is indispensable in science. The deductive method of justifying theorems is used in all sciences and it is the only method of justifying theorems in deductive disciplines. It is based on the notion of proof, thus it is a method of proving theorems. In the Warsaw School of Logic (WSL) – the famous branch of the Lvov-Warsaw School (LWS) – two types of the method: axiomatic deduction (...) method and natural deduction method were developed and practiced. In this paper, both of these methods are briefly discussed with an emphasis on their historical, groundbreaking significance for logic. The axiomatic method by means of rejection (proposed by Jan Łukasiewicz – a co-creator of the WSL), which is the method of the so-called rejection proof (rejection/refutation method) in logical systems and the proving method of generalized natural deduction, which is a hybrid deduction–refutation method of proving theorems, are also outlined in the paper. The author discusses their historical significance. This paper also contains a brief mention of the most significant results which the application of the discussed methods introduced into contemporary scientific research, not only logical one. (shrink)

Since Opuz v. Turkey (2009), the European Court of Human Rights (ECHR) delivered over a dozen judgments in which it examined domestic violence through the prism of gender-based discrimination. Apart from the individual circumstances of the cases, the Court considered the general approach to domestic violence in the defendant states, searching for a large-scale structural gender bias. Hence, although the Court has not directly referred to the notion of “structural discrimination” in relation to domestic violence, it engaged in unveiling this (...) problem within the state parties. Building on the case law of the Court, the article presents and systemizes information that may prove structural gender discrimination in domestic violence cases. It navigates potential applicants through the Court’s interpretation and indicates arguments and sources that may support their claims. In particular, it discusses what kind of data and information may demonstrate the general, discriminatory attitude of the authorities towards domestic violence and what sources the applicants may use while seeking the evidence. (shrink)

This paper proves a precisification of Hume’s Law—the thesis that one cannot get an ought from an is—as an instance of a more general theorem which establishes several other philosophically interesting, though less controversial, barriers to logical consequence.

The concept of burden of proof is used in a wide range of discourses, from philosophy to law, science, skepticism, and even in everyday reasoning. This paper provides an analysis of the proper deployment of burden of proof, focusing in particular on skeptical discussions of pseudoscience and the paranormal, where burden of proof assignments are most poignant and relatively clear-cut. We argue that burden of proof is often misapplied or used as a mere rhetorical gambit, with little appreciation of the (...) underlying principles. The paper elaborates on an important distinction between evidential and prudential varieties of burdens of proof, which is cashed out in terms of Bayesian probabilities and error management theory. Finally, we explore the relationship between burden of proof and several (alleged) informal logical fallacies. This allows us to get a firmer grip on the concept and its applications in different domains, and also to clear up some confusions with regard to when exactly some fallacies (ad hominem, ad ignorantiam, and petitio principii) may or may not occur. (shrink)

This paper introduces and describes new protocols for proving knowledge of secrets without giving them away: if the verifier does not know the secret, he does not learn it. This can all be done while only using one-way hash functions. If also the use of encryption is allowed, these goals can be reached in a more efficient way. We extend and use the GNY authentication logic to prove correctness of these protocols.

In the Lambek calculus of order 2 we allow only sequents in which the depth of nesting of implications is limited to 2. We prove that the decision problem of provability in the calculus can be solved in time polynomial in the length of the sequent. A normal form for proofs of second order sequents is defined. It is shown that for every proof there is a normal form proof with the same axioms. With this normal form we can give (...) an algorithm that decides provability of sequents in polynomial time. (shrink)

Hume’s famous character Cleanthes claims that there is no difficulty in explaining the existence of causal chains with no first cause since in them each item is causally explained by its predecessor. Relying on logico-mathematical resources, we argue for two theses: (1) if the existence of Cleanthes’ chain can be explained at all, it must be explained by the fact that the causal law ruling it is in force, and (2) the fact that such a causal law is in force (...) cannot explain the occurrence of the events in the chain. In order to perform (1), we manage to express in mathematical terms the intuitive idea that indefinitely delayed explanation is ultimately no explanation. In order to achieve (2), we identify a logical relation we can prove to be as strong as the causal relation at issue in the Cleanthes passage, according to a precise notion of strength of relations. (shrink)

Uniform proofs systems have recently been proposed [Mi191j as a proof-theoretic foundation and generalization of logic programming. In [Mom92a] an extension with constructive negation is presented preserving the nature of abstract logic programming language. Here we adapt this approach to provide a complete theorem proving technique for minimal, intuitionistic and classical logic, which is totally goal-oriented and does not require any form of ancestry resolution. The key idea is to use the Godel-Gentzen translation to embed those logics in the (...) syntax of Hereditary Harrop formulae, for which uniform proofs are complete. We discuss some preliminary implementation issues. (shrink)

Gauss’s quadratic reciprocity theorem is among the most important results in the history of number theory. It’s also among the most mysterious: since its discovery in the late 18th century, mathematicians have regarded reciprocity as a deeply surprising fact in need of explanation. Intriguingly, though, there’s little agreement on how the theorem is best explained. Two quite different kinds of proof are most often praised as explanatory: an elementary argument that gives the theorem an intuitive geometric interpretation, due to Gauss (...) and Eisenstein, and a sophisticated proof using algebraic number theory, due to Hilbert. Philosophers have yet to look carefully at such explanatory disagreements in mathematics. I do so here. According to the view I defend, there are two important explanatory virtues—depth and transparency—which different proofs (and other potential explanations) possess to different degrees. Although not mutually exclusive in principle, the packages of features associated with the two stand in some tension with one another, so that very deep explanations are rarely transparent, and vice versa. After developing the theory of depth and transparency and applying it to the case of quadratic reciprocity, I draw some morals about the nature of mathematical explanation. (shrink)

Proving academic plagiarism is difficult. This volume borrows principles from textual criticism to illustrate new techniques for demonstrating plagiarism. These techniques can be used to persuade others—colleagues, editors, publishers, and research integrity committees—when academic plagiarism has been committed.

A new technique for proving realisability results is presented, and is illustrated in detail for the simple case of arithmetic minus induction. CL is a Gentzen formulation of classical logic. CPQ is CL minus the Cut Rule. The basic proof theory and model theory of CPQ and CL is developed. For the semantics presented CPQ is a paraconsistent logic, i.e. there are non-trivial CPQ models in which some sentences are both true and false. Two systems of arithmetic minus induction (...) are introduced, CL-A and CPQ-A based on CL and CPQ, respectively. The realisability theorem for CPQ-A is proved: It is shown constructively that to each theorem A of CPQ-A there is a formula A *, a so-called “realised disjunctive form of A ”, such that variables bound by essentially existential quantifiers in A * can be written as recursive functions of free variables and variables bound by essentially universal quantifiers. Realisability is then applied to prove the consistency of CL-A, making use of certain finite non-trivial inconsistent models of CPQ-A. (shrink)

In this paper I critically review the long history of attempts to formulate and derive the geodesic principle, which claims that massive bodies follow geodesic paths in general relativity theory. I argue that if the principle is interpreted as a dynamical law of motion describing the actual evolution of gravitating bodies as endorsed by Einstein, then it is impossible to apply the law to massive bodies in a way that is coherent with his own field equations. Rejecting this canonical interpretation, (...) I propose an alternative interpretation of the geodesic principle as a type of universality thesis analogous to the universality behavior exhibited in thermal systems during phase transitions. (shrink)

Higher-Order Logic (HOL) is a proof development system intended for applications to both hardware and software. It is principally used in two ways: for directly proving theorems, and as theorem-proving support for application-specific verification systems. HOL is currently being applied to a wide variety of problems, including the specification and verification of critical systems. Introduction to HOL provides a coherent and self-contained description of HOL containing both a tutorial introduction and most of the material that is needed for (...) day-to-day work with the system. After a quick overview that gives a "hands-on feel" for the way HOL is used, there follows a detailed description of the ML language. The logic that HOL supports and how this logic is embedded in ML, are then described in detail. This is followed by an explanation of the theorem-proving infrastructure provided by HOL. Finally two appendices contain a subset of the reference manual, and an overview of the HOL library, including an example of an actual library documentation. (shrink)

I define predeterminism as the claim that what is actual is actual with certainty, and provide a proof of it in this paper. Predeterminism solves a major problem: modal realism’s probability distributions for selecting the actual world from all the possible worlds, are either arbitrary, because they are not unique, or they do not sum up to one. This problem is solved by replacing modal realism with a set-theoretic plenitude subjected to cosmological natural selection. Essentially, because worlds reproduce with unequal (...) success, and because there are so many of them in the plenitude, worlds outnumber and outweigh each other with infinite factors. An infinitely growing sequence of worlds, or a world life, comes out as the unique champion in this evolutionary competition and is certainly actual. The proof uses the ideas that the probability to be actual for a world is proportional to its size, age, and abundance, and that all the possible worlds are set-theoretically well-ordered by cosmological natural selection. (shrink)

Riassunto Nell’ambito degli studi su Vegezio la datazione dell’Epitoma rei militaris e l’identificazione dell’anonimo imperatore sono questioni lungamente dibattute e approdate a varie soluzioni; Teodosio I ora costituisce la dottrina vulgata. Nessuno ha mai messo in dubbio la pertinenza di Vegezio all’impero romano d’Occidente. Il presente articolo parte dai risultati innovativi di un precedente studio, dove si dimostra che Vegezio scrisse l’Epitoma nell’impero romano d’Oriente intorno al 435 e la dedicò a Teodosio II. Qui l’appartenenza di Vegezio all’impero romano d’Oriente (...) e l’identificazione del destinatario con Teodosio II vengono ulteriormente corroborate, ma si propone una datazione leggermente più alta, più precisamente verso il 425. (shrink)