Events
Final Conference:
- LogICCC Final Conference, 15-18 September 2011, Berlin
Talks:
Talks in Tübingen take place on Tuesdays in room A104, Sand 14 (WSI) at 18h c.t.
- May 10, 2011, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Paweł Urzyczyn (Warsaw): "Proof search in some propositional logics"(Joint work with Morten H. Sørensen.)
Abstract: In 1938 Mordchaj Wajsberg proved that intuitionistic propositional connectives are not definable from each other. For this, he developed a proof search algorithm, a forerunner of the Ben-Yelles inhabitation algorithm. A classification of normal forms, implicit in this algorithm, can be extended to second order propositional logic; we show how to use it in a syntactic Loeb-style embedding of first-order logic. As another example we consider the Wajsberg/Ben-Yelles approach to intersection logics.
- February 8, 2011, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Peter Dybjer (Göteborg): "Program testing and constructive validity"Abstract: In this talk I shall argue that program testing provides the basis for mathematical truth, and that mathematics is an empirical science. This point of view is the result of an analysis of Martin-Löf's meaning explanations for intuitionistic type theory, where the judgements of type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. One consequence is a new perspective of hypothetical judgments, since tests for such judgments need methods for generating inputs. Among other things, we need to generate function input. The continuity principle is relevant here and it follows that the alleged impredicativity of functionals can be rejected. Furthermore, our testing semantics suggests that we should only allow the formation of identity types over decidable types. At the end we turn to impredicative type theory, and discuss possible testing semantics for such theories. In particular we propose that testing for impredicative type theory should be based on the evaluation of open expressions rather than of closed expressions as for predicative type theory.
- January 25, 2011, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Laura Tesconi (Pisa): "A Labelled Sequent Calculus Isomorphic with Natural Deduction"Abstract: As it is well known, standard sequent calculus and natural deduction are not isomorphic to each other. This failure of one-to-one correspondence has its origins in the translation from/to left-side to/from elimination rules – on the one hand – and the translation of the cut rule – on the other hand. Von Plato's proposal of modifying natural deduction represents a solution to this problem, but the same result may be pursued "the other way around" as well – that is, by singling out some restrictions on the sequent calculus rules that guarantee isomorphism to natural deductions.
These restrictions concern the features of the calculus responsible of the failure of the isomorphism, that is left-side rules and the cut rule. This leads to the definition of a system of "labelled" sequent calculus, which presents the following characteristics: (a) the principal formula of any inference receives a label, so that it is possible to recognize the last inference of a derivation just by looking at its final sequent; (b) only when the cut formula is principal in both premisses is the cut rule allowed, all other cases require what is called "substitution rule"; (c) the right premiss of left-implication and the premiss of left-conjunction must be initial sequents; (c) left-side rules must be followed by a cut rule or a substitution rule, with the principal formula as cut formula or substitution formula (respectively). Labelled sequent calculus is proved to be deductively equivalent to the standard calulus.
Thanks to isomorphism to natural deduction, a cut elimination result for labelled sequent calculus obviously holds. However, the steps that leads to cut free derivations cannot be the same as for standard sequent calculus, due to the restrictions on left-side rules. - January 17, 2011, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Alberto Naibo (Paris) and Mattia Petrolo (Paris): "Logical Constants from a Computational Point of View: Towards an Untyped Setting"(Joint work with Thomas Seiller.)
Abstract: We investigate the conditions used to establish what counts as a logical constant from a proof-theoretical point of view. In the first part we present some limitations of Prawitz's inversion principle. Our criticism naturally leads to an additional requirement (eta-expansion) based on the Curry-Howard isomorphism, showing that the properties owned by logical constants have a computational nature. Nevertheless, lambda-calculus does not allow a satisfactory reconstruction of logical inferentialism on computational basis rather than linguistic ones. What is needed is a combinatorial and untyped setting from which logical constants emerge as those sets of objects whose interaction define logical types.
- January 11, 2011, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Peter Milne (Stirling): "Thinking about Negation" - November 23, 2010, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Tor Sandqvist (Stockholm): "Atomic Bases and Classical Logic"Abstract: On one conception put forward within the tradition of proof-theoretical semantics, a consequence relation for a language containing logical vocabulary is to be thought of as a two-layered affair. At bottom lies a primitively given set of rules regulating inferences among atomic, logic-free sentences. Upon this atomic basis, an inference relation pertaining to arbitrary sentences is then recursively built up, in accordance with fixed semantic clauses - much as, in standard semantics for classical logic, the truth values of logical compounds are determined by the truth values of atoms.
Typically, the consequence relations arising from semantic theories of this kind fall short of classical logic - a natural effect of their emphasis on rational acceptance, as opposed to recognition-transcendent truth. Much of my recent work, however, has been devoted to showing how the basic idea can in fact be adapted so as to justify classical inference. In my presentation I will describe some recent advances in this endeavour; compared to earlier efforts, the current theory features, above all, a much greater flexibility in the makeup of atomic bases. - October 12, 2010, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
David Miller (Warwick): "Dual Intuitionistic Logic and Its Dual"Abstract: Intuitionistic logic appears in many parts of mathematics, and amongst philosophers is perhaps the best known and most respected alternative to classical logic. Less attention has been paid to its dual, sometimes often called Brouwerian logic, which retains the law of excluded middle and discards the law of non-contradiction. Dual-intuitionistic logic is notable for containing, instead of a conditional →, the dual operation of remainder —.
The lecture aims to identify some areas of philosophical interest where the duality is compromised, and dual-intuitionistic logic, and its associated Brouwerian algebras, are more appropriate objects of study than are intuitionistic logic and its associated Heyting algebras. Special consideration will be given to the theory of deductive theories by Tarski, and to current axiomatizations of theory of probability and of deductive dependence. - July 6, 2010, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Christopher Menzel (Texas A&M): "Strict Actualism and the Logic of the Possible"Abstract: Actualists believe that, if an individual x had not existed, there would in no sense have been any such thing as x. Some actualists, however, believe that, even if x had failed to exist - or, at least, failed to exhibit the sort of ontological robustness that we associate with the contingent beings of our ordinary experience - there would still have been some sort of trace, or vestige, of x in virtue of which there would still, in effect, have been facts or truths about x. Strict actualists deny this. In this talk, I will examine three arguments against strict actualism. The first (formulated originally by Plantinga) is designed to show that the view is internally inconsistent. The others (found in the work of Robert Adams and Gregory Fitch) purport to show that the view, while not inconsistent per se, is inconsistent with the characteristic principle of the modal logic S5 that what is possible is necessarily possible, a principle that most modal metaphysicians consider highly intuitive. Each argument can be understood to turn on some aspect of the logic of the possible - more specifically, the logic of truth, possibility, and exemplification with respect to other possible worlds. Building on Adams' notion of truth at a possible world, in each case, I will argue that there is a reasonable way of understanding the premises of the argument that is entirely consistent with strict actualism but which renders the argument unsound.
- July 1, 2010, 10h c.t., Room A104, Sand 14 (WSI), Tübingen:
Nissim Francez (Haifa): "Proof-Theoretic Reconstruction of Communication in Natural Language: Speaker-Meaning vs. Hearer-Meaning"Abstract: The talk utilizes the framework of proof-theoretic semantics (PTS) to introduce into formal semantics the notion of speaker-hearer communication, by distinguishing two (objective!) sentential meanings: s-meaning (for the speaker) and h-meaning (for the hearer). The speaker meaning is based on the verificationalist view of PTS, where I-rules are taken to confer meaning, while the hearer meaning is based on the pragmatist view of PTS, where E-rules are taken to confer meaning. Successful communication between speaker and hearer relies on the meaning-conferring natural-deduction proof system being harmonious (I-rules and E-rules being balanced), shedding some new light on the property of harmony, so far viewed in PTS only as a condition of justifying the rules as being meaning conferring. The PTS approach thus provides new avenues for the semantics-pragmatics interface.
- June 16, 2010, 10h c.t., Room A301, Sand 14 (WSI), Tübingen:
Robert van Rooij (Amsterdam): "Extending syllogistics, and providing an intensional semantics"Abstract: Traditional logic, also known as term logic, is a loose term for the logical tradition that originated with Aristotle and survived until the advent of algebraic logic and modern predicate logic in the mid and late nineteenth century, respectively. Modern logicians used quite a number of arguments as to why traditional logic should be abandonded. First and foremost, the complaint is that traditional logic is not rich enough to account for mathematical reasoning, or to give a serious semantics of natural language. In the first part of the talk I will extend syllogistic logic first to full propositional logic, and then an interesting fragment of predicate logic that includes relations.
Modern logicians give to syllogistic logic an extensional semantics: terms are interpreted as sets of individuals. But Leibniz and others preferred an intensional semantics according to which terms are interpreted as sets of properties. Unfortunately, he didn't succeed for the full syllogistic fragment containing negative and conjunctive terms. In the second part of the talk I will show how to give such an intensional semantics. I will also suggest how this semantics might be used to account for Aristotle's modal syllogisms. - May 18, 2010, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Erik C. W. Krabbe (Groningen): "Hamblin's and Lorenzen's Systems of Dialogue: Comparison and Integration"Abstract: When Charles Hamblin introduced the notion of a formal dialectic, he did not refer to the dialogical logic of Paul Lorenzen and Kuno Lorenz. However, in hindsight the dialogue games of Lorenzen and Lorenz clearly present us with examples of a kind of formal dialectical systems avant la lettre. One may speak of Hamblin-type and of Lorenzen-type systems. How do these types compare? And can they be brought together?
After a short introduction about the concept of a formal dialectical system, this talk will focus on two exemplars, each of a different type: Hamblin’s Why–Because system with questions, also known as "System H", and a Lorenzen-type constructive propositional system, Constructive NOT-Dialectics (CND). We shall scrutinize Hamblin’s (unique) example of a dialogue in System H, and have a briefer look at a CND dialogue. Motivations for these systems as well as problematic aspects will be discussed. It will be obvious that "completeness" makes no sense for Hamblin-systems; but, as an excursion, we shall briefly delve into a method for obtaining relatively short completeness proofs for Lorenzen-type systems. Finally, we shall see how systems of these two types can be profitably integrated into one model of reasonable discussion. - July 21, 2009, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Laurent Keiff (Lille): "Dialogues and GTS games. Some remarks about the meaning of logical constants"Abstract: The aim of the talk is to systematically compare two game-theoretically flavored approaches to logic: dialogical logic founded by Paul Lorenzen and Kuno Lorenz, and the game-theoretical semantics of Jaakko Hintikka. For classical Propositional logic and for classical First-order logic, an exact connection between 'intuitionistic dialogues with hypotheses' and semantical games is established. Various questions of a philosophical nature are also shown to arise as a result of the comparison, among them the relation between the model-theoretical and proof-theoretical approaches to the philosophy of logic and mathematics. At the end and briefly, a link will be established on how the dialogical approach is immune to tonk-particles.
- June 16, 2009, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Kai Wehmeier (Irvine/Nancy): "Subjunctivity and Cross-World Predication"Abstract: While I couldn't possibly have been taller than myself, I might well have been taller than I am. In terms of possible worlds semantics, this difference can be cashed out by distinguishing between intra-world and cross-world predications, the latter typically involving the comparison of an individual in one world with an individual in some other world. In my talk, I will discuss the standard formalization strategy for cross-world predications that goes back to Russell, offer an alternative logical analysis in terms of an extension of my subjunctive modal logic, and apply the new analysis to Kripke's modal argument against descriptive theories of proper names.
- May 12, 2009, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Heinrich Herre (Leipzig): "Formal Ontology - A New Interdisciplinary Research Field"Abstract: In this talk we present an overview about the field of formal ontology. The importance of ontologies as information systems is increasingly recognized in fields diverse as the semantic web, enterprise, information integration, natural language processing, knowledge engineering, and databases. We present an overview about the top level ontology GFO (General Formal Ontology), which is being developed at the IMISE, University of Leipzig, and show the roots of this science in philosophy, logic, and computer science. Top level ontologies can be used as a framework for modelling and categorizing particular domains. Furthermore, we discuss a number of examples more in detail, in particular Brentanian space and time, ontological reductions, object-process-integration, sequences in biomedical ontology, functions and dispositions, and mereological foundation of set theory.
-
March 31, 2009, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Gabriele Usberti (Siena): "The notion of c-justification for atomic statements".Abstract: The aim of my talk is to define the notion of c-justification ("c-" for "cognitive", but also for "computational") for atomic statements, i.e. for statements not containing logical constants. For the sake of simplicity, I will consider only predications of the form "P(n)" where P is a predicate and n is a name. The problem is evidently a vast one, because the variety of atomic statements of a natural language is immense. I will be concerned only with a restricted number of cases, but I will select them in such a way that they are sufficiently representative of the generality of cases. In particular I will keep present, beside mathematical ones, observational statements and several other empirical statements in the present tense and in the third singular person.
-
February 17, 2009, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Luiz Carlos Pereira (Rio de Janeiro): "Constructive fragments of classical logic"Abstract: Gödel showed that any classical theorem in the fragment {not,and} is also an intuitionistic theorem. The immediate effect of this result is that the fragment {not,and} is insufficient to distinguish the class of classical propositional theorems from the class of intuitionistic propositional theorems. A nice way to understand the import of Gödel's result is through the slogan: we can do classical propositional logic without classical logic! In the remaining parts of this talk we shall examine other constructive properties of different fragments of classical first order logic and classical modal logic.
(Joint work with Edward Hermann Haeusler (PUC-Rio) and Maria da Paz N. de Medeiros (UFRN).)
- January 13, 2009, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Helge Rückert (Mannheim): "Die Dialogische Logik als semantischer Ansatz"Abstract: Die Dialogische Logik, die im Rahmen des konstruktivistischen Programms der Erlanger Schule von Paul Lorenzen und Kuno Lorenz entwickelt worden war, wird zunächst unabhängig von diesem historischen Hintergrund präsentiert. Dann wird diskutiert, inwieweit sich die Dialogische Logik als semantischer Ansatz auszeichnet und es werden Gemeinsamkeiten und Unterschiede mit anderen semantischen Ansätzen wie modelltheoretischen und beweistheoretischen erörtert. Schließlich werden wichtige begriffliche Unterscheidungen hervorgehoben, die im Rahmen des dialogischen Ansatzes von besonderer Wichtigkeit sind (u.a. Partieebene vs. Strategieebene, Rahmenregeln vs. Partikelregeln und Gültigkeit als generelle Wahrheit vs. Gültigkeit als formale Wahrheit).
Workshops:
- The cross-CRP workshop "Proof and Dialogues (ProDi)" takes place at the University of Tübingen on 25-27 February 2011.
The workshop aims at bringing together two EUROCORES / LogICCC projects, DiFoS and LoMoReVI, to discuss several aspects of the relationship between the notions of 'proof' and 'dialogues'.
Invited Speakers include:
- Andreas R. Blass (University of Michigan)
- Alain Lecomte (University of Paris 8)
- Kuno Lorenz (Universität des Saarlandes)
- George Metcalfe (University of Bern)
- Shahid Rahman (University of Lille 3)
- Helge Rückert (University of Mannheim)
- Morten Heine Sørensen (FORMALIT)
- Tero Tulenheimo (University of Lille 3)
- The cross-CRP workshop "Dialogues, Inference, and Proof – Logical and Empirical Perspectives (DIPLEAP)" takes place at the Vienna University of Technology on 26-28 November 2010.
Traditional conceptions of logic model correct inference quite abstractly by Tarski style semantics or by reference to formal proof systems without much concern about empirical findings about human reasoning. The fact that logical inference has to be embedded in language use and thus implies communicative interaction between human agents, that is to be addressed also by empirical methods, is often neglected. The three EUROCORES/ LogICCC projects organising this workshop DiFoS, LcpR, and LoMoReVI address this challenge in various ways. The workshop aims at corresponding cross fertilization, stimulated by invited talks by external experts.
Invited Speakers:
- Michiel van Lambalgen (Universiteit van Amsterdam)
- Keith Stenning (University of Edinburgh)
- Lance Rips (Northwestern University, WCAS, Illinois)
- David Over (Durham University)
- The cross-CRP workshop "Modelling Interaction, Dialog, Social Choice, and Vagueness (MIDiSoVa)" takes place at the Institute for Logic, Language and Computation of the University of Amsterdam on 26-28 March 2010.
Members of the CFSC, DiFoS, LINT and VAAG LogICCC projects will participate in this workshop, organized by Jouko Väänänen, which aims to further cross-CRP cooperation.
Four external experts, chosen among the top in their respective fields, will also participate in the workshop: Samson Abramsky, Wilfrid Hodges, Ewan Klein and Jean-François Laslier.