January 20, 2014, 17 Uhr c.t., Forum Scientiarum, Seminarraum 2.3, Tübingen:
Vincent Degauquier (Louvain-la-Neuve): A Uniform Proof-Search Method for Partial and Paraconsistent Four-Valued Logics

Abstract: This talk aims to provide a proof-theoretic framework for partial and paraconsistent four-valued logics. Specifically, our purpose consists in developing a unified sequent calculus and providing a uniform proof-search method for these logics.

January 13, 2014, 17 Uhr c.t., Forum Scientiarum, Seminarraum 2.3, Tübingen:
Vito Michele Abrusci (Roma): Antinomy of the liar: an analysis inspired by linear logic and transcendental syntax

Abstract: I will expose a logical and philosophical analysis of the well-known antinomy of the liar, inspired by results and methods of linear logic and also by the program of "transcendental syntax" proposed by J.-Y. Girard.
In particular, I will focus on the role played by structural rules, and I will consider the antinomy of the liar as a result concerning a central notion of "transcendental syntax", the notion of "format".



December 6, 2013, 15h c.t., Seminarraum 1, Sand 6 (WSI), Tübingen:
Edward Hermann Haeusler (Rio de Janeiro): On computational complexity of propositional logics and the sub-formula principle

Abstract: The computational complexity of Tautology-Checking for purely implicational minimal propositional logic is known to be PSPACE-complete. Intuitionistic Propositional Logic is also known to be PSPACE-complete, while Classical Propositional Logic is CONP-complete for Tautology checking and NP-complete for Satisfiability checking. We show how proof-theoretical results on Natural Deduction help analysing the polynomial relationship among Intuitionistic, Classical, Minimal and Minimal Purely Implicational Propositional Logics. This analysis is based on the sub-formula principle property. We extend the polynomial reduction of purely implicational logic to any propositional logic satisfying the sub-formula principle. Hence, any propositional logic satisfying the sub-formula principle is shown to be PSPACE-hard. We conclude that some well-known logics, such as Propositional Dynamic Logic and S5C (n = 2), for example, hardly satisfy the sub-formula property. On the other hand, these logics have proof procedures. They are told to be mechanizable despite being EXPTIME-complete. We (re)raised up some questions on propositional logics mechanisation.

December 6, 2013, 16h c.t., Seminarraum 1, Sand 6 (WSI), Tübingen:
Luiz Carlos Pereira (Rio de Janeiro): On the proof thory of classical logic

November 11, 2013, 17 Uhr c.t., Forum Scientiarum, Seminarraum 2.3, Tübingen:
Ole Hjortland (München): Proof Theoretic Harmony in the Substructural Era

Abstract: Logical inferentialism is the idea that the meaning of a logical connective is determined by the inference rules that govern its use. Proof theoretic semantics attempts to make this idea precise in a proof theoretic framework, using for example natural deduction or sequent calculus rules. Since Prior's infamous connective tonk much of proof theoretic semantics have been occupied with formal (anti-tonk) conditions which rule out ill-behaved connectives (e.g. conservativeness, harmony). Common between them is that inference rules only succeed in determining the meaning of a connective only if the proof theoretic conditions are fulfilled. On the traditional account, however, such conditions are insensitive to substructural dimensions of proof theory, e.g. the distinction between additive and multiplicative connectives. We argue that proof theoretic semantics ought to have the resources to attribute different meanings to substructurally distinct connectives. Subsequently we show how to develop a notion of proof theoretic harmony that preserves substructural distinctions from introduction to elimination rules.

October 29, 2013, 15h c.t., Seminarraum 1, Sand 6, Sand 6 (WSI), Tübingen:
Thomas Seiller (Savoie): Geometry of Interaction

Abstract: Geometry of interaction is the trade name for Girard's interpretation of linear logic in the algebra of operators on Hilbert spaces.
In this all-afternoon intensive course, Thomas Seiller will present a comprehensive introduction into GoI that is based on the proof net representation of linear logic.

October 21, 2013, 17 Uhr c.t., Forum Scientiarum, Seminarraum 2.3, Tübingen:
Kai Wehmeier (Irvine): The Modal Rubicon

Abstract: The languages of modal logic are typically taken to be examples of intensional languages par excellence. I will argue that, in the case of most modal logics applied in philosophy, this is a mistake. The "Modal Rubicon" separating the intensional from the extensional turns out to be a modal logic's susceptibility to the addition of the actuality operator.

June 25, 2013, 18h c.t., Schellingzimmer, Alte Burse, Tübingen:
René Gazzari (Tübingen): Der Kalkül des natürlichen Rechnens

Abstract: Im ersten Teil des Vortrags stellen wir den Kalkül des natürlichen Rechnens vor. Dabei handelt es sich um eine Erweiterung des natürlichen Schließens, in der Gleichheiten durch explizite Manipulation von Termen ausgerechnet werden. Dieses Vorgehen ist formal gleichwertig zum traditionellen Umgang mit Gleichheiten, ermöglicht aber im Gegensatz zum traditionellen Vorgehen, Rechnungen, wie sie im mathematischen Alltag immer wieder vorkommen, auf eine natürliche Weise zu formalisieren.
Offensichtlich läßt sich der Formalismus auf Rechnungen mit weiteren Relationen ausweiten, insbesondere etwa auf die Kleiner-Gleich-Relation in der Arithmetik oder die Teilmengenbeziehung in der Mengenlehre. Im zweiten Teil des Vortrags werden wir solche Erweiterungen des Kalküls diskutieren. Vor allem werden wir andeuten, wie eine Reihe von weiteren Argumentationsweisen der Mathematik in derartigen Erweiterungen auf natürliche Art formalisiert werden können. Dabei sollen nicht nur Erweiterungen nach "unten", in denen Terme und Relationen behandelt werden können, sondern auch Erweiterungen nach "oben" für metalogische Relationen vorgestellt werden.

June 4, 2013, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Ivo Pezlar (Brno): Towards a More General Concept of Inference

Abstract: Sequent calculus is often seen just as a technical tool that lacks the intuitive appeal of natural deduction. I will try to show that this is not necessarily the case. I will argue that sequent calculus is a philosophically well founded system in its own right and that it can be viewed just as "natural" as natural deduction. Consequently, it will be argued that sequent calculus provides a basis for a more general notion of inference that is exemplified by the so-called 2D inference, i.e., deduction-to-deduction inference.

July 2, 2013, 18h c.t., Schellingzimmer, Alte Burse, Tübingen:
Pablo Cobreros (Navarra): S'valuationism and their logics

Abstract: Supervaluationism and subvaluationism are paracomplete and paraconsistent weakening of classical logic. Both logics have been claimed to provide solutions to the paradoxes of vagueness. Most of the studies, however, have taken a semantic perspective. In this talk we will review the different proof theories that have been proposed for these logics and point out to some open questions.

May 28, 2013, 18h c.t., Schellingzimmer, Alte Burse, Tübingen:
David Makinson (London): Intelim Rules for Classical Connectives: Questions of Existence and Uniqueness

Abstract: Introduction and elimination (briefly intelim) rules are in a natural sense the simplest of all Horn rules for propositional connectives. They have also played a prominent role in some philosophical discussions of the meaning of the connectives. For this reason, their behaviour has more than a purely formal interest. We consider two questions about such rules for truth-functional connectives: the existence, for a given connective, of at least one such rule that it satisfies, and the uniqueness of a connective with respect to the set of all of them. The answers are easy and well known in the context of rules using set/set sequents of formulae, but more complex and interesting for the restricted (but more often used) context of set/formula sequents, on which we focus.

April 23, 2013, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Grigory Olkhovikov (Ekaterinburg): Intuitionistic predicate logic of constant domains does not have Beth property

Abstract: Strengthening the previous result of Mints, Olkhovikov and Urquhart on interpolation failure, we show that Beth's definability theorem does not hold for intuitionistic predicate logic of constant domains without identity.

January 22, 2013, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Peter Schroeder-Heister (Tübingen): "On Flattening Elimination Rules"

Abstract: In proof-theoretic semantics of intuitionistic logic it is well-known that elimination rules can be generated from introduction rules in a uniform way. If introduction rules discharge assumptions, the corresponding elimination rule is a rule of higher level, which allows one to discharge rules occurring as assumptions. In some cases these uniformly generated elimination rules can be equivalently replaced with elimination rules that only discharge formulas or do not discharge any assumption at all - they can be "flattened" in a terminology proposed by Read. We show by an example from propositional logic that not all introduction rules have flat elimination rules. We translate the general form of flat elimination rules into a formula of second-order propositional logic and demonstrate that our example is not equivalent to any such formula. The proof uses elementary techniques from propositional logic and Kripke semantics.
(Joint work with Grigory K. Olkhovikov.)

January 15, 2013, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Ernst Zimmermann: "Kripke Rahmen für Algebren"

Abstract: Durch die Relevanzlogik ist seit langem bekannt, dass zweistellige syntaktische Operatoren mittels dreistelliger Relationen im Rahmen geeigneter Kripke Semantiken interpretiert werden koennen. Der Vortrag versucht zu zeigen, dass solche Ueberlegungen verallgemeinert werden koennen auf beliebige durch Axiome gegebene Groupoide. Dabei werden Groupoide auf logischem und auf algebraischem Hintergrund betrachtet. Ueberlegungen zur Definierbarkeit, Vollstaendigkeit, Repraesentierbarkeit und Dualitaet werden vorgestellt als Anwendung bekannter Methoden der Kripke Semantik.



December 18, 2012, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Patrizio Contu (Zürich): "Über Evaluationsordnung in formalen Theorien"

Abstract: Ausgehend vom Lambda-Kalkül und den funktionalen Programmiersprachen hat sich die Unterscheidung zwischen "lazy" (normal order) und strikter (applicative order) Evaluation fest etabliert. Es wird untersucht, inwiefern diese Ideen auf die Analyse der herkömmlichen formalen Theorien in der Logik und Grundlagen der Mathematik anwendbar sind. Unter anderem werden folgende Gebiete berücksichtigt: Intensionalität und Modallogik, Mengenlehre, konstruktive Beweise.

November 27, 2012, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Vincent Degauquier (Louvain-la-Neuve): "Cut-Redundancy, Partiality and Paraconsistency"

Abstract: Resulting from an interest in proof theory and non-classical logic, our purpose is to highlight the relationships between the concepts of cut, partiality and paraconsistency. To do this, we propose a unified hypersequent-inspired calculus to explain the role played by these concepts in some partial and/or paraconsistent predicate logics such as Kleene's strong three-valued logic, Priest's three-valued logic of paradox and Dunn-Belnap's four-valued logic. We show that several forms of cut are possible in this calculus and that some of them are equivalent to the principle of completeness or the principle of consistency.

November 21, 2012, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Jon Litland (Oslo): "Proof-Theoretic Semantics Based on Elimination Rules"

Abstract: Proof-theoretic semantics based on introduction-rules have been studied a fair bit. Much less work has been made on trying to base a proof-theoretic semantics on elimination rules. In this talk I show how we can build a proof-theoretic semantics for the standard intuitionistic propositional connectives based on their (standard) elimination rules. I show that intuitionistic propositional logic is complete with respect to this semantics. I briefly discuss the philosophical significance of these results.

November 12, 2012, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Francesco Paoli (Cagliari): "Semantic Minimalism for Logical Constants"

Abstract: In a 2003 paper ("Quine and Slater on paraconsistency and deviance", J. Phil. Log. 32, 2003, pp. 531-548), I defended a minimalist account of meaning for logical constants as a way to ward off Quine's meaning variance charge against deviant logics. Its key idea was that some deviant propositional logics share with classical logic the operational meanings of all their connectives, as encoded in their sequent calculus operational rules, yet validate different sequents than classical logic; therefore, we can have genuine rivalry between logics without meaning variance. In his PhD thesis, Ole Hjortland levelled several objections at this view. The aim of this talk is to address these criticisms, highlighting at the same time the rôle played by logical consequence in this version of semantic minimalism.

July 10, 2012, 18h c.t., Room A104, Sand 14 (WSI), Tübingen:
Reinhard Kahle (Lisbon): "Notwendigkeit"

Abstract: Wir stellen eine alternative logische Behandlung der Modalitäten "möglich" und "notwendig" vor, die auf der Analyse von Beweisen (bzw. Argumenten) beruht. Dabei kann die bekannte Mögliche-Welten-Semantik der Modallogik als eine Art Epiphänomen rekonstruiert werden. Zusätzlich zeigen wir, wie der zugrunde gelegte Ansatz auch auf andere intensionale Phänomene, insbesondere irreale Konditionalsätze, ausdehnt werden kann.



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"

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 A301, Sand 14 (WSI), Tübingen:
Peter Milne (Stirling): "Thinking about Negation"



December 16, 2010, Paris:
Peter Schroeder-Heister (Tübingen): "Proof-Theoretic Semantics and its Basic Logic"

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