Dieser Beitrag zielt darauf ab, verschiedene geschichtswissenschaftliche Perspektiven auf den wechselseitigen Zusammenhang von Herrschaft und Gewalt kritisch zu beleuchten. Dabei spielt die häufig unzureichende Differenzierung zwischen Quellenbegriff und Forschungsbegriff erkenntnistheoretisch eine wichtige Rolle. Mit „Ordnung" und „Sicherheit" sollen dann zwei akteurszentrierte Bezugssysteme herangezogen werden, um die historische Forschungsperspektive so erweitem zu konnen, dass mogliche Auswege aus dem hier behandelten erkenntnistheoretischen Dilemma aufgezeigt werden können.

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)

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)

The hard problem of induction is to argue without begging the question that inductive inference, applied properly in the proper circumstances, is conducive to truth. A recent theorem seems to show that the hard problem has a deductive solution. The theorem, provable in ZFC, states that a predictive function M exists with the following property: whatever world we live in, M ncorrectly predicts the world’s present state given its previous states at all times apart from a well-ordered subset. On the (...) usual model of time a well-ordered subset is small relative to the set of all times. M’s existence therefore seems to provide a solution to the hard problem. My paper argues for two conclusions. First, the theorem does not solve the hard problem of induction. More positively though, it solves a version of the problem in which the structure of time is given modulo our choice of set theory. (shrink)

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

These notes are meant to continue from the paper on Consistency, in proving number-theoretic theorems from the second-order arithmetical system called FFFF. Its ultimate target is Quadratic Reciprocity, although it introduces and proves some facts about the least common multiple at the start.

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)

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

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.

John Forrester’s book Thinking in Cases does not provide one ultimate definition of what it means to ‘think in cases’, but rather several alternatives: a ‘style of reasoning’ (Hacking), ‘paradigms’ or ‘exemplars’ (Kuhn), and ‘language games’ (Wittgenstein), to mention only a few. But for Forrester, the stories behind each of the figures who suggested these different models for thinking (in cases) are as important as the models themselves. In other words, the question for Forrester is not only what ‘thinking in (...) cases’ is, but also who might be considered a ‘thinker in cases’. Who could serve as a case study for such a thinker? The major candidates that Forrester considers in his book to be ‘thinkers in cases’ are Kuhn, Foucault, Freud, and Winnicott. In what follows, I will argue that one name is missing from this list, as well as from Forrester’s book more generally: Michael Balint. This name is missing not only because Balint was a great ‘thinker in cases’, but also because we have some reasons to believe that Forrester himself thought so and wished to add him to the list. Forrester, I will argue, found in Balint an exemplar for a thinker in cases that combined elements from Winnicott’s psychoanalytic theory and Foucault’s philosophy of the case-based sciences. (shrink)

A system for the modal logic K furnishes a simple mechanical process for proving theorems.

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)

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 article assumes that a profession is a number of individuals in the same occupation voluntarily organized to earn a living by openly serving a moral ideal in a morally-permissible way beyond what law, market, morality, and public opinion would otherwise require. Our question is whether the concept of profession may have a far wider range than the term, so that, for example, pointing out that a certain language lacks a word for “profession” in our sense, is not enough to (...) show that those who speak the language also lack the concept. We believe the survey of 71 Chinese reported here begins to answer that question. This article has four parts. The first describes who was interviewed, how, when, and so on. The second describes some important features of the survey’s questions, explaining how the questions track the concept of profession. The third part reports and interprets the results relevant to our question. The forth defends a tentative answer to the question with which we began—arguing the survey supports the claim that China has a profession of engineering. This article should serve as a “proof of concept”, that is, a model for similar studies around the world both of engineering and of other occupations thought to be professions. (shrink)

Geared to preparing students to make the transition from solving problems to proving theorems, this text teachs them the techniques needed to read and write proofs. The book begins with the basic concepts of logic and set theory, to familiarize students with the language of mathematics and how it is interpreted. These concepts are used as the basis for a step-by-step breakdown of the most important techniques used in constructing proofs. To help students construct their own proofs, this new (...) edition contains over 200 new exercises, selected solutions, and an introduction to Proof Designer software. No background beyond standard high school mathematics is assumed. Previous Edition Hb (1994) 0-521-44116-1 Previous Edition Pb (1994) 0-521-44663-5. (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)

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)

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)

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.

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)

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)

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)

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)

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)

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.]).

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)

Ordinary mathematical proofs—to be distinguished from formal derivations—are the locus of mathematical knowledge. Their epistemic content goes way beyond what is summarised in the form of theorems. Objections are raised against the formalist thesis that every mainstream informal proof can be formalised in some first-order formal system. Foundationalism is at the heart of Hilbert's program and calls for methods of formal logic to prove consistency. On the other hand, ‘systemic cohesiveness’, as proposed here, seeks to explicate why mathematical knowledge is (...) coherent (in an informal sense) and places the problem of reliability within the province of the philosophy of mathematics. (shrink)

We review some fundamental questions concerning the real line of mathematical analysis, which, like the Continuum Hypothesis, are also independent of the axioms of set theory, but are of a less ‘problematic’ nature, as they can be solved by adopting the right axiomatic framework. We contend that any foundations for mathematics should be able to simply formulate such questions as well as to raise at least the theoretical hope for their resolution.The usual procedure in set theory is to add so-called (...) strong axioms of infinity to the standard axioms of Zermelo-Fraenkel, but then the question of their justification becomes to some people vexing. We show how the adoption of a view of the universe of sets with classes, together with certain kinds of Global Reflection Principles resolves some of these issues. (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.

There are two distinct meanings to ‘mathematical proof’. The connection between them is an unsolved problem. The first step in attacking it is noticing that it is an unsolved problem.

This article investigates “impaired insight,” a controversial psychiatric category describing a mad person unable to know his or her madness. Like “moral insanity” and other concepts before it, impaired insight offers a way to link the disparate logics of human responsibility in psychiatry and the law. I attribute its development to changes wrought by deinstitutionalization, the rise of antipsychotic medication, and patient incarceration in penal settings. In a system that aims to govern psychiatric patients through their freedom, the logic of (...) impaired insight introduces a wrinkle: can a person make an informed choice to refuse treatment if madness itself impairs awareness of illness? Drawing on tools from the sociology of science, I trace the process by which researchers recast psychodynamic “denial” as a neurological and therefore non-volitional “impairment” in the 1990s. I then show how social movement actors mobilized the materialized form in the legal and policy fields in the 2000s, bringing insight science to bear upon the very questions of custodial management and patient rights that gave birth to it. At stake is this dilemma: how can societies that simultaneously privilege individual responsibility and somatic accounts of behavior govern those at the border of legal capacity, and with what justification? (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.

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)

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.

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)