This paper investigates the following question: when can one reliably infer the existence of an intersection point from a diagram presenting crossing curves or lines? Two cases are considered, one from Euclid's geometry and the other from basic real analysis. I argue for the acceptability of such an inference in the geometric case but against in the analytic case. Though this question is somewhat specific, the investigation is intended to contribute to the more general question of the extent and limits (...) of reliable diagrammatic reasoning in mathematics. (shrink)

The aim of this article is to investigate the roles of commutative diagrams (CDs) in a specific mathematical domain, and to unveil the reasons underlying their effectiveness as a mathematical notation; this will be done through a case study. It will be shown that CDs do not depict spatial relations, but represent mathematical structures. CDs will be interpreted as a hybrid notation that goes beyond the traditional bipartition of mathematical representations into diagrammatic and linguistic. It will be argued that one (...) of the reasons why CDs form a good notation is that they are highly mathematically tractable: experts can obtain valid results by ‘calculating’ with CDs. These calculations, take the form of ‘diagram chases’. In order to draw inferences, experts move algebraic elements around the diagrams. It will be argued that these diagrams are dynamic. It is thanks to their dynamicity that CDs can externalize the relevant reasoning and allow experts to draw conclusions directly by manipulating them. Lastly, it will be shown that CDs play essential roles in the context of proof as well as in other phases of the mathematical enterprise, such as discovery and conjecture formation. (shrink)

A noticeable shift in focus has occurred in public discourse from What is our best course of action? to What are the true facts of the situation? At the center of these debates are questions on the proper use of evidence, Legal scholar Schauer offers clarity based on how legal systems grapple with these questions-and by drawing insights from psychology, philosophy, economics, history, and decision theory.

College students struggle with the switch from thinking of mathematics as a calculation based subject to a problem solving based subject. This book describes how the introduction to proofs course can be taught in a way that gently introduces students to this new way of thinking. This introduction utilizes recent research in neuroscience regarding how the brain learns best. Rather than jumping right into proofs, students are first taught how to change their mindset about learning, how to (...) persevere through difficult problems, how to work successfully in a group, and how to reflect on their learning. With these tools in place, students then learn logic and problem solving as a further foundation. Next various proof techniques such as direct proofs, proof by contraposition, proof by contradiction, and mathematical induction are introduced. These proof techniques are introduced using the context of number theory. The last chapter uses Calculus as a way for students to apply the proof techniques they have learned. (shrink)

The “erasing race” effect is the reduction of the salience of “race” as an alliance cue when recalling coalition membership, once more accurate information about coalition structure is presented. We conducted a random-effects model meta-analysis of this effect using five United States studies (containing nine independent effect sizes). The effect was found (ρ = 0.137, K = 9, 95% CI = 0.085 to 0.188). However, no decline effect or moderation effects were found (a “decline effect” in this context would be (...) a decrease in the effect size over time). Furthermore, we found little evidence of publication bias. Synthetically correcting the effect size for bias stemming from the use of an older method for calculating error base rates reduced the magnitude of the effect, but the it remained significant. Taken together, these findings indicate that the “erasing race” effect generalizes quite well across experimental contexts and would, therefore, appear to be quite robust. We reinterpret the theoretical basis for these effects in line with Brunswikian evolutionary-developmental theory and present a series of predictions to guide future research in this area. (shrink)

I criticize a recent paper by Thomas Tymoczko in which he attributes fundamental philosophical significance and novelty to the lately-published computer-assisted proof of the four color theorem (4CT). Using reasoning precisely analogous to that employed by Tymoczko, I argue that much of traditional mathematical proof must be seen as resting on what Tymoczko must take as being "empirical" evidence. The new proof of the 4CT, with its use of what Tymoczko calls "empirical" evidence is therefore not so novel as he (...) maintains. Finally, without attempting to give a full account of the notion of empirical mathematical evidence, I sketch a view showing how the use of calculation injects an empirical ingredient into proof. (shrink)

In this paper, I present an interpretation of the use of constructions in both the problems and theorems of Elements I–VI, in light of the concept of given as developed in the Data, that makes a distinction between the way that constructions are used in problems, problem-constructions, and the way that they are used in theorems and in the proofs of problems, proof-constructions. I begin by showing that the general structure of a problem is slightly different from that stated (...) by Proclus in his commentary on the Elements. I then give a reading of all five postulates, Elem. I.post.1–5, in terms of the concept of given. This is followed by a detailed exhibition of the syntax of problem-constructions, which shows that these are not practical instructions for using a straightedge and compass, but rather demonstrations of the existence of an effective procedure for introducing geometric objects, which procedure is reducible to operations of the postulates but not directly stated in terms of the postulates. Finally, I argue that theorems and the proofs of problems employ a wider range of constructive and semi- and non-constructive assumptions that those made possible by problems. (shrink)

In this paper we prove some results about the complexity of proofs. We consider proofs in Hilbert-style formal systems such as in [17]. Thus a proof is a sequence offormulas satisfying certain conditions. We can view the formulas as being strings of symbols; hence the whole proof is a string too. We consider the following measures of complexity of proofs: length , depth and number of steps For a particular formal system and a given formula A we (...) consider the shortest length of a proof of A , the minimal depth of a proof of A and the minimal number of steps in a proof of A . The main results are the following: a bound on the depth in terms of the number of steps: Theorem 2.2, a bound on the depth in terms of the length: Theorem 2.3, a bound on the length in terms of the number of steps for restricted systems: Theorem 3.1. These results are applied to obtain several corollaries. In particular we show: a bound on the number of steps in a cut-free proof, some speed-up results, bounds on the number of steps in proofs of Paris-Harrington sentences. Some papers related to our research are listed in the references. We were especially influenced by Parikh's paper [17] on the famous conjecture of Kreisel . Many important problems in this field remain open. We hope that our paper will contribute to progress in this area. It should be noted that some results of this paper can be equally well obtained using unification theory , by translating a complexity-of-proof problem into a unification problem. A unification algorithm solving the unification problem can then be constructed and the complexity of the unification algorithm analyzed. As pointed out by the referee this method can be used to solve the problem stated in Section 3 for some non-simple schematic systems. (shrink)

In this paper we prove some results about the complexity of proofs. We consider proofs in Hilbert-style formal systems such as in [17]. Thus a proof is a sequence offormulas satisfying certain conditions. We can view the formulas as being strings of symbols; hence the whole proof is a string too. We consider the following measures of complexity of proofs: length , depth and number of steps For a particular formal system and a given formula A we (...) consider the shortest length of a proof of A , the minimal depth of a proof of A and the minimal number of steps in a proof of A . The main results are the following: a bound on the depth in terms of the number of steps: Theorem 2.2, a bound on the depth in terms of the length: Theorem 2.3, a bound on the length in terms of the number of steps for restricted systems: Theorem 3.1. These results are applied to obtain several corollaries. In particular we show: a bound on the number of steps in a cut-free proof, some speed-up results, bounds on the number of steps in proofs of Paris-Harrington sentences. Some papers related to our research are listed in the references. We were especially influenced by Parikh's paper [17] on the famous conjecture of Kreisel . Many important problems in this field remain open. We hope that our paper will contribute to progress in this area. It should be noted that some results of this paper can be equally well obtained using unification theory , by translating a complexity-of-proof problem into a unification problem. A unification algorithm solving the unification problem can then be constructed and the complexity of the unification algorithm analyzed. As pointed out by the referee this method can be used to solve the problem stated in Section 3 for some non-simple schematic systems. (shrink)

SummaryLooking at proof theory as an attempt to ‘code’ the general pattern of the logical steps of a mathematical proof, the question of what kind of rules can make the meaning of a logical connective completely explicit does not seem to have been answered satisfactorily. The lambda calculus seems to have been more coherent simply because the use of ‘λ’ together with its projection 'apply' is specified by what can be called a 'reduction' rule: β‐conversion. We attempt to analyse the (...) role of proof rules, making use of a set of formal rules designed to capture both the notions of proof theory and those of the lambda‐calculus: Martin‐Löf's Intuitionistic Type Theory.RésuméSi on considère la théorie de la démonstration comme une tentative de ‘codifier’ les pas logiques d'une démonstration mathématique, on se rendra compte qu'on n'a pas répondu de façon satisfaisante à la question suivante: quelles sont les règies qui rendent complètement explicite le sens d'un connecteur logique? Le lambda‐calcul a été apparemment plus cohérent, tout simplement parce que l'utilisation du‘λ’ avec sa projection 'apply' est spécifiée par une regie de 'réduction': β‐conversion. Nous essayons d'analyser le rôle des règies de démonstration, en utilisant un système formel de règies conçu pour englober à la fois les notions de la théorie de la démonstration et celles du lambda‐calcul: la Théorie Intuitionniste des Types de Martin‐Löf.ZusammenfassungWenn man Beweistheorie als einen Versuch, ein allgemeines Muster der logischen Schritte in einem mathematischen Beweis zu kodifizieren, betrachtet, so scheint die Frage nach der Art von Regeln , die die Bedeutung von logischen Operatoren vollständig beschreiben, nicht zufriedenstellend beantwortet. Der Lambda‐Kalkül erscheint, kohärenter, einfach deshalb weil der Gebrauch von ‘λ’ zusammen mit dessen Projektion 'apply' durch Regeln bestimmt wird, die man 'Reduktions'‐Regeln nennen kann: β‐Konversion. Wir versuchen, die Rolle von Beweisregeln zu analysieren, indem wir ein Regelsystem verwenden, das sowohl die Begriffe der Beweistheorie als auch diejenigen des Lambda‐Kalküls erfasst, nämlich die Martin‐Löfsche Typentheorie. (shrink)

Proof and Disproof in Formal Logic is a lively and entertaining introduction to formal logic providing an excellent insight into how a simple logic works. Formal logic allows you to check a logical claim without considering what the claim means. This highly abstracted idea is an essential and practical part of computer science. The idea of a formal system-a collection of rules and axioms, which define a universe of logical proofs-is what gives us programming languages and modern-day programming. This (...) book concentrates on using logic as a tool: making and using formal proofs and disproofs of particular logical claims. The logic it uses-natural deduction-is very small and very simple; working with it helps you see how large mathematical universes can be built on small foundations. The book is divided into four parts: Part I "Basics" gives an introduction to formal logic with a short history of logic and explanations of some technical words. Part II "Formal Syntactic Proof" show you how to do calculations in a formal system where you are guided by shapes and never need to think about meaning. Your experiments are aided by Jape, which can operate as both inquisitor and oracle. Part III "Formal Semantic Disproof" shows you how to construct mathematical counterexamples to shoe that proof is impossible. Jape can check the counterexamples you build. Part IV " Program Specification and Proof" describes how to apply your logical understanding to a real computer science problem, the accurate description and verification of programs. Jape helps, as far as arithmetic allows. Aimed at undergraduates and graduates in computer science, logic, mathematics and philosophy, the text includes reference to and exercises based on the computer software package Jape, an interactive teaching and research tool designed and hosted by the author that is freely available on the web. (shrink)

Dung’s argumentation frameworks are formalisms widely used to model interaction among arguments. Although their study has been profusely developed in the field of Artificial Intelligence, it is not common to see its treatment among those less connected to computer science within the logical-philosophical community. In this paper we propose to bring to that audience a proof-theory for argument justification based on tableaux, very similar to those the Logic students are familiar with. The tableaux enable to calculate whether an argument or (...) subset of arguments are accepted or rejected in accordance to Dung’s preferred and grounded extension-based semantics. Soundness and completeness results regarding those semantics are provided. (shrink)

This paper examines the relevance and importance of the large number of examples which Aristotle uses in his "Prior Analytics." In the first part of the paper three preliminary issues are raised: First, it investigates what counts as an example in Aristotle's syllogistic, and especially whether only examples expressed in concrete terms should be considered as examples or maybe also propositions and arguments with letters of the alphabet. The second issue concerns the kinds of examples Aristotle actually uses from everyday (...) life as well as from various scientific and philosophical forms of discourse; among these, it seems that biological examples, rather than mathematical ones, have a predominant place. Finally, I discuss what Aristotle himself has to say about the use of examples, and in particular about the similarity between the use of an example and the use of induction. The second part of the paper focusses on the functions of Aristotle's logical examples. It is of course obvious that some of the examples in the Prior Analytics are used to illustrate, and thus to clarify, a definition, a logical rule, a type of argument. However, I think that Aristotle's logical examples have another function, which is philosophically more interesting, namely as integral parts of the procedure of proving something. To support this claim, I analyse three passages from the "Prior Analytics" in which examples are used either in order to prove that something is not the case, i.e. as counter-examples, or in order to prove positively that it is possible for something to be the case. At the end, I argue that for such uses of examples Aristotle uses the notion of 'ekthesis', which seems to have a wider sense than usually suggested; that is to say, it is used to refer to any proof by means of an example, and not only for the procedure which Aristotle uses to reduce imperfect to perfect syllogisms. (shrink)

This paper examines the relevance and importance of the large number of examples which Aristotle uses in his "Prior Analytics." In the first part of the paper three preliminary issues are raised: First, it investigates what counts as an example in Aristotle's syllogistic, and especially whether only examples expressed in concrete terms should be considered as examples or maybe also propositions and arguments with letters of the alphabet. The second issue concerns the kinds of examples Aristotle actually uses from everyday (...) life as well as from various scientific and philosophical forms of discourse; among these, it seems that biological examples, rather than mathematical ones, have a predominant place. Finally, I discuss what Aristotle himself has to say about the use of examples, and in particular about the similarity between the use of an example and the use of induction. The second part of the paper focusses on the functions of Aristotle's logical examples. It is of course obvious that some of the examples in the Prior Analytics are used to illustrate, and thus to clarify, a definition, a logical rule, a type of argument. However, I think that Aristotle's logical examples have another function, which is philosophically more interesting, namely as integral parts of the procedure of proving something. To support this claim, I analyse three passages from the "Prior Analytics" in which examples are used either in order to prove that something is not the case, i.e. as counter-examples, or in order to prove positively that it is possible for something to be the case. At the end, I argue that for such uses of examples Aristotle uses the notion of 'ekthesis', which seems to have a wider sense than usually suggested; that is to say, it is used to refer to any proof by means of an example, and not only for the procedure which Aristotle uses to reduce imperfect to perfect syllogisms. (shrink)

Stephen Toulmin once observed that ”it has never been customary for philosophers to pay much attention to the rhetoric of mathematical debate’ [Toulmin et al., 1979, An Introduction to Reasoning, Macmillan, London, p. 89]. Might the application of Toulmin’s layout of arguments to mathematics remedy this oversight? Toulmin’s critics fault the layout as requiring so much abstraction as to permit incompatible reconstructions. Mathematical proofs may indeed be represented by fundamentally distinct layouts. However, cases of genuine conflict characteristically reflect an (...) underlying disagreement about the nature of the proof in question. (shrink)

Case-cohort design is a biased sampling method. Due to its cost-effective and theoretical significance, this design has extensive application value in many large cohort studies. The case-cohort data includes a subcohort sampled randomly from the entire cohort and all the failed subjects outside the subcohort. In this paper, the adjustment for the distorted covariates is considered to case-cohort data in Cox’s model. According to the existing adjustable methods of distorted covariates for linear and nonlinear models, we propose estimating the distorting (...) functions by nonparametrically regressing the distorted covariates on the distorting factors; then, the estimators for the parameters are obtained using the estimated covariates. The proof of consistency and being asymptotically normal is completed. For calculating the maximum likelihood estimates of the regression coefficients subject in Cox’s model, a minorization-maximization algorithm is developed. Simulation studies are performed to compare the estimations with the covariates undistorted, distorted, and adjusted to illustrate the proposed methods. (shrink)

The increased use of information technology in every day health care creates vast amounts of stored health data that can be used for research. The secondary research use of routinely collected data raises questions about appropriate consent mechanisms for such use. One option is meta consent where individuals state their own consent preferences in relation to future use of their data, e.g. whether they want the data to be accessible to researchers under conditions of specific consent, broad consent, blanket consent (...) or not at all. This study investigates whether meta consent preferences can be successfully elicited by a smartphone application in the adult Danish population. A smartphone app was developed for the elicitation of meta consent preferences. An invitation to use the app was distributed to a stratified, representative sample of the Danish adult population. The meta consent choices, the use of the app, user experience data, and demographic data were logged and analysed statistically using IBM SPSS version 20. Of 1000 potential respondents 221 used the app. One hundred eighty-eight of the respondents were female and 103 male. The age range was 19 to 79 years with an average of 51 years. Most users indicate 1) that they find the choices they are asked to make easy to understand, 2) that the application is easy to use, and 3) that this kind of choice should be offered to people. It is possible to collect meta consent preferences in the general, adult population using a smartphone app. (shrink)

The Born’s rule to interpret the square of wave function as the probability to get a specific value in measurement has been accepted as a postulate in foundations of quantum mechanics. Although there have been so many attempts at deriving this rule theoretically using different approaches such as frequency operator approach, many-world theory, Bayesian probability and envariance, literature shows that arguments in each of these methods are circular. In view of absence of a convincing theoretical proof, recently some researchers have (...) carried out experiments to validate the rule up-to maximum possible accuracy using multi-order interference (Sinha et al, Science, 329, 418 [2010]). But, a convincing analytical proof of Born’s rule will make us understand the basic process responsible for exact square dependency of probability on wave function. In this paper, by generalizing the method of calculating probability in common experience into quantum mechanics, we prove the Born’s rule for statistical interpretation of wave function. (shrink)

Background: Clinical tests for detecting central and peripheral shoulder fatigue are limited. The discrimination of these two types of fatigue is necessary to better adapt recovery intervention. The Kinematic Theory of Rapid Human Movements describes the neuromotor impulse response using lognormal functions and has many applications in pathology detection. The ideal motor control is modeled and a change in the neuromuscular system is reflected in parameters extracted according to this theory. Objective: The objective of this study was to assess whether (...) a shoulder neuromuscular fatigue could be detected through parameters describing the theory, if there is the possibility to discriminate central from peripheral fatigue, and which handwriting test gives the most relevant information on fatigue. Methods: Twenty healthy participants performed two sessions of fast stroke handwriting on a tablet, before and after a shoulder fatigue. The fatigue was in internal rotation for one session and in external rotation during the other session. The drawings consisted of simple strokes, triangles, horizontal and vertical oscillations. Parameters of these strokes were extracted according to the Sigma-Lognormal model of the Kinematic Theory. The evolution of each participant was analyzed through a U-Mann-Whitney test for individual comparisons. A Hotelling’s T² test and a U-Mann-Whitney test were also performed on all participants to assess the group evolution after fatigue. Moreover, a correlation among parameters was calculated through Spearman coefficients to assess intrinsic parameters properties of each handwriting test. Results: Central and peripheral parameters were statistically different before and after fatigue with a possibility to discriminate them. Participants had various responses to fatigue. However, when considering the group, parameters related to the motor program execution showed significant increase in the handwriting tests after shoulder fatigue. The test of simple strokes permits to know more specifically where the fatigue comes from, whereas the oscillations tests were the most sensitive to fatigue. Conclusion: The results of this study suggest that the Sigma-Lognormal model of the Kinematic Theory is an innovative approach for fatigue detection with discrimination between the central and peripheral systems. Overall, there is a possibility to implement the setting for clinics and sports personalized follow-up. (shrink)

This paper explores the relationship between informal reasoning, creativity in mathematics, and problem solving. It underscores the importance of environments that promote interaction, hypothesis generation, examination, refutation, derivation of new solutions, drawing conclusions, and reasoning with others, as key factors in enhancing mathematical creativity. Drawing on argumentation logic, the paper proposes a novel approach to uncover specific characteristics in the development of formalized proving using “proof-events.” Argumentation logic can offer reasoning mechanisms that facilitate these environments. This paper proposes how argumentation (...) can be implemented to discover certain characteristics in the development of formalized proving with “proof-events”. The concept of a proof-event was introduced by Goguen who described mathematical proof as a multi-agent social event involving not only “classical” formal proofs, but also other informal proving actions such as deficient or alleged proofs. Argumentation is an integral component of the discovery process for a mathematical proof since a proof necessitates a dialogue between provers and interpreters to clarify and resolve gaps or assumptions. By formalizing proof-events through argumentation, this paper demonstrates how informal reasoning and conflicts arising during the proving process can be effectively simulated. The paper presents an extended version of the proof-events calculus, rooted in argumentation theories, and highlights the intricate relationships among proof, human reasoning, cognitive processes, creativity, and mathematical arguments. (shrink)

The aim of this article is to present and discuss the language of the «givens», a typical stylistic resource of Greek mathematics and one of the major features of the proof format of analysis and synthesis. I shall analyze its expressive function and its peculiarities, as well as its general role as a deductive tool, explaining at the same time its particular applications in subgenres of a geometrical proposition like the locus theorems and the so-called «porisms». The main interpretative theses (...) of this study are the following: the language of the «givens» (1) is the standard idiom in which “existence and uniqueness” of a mathematical object was proved, (2) was conceived as an unified framework reducing to a strictly deductive format disparate argumentative steps such as deductions, constructions, and calculations. (shrink)

The topic of identity of proofs was put on the agenda of general (or structural) proof theory at an early stage. The relevant question is: When are the differences between two distinct proofs (understood as linguistic entities, proof figures) of one and the same formula so inessential that it is justified to identify the two proofs? The paper addresses another question: When are the differences between two distinct formulas so inessential that these formulas admit of identical (...) class='Hi'>proofs? The question appears to be especially natural if the idea of working with more than one kind of derivations is taken seriously. If a distinction is drawn between proofs and disproofs (or refutations) as primitive entities, it is quite conceivable that a proof of one formula amounts to a disproof of another formula, and vice versa. A notion of inherited identity of derivations is introduced for derivations in a cut-free sequent system for Almukdad and Nelson’s constructive paraconsistent logic N4 with strong negation. The notion is obtained by identifying sequent rules the application of which has no effect on the identity of derivations. Then the notion of inherited identity is used to define a bilateralist notion of synonymy between formulas, which is a relation drawing more fine-grained distinctions between formulas than strong equivalence. (shrink)

In criminal trials the state must establish, to a particular standard of proof, the defendant's guilt. The most widely used and important standard of proof for criminal conviction is the ‘beyond a reasonable doubt' standard. But what legitimates this standard, rather than an alternative? One view holds the standard of proof should be determined or justified – at least in large part – by its consequences. In this spirit, Laudan uses crime statistics to estimate risks the average citizen runs of (...) being violently victimised and falsely convicted. He argues that since the former risk is higher, and the aggregate harms are worse, the standard of proof should be substantially lowered. He presents a formula for calculating the preferred standard. In this article I outline various ways Laudan's uses of crime statistics are flawed, and explain how he substantially overestimates risks of victimhood and underestimates costs of false convictions. I also explain why his formula is mistaken, and illuminate consequences Laudan neglects. I conclude that, even if consequences determine the appropriate standard of proof, Laudan's arguments fail to show the standard is too high. I conclude by suggesting that the inadequacies of Laudan's reasoning might be good news for consequence-based justifications of the standard of proof. (shrink)

When physical structures resonate in proximity to each other they will under certain circumstances 'sync up' in a shared resonance frequency. This is the phenomenon of spontaneous selforganization. General resonance theory (GRT), a theory of consciousness developed by Hunt and Schooler, suggests that consciousness is a product of various shared resonance frequencies at different physical scales. I suggest a heuristic for calculating the boundaries and resulting capacity for phenomenal consciousness in such resonating structures. Shared resonance results in phase transitions in (...) the speed and bandwidth of information exchange and thus richer and more complex consciousness. This approach is a solution to the 'combination problem' and 'boundary problem' of consciousness. The proposed mathematical heuristic is a practical approach for identifying potential conscious structures and the spatial and temporal boundaries of such structures over time, and also for calculating the capacity for phenomenal consciousness of any putative conscious entity. The slowest-frequency shared resonance -- the 'slowest common denominator'-- is the limiting factor for the spatial extent of any macro-consciousness. Various synchrony indexes are discussed. I describe some limitations of the proposed framework, and how it compares to Tononi's integrated information theory. IIT's constellation- qualia characterization framework is compatible with GRT and may be a useful tool in conjunction with GRT's quantification framework. (shrink)

We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus \(\mathtt{SC2Int}\) for the bi-intuitionistic logic \(\mathtt{2Int}\). A distinctive feature of \(\mathtt{SC2Int}\) is that it makes use of two kind of sequents, one representing proofs, the other representing refutations. The structural rules of \(\mathtt{SC2Int}\), in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, (...) mediated through two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of \(\mathtt{2Int}\). By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in \(\mathtt{SC2Int}\) is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously. (shrink)

ArgumentThe British Astronomer Royal, Nevil Maskelyne, spent four months on a Scottish mountainside in 1774, making observations of zenith stars and coordinating a detailed survey of the size and shape of the mountain Schiehallion, in order to demonstrate and quantify what was known as “the attraction of mountains.” His endeavors were celebrated in London, where it was stated that he had given proof of the universality of Newtonian gravitation and allowed for a calculation of the relative densities of the (...) earth as a whole and the earth near its surface. This paper argues that the “Schiehallion Experiment” was as much a trial of the precision of Maskelyne's instruments and their expert management as it was a trial of Newtonian theory. By tracing the biography of the key instrument used by Maskelyne, his zenith sector, we see how much personal credibility was a stake for him in Scotland. By considering the mountainside as a place to test and reveal the precision of astronomical instruments we see a link between the Scottish endeavors and Maskelyne's ambitions for the Greenwich Observatory. (shrink)

The science of operations research is one of the modern sciences that have made a great revolution in all areas of life through the methods provided by it, suitable and appropriate to solve most of the problems that were facing researchers, scholars and those interested in the development of societies, and the most beneficiaries of this science were companies and institutions that are looking for scientific methods that help them manage their work so that they achieve the greatest profit and (...) the lowest cost, and one of the important methods that have been used in the management of companies we offer in this research two methods, Dynamic programming method. This method has been used in many practical matters and helped decision-makers in companies to achieve a maximum profit and less cost by formulating the reality of the state of the company and the data provided by decision-makers with a dynamic mathematical model that is solved using methods of solving dynamic models and we will provide in this research an example of this through the issue of choosing the optimal investment for the budget of a company so that it achieves a maximum profit, and the method of programming with integers: the method that provided these companies with solutions with integer values suitable for the nature of its work, through the use of the binary integer in the formulation of the appropriate mathematical model on the one hand, and on the other hand, the use of the binary integer variable helped to convert some nonlinear models that lead to some practical problems into linear models, and it should be noted here that in the previous two methods there is something indeterminable because we must make a decision in choosing or not choosing something, but the optimal solution that we will get remains A specific value because we are building the mathematical model for any realistic issue through the data provided by those responsible for the work and these data are calculated quantities and therefore they are uncertain values because their validity depends on the circumstances surrounding the work environment, they may be exposed to increase or decrease, and therefore the optimal solution on which the company will base its decision is suitable for specific values and any change in them can cause the company an uncalculated loss, so in this research we will use the concepts of neutrosophic science, the branch of science founded by the American scientist Florentin Smarandache in 1995 based on his belief that there is no absolute truth, a science that is interested in the study of ideas and concepts that are neither true nor false, but just in between, and we will take the data (calculated quantities) neutrosophic values that are specified or unspecified values are any set close to the calculated quantities, then the resulting mathematical model is a neutrosophic model and the optimal solution has neutrosophic values and thanks to the indefinite uncertainty that these values have, companies from the development of appropriate plans for all circumstances and thus achieve the greatest profit and the lowest cost, and we will clarify the above through two issues, the issue of optimal designation of a warehouse site, which we will formulate the mathematical model of using the neutrosophic integer programming method - and the issue of capital budget, which we will present in two different forms, we use in the first form the neutrosophic integer programming method and in the second the neutrosophic dynamic programming method. (shrink)

To solve the probability problem of the Many Worlds Interpretation of Quantum Mechanics, D. Wallace has presented a formal proof of the Born rule via decision theory, as proposed by D. Deutsch. The idea is to get subjective probabilities from rational decisions related to quantum measurements, showing the non-probabilistic parts of the quantum formalism, plus some rational constraints, ensure the squared modulus of quantum amplitudes play the role of such probabilities. We provide a new presentation of Wallace’s proof, reorganized to (...) simplify some arguments, and analyze it from a formal perspective. Similarities with classical decision theory are made explicit, to clarify its structure and main ideas. A simpler notation is used, and details are filled in, making it easier to follow and verify. Some problems have been identified, and we suggest possible corrections. (shrink)

As recent studies in economic and financial sociology have underscored, calculation is central to economic practices. While some sociological accounts locate the performance of calculation within individual ability, networks of human agents or their cultural embeddedness, studies operating on the background of the sociology of (scientific) knowledge conceive of calculation as situated in the practice of the participants engaged, the technological tools used and their requirements. The article explores this point further, using a distinction which can be (...) traced back to Heidegger’s notion of Gestell (enframing): the ‘calculation of something’ and the ‘calculation with something’ are analysed taking the practices of risk management departments of big international banks as an example. It is argued that, through the use of calculation tools, the corporate clients are constituted anew and that written documents which are the outcome of this process constitute a social prosthesis for remote communication taking place between subsidiaries and the headquarters of international banks. (shrink)

When considering controversial thermodynamic scenarios such as Maxwell's demon, it is often necessary to consider probabilistic mixtures of states. This raises the question of how, if at all, to assign entropy to them. The information-theoretic entropy is often used in such cases; however, no general proof of the soundness of doing so has been given, and indeed some arguments against doing so have been presented. We offer a general proof of the applicability of the information-theoretic entropy to probabilistic mixtures of (...) macrostates, making clear the assumptions on which it depends, in particular a probabilistic version of the Kelvin statement of the Second Law. We briefly discuss the interpretation of our result. (shrink)

At some step in proving the Liar Paradox in natural language, a sentence is derived that seems overdetermined with respect to its semantic value. This is complemented by Tarski’s Theorem that a formal language cannot consistently contain a naive truth predicate given the laws of logic used in proving the Liar paradox. I argue that proofs of the Eubulidean Liar either use a principle of truth with non-canonical names in a fallacious way or make a fallacious use of substitution (...) of identicals. Tarski never committed the first fallacy and may have himself considered it fallacious. Nevertheless, I clarify that it is fallacious. I then argue substitution of identicals needs to be restricted within the scope of the truth predicate. A logic for truth implementing this restriction is a monotonic extension of a classical first order logic, or indeed a formalizable fragment of natural language. Proofs of Tarski’s Indefinability of Truth theorem are invalid in this logic. This approach generalizes to invalidate proofs of Liar-like paradoxes, particularly the predicate form of the Knower paradox. Consequently, such a logic can be further extended in a way that avoids Montague’s theorem for such a system. Yet, the semantic status of a Liar sentence is not fully resolved. It is no longer overdetermined; it is now underdetermined. (shrink)

The paper suggests a revision of the notion of harmony, a major necessary condition in proof-theoretic semantics for a natural-deduction proof-system to qualify as meaning conferring, when moving to a bilateral proof-system. The latter considers both forces of assertion and denial as primitive, and is applied here to positive logics, lacking negation altogether. It is suggested that in addition to the balance between (positive) introduction and elimination rules traditionally imposed by harmony, a balance should be imposed also on: (i) negative (...) introduction and elimination rules, and (ii) positive and negative introduction rules. The paper suggests a proof-theoretical definition of duality (not referring to truthtables), using which double harmony is defined. The paper proves that in a doubly-harmonious system, the coordination rule, typical to bilateral systems, is admissible. (shrink)

Having analyzed the formal aspects of Wallace’s proof of the Born rule, we now discuss the concepts and axioms upon which it is built. Justification for most axioms is shown to be problematic, and at times contradictory. Some of the problems are caused by ambiguities in the concepts used. We conclude the axioms are not reasonable enough to be taken as mandates of rationality in Everettian Quantum Mechanics. This invalidates the interpretation of Wallace’s result as meaning it would be rational (...) for Everettian agents to decide using the Born rule. (shrink)

We investigated whether mathematicians typically agree about the qualities of mathematical proofs. Between-mathematician consensus in proof appraisals is an implicit assumption of many arguments made by philosophers of mathematics, but to our knowledge the issue has not previously been empirically investigated. We asked a group of mathematicians to assess a specific proof on four dimensions, using the framework identified by Inglis and Aberdein (2015). We found widespread disagreement between our participants about the aesthetics, intricacy, precision and utility of the (...) proof, suggesting that a priori assumptions about the consistency of mathematical proof appraisals are unreasonable. (shrink)

The paper suggests a revision of the notion of harmony, a major necessary condition in proof-theoretic semantics for a natural-deduction proof-system to qualify as meaning conferring, when moving to a bilateral proof-system. The latter considers both forces of assertion and denial as primitive, and is applied here to positive logics, lacking negation altogether. It is suggested that in addition to the balance between introduction and elimination rules traditionally imposed by harmony, a balance should be imposed also on: negative introduction and (...) elimination rules, and positive and negative introduction rules. The paper suggests a proof-theoretical definition of duality, using which double harmony is defined. The paper proves that in a doubly-harmonious system, the coordination rule, typical to bilateral systems, is admissible. (shrink)

This paper analyses the hidden use of new axioms in set-theoretic practice with a focus on large cardinal axioms and presents a general overview of set-theoretic practices using large cardinal axioms. The hidden use of a new axiom provides extrinsic reasons in support of this axiom via the idea of verifiable consequences, which is especially relevant for set-theoretic practitioners with an absolutist view. Besides that, the hidden use has pragmatic significance for further important sub-groups of the set-theoretic community---set-theoretic practitioners with (...) a pluralist view and set-theoretic practitioners who aim for ZFC-proofs. By describing this, the paper gives a more complete picture of new axioms in set-theoretic practice. These observations, for instance, show that set-theoretic practitioners interested in ZFC-proofs use tools that go beyond ZFC. The analysis is based on empirical data that was collected in an extensive interview study with set-theoretic practitioners. (shrink)

Jullien's indecomposability theorem (INDEC) states that if a scattered countable linear order is indecomposable, then it is either indecomposable to the left, or indecomposable to the right. The theorem was shown by Montalbán to be a theorem of hyperarithmetic analysis, and then, in the base system RCA₀ plus ${\mathrm{\Sigma }}_{1}^{1}\text{\hspace{0.17em}}$ induction, it was shown by Neeman to have strength strictly between weak ${\mathrm{\Sigma }}_{1}^{1}$ choice and ${\mathrm{\Delta }}_{1}^{1}$ comprehension. We prove in this paper that ${\mathrm{\Sigma }}_{1}^{1}$ induction is needed for (...) the reversal of INDEC, that is for the proof that INDEC implies weak ${\mathrm{\Sigma }}_{1}^{1}$ choice. This is in contrast with the typical situation in reverse mathematics, where reversals can usually be refined to use only ${\mathrm{\Sigma }}_{1}^{0}$ induction. (shrink)

The “beyond a reasonable doubt” standard of proof, currently used in criminal trials, is notoriously vague and undermotivated. This paper discusses two popular strategies for justifying our choice of a particular precise interpretation of the standard: the “ratio-to-standard strategy” identifies a desired ratio of trial outcomes and then argues that a certain standard is the one that we can expect to produce our desired ratio, while the “utilities-to-standard strategy” identifies utilities for trial outcomes and then argues that a certain standard (...) maximizes expected utility. I argue that both strategies fail on their own terms, by requiring us to perform calculations that we simply cannot perform. No version of either strategy can be performed by jurors or legislators in our actual epistemic position, in which, since we do not know which of the defendants in our trial system are genuinely innocent and which are genuinely guilty, we cannot determine the extent to which our trial system tends to produce evidence that misleadingly incriminates the innocent or misleadingly exonerates the guilty. But we would need to determine this in order to perform the calculations required by any possible version of the ratio-to-standard or utilities-to-standard strategies. I then suggest some empirical reasons to be pessimistic about the evidence produced by our actual trial system. The upshot is that the “beyond a reasonable doubt” standard lacks a clear interpretation and rationale, nor do we have a promising way to identify an alternative. This is the trouble with standards of proof. (shrink)

At the turn of the nineteenth century, mathematics exhibited a style of argumentation that was more explicitly computational than is common today. Over the course of the century, the introduction of abstract algebraic methods helped unify developments in analysis, number theory, geometry, and the theory of equations; and work by mathematicians like Dedekind, Cantor, and Hilbert towards the end of the century introduced set-theoretic language and infinitary methods that served to downplay or suppress computational content. This shift in emphasis away (...) from calculation gave rise to concerns as to whether such methods were meaningful, or appropriate to mathematics. The discovery of paradoxes stemming from overly naive use of set-theoretic language and methods led to even more pressing concerns as to whether the modern methods were even consistent. This led to heated debates in the early twentieth century and what is sometimes called the “crisis of foundations.” In lectures presented in 1922, David Hilbert launched his Beweistheorie, or Proof Theory, which aimed to justify the use of modern methods and settle the problem of foundations once and for all. This, Hilbert argued, could be achieved as follows. (shrink)

This paper discusses critically what simulation models of the evolution ofcooperation can possibly prove by examining Axelrod’s “Evolution of Cooperation” and the modeling tradition it has inspired. Hardly any of the many simulation models of the evolution of cooperation in this tradition have been applicable empirically. Axelrod’s role model suggested a research design that seemingly allowed to draw general conclusions from simulation models even if the mechanisms that drive the simulation could not be identified empirically. But this research design was (...) fundamentally flawed, because it is not possible to draw general empirical conclusions from theoretical simulations. At best such simulations can claim to prove logical possibilities, i.e. they prove that certain phenomena are possible as the consequence of the modeling assumptions built into the simulation, but not that they are possible or can be expected to occur in reality I suggest several requirements under which proofs of logical possibilities can nevertheless be considered useful. Sadly, most Axelrod-style simulations do not meet these requirements. I contrast this with Schelling’s neighborhood segregation model, thecore mechanism of which can be retraced empirically. (shrink)

The use of figurate numbers (e. g. in the context of elementary number theory) can be considered a heuristic in the field of problem solving or proving. In this paper, we want to discuss this heuristic from the perspectives of the semiotic theory of Peirce (“diagrammatic reasoning” and “collateral knowledge”) and cognitive psychology (“schema theory” and “Gestalt psychology”). We will make use of several results taken from our research to illustrate first-year students’ problems when dealing with figurate numbers in the (...) context of proving. The considerations taken from both theoretical perspectives will help to partly explain such phenomena. It will be shown that the use of figurate numbers must not be considered to be any kind of help for learners or some way of ‘easy’ mathematics. Working in this representational system has to be learned and practiced as another kind of knowledge is necessary for working with figurate numbers. The named findings also touch upon the concept of ‘proofs that explain’. Finally, we will highlight some implications for teaching and point to a number of demands for future research. (shrink)

According to the deductivist view of mathematics which became the rule during the nineteenth century, formal proofs working with symbolic formulas replaced the intuitive knowledge that used to be gained by the step-by-step construction of geometric fgures and diagrams. Twentieth century epistemological refection on symbolic formulas and formal proofs, however, took them to be diagrams respectively exhibiting formal relations and transformations. The claim was also made that, for such diagrams to be proofs, temporal displays of transformations—and of (...) other speech acts—were required. By returning to the signifcant elements of contemporary theories of mathematical proofs, we will here show how these proofs came to be a matter for semiotics and pragmatics as much as for formal logic. Once this is done, we will provide a few arguments against the standard objections to the ability of diagrams to present temporal order or perform speech acts. (shrink)

Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects (...) of forcing that are useful in this respect, and some sample applications. The latter include ways of obtaining conservation results for classical and intuitionistic theories, interpreting classical theories in constructive ones, and constructivizing model-theoretic arguments. (shrink)

Proof-theoretic validity has proven a useful tool for proof-theoretic semantics, because it explains the harmony found in the introduction and elimination rules for the intuitionistic calculus. However, the demonstration that a rule of proof is proof-theoretically valid requires checking an infinite number of cases, which raises the question of whether proof-theoretic validity is decidable. It is proven here that it is for the most prominent formulations in the literature for propositional logic.

This paper discusses critically what simulation models of the evolution of cooperation can possibly prove by examining Axelrod’s “Evolution of Cooperation” (1984) and the modeling tradition it has inspired. Hardly any of the many simulation models in this tradition have been applicable empirically. Axelrod’s role model suggested a research design that seemingly allowed to draw general conclusions from simulation models even if the mechanisms that drive the simulation could not be identified empirically. But this research design was fundamentally flawed. At (...) best such simulations can claim to prove logical possibilities, i.e. they prove that certain phenomena are possible as the consequence of the modeling assumptions built into the simulation, but not that they are possible or can be expected to occur in reality. I suggest several requirements under which proofs of logical possibilities can nevertheless be considered useful. Sadly, most Axelrod-style simulations do not meet these requirements. It would be better not to use this kind of simulations at all. (shrink)

There is no topic that attracts more attention, more energy and time and devotion, than love. As long as there's been recorded history, love has taken center seat as the inspiration for countless paintings, instigator of wars, muse of untold poets and musicians. And just as poetry, art and music have the ability to communicate something about love that is difficult to articulate with words, the same is true of mathematics. Of course, mathematics can't easily help us translate the emotional (...) side of love, emotions rarely behave in a neatly ordered, rational and easily predictable way. It is difficult to quantify the rollercoaster of romance or to define how lovers might feel via a set of simple equations. But that doesn't mean that mathematics isn't crucial to understanding love. Love, like most things in life, is full of patterns. And mathematics is ultimately the study of patterns, from predicting the weather to the fluctuations of the stock market, the movement of planets or the growth of cities. These patterns twist and turn and warp and evolve just as the rituals of love do. In [this book, the author] takes the listener on a fascinating journey through the patterns that define our love lives, tackling some of the most common yet complex questions pertaining to love: What's the chance of us finding love? What's the chance that it will last? How does online dating work, exactly? When should you settle down? How can you avoid divorce? When is it right to compromise? Can game theory help us decide whether or not to call? From evaluating the best strategies for online dating to defining the nebulous concept of beauty, Dr. Fry proves, with great insight, wit and fun, that math is a surprisingly useful tool to negotiate the complicated, often baffling, sometimes infuriating, always interesting, patterns of love. (shrink)

The problem of Galileo's logical methodology has long interested scholars. In this volume William A. Wallace offers a solution that is completely unexpected, yet backed by convincing documentary evidence. His analysis starts with an early notebook Galileo wrote at Pisa, appropriating a Jesuit professor's exposition of the Posterior Analystics of Aristotle, and ends with one of the last letters Galileo wrote, stating that in logic he has been a Peripatetic all his life. Wallace's detective work unearths the complete logic course (...) from which the notebook was excerpted, then proceeds to show how its terminology and methodology continue to surface in Galileo's later writings in which he founds his new sciences of the heavens and of local motion. The result is a tour de force that commends itself not only to Galileo's scholars and to logicians, philosophers, and historians, but to anyone interested in the epistemic roots of modern science. (shrink)