Logic and Computation is concerned with techniques for formal theorem-proving, with particular reference to Cambridge LCF (Logic for Computable Functions). Cambridge LCF is a computer program for reasoning about computation. It combines methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of statements in a programming language. This book consists of two parts. Part I outlines the mathematical preliminaries: elementary logic and domain theory. They are explained at an intuitive level, giving references (...) to more advanced reading. Part II provides enough detail to serve as a reference manual for Cambridge LCF. It will also be a useful guide for implementors of other programs based on the LCF approach. (shrink)

Equational reasoning arises in many areas of mathematics and computer science. It is a cornerstone of algebraic reasoning and results essential in tasks of specification and verification in functional programming, where a program is mainly a set of equations. The usual manipulation of identities while conducting informal proofs obviates many intermediate steps that are neccesary while developing them using a formal system, such as the equationally complete Birkhoff calculus ${\mathcal{B}}$. This deductive system does not fit in the common manner of (...) doing mathematical proofs, and it is not compatible with the mechanisms of proof assistants. The aim of this work is to provide a deductive system ${\mathcal{B}}^{\textrm{GOAL}}$ for equality, equivalent to ${\mathcal{B}}$ but suitable for constructing equational proofs in a backward fashion. This feature makes it adequate for interactive proof-search in the approach of proof assistants. This will be achieved by turning ${\mathcal{B}}^{\textrm{GOAL}}$ into a transition system of formal tactics in the style of Edinburgh LCF, such transformation allows us to give a direct formal definition of backward proof in equational logic. (shrink)

In 1950, Alan Turing proposed his eponymous test based on indistinguishability of verbal behavior as a replacement for the question "Can machines think?" Since then, two mutually contradictory but well-founded attitudes towards the Turing Test have arisen in the philosophical literature. On the one hand is the attitude that has become philosophical conventional wisdom, viz., that the Turing Test is hopelessly flawed as a sufficient condition for intelligence, while on the other hand is the overwhelming sense that were a machine (...) to pass a real live full-fledged Turing Test, it would be a sign of nothing but our orneriness to deny it the attribution of intelligence. The arguments against the sufficiency of the Turing Test for determining intelligence rely on showing that some extra conditions are logically necessary for intelligence beyond the behavioral properties exhibited by an agent under a Turing Test. Therefore, it cannot follow logically from passing a Turing Test that the agent is intelligent. I argue that these extra conditions can be revealed by the Turing Test, so long as we allow a very slight weakening of the criterion from one of logical proof to one of statistical proof under weak realizability assumptions. The argument depends on the notion of interactive proof developed in theoretical computer science, along with some simple physical facts that constrain the information capacity of agents. Crucially, the weakening is so slight as to make no conceivable difference from a practical standpoint. Thus, the Gordian knot between the two opposing views of the sufficiency of the Turing Test can be cut. (shrink)

ABSTRACT This paper presents an attempt to create a shell for generic interactive proof search and proof assistant software based on it.

The notion of efficient proof-checking has always been central to complexity theory, and it gave rise to the definition of the class NP. In the last 15 years there has been a number of exciting, unexpected and deep developments in complexity theory that exploited the notion of randomized and interactive proof-checking. Results developed along this line of research have diverse and powerful applications in complexity theory, cryptography, and the theory of approximation algorithms for combinatorial optimization problems. In (...) this paper we survey the main lines of developments in interactive and probabilistic proof-checking, with an emphasis on open questions. (shrink)

Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics and computer science. The book contains a wealth of results on proof-theoretical systems, including extensions of such (...) systems from logic to mathematics, and on the connection between the two main forms of structural proof theory - natural deduction and sequent calculus. The authors emphasize the computational content of logical results. A special feature of the volume is a computerized system for developing proofs interactively, downloadable from the web and regularly updated. (shrink)

Driven by the question, 'What is the computational content of a (formal) proof?', this book studies fundamental interactions between proof theory and computability. It provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science. Part I covers basic proof theory, computability and Gödel's theorems. Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to Π11-CA0. Ordinal analysis and the (Schwichtenberg-Wainer) subrecursive hierarchies play a central (...) role and are used in proving the 'modified finite Ramsey' and 'extended Kruskal' independence results for PA and Π11-CA0. Part III develops the theoretical underpinnings of the first author's proof assistant MINLOG. Three chapters cover higher-type computability via information systems, a constructive theory TCF of computable functionals, realizability, Dialectica interpretation, computationally significant quantifiers and connectives and polytime complexity in a two-sorted, higher-type arithmetic with linear logic. (shrink)

In Prior Analytics 1.15 Aristotle undertakes to establish certain modal syllogisms of the form XQM. Although these syllogisms are central to his modal system, the proofs he offers for them are problematic. The precise structure of these proofs is disputed, and it is often thought that they are invalid. We propose an interpretation which resolves the main difficulties with them: the proofs are valid given a small number of intrinsically plausible assumptions, although they are in tension with some claims found (...) elsewhere in Aristotle’s modal syllogistic. The proofs make use of a rule of propositional modal logic which we call the possibility rule. We investigate how this rule interacts and coheres with the core elements of the modal syllogistic. (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)

The Many-Interacting-Worlds (MIW) approach to a quantum theory without wave functions proposed in [8] leads naturally to numerical integrators of the Schrödinger equation on comoving grids. As yet, little is known about concrete MIW models for more than one spatial dimension and/or more than one particle. In honour of Detlef Dürr, we report on a further development of the MIW approach to treat arbitrary degrees of freedom and provide a numerical proof of concept for ground states in 2d. The (...) latter is part of a systematic numerical study [22] that includes also 1d ground and excited states. With this step towards the treatment of higher degrees of freedom we hope to stimulate their further study. (shrink)

Proof, Computation and Agency: Logic at the Crossroads provides an overview of modern logic and its relationship with other disciplines. As a highlight, several articles pursue an inspiring paradigm called 'social software', which studies patterns of social interaction using techniques from logic and computer science. The book also demonstrates how logic can join forces with game theory and social choice theory. A second main line is the logic-language-cognition connection, where the articles collected here bring several fresh perspectives. Finally, the (...) book takes up Indian logic and its connections with epistemology and the philosophy of science, showing how these topics run naturally into each other. (shrink)

This paper explores the nature of mathematical beauty from a Kantian perspective. According to Kant’s Critique of the Power of Judgment, satisfaction in beauty is subjective and non-conceptual, yet a proof can be beautiful even though it relies on concepts. I propose that, much like art creation, the formulation and study of a complex demonstration involves multiple and progressive interactions between the freely original imagination and taste. Such a proof is artistic insofar as it is guided by beauty, (...) namely, the mere feeling about the imagination’s free lawfulness. The beauty in a proof’s process and the perfection in its completion together facilitate a transition from subjective to objective purposiveness, a transition that Kant himself does not address in the third Critique. (shrink)

In Prawitz’s semantics, the validity of an argument may be defined, either relatively to an atomic base which determines the meaning of the non-logical terminology, or relatively to the whole class of atomic bases, namely as logical validity. In the first case, which may be qualified as local, one has to choose whether validity of arguments is or not monotonic over expansions of bases, while in the second case, which may be qualified as global, one has to choose whether the (...) reduction functions which justify non-primitive inferences are or not base-depending. I claim that these oppositions enjoy some conceptual symmetries, and that these symmetries may be understood as putting restrictions on one’s choice both at the local and at the global level. This produces two different proof-theoretic semantics in line with Prawitz’s tenets. However, I also argue that the symmetries stem from a deeper interaction within Prawitz’s semantics, i.e. non-logical meanings vs interpretation of rules. This interaction is in turn based on some primitive ingredients which, when suitably combined, produce other two Prawitz-compatible readings. The four readings form a diagram where some order relations hold. I finally claim that this diagram is complete, namely that, if we combine the ingredients in ways other than those giving rise to the four readings above, we obtain nothing new, or nothing compatible with general semantic requirements. Thus, symmetries between the local and the global level, and interaction between non-logical meaning and interpretation of rules, produce a complete classification of potential Prawitzian semantics. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Feminist Studies 41, no. 3. © 2015 by Feminist Studies, Inc. 623 Jaye Cee Whitehead, Kath Bassett, Leia Franchini, and Michael Iacolucci “The Proof Is in the Pudding”: How Mental Health Practitioners View the Power of “Sex Hormones” in the Process of Transition In the United States today, popular discourse touts the power of “sex hormones” and hormone receptors in the brain to chemically produce gender expressions (manifested (...) in physical sex traits, behaviors, and attitudes) and identities (a sense of self as feminine or masculine). These accounts range from common assumptions that Western ideals of femininity (such as empathy understanding, cooperative orientation, nurturing behavior) and masculinity (rational/spatial understanding, competitive orientation, violent behavior) are produced by corresponding sex hormones, to studies that reduce complex gender identities and macrosocial economic phenomena to presocial, binary, hormonal processes.1 For sociologists, accounts that reduce complex identities to internal hormonal reactions are problematic for two primary reasons: first, they are inaccurate because they fail to examine how hormonal reactions are embedded in a complex cultural process of meaning and interpretation; second, they operate as bioreductive ideologies that obscure the social power inherent to the process of gender identity construction. In what follows, we extend both of these insights by examining mental health 1. For an example of a hybrid popular-scientific account of the power of sex hormones to destabilize economic structures, see Jon Coates and Joe Herbert, “Endogenous Steroids and Financial Risk Taking on a London Trading Floor,” Proceedings of the National Academy of Sciences 105, no. 16 (April 2008): 6167–72. 624 Whitehead, Bassett, Franchini, and Iacolucci practitioners’ divergent interpretations of the power of sex hormones in the process of gender transition.2 In doing so, we examine the cultural power of sex hormones in crafting gender identities without reproducing reductionist interpretations of trans embodiment. Perhaps what is most perplexing about the way we speak of sex hormones is that we know it is inaccurate to describe these hormones as sexed; scientists have acknowledged since the 1930s that they are neither sex specific in their function, nor in terms of their location in male or female bodies.3 In her extensive historicization of sex hormones, Anne Fausto-Sterling concludes that it is more accurate to call androgen- and estrogen-based hormones, “steroid hormones” as they have functions that are not confined to corresponding sexed bodies. In fact she urges scientists to “break out of the sex hormone straightjacket” and to look at steroids as just one of a number of components that are important to the creation of sex and gender, including environment and experience.4 Scholars also point to an inextricable link between the chemical operation of hormones and the social process of constructing meaning, both at the level of social interaction and macrocultural constructions of sex categories and gender ideologies.5 While brain organization/activation theory attributes sex and gender differences to hormonal interactions within the developing brain, Fausto-Sterling questions the distinction between activation and organization by pointing out how “the brain can respond to hormonal stimuli with anatomical changes…hormonal systems, after all, respond exquisitely to experience, be it in the form of nutrition, stress, or sexual activity (to name but a few possibilities ).”6 Drawing from Elizabeth Grosz, Fausto-Sterling argues that the power of hormones is best understood according to the model of the 2. “Gender transition” is a controversial phrase, as it implies that transgendered individuals who receive hormone therapy are changing identities. We are only using it for lack of clear alternative phrasing, not because we believe body modifications change gender identities. 3. See Anne Fausto-Sterling, Sexing the Body: Gender Politics and the Construction of Sexuality (New York: Basic Books, 2000); Rebecca Jordan-Young, Brainstorm: The Flaws in the Science of Sex Differences (Cambridge, MA: Harvard University Press, 2010); and Nelly Oudshoorn, Beyond the Natural Body: An Archeology of Sex Hormones (New York: Routledge, 1994). 4. Fausto-Sterling, Sexing the Body, 193–94. 5. Fausto-Sterling, Sexing the Body. 6. Ibid., 232. Whitehead, Bassett, Franchini, and Iacolucci 625 Möbius strip, wherein internal components of the self are always connected to and continuous with outer components such as culture and environment.7 In other... (shrink)

A modified Young double-slit experiment proposed by Wootters and Zurek is considered in which a system P of parallel plates covered with a photographic emulsion has been set up in the region where we would normally expect the central interference fringes. Because under certain conditions P makes it possible to conclude with much more than50% certainty through which of the two slits each particular photon passed, the relevant interference pattern becomes blurred. It is proved that this implies a retroactive effect (...) because the setup of P and the interaction of photons with P appear to influence the momentum transferred to the photons by the edges of the slits at an earlier stage of the experiment. (shrink)

This article generalises the refined A-translation method for extracting programs from classical proofs [U. Berger,W. Buchholz, H. Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114 3–25] to the scenario where additional assumptions such as choice principles are involved. In the case of choice principles, this is done by adding computational content to the ‘translated’ assumptions, an idea which goes back to [S. Berardi, M. Bezem, T. Coquand, On the computational content of the axiom of (...) choice, JSL 63 600–622] and has been further elaborated in [U. Berger, P. Oliva, Modified bar recursion and classical dependent choice, in: M. Baaz, S.D. Friedman, J. Kraijcek , Logic Colloquium ’01, in: Lecture Notes in Logic, vol. 20, Springer, Berlin, 2005, pp. 89–107]. We further investigate the applicability of this extension by means of a small but non-trivial example, and discuss the formalisation as well as some optimisations necessary in order to extract terminating programs. Both formalisation and term extraction have been implemented in the interactive proof assistant Minlog. (shrink)

This volume covers a wide range of topics in the most recent debates in the philosophy of mathematics, and is dedicated to how semantic, epistemological, ontological and logical issues interact in the attempt to give a satisfactory picture of mathematical knowledge. The essays collected here explore the semantic and epistemic problems raised by different kinds of mathematical objects, by their characterization in terms of axiomatic theories, and by the objectivity of both pure and applied mathematics. They investigate controversial aspects of (...) contemporary theories such as neo-logicist abstractionism, structuralism, or multiversism about sets, by discussing different conceptions of mathematical realism and rival relativistic views on the mathematical universe. They consider fundamental philosophical notions such as set, cardinal number, truth, ground, finiteness and infinity, examining how their informal conceptions can best be captured in formal theories. The philosophy of mathematics is an extremely lively field of inquiry, with extensive reaches in disciplines such as logic and philosophy of logic, semantics, ontology, epistemology, cognitive sciences, as well as history and philosophy of mathematics and science. By bringing together well-known scholars and younger researchers, the essays in this collection – prompted by the meetings of the Italian Network for the Philosophy of Mathematics (FilMat) – show how much valuable research is currently being pursued in this area, and how many roads ahead are still open for promising solutions to long-standing philosophical concerns. Promoted by the Italian Network for the Philosophy of Mathematics – FilMat. (shrink)

Public and professional debates have come to rely heavily on a special type of reasoning: the argument-from-ignorance, in which conclusions depend on the _lack_ of compelling information. "I win my argument," says the skillful advocate, "unless you can prove that I am wrong." This extraordinary gambit has been largely ignored in modern rhetorical and philosophical studies. Yet its broad force can be demonstrated by analogy with the modern legal system, where courts have long manipulated burdens of proof with skill (...) and subtlety. This legal, philosophical, and rhetorical study by Richard H. Gaskins provides the first systematic treatment of arguments-from-ignorance across a wide range of modern discourse—from constitutional law, scientific inquiry, and moral philosophy to organizational behavior, computer operation, and personal interaction. Gaskins reviews the historic shifts in constitutional proof burdens that have shaped public debate on fundamental rights and, by analogy, on the fundamental status of intellectual and cultural authority. He shows how similar shifts have dominated polemical battles between scientific and ethical modes of authority, affecting both academic and popular discussion. Finally, he discovers the philosophical roots of default reasoning strategies in the arguments of Kant and nineteenth-century Kantian schools. Concluding that shifting proof burdens are inescapable in a world of scientific and moral uncertainty, Gaskins emphasizes the common strategic ground shared by dogmatic and skeptical reasoning. Using Hegelian strategies, he describes a more pluralistic temper that can move critical thinking beyond polemics and strengthen our capacities for common discourse. (shrink)

First it is proved that, in a deterministic theory, Malus' law requires that, if a photon is successively transmitted by two polarizers with appropriately chosen settings, the first transmission influences a hidden variable (co-) determining the second one. We derive from this that in an ideal EPR experiment (giving the result predicted by quantum mechanics for two correlated photons transmitted by two polarizers with suitably chosen settings) there has to be a nonlocal influence from the “first” transmission interaction to the (...) second. Subsequently we argue that we can abandon determinism as an assumption so that the locality hypothesis is in any case untenable if the predictions of quantum mechanics are all correct. (shrink)

In this paper, I attempt a reconstruction of the theory of intersections in the geometry of Euclid. It has been well known, at least since the time of Pasch onward, that in the Elements there are no explicit principles governing the existence of the points of intersections between lines, so that in several propositions of Euclid the simple crossing of two lines (two circles, for instance) is regarded as the actual meeting of such lines, it being simply assumed that the (...) point of their intersection exists. Such assumptions are labelled, today, as implicit claims about the continuity of the lines, or about the continuity of the underlying space. Euclid’s proofs, therefore, would seem to have some demonstrative gaps that need to be filled by a set of continuity axioms (as we do, in fact, find in modern axiomatizations).I show that Euclid’s theory of intersections was not in fact based on any notion of continuity at all. This is not only because Greek concepts of continuity (such as the Aristotelian ones) were largely insufficient to ground a geometrical theory of intersections, but also, at a deeper level, because continuity was simply not regarded as a notion that had any role to play in the latter theory. Had Euclid been asked to explain why the points of intersections of lines and circles should exist, it would have never occurred to him to mention continuity in this connection. Ancient geometry was very different from ours, and it is only our modern views on continuity that tend to give rise to the expectation that this latter must be included in the foundations of elementary mathematics.We may hope to reconstruct Euclid’s views on intersections if we undertake a critical examination both of the extension and of the limits of ancient diagrammatic practices. This is tantamount to attempting to understand to what extent the existence of an intersection point may be inferred just from the inspection of a diagram, and in which cases we need rather to supplement such inference by propositional rules. This leads us to discuss Euclid’s definition of a point, and to work out the details of the complex interaction between diagrams and text in ancient geometry. We will see, then, that Euclid may have possessed a theory of intersections that was sufficiently rigorous to dispel the main objections that could be advanced in antiquity. (shrink)

This book's activities highlight the important cycle of exploration, conjecture, and justification in all five mathematical strands. Students recognize patterns and make conjectures, learn the value of a counterexample, explore the strengths and weaknesses of visual proofs, discover the power of algebraic representations, and learn that theoretical approaches can substantiate empirical results. The supplemental CD-ROM features interactive electronic activities, master copies of activity pages for students, and additional readings for teachers. --publisher description.

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)

We introduce a graph-theoretical representation of proofs of multiplicative linear logic which yields both a denotational semantics and a notion of truth. For this, we use a locative approach related to game semantics and the Danos–Regnier interpretation of GoI operators as paths in proof nets . We show how we can retrieve from this locative framework both a categorical semantics for Multiplicative Linear Logic with distinct units and a notion of truth. Moreover, we show how a restricted version of (...) our model can be reformulated in the exact same terms as Girardʼs geometry of interaction . This shows that this restriction of our framework gives a combinatorial approach to J.-Y. Girardʼs geometry of interaction in the hyperfinite factor, while using only graph-theoretical notions. (shrink)

"Contains a balanced account of recent advances in set theory, model theory, algebraic logic, and proof theory, originally presented at the Tenth Latin American Symposium on Mathematical Logic held in Bogata, Columbia. Traces new interactions among logic, mathematics, and computer science. Features original research from over 30 well-known experts worldwide.".

Over the past few years several drugs that target epigenetic modifications have shown clinical benefits, thus seemingly validating epigenetic cancer therapy. More recently, however, it has become clear that these drugs are either characterized by low specificity or that their target enzymes have low substrate specificity. As such, clinical proof‐of‐concept for epigenetic cancer therapies remains to be established. Human cancers are characterized by widespread changes in their genomic DNA methylation and histone modification patterns. Epigenetic cancer therapy aims to restore (...) normal epigenetic modification patterns through the inhibition of epigenetic modifier enzymes. In this review, we provide an overview about the known functional roles of DNA methyltransferases, histone deacetylases, histone methyltransferases, and demethylases in cancer development. The available data identify several examples that warrant further consideration as drug targets. Future research should be directed toward targeted enzyme inhibition and toward exploring interactions between epigenetic pathways to maximize cancer specificity. (shrink)

The most fundamental subject and aim of the Islamic belief system is the subject of maʿrifatullah (knowing Allah). Studies on this subject are mostly called ithbāt al-wājib (the demonstration of God) in the literature. They are considered the most valuable work for kalām, philosophy and mysticism schools. Kalām schools started to use this conceptualization intensively after Fakhr al-Dīn al-Rāzī, mainly under the influence of Ibn Sīnā. Sūfis, on the other hand, most participated in these studies based on the theory of (...) the unity of existence. In kalām, all the principles of belief are ultimately grounded to explain and strengthen faith in Allah. For this reason, belief in Allah is referred to as aṣl al-uṣūl (the origin of all principles). Throughout history, scholars of kalām discussed the creedal issues of Islam in the Muslim society while it tried to answer the creedal issues abroad by the expanding Islamic geography with studies on ithbāt al-wājib. In this framework, the problems of prophecy and the hereafter are included in kalām. Since the beginning of the history of kalām, it has used the theory of atomism to a large extent, especially in defending the existence of Allah against materialists. The systematisation of Islamic philosophy and mysticism in time, the kalām cosmological argument, the argument from contingency of philosophers and the argument from kashf and ilhām of Sūfis strengthened this area from three different branches. On the other hand, the interaction of these schools within themselves and the diversification of the interlocutors of studies on ithbāt al-wājib brought these arguments closer together. The convergence in terms of terminology, subject and methodology, especially after Shahrestānī and Rāzī, revealed the tradition of philosophical theology. In this process, theologians began to use both the concepts of temporality (hudūth) and contingency (imkān) to use ontological, cosmological and teleological proofs. Dawānī, one of the eminent figures of these studies in the last periods of Ottomans, is the subject of our research, due to his skills in utilising these proofs of ithbāt al-wājib and his influence in the studies after him. His review of the matter can be observed in his effort in his works where he deals with the so-called deficiencies and errors of his predecessors regarding ithbāt al-wājib. For this reason, many annotations and commentaries were made for his treatises and ideas until the 19th century. Especially, the advance of materialism in the West in this century showed great influence on many scholars and intellectuals in the Ottoman Empire seems to be a parallel historical experience. Therefore, it has become necessary to utilise the arguments for the existence of Allah by supporting each individual argument together. In this regard, in our study, to see the process, we also discussed the views of Aḥmad Nūrī, one of the scholars in the last period Ottoman, who dealt with the common arguments about ithbāt al-wājib produced by the three primary schools of Islamic thought: kalām, Islamic philosophy and mysticism. (shrink)

We can find some of the works of Indian Buddhist philosophers that prove the authenticity of the Mahāyāna sutras within Sanskrit, Tibetan, and Chinese textual sources. *Jayasena’s critique of *Asvabhāva’s proof was first introduced in the commentaries of Kuiji. Numerous references to *Jayasena in Chinese Yogācāra scriptures indicate that he was regarded as a Yogācāra master. His revised proof was further revised by Xuanzang. According to Xuanzang’s biographies, *Jayasena was an Indian lay Buddhist scholar who had many non-Buddhist (...) disciples. It is, therefore, possible that he discussed the authenticity of the Mahāyāna sutras with his disciples. Following Kuiji’s introduction of *Jayasena’s proof in East Asia, this proof and Xuanzang’s critique have been widely discussed. Wonhyo, one of the most famous Silla Buddhist scholars, critiqued Xuanzang’s revision and published his revised formula. Zenju, a representative Yogācāra master of the Nara period, pointed out some logical problems to be seen in Wonhyo’s revision, but did not provide any alternative. Proof of the authenticity of the Mahāyāna sutras was originally developed as a result of interactions between Mahāyāna and non-Mahāyāna Buddhists. However, the purpose of the proof seems to have shifted from being based on arguments with actual opponents to internal discussions among Mahāyāna Buddhists, especially within East Asia. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:The Nature of Proof in PsychiatryPaul Lieberman (bio)Keywordspsychotherapy process, knowledge and psychiatry, externalism, WittgensteinThis vivid clinical report illustrates recognizably, and provocatively, a number of routine, but often unexamined, clinical questions. In its few paragraphs, it depicts challenges that each practitioner confronts, and, in the flux of clinical work, addresses, however implicitly and imperfectly, every day: From what data, and by what processes, does a clinical formulation, or way (...) of understanding, come into being? How do we appraise its accuracy and adequacy? Of what value is even a well-substantiated understanding, in the mind of the therapist, to the patient? What is the power of empathy as a treatment tool? How do we assess someone's status as a “good candidate for therapy?” When, typically, only the outlines of a problem are visible, and its origins and implications are largely hidden, by what right do we recommend psychotherapy, and with what conception, at what level of detail, of what its outcome will be? These are among the questions that Dr. Bailey's story challenges us to address.They are clinical questions, of course, because they deal with empirical matters of fact—psychological processes, outcomes studies, and evidence. But they are also philosophical because, as Freud insisted and Dr. Bailey shows, information obtained in the clinical situation often has power and authority that lead us to believe we understand what is going on, understand the other person, even in the absence of scientifically tested hypotheses, or the clear application of research-based evidence. Interactions between people—including clinical interactions—have a life and ability to engage us. Their meanings can seem so transparent and convincing that no doubt or questioning may seem cogent. At their most powerful, such experiences can reawaken us to important realms of experience and feeling which we might, otherwise, forget, ignore, suppress, deny, or in other ways keep out of awareness; they have the potential to arouse us and reconnect us with truths that, once revived, can seem both valid and important—perhaps the kind of experience that we may derive from works of art or literature (in fact, Dr. Bailey's account could be seen as a clinical parable—meant to be neither true nor false, but instructive). But even less dramatic examples are commonplace: we do routinely claim to know and be able to interpret and understand the actions of other people from our everyday interactions with and observations of them.What is less clear is how to account for these convictions and how to appraise their value, because they do not derive from established scientific procedures. Clinical intuition has a role throughout medicine, but we usually expect it to be subjected later to more rigorous tests to establish the correct diagnosis. Yet, as Dr. Bailey's case illustrates, clinical intuition in the psychiatric encounter seems somehow different. When Colin [End Page 225] leads Dr. Bailey to the conclusion that a “painful lack of wounds” has made him depressed, we find this credible. It seems similarly credible that Dr. Bailey might be anxious about his own capacity to defend his young family, because he says he is, that he perceives Colin as testing his manhood or sincerity, because that seems to fit Colin's temperament, that being accurately understood is helpful, because most of us have had that experience and valued it, and that, most generally, an absence of challenge or of activity could be depressing. But suppose a patient believed that a painful lack of wounds produced diabetes instead of depression, or suppose he had developed epilepsy and attributed that to an absence of combat experience. We might see these as ‘pre-scientific’ or ‘hypothesis-generating’ (or worse). By contrast, it seems timid to consider psychiatric formulations to be always and only provisional or hypothetical.In what ways and to what extent should we expect psychiatry to be different, and why? Several considerations suggest that psychiatry's reasons are not, always and everywhere, the same as those of general medicine, nor are its objectives.In general medicine, we distinguish between signs and symptoms, on the one hand, and “underlying” disease processes, on the other. But in psychiatry, this distinction can be... (shrink)

The paper gives a soundness and completeness proof for the implicative fragment of intuitionistic calculus with respect to the semantics of computability logic, which understands intuitionistic implication as interactive algorithmic reduction. This concept — more precisely, the associated concept of reducibility — is a generalization of Turing reducibility from the traditional, input/output sorts of problems to computational tasks of arbitrary degrees of interactivity.

Transfinite ordinal numbers enter mathematical practice mainly via the method of definition by transfinite recursion. Outside of axiomatic set theory, there is a significant mathematical tradition in works recasting proofs by transfinite recursion in other terms, mostly with the intention of eliminating the ordinals from the proofs. Leaving aside the different motivations which lead each specific case, we investigate the mathematics of this action of proof transforming and we address the problem of formalising the philosophical notion of elimination which (...) characterises this move. (shrink)

In this paper, we continue our research on a hybrid narrative-argumentative approach to evidential reasoning in the law by showing the interaction between factual reasoning (providing a proof for ‘what happened’ in a case) and legal reasoning (making a decision based on the proof). First we extend the hybrid theory by making the connection with reasoning towards legal consequences. We then emphasise the role of legal stories (as opposed to the factual stories of the hybrid theory). Legal stories (...) provide a coherent, holistic legal perspective on a case. They steer what needs to be proven but are also selected on the basis of what can be proven. We show how these legal stories can be used to model a shift of the legal perspective on a case, and we discuss how gaps in a legal story can be filled using a factual story (i.e. the process of reasoning with circumstantial evidence). Our model is illustrated by a discussion of the Dutch Wamel murder case. (shrink)

To open a newspaper or turn on the television it would appear that science and religion are polar opposites - mutually exclusive bedfellows competing for hearts and minds. There is little indication of the rich interaction between religion and science throughout history, much of which continues today. From ancient to modern times, mathematicians have played a key role in this interaction. This is a book on the relationship between mathematics and religious beliefs. It aims to show that, throughout scientific history, (...) mathematics has been used to make sense of the 'big' questions of life, and that religious beliefs sometimes drove mathematicians to mathematics to help them make sense of the world. Containing contributions from a wide array of scholars in the fields of philosophy, history of science and history of mathematics, this book shows that the intersection between mathematics and theism is rich in both culture and character. Chapters cover a fascinating range of topics including the Sect of the Pythagoreans, Newton's views on the apocalypse, Charles Dodgson's Anglican faith and Gödel's proof of the existence of God. (shrink)

Violations of the Bell inequalities in EPR-Bohm type experiments have set the literature on the metaphysics of microscopic systems to flirting with some sort of metaphysical holism regarding spatially separated, entangled systems. The rationale for this behavior comes in two parts. The first part relies on the proof, due to Jon Jarrett [2] that the experimentally observed violations of the Bell inequalities entail violations of the conjunction of two probabilistic constraints. Jarrett called these two constraints locality and completeness. We (...) prefer the terminology of locality and factorizability.[3] The first part of the rationale for metaphysical holism urges that only Jarrett’s locality allows for “peaceful coexistence” between any model of EPR-Bohm type experiments and special relativity. Factorizability, it is suggested, must be jettisoned. (shrink)

Zeilinger's observation that phenomena of the Aharonov-Bohm type lead to non-dispersive, i.e., energy-independent, phase shifts in interferometers is generalized in a new proof which shows that the precise condition for nondispersivity is a force-free interaction. The converse theorem is disproved by a conceptual counter-example. Applications to several nondispersive interference phenomena are reviewed briefly. Those fall into two classes which are objectively distinct from each other in that in the first class phase shifts depend only on the topology of the (...) interfering beam paths, while in the second class force-free physical interactions take place at identifiable points along the path. Apparent disagreements in the literature about the topological nature of the phenomena in the second class stem from differing definitions. (shrink)

We consider the question, of longstanding interest, of realizing types in regular ultrapowers. In particular, this is a question about the interaction of ultrafilters and theories, which is both coarse and subtle. By our prior work it suffices to consider types given by instances of a single formula. In this article, we analyze a class of formulas φ whose associated characteristic sequence of hypergraphs can be seen as describing realization of first- and second-order types in ultrapowers on one hand, and (...) properties of the corresponding ultrafilters on the other. These formulas act, via the characteristic sequence, as points of contact with the ultrafilter D, in the sense that they translate structural properties of ultrafilters into model-theoretically meaningful properties and vice versa. Such formulas characterize saturation for various key theories , yet their scope in Keisler’s order does not extend beyond Tfeq. The proof applies Shelah’s classification of second-order quantifiers. (shrink)

We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests. The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. One can also use the system to reason about properties of simple imperative programs using schematic KAT. We explain how the system works and illustrate its use with some examples, including an extensive scheme equivalence proof.

John von Neumann's proof that quantum mechanics is logically incompatible with hidden varibales has been the object of extensive study both by physicists and by historians. The latter have concentrated mainly on the way the proof was interpreted, accepted and rejected between 1932, when it was published, and 1966, when J.S. Bell published the first explicit identification of the mistake it involved. What is proposed in this paper is an investigation into the origins of the proof rather (...) than the aftermath. In the first section, a brief overview of the his personal life and his proof is given to set the scene. There follows a discussion on the merits of using here the historical method employed elsewhere by Andrew Warwick. It will be argued that a study of the origins of von Neumann's proof shows how there is an interaction between the following factors: the broad issues within a specific culture, the learning process of the theoretical physicist concerned, and the conceptual techniques available. In our case, the ‘conceptual technology’ employed by von Neumann is identified as the method of axiomatisation. (shrink)

The paper proves refined feasibility properties for the disjunction property of intuitionistic propositional logic. We prove that it is possible to eliminate all cuts from an intuitionistic proof, propositional or first-order, without increasing the Horn closure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs. The feasibility of the disjunction property is proved for sequents containing Harrop formulas. Under hardness assumptions for NP and for factoring, it is shown that the intuitionistic (...) propositional calculus does not always have polynomial size proofs and that the classical propositional calculus provides a superpolynomial speedup over the intuitionistic propositional calculus. The disjunction property for intuitionistic propositional logic is proved to be P-hard by a reduction to the circuit value problem. (shrink)

We further develop a recent new proof (by Greenberger, Horne, and Zeilinger—GHZ) that local deterministic hidden-variable theories are inconsistent with certain strict correlations predicted by quantum mechanics. First, we generalize GHZ's proof so that it applies to factorable stochastic theories, theories in which apparatus hidden variables are causally relevant to measurement results, and theories in which the hidden variables evolve indeterministically prior to the particle-apparatus interactions. Then we adopt a more general measure-theoretic approach which requires that GHZ's argument (...) be modified in order to produce a valid proof. Finally, we motivate our more general proof's assumptions in a somewhat different way from previous authors in order to strengthen the implications of our proof as much as possible. After developing GHZ's proof along these lines, we then consider the analogue, for our proof, of Bohr's reply to the EPR argument, and conclude (pace GHZ) that in at least one respect (viz. that of most concern to Bohr) the proof is no more powerful than Bell's. Nevertheless, we point out some new advantages of our proof over Bell's, and over other algebraic proofs of nonlocality. And we conclude by giving a modified version of our proof that, like Bell's, does not rely on experimentally unrealizable strict correlations, but still leads to a testable “quasi-algebraic” locality inequality.“... to admit things not visible to the gross creatures that we are is, in my opinion, to show a decent humility, and not just a lamentable addiction to metaphysics.”J. S. Bell. (shrink)

Checking the equivalence of two Boolean functions, or combinational circuits modeled as Boolean functions, is often desired when reliable and correct hardware components are required. The most common approaches to equivalence checking are based on simulation and model checking, which are constrained due to the popular memory and state explosion problems. Furthermore, such tools are often not user-friendly, thereby making it tedious to check the equivalence of large formulas or circuits. An alternative is to use mathematical tools, called interactive (...) theorem provers, to prove the equivalence of two circuits; however, this requires human effort and expertise to write multiple output functions and carry out interactive proof of their equivalence. In this paper, we define two simple, one formal and the other informal, gate-level hardware description languages, design and develop a formal automatic combinational circuit equivalence checker tool, and test and evaluate our tool. The tool CoCEC is based on human-assisted theorem prover Coq, yet it checks the equivalence of circuit descriptions purely automatically through a human-friendly user interface. It either returns a machine-readable proof of circuits’ equivalence or a counterexample of their inequality. The interface enables users to enter or load two circuit descriptions written in an easy and natural style. It automatically proves, in few seconds, the equivalence of circuits with as many as 45 variables. CoCEC has a mathematical foundation, and it is reliable, quick, and easy to use. The tool is intended to be used by digital logic circuit designers, logicians, students, and faculty during the digital logic design course. (shrink)