ÿþ<html> <head> <title>Logical Methods in the Humanities Workshop Abstracts</title> </head> <body> <H1><center><FONT COLOR="#FF0033">Logical Methods in the Humanities Workshop Abstracts Spring 2006</FONT></center></H1> <a name="Koepke"><p><center><b>Peter Koepke</b> (Bonn)<br>Proof Checking with a Natural Language Interface </center> <p>According to Godel's completeness theorem, every mathematical proof is equivalent to a formal proof in a finitary logical calculus. On this basis, various proof checking software systems have been designed focusing on different aspects of ``proving''. A recurring issue is the relation between ``natural'' and formal proofs. In my talk I want to discuss proof checking as a tool for teaching how to prove (basic) mathematical statements. Proofs should be input as simple (English) texts including mathematically typeset formulas. The checking algorithm may have limited capabilities, forcing the user to write detailed arguments. I present a prototypical system NAPROCHE (NAtural PROof CHEcker) which extends the mathematical text editor TeXmacs with a prolog proof checker and which is being used in courses at Bonn. I shall discuss some logical and linguistic issues which come up in the course of this work.</p> <hr> <a name="Yap"><p><center><b>Audrey Yap</b> (Stanford)<br>Dedekind's Structuralism in Historical Context </center> <p>Richard Dedekind's views are typically associated with two different schools of thought in the philosophy of mathematics. More traditionally, Dedekind is thought to be a logicist, for whom the truths of mathematics are analytic and follow from the laws of thought. Others, however, identify Dedekind as one of the earliest mathematical structuralists, who claim that the real subject-matter of mathematics are mathematical patterns, or structures. I follow Erich Reck's general interpretation of Dedekind as a logical structuralist, combining elements of both views, but ultimately better identified as a structuralist. Reck's argument for this, however, uses Dedekind's work on the natural numbers to prove his point; in my view, Dedekind's structuralism comes out much more clearly when we look at his other mathematical work, and at the historical context in which this work in situated.</p> <hr> <a name="MayoWilson"><p><center><b>Conor Mayo-Wilson</b> (Stanford)<br> Causes For Undecidability of the Theory of Relation Algebras</center> <p>Relation Algebras are algebraic structures intended to capture the mathematical behavior of binary relations. Tarski proved that the language of relation algebras is as expressive as the three variable fragment of FOL. Because only three variables are needed to express Zermelo-Fraenkel set theory, the language of relation algebras is sufficient to express nearly all of modern mathematics. Moreover, Tarski and his students carried out extensive research in the complexity of the theory of relation algebras when particular axioms are omitted or modified. Hence, in investigating the computational complexity of many first order theories, it is often helpful to seek what is known about its relation-algebraic equivalent. My talk will provide a survey of what is known about the computation complexity of theories of relation algebras and causes for undecidability. I will focus on the work of Maddux, Nemeti, and recently, Marx.</p> <hr> <a name="Devlin"><p><center><b>Keith Devlin</b> (Media X, CSLI)<br>Trying to find a logic of intelligence analysis</center> <p>For the past few years I've been looking at the work of trained intelligence analysts, trying to find ways of capturing/modeling what they do by some form of logical framework. In my talk I'll describe the general problem, what the powers-that-be would like to come out of this work, and outline one or two modeling attempts I've made.</p> <hr> <a name="Bos"><p><center><b>Henk Bos</b> (Utrecht University)<br>Descartes Attempt, in the "Regulae", to Base the Certainty of Algebra on Mental Vision</center> <p>In his unfinished (and at the time unpublished) `Regulae ad Directionem Ingenii' (`Rules for the Direction of the Mind', composed during the 1620's) Descartes used examples from mathematics to illustrate how the human mind can attain certain knowledge. The crucial example was the certainty of the arithmetical operations. For adding, subtracting, multiplying and dividing he produced arguments which convinced him. However, the text which we have strongly suggests that he was not able to prove the certainty of root extraction (both square and higher-order roots) in a manner he found satisfactory. He later abandoned this line of approaching the problem of certainty in philosophy.<br><br> The criteria for certainty which Descartes used in the `Regulae' were strongly visual; attaining certainty involved a process of `imagination' in which figures were created by the mind on a kind of mental screen, observable by some inner eye.<br><br> At Descartes' time one of the novelties in mathematics was the use of algebra in geometry. This necessitated a geometrical interpretation of the arithmetical operations; a theme in which Descartes had a keen interest (also after he gave up the `Regulae').<br><br> I shall argue that the then common geometrical interpretations of the algebraic operations help us to identify the reasons why Descartes could accept adding, subtracting, multiplying and dividing as certain, but not the extracting of roots, and why this constituted an obstacle severe enough for him to give up the project of the `Regulae.'<br><br> I have dealt with this topic in my book `Redefining Geometrical Exactness : Descartes' Transformation of the Early Modern Concept of Construction' (New York, Springer, 2001), pp. 261-269; in the lecture, however, I shall be more explicit in reconstructing the visual imagining involved in his argument.</p> <hr> <a name="deQueiroz"><p><center><b>Ruy de Queiroz</b> (Stanford and UFPE)<br>Natural Deduction for Equality </center> <p>The formulation of the so-called "equality types" in Martin-L"of's type theory has brought about the need to give a proof-theoretic counterpart to the distinction between definitional equality and propositional equality. While the former may involve rewrites, the latter has the status of a statement. Here we wish offer an approach to a natural deduction style proof theory for propositional equality. The basic idea is that when analysing an equality statement into (i) proof conditions ("introduction") and (ii) immediate consequences ("elimination"), one is faced with the need to bring in identifiers (i.e. function symbols) for (sequences of) rewrites, and this seems to claim for a "missing entity" in Martin-L"of's equality types. What we end up with is a formulation of what appears to be a middle ground approach to the "intensional" vs. "extensional" dichotomy which appears in type-theoretic formulations of equality.<br><br> (Joint work with Dov Gabbay & Anjolina de Oliveira)</p> <hr> <!-- Created: Sun Sep 27 18:20:05 PDT 1998 --> <!-- hhmts start --> <!-- hhmts end --> </body> </html>