Research seminars prior 2013

The archive of seminars from 2005 to 2019 is divided into two pages. Below you will find all Logic Seminars from 2005 to 2013. Schedules for later years, 2013 until 2019, are available on this page.

Seminar listings from 2019 onwards are found on the main seminar page.

2013

25/1 Kaj Börje Hansen (Uppsala) Formal logic, models, reality.

1. I prove an observation to the effect that formal logic is concerned only with semantic models and not directly with reality.
2. Philosophers like Russell and Quine have had troubles in finding flawless formalisations of sentences expressing theism and atheism in predicate logic. Observation 1 leads to a detection of the source of the troubles and to a simple solution.
3. Observation 1 is used to show that Quine’s idea of ontological commitment is unsustainable.
4. Observation 1 suggests a correspondence theory of truth for natural languages. Two counterexamples to it are suggested. The theory is a toy theory and not seriously meant. The analysis of it leads, however, to valuable insights.
5. I begin to sketch ideas for a non-formal logic which applies directly to reality.

8/2 Jörgen Sjögren (Skövde) The Viability of Social Constructivism as a Philosophy of Mathematics.

Attempts have been made to analyse features in mathematics within a social constructivist context. In this paper we critically examine some recent such attempts with focus on problems of the objectivity, ontology, and necessity of mathematics. Our conclusion is that these attempts fare no better than traditional alternatives, and that they, furthermore, create new problems of their own. Joint work with Christian Bennet. (The seminar will be in Swedish)

22/2 Håkon Robbestad Gylterud (Stockholm) Groupoids, data structures and derivatives.

In this talk I will present my ongoing work on polynomial functors on groupoids. I will begin the talk with an introduction to groupoids from the perspective of looking at them as generalised sets[1]. The notion of a polynomial functor on sets, may be seen as a mathematical model of data structures[1]. Polynomial functors on sets are equipped with an algebraic structure, and an operation similar to derivation in mathematical analysis satisfying Leibniz’ Rule. My work involves showing how moving on to groupiods lets us find some anti-derivatives (indefinite integrals) of polynomial functors on sets and further analogies to calculus.

[1] Martin Hofmann and Streicher, T.: 1998, The groupoid interpretation of type theory, Twenty-five years of constructive type theory (Venice, 1995), Vol. 36 of Oxford Logic Guides, Oxford Univ. Press, New York, pp. 83–111.

[2] Michael Abbott, Thorsten Altenkirch and Neil Ghani: 2005, Containers: constructing strictly positive types, Theoretical Computer Science 342(1), 3–27.

22/3 Ole Hjortland (LMU Munich) Logical Inferentialism and the Context of Deducibility. CANCELLED due to air strike.

5/4 Pietro Galliani (Helsinki) On Inclusion Logic. In this talk I will present some recent results concerning Inclusion Logic, a formalism obtained by adding database-theoretic inclusion dependencies to First Order Logic. I will discuss its relationship with other extensions of First Order Logic, and I will prove some results concerning its expressive power.

3/5 Meeting in honor of Dag Westerståhl on the occasion of his retirement

17/5 Janet Folina (Minneapolis, USA) Why the Proof is not in the Picture: Seeing, Believing and Justifying. What roles can pictures or diagrams play in mathematical proofs? Can they be proofs? In this talk we’ll consider some old and some new objections to “picture proofs”. I’ll argue that pictures are not proofs, at least not on their own. I’ll also argue that pictures fail to be proofs for different reasons in different areas of math.

27-31/5 Nordic Spring School in Logic 2003, Nordfjordeid, Norway: 27-31/5

7/6 (T307) Patrick Blackburn (Roskilde) Hybrid Deduction

In this talk I will discuss why modal deduction is tricky, and why hybrid logic fixes (some of) its problems. Themes I will emphasize include the second-order nature of modal logic, how hybrid logic yields a first-order perspective on frame structure, and how ‘‘non-standard’’ hybrid inference rules turn out to be sequent rules ‘‘missing’’ from orthodox modal logic. I shall close the talk by discussing recent joint work with Thomas Bolander, Torben Braüner, and Klaus Frovin Jørgensen on what we term Seligman-style tableaux, in honour of classic (but overlooked) work by Jerry Seligman from the 1990s on hybrid deduction. The talk will be relatively self contained and won’t presuppose any particular expertise in modal (let alone hybrid) logic. Indeed, one of my main aims will be to make the intuitions underlying modal and hybrid logic clear to non-specialists. (Joint with the Human Reasoning seminar)

14-16/6 Swedish Congress of Philosophy 2013, Stockholm

30/8 Elizabeth Coppock (Göteborg) Kind Reference and Intensional Type-Shifting

In this talk, I will present an intensional compositional semantics with type-shifting, designed to implement Chierchia’s (1998) influential theory of kind reference (as in e.g. “Tigers are rare”; “The dodo is extinct”). The system, meant to stay as close to familiar textbook assumptions as possible, overcomes several serious technical problems in Chierchia’s original formulation, and includes a set of explicit composition rules, whose formulation turns out to be non-trivial due to the extensive use of type-shifting and intensionality. The system crucially allows (i) multiple meanings for a single expression, (ii) composition via both intensional and extensional functional application, and (iii) intensional as well as extensional type-shifting. All of these contribute to the interpretation of expressions that can refer to kinds, as I will show with examples.

6/9 Ali Enayat (Göteborg) Interpretations and set theory

The first half of the talk will be devoted to a tutorial-style development of certain key concepts and classical theorems of interpretability theory. The second half will survey old and new results in the interpretability theoretic study of Zermelo-Fraenkel set theory.

13/9 Dag Westerståhl (Stockholm) (T302) New light on ‘Carnap’s problem’

In his book Formalization of Logic (1943), Carnap pointed out that there exist what he called non-normal interpretations of classical propositional logic (PL), i.e. interpretations of some of the usual propositional connectives that differ from the standard truth tables, but are consistent with all classical laws of PL. Carnap thought this was a major problem for formalizations of PL and suggested two kinds of remedy. His observations are not very well known among logicians or philosophers today, but recently they have been the subject of some debate, e.g. in Analysis: T. Smiley (1996), P. Raatikainen (2008), J. Murzi & O. Hjortland (2009), L. Incurvati & P. Smith (2010). These authors all take Carnap’s observations for granted but differ about their import. We take a new look at Carnap’s question from the perspective of modern (formal) semantics (a perspective Carnap could not have taken in 1943). We show that under very reasonable assumptions about such a semantics—the main one being that meaning assignment is compositional—there are no non-normal interpretations of PL. In fact, most of the relevant facts about PL can be found already in Carnap’s book, but he didn’t assign any special role to compositionality. We also suggest that some of the modern logical study of PL might profit from taking compositionality seriously. Finally, we raise Carnap’s question for first-order logic (FOL): Are there non-normal interpretations of the quantifiers consistent with all classical FOL laws? The answer (which is less easy to find than for PL) is Yes, but only to the extent that quantification is interpreted as in free logic. And with an extra, also natural, assumption (topic neutrality, or permutation invariance), this ‘non-normal’ interpretation is eliminated too. (This is joint work with Denis Bonnay.)

20/9 Ali Enayat (Göteborg) Interpretations and set theory (part 2)

This is a continuation of my earlier talk (7 September). In the first part of the talk, I will contrast the classical methodologies of internally building “new models from old models” in the realms of arithmetic and set theory. In the second part, I will present a detailed proof of the fact that no two consistent deductively closed extensions of Zermelo-Fraenkel set theory are bi-interpretable.

27/9 Fredrik Engström (Göteborg) Dependence and axiomatizations

The notion of dependence of variables in logical formulas, or equivalently the information-flow in semantic games corresponding to formulas, turns out to be very similar to notions of dependence used when designing relational databases. Dependence theory, the study of such dependence relations on relational databases, rose as an independent field of research in the 70’s with its heydays in the early 80’s. Later the interest in the field declined, partly due to some undecidability results. In this lecture I will start by giving an overview of dependence theory (in the context of relational databases), and its connection to logical games. In particular I will focus on questions regarding axiomatizations. I will end by presenting some fairly new results (joint with Kontinen and Väänänen) on the axiomatization of dependence logic with generalized quantifiers.

18/10 Claes Strannegård (Göteborg) Deduction, induction, and abduction with bounded cognitive resources

I will present a general computational model for solving reasoning problems with bounded cognitive resources. The model handles problems of deduction, induction and abduction. It learns from positive and negative examples by searching for the smallest extension of its previous theory that enables all positive and no negative examples to be computable with bounded resources. I will go through several examples showing how the model can be used for solving simple problems of logic, mathematics, and functional programming.

24/10 Albert Visser (Utrecht) (Public Lecture 16:15 - 17:45 in T302) The semantics of fiction

Is fictional discourse really discourse? Or do we just pretend to be saying things? And if fictional discourse is indeed discourse, then what is its proper semantical treatment? I briefly discuss ideas of Frege, Montague and Kripke concerning these matters. Various tensions in Frege’s notion of Sinn can be brought out by considering his discussion of Sinn in fictional discourse. I sketch my own idea of the proper treatment. I claim that just like admiring Sherlock Holmes does not imply Holmes’ existence, neither does referring to Sherlock Holmes imply his existence. Thus, we can hold that “Sherlock Holmes’’ in “Albert Visser admires Sherlock Holmes’’ simply refers to Holmes, without committing ourselves to the conclusion that Holmes exists. This opens the road to a naive treatment of the semantics of “Albert Visser admires Sherlock Holmes’’.

25/10 Albert Visser (Utrecht) Feferman’s Theorem

Feferman’s Theorem tells us that we not only have the underivability of consistency but also the interpretability of inconsistency. In the talk I introduce Feferman’s Theorem and discuss various proofs. I will show that Feferman’s Theorem has a converse. Very roughly, not only is inconsistency interpretable but everything that is interpretable is —in a sense that will be explained— an inconsistency. I briefly explain how Friedman’s result that the disjunction property implies the numerical existence property blocks Feferman’s Theorem in the constructive case. The proper constructive analogue of Feferman’s Theorem is an open problem. Finally, I discuss two interesting extensions of theories connected to Feferman’s Theorem: the Krajíček theory and Jeřábek intrinsic extension. The Krajíček theory provides an example that the schematic logic of a theory can be complete Π2. Jeřábek’s intrinsic extension illustrates that if we force a Nelson-style program of theory extension based on interpretability to yield a unique result, then the result of this systematic extension contains, strangely enough, lots of inconsistency statements.

1/11 Ole Hjortland (LMU, Munich) Logical Inferentialism and the Context of Deducibility.

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

8/11 Martin Kaså (Göteborg) Trial and error logics - something old, something new,…

This talk will present a mix of older and newer results on what I have dubbed “trial and error logics”. Consider it a report on work in progress. I will introduce and briefly philosophically motivate the basic framework - a logical language, where the predicate symbols correspond to “empirically decidable” trial and error classifiers, using the ordinary syntax of first order logic, but with an in-the-long-run-satisfaction relation now defined relative to certain ω-sequences of ordinary models.

There is a standard translation from trial and error logic to FOL which, in combination with a lemma on how to extract omega-sequences from “generalized trial and error models”, will prove that the logic is compact and complete. Though obviously not decidable, it has a natural fragment (natural in the sense of having independent philosophical motivation) which can be given a finitary analytic tableau system, and hence is decidable. (The same fragment has also been given a complete proof system in natural deduction style.) Among the open questions is a prominent one that has eluded me for some time now, viz. whether the logic is compact or not if we allow uncountable vocabularies. The talk more or less corresponds to the outline of a paper I am in the process of writing.

14/11 The Lindström Lectures 2013 Wilfrid Hodges Ibn Sina on the foundations of logic (Thursday November 14, 2013. 16:00 - 17:30 in T302, Olof Wijksgatan 6.)

Ibn Sina (Avicenna, 11th century Iran) believed that the foundations of logic lie in metaphysics. He complained bitterly that this has led people to confuse logic itself with its foundations and dress up metaphysics as logic. His own description of the foundations of logic is in overtly ontological language. But from a modern perspective it becomes clear that in fact he is talking about methodological issues, like how to represent occurrences of a component within a compound, and whether the primitive notions of a theory should be stipulated from outside (as in Tarski) or incorporated into the objects (as in web ontology and object-based programming). This all has strong implications for any project to formalise Ibn Sina’s logic. My own readings of some key passages are different from the traditional metaphysical ones, and seem to me more intelligible and highly comparable with some modern metalogical and metalinguistic views; but then I have a deaf ear for metaphysics.

15/11 Wilfrid Hodges Ibn Sina on discharging assumptions in proofs

Ibn Sina (Avicenna, 11th century Iran) believed that the foundations of logic lie in metaphysics. He complained bitterly that this has led people to confuse logic itself with its foundations and dress up metaphysics as logic. His own description of the foundations of logic is in overtly ontological language. But from a modern perspective it becomes clear that in fact he is talking about methodological issues, like how to represent occurrences of a component within a compound, and whether the primitive notions of a theory should be stipulated from outside (as in Tarski) or incorporated into the objects (as in web ontology and object-based programming). This all has strong implications for any project to formalise Ibn Sina’s logic. My own readings of some key passages are different from the traditional metaphysical ones, and seem to me more intelligible and highly comparable with some modern metalogical and metalinguistic views; but then I have a deaf ear for metaphysics.

22/11 Zachiri McKenzie (Cambridge University) Extensions of NFU

NFU is a modification of Quine¿s ¿New Foundations¿ (NF) set theory, introduced by Ronald Jensen in 1969, which allows non-sets into the domain of discourse. Jensen was able to build models of NFU inside sub-systems of Zermelo-Fraenkel (ZF) set theory and show that NFU is consistent with the Axiom of Choice. In contrast, NF refutes Choice and the relative consistency question for NF has only recently been settled. In this talk I will describe the set theory NFU giving brief accounts of how models of NFU can be built inside ZF set theory and how subsystems of ZF can be interpreted in NFU. I will then discuss some natural axioms that extend NFU. I will survey some of the work that has been done toward determining the strengths of these extensions relative to subsystems and extensions of ZF.

29/11 Rasmus Blanck (Göteborg) Flexible formulas in arithmetic

In the early 1960s, Kripke introduced the concept of a flexible arithmetical formula. Roughly, a Σk formula P is flexible if the theory Q ∀x ( P(x) ↔ R(x) ) is consistent for every Σk formula R. Speaking model-theoretically, while P is empty in the standard model, there is another model of arithmetic in which P and R have the same extension. Recently (2011), Woodin has shown that, for extensions of PA, a uniform version of Kripke’s result holds for finite sets. In this talk we will discuss certain strengthenings of Kripke’s and Woodin’s results, sketch a “optimal” uniform flexibility result, and consider some obstacles in proving this result.

6/12 Hans Kamp (Universität Stuttgart) First-order reducible and non-first-order reducible parts of natural language

1. Formal semantics of natural language, as it has been practiced over the past half century following the work of Richard Montague, involves assigning terms of some ‘Logical Form Formalism’ (LFF) to expressions of the given object language (OL) as their ‘logical forms’. In each application of this method, LFF is given (I assumed given) as a logical formalism with its own syntax and, normally, a model-theoretic semantics, both of which are specified independently of OL. The model-theoretic semantics defines the relation of entailment relation between the sentences of LFF (viz. as the relation of logical consequence). The ntailmnt relation for LFF is to impose an entailment relation between the sentences of OL: OL-sentence A entails OL-sentence B iff the logical forms of A and B stand in the entailment relation that is defined for LFF.
2. One of the prominent features of Montague’s work, and of much of the Montague Grammar that followed in its wake, is that the logical forms assigned to certain sentence constituents are of higher type. For example: the logical forms of noun phrases are of the type of sets of properties; the logical forms of adjectives are of the type of functions from properties to properties. Nevertheless the logical forms assigned (‘compositionally’) to sentences of OL are often first order formulas of LFF, even if the logical forms of some of their constituents are not first order.
3. On the other hand the expressive power of even comparatively small fragments of natural language often extends beyond first order expressibility. (Examples of what can bring this about: plural noun phrases; non-standard quantifiers such as ‘most’; branching quantifiers; adjectival and adverbial modifiers.) Many sentences containing such constituents cannot have first order logical forms. Moreover, the entailment relation for such fragments is as a rule ‘essentially higher order’: it is not axiomatisable (i.e. not recursively enumerable).
4. There are also fragments OL, however, with some sentences whose logical forms are not first order, but for which the entailment relation is axiomatisable nonetheless. (This is so, for instance, for certain natural language fragments which are first order except that they allow for certain forms of adjectival modification.)
5. On the whole this rather complex and confusing situation, which leads to the following general questions:
   • Q1: Which fragments of a language like English have a tractable (i.e. recursively enumerable) entailment relation (even though some of their sentences have logical forms that are essentially not first order)?
   • Q2: What are the tractable fragments of powerful LFFs such as the typed lambda calculus or Montague’s Higher Order Intensional Logic, which are widely used in model-theoretic semantics?
   • Q3: How can we decide whether the logical form assigned to some particular sentence of OL is or is not essentially higher order (i.e. not equivalent to any first order formula of LFF)?

In the talk I will first outline the general architecture of model-theoretic semantics and discuss some of the linguistic phenomena that give rise to these questions. I will then describe a few formal results, mostly connected with adjectival modification. The talk will conclude with a more general conjecture, but - at least as of now - no conclusive confirmation for it.

13/12 Dora Achourioti (Amsterdam) An intensional notion of truth

We start by briefly reviewing two widely accepted `desiderata’ for formal theories of truth; 1) that truth should not be construed as an operator, 2) that, to the extent it is possible, truth should be formalised primarily so as to satisfy the T-schema. We argue that both norms are challenged as soon as one adopts a different starting point as compared to the standard practice of adding a truth predicate to a base theory or a single model. We choose as our model theory a family of models connected with homomorphisms and we define a satisfaction predicate. This is done by means of a co-recursive equation the solution for which is given by a greatest fixed point construction.

The so-defined satisfaction predicate captures an intensional notion of truth in that what is true at a certain stage depends on what is true at later stages. As such, this predicate has modal properties; in order to study these properties we introduce a modal operator which borrows its extension from the predicate. We provide a sound and complete logic for the semantics of this operator by an expansion of geometric logic with a non-normal S4 modal operator and we draw the philosophical conclusions in the light of these results. Time permitting, we will present an embedding of classical logic into geometric logic expanded with the intensional satisfaction predicate which gives some insight into the expressive power of the latter.

2012

3/2 Tor Sandqvist (KTH) Atomic Bases and Classical Logic. 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. The talk will be given in Swedish or English according to audience preference.

2/3 Paula Quinon (Lund) Funes the Memorious, Humpty Dumpty, and Natural Numbers. This paper describes how the concept of natural numbers can be conceived as inherited from the concept of computability understood as character manipulation. The idea is that `computation on strings of characters’ is a basic or primitive notion, which does not presuppose any other notion of computability and which does not presuppose an independent conception of natural numbers. On this basis, it is argued that natural numbers can be adequately characterized as abstract mathematical entities which can be named by strings of characters on which computations can be performed, in particular computations of addition and multiplication.

16/3 Sebastian Enqvist (Lund) Some problems concerning characterizations of fragments of FOL I will present a project I am currently planning, which will concern Lindström-style characterizations of relatively weak languages. Sofar I have mainly considered problems in the abstract model theory of modal languages, building on work by Maarten de Rijke and Johan van Benthem. They have obtained two characterization results for the basic modal languages, i.e. the normal modal logics without any additional axioms, valid for the class of all relational structures of a given similarity type. However, in most applications of modal logic a restriction is made to some subclass of models satisfying certain constraints. For example, the logic S5 corresponds to a restriction to models based on equivalence relations, and it is more natural to consider the system as a fragment of a first-order theory - the theory of equivalence relations - than as a fragment of first-order logic.

The results of van Benthem and de Rijke do not automatically transfer to cases like this. I will explain this in more detail and list some problems and directions for future research that I find particularly promising. The central theme that I wish to explore is under what conditions van Benthem’s and de Rijke’s results, possibly with some suitable modification, can be transferred to some restricted class of models. The results of de Rijke and van Benthem belong to a tradition where modal languages are viewed simply as well-behaved fragments of FOL, usually associated with the Amsterdam school. This naturally leads to considering characterization problems for other interesting fragments of FOL, an idea that has been taken up by Balder ten Cate, Johan van Benthem and Joukko Väänänen, and later by Martin Otto and Robert Piro. The last two authors have jointly proved a characterization result for the guarded fragment of FOL, which generalizes modal logic.

As in the case of modal logics there is a distinction to be made between fragments of FOL and fragments of first-order theories, and the latter perspective provides an interesting source of open problems. In particular it is natural in this case also to ask under what conditions the characterization of the guarded fragment remains valid for restricted classes of models.

30/3 Urban Larsson (Chalmers) From children’s games to the limits of computability We study two impartial heap games with simple rules capable of universal computation. An impartial game is a combinatorial game for which the two players have the same move options, a player not able to move loses and the other wins. For such games there is no element of chance nor any hidden information.

If the game is played on a finite number of positions, the outcome belongs to one of two classes, either N or P, meaning Next- or Previous player wins. Hence each terminal position is in P. A heap game is played on a fixed number of piles of matches (or tokens), each heap-size being finite, the players alternate in removing matches according to some given rules until one of the players cannot do so any longer. A classical children game is played on one heap of 21 matches, remove precisely one or two matches. This position is in P. The second player to move wins. (How?) For our first game, which is a generalization of such subtraction games to several heaps, we show that it is algorithmically undecidable whether two games have identical sets of P-positions. This part is joint work with Johan Wästlund. The second game is played on two heaps. It uses so called move-size dynamic rules (similar to those of a game called Imitation Nim, a restriction of the classical game of Nim) to emulate the patterns obtained from Wolfram’s rule 110 cellular automaton.

Matthew Cook recently proved that given fixed left and right repetitive initial conditions together with a central data pattern, the behavior of the rule 110 CA is in general undecidable. We explain how similar conclusions hold for our rule 110 game.

13/4 Øystein Linnebo (Birkbeck, London) The Potential Infinite. Aristotle famously distinguished the potential from the actual infinite, defending the former while rejecting the latter. Two millennia later, the subject was transformed by Cantor, whose rightly celebrated theory of actual infinities eventually led to the elimination of the notion of the potential infinite from contemporary mathematics. This article is an attempt to revive the notion, while holding on to important Cantorian insights. Accordingly, a version of the notion of the potential infinite is articulated, shown to do important explanatory work in set theory and its philosophy, and defended against some objections.

27/4 Denis Bonnay (Paris) Trust and Bayes (joint work with M. Cozic). How should an agent take into account the probabilistic opinion of other agents in a group? The traditional Bayesian answer would be to use Bayes’ rule and higher-order probabilities. In the 80′s, Lehrer and Wagner proposed a different and much simpler model based on the attribution of epistemic weights. These weights are meant to express degrees of trust and the corresponding update rule is a simple weighted averaging. Beyond its intrinsic simplicity, the interest of the model is to allow for a detailed study of the conditions under which agents may reach consensus by repeatedly updating on each other’s beliefs. However, the absence of a principled justification for their update mechanisms casted some doubts on the significance of the results. In this talk, I will discuss whether such a justification can be given and prove representation theorem for Lehrer and Wagner’s updates with respect to Bayesian updates.

11/5 Fredrik Engström (GU) Some recent results in dependence logic. I will present some new results on generalized quantifiers in dependence (and independence) logic. Part of these results are joint work with Juha Kontinen.

25/5 Vera Koponen (Uppsala) Incompleteness results for logics that are able to express properties of symmetry groups. This talk will be about incompleteness of every logic which is at least as strong as first order logic (FO) and which is able to express any one of the properties listed below (the list can be made longer); it follows that none of the properties can be expressed with FO. The proofs rely on results from random graph theory. I now clarify some of the notions involved. Let L be a model theoretic logic (a formal language together with a model theoretic semantics).

• If T is a set of L-sentences and S is an L-sentence, then S is called a consequence of T if whenever M is a model of T, then M is also a model of S.
• We say that L is compact if whenever T is a set of L-sentences and every finite subset of T has a model, then T has a model.
• A proof system for L is a set of sequences of L-formulas such that finitely many (possibly 0) of the formulas are marked “premisses” and all of these are sentences, and exactly one of the formulas is marked “conclusion” and this one is also a sentence.
• A proof system for L is called complete if whenever T is a set of L-sentences, S an L-sentence and S is a consequence of T, then there is a proof (a sequence from the proof system) with all (finitely many) premisses from T and conclusion S.
• We say that L is at least as strong as FO if for every FO-sentence S there is an L-sentence S’ such that for every FO-structure M, M is a model of S if and only if M is a model of S’.

THEOREM For P as in the list (and several other properties about automorphism groups) the following holds:

1. P is not expressible in FO.
2. If L is a logic such that L is at least as strong as FO and P is expressible in L, then L is not compact and L does not have a complete proof system.

List of properties P that a structure M may, or may not, have: Let k be any positive integer.

• “(If M is a graph then) M has at least (most) k connected components.”
• “(If M is a graph then) M is hamiltonian”’.
• “M has no nontrivial automorphism (i.e. M is rigid).”
• “M has an automorphism that moves at least (most) k element.”
• “M has an automorphism with at least (most) k orbits.”
• “The automorphism group of M is finite.”
• “The automorphism group of M has at least (most) k elements.”
• For any countable G: “G is a subgroup of the automorphism group of M.”

Finally we note that the notion of automorphism is closely connected with the intuitive notion of symmetry, and, indeed, automorphism groups are also called symmetry groups.

14/9 Ali Enayat (Washington) Varieties of Satisfaction Classes. This is a report of recent joint work with Albert Visser on new model-theoretic methods of constructing a diverse variety of satisfaction classes over nonstandard models of Peano arithmetic (and other sufficiently rich theories). I will also address the consequences of this work to questions related to conservativity and interpretability of axiomatic theories of truth.

Trial lectures for the professorship in logic
14/9 14:00-15:00: Ali Enayat (T307) When is Truth Definable?
18/9 14:00-15:00: Valentin Goranko (D404, Humanisten) Logics for multi-agent systems: an appetizer
19/9 14:00-15:00: Reinhard Muskens (T219) Reasoning, Meaning, and Model Search

5/10 Carlo Proietti A paraconsistent approach to the future contingents problem Supervaluationism holds that the future is undetermined, and as a consequence of this, statements about the future may be neither true nor false. Here we explore the novel and quite different view that the future is abundant: statements about the future do not lack truth-value, but may instead be glutty, that is both true and false. We will show that (1) the logic resulting from this ``abundance of the future’’ is a non-adjunctive paraconsistent formalism based on subvaluations, which has the virtue that all classical laws are valid in it, while no formula like “A and not-A” is satisfiable (though both “A” and “not-A” may be true in a model); (2) The peculiar behaviour of abundant logical consequence has a meaningful interesting parallel in probability logic; (3) abundance preserves some important features of classical logic (that supervaluationism does not preserve) when it comes to express those important retrogradations of truth which are presupposed by the argument de praesenti ad praeteritum.

19/10-21/10 Conference Numbers and Truth

16/11 Fredrik Engström On logicality, invariance and definability. The traditional account of what a logical consequence is says that A follows logical from T if for every reinterpretation of all the non-logical expressions in T and A; if all the sentences in T are true then so is A. This definition rests on the fact that we know how to distinguish between logical and non-logical expressions, this is the problem of identifying the logical constants. The talk will start with a general outline on logicality and logical constans and alternative ways of defining when an operator should be considered a logical constant. I will then focus on the model theoretic answer: An operator is a logical constant if it is invariant under the most general transformations.

I hope to be able to both give background material and some recent technical results (jointly with Denis Bonnay) on Galois correspondences between invariance and definability: The dual character of invariance under transformations and definability by some operations has been used in classical work by for example Galois and Klein. In this talk I will study this duality from a logical viewpoint and generalize results from Krasner and McGee into a full Galois correspondence of invariance under permutations and definability in $L_{\infty\infty}$. I will also present a similar correspondence for invariance under similarity relations and definability in $L_{\infty\infty}^-$, the equality free version of $L_{\infty\infty}$.

30/11–1/12 1st Informal Oslo-Gothenburg Workshop on Logic. The workshop will start Friday 30/11 at 1pm in Oslo and end with lunch on Saturday 1/12. If you would like to attend please send an email to fredrik dot engstrom at gu dot se.

Preliminary schedule:
Friday 30 November
13.30 - 14.50: Sam Roberts (Birkbeck and Oslo), Actualism, potentialism, and reflection principles
15.10 - 16.30: Martin Kaså (Göteborg) will talk on experimental logics
16.50 - 18.10: Claes Strannegård (Göteborg) on human reasoning and logic
19: dinner
Saturday 1 December
9.00 - 10.20: Henrik Forssell (Oslo) on logicality
10.40 - 12.00: Fredrik Engström (Göteborg) on logicality
lunch

14/12

1. Martin Filin Karlsson Model-theoretic semantics for quantification over absolutely everything there is. In this talk I develop, and philosophically motivates, a model-theoretic semantics within NFU_p, i.e. Quine’s NF with urelements and a primitive pairing operation. My motivation comes from investigations of the possibility of providing a semantics for absolute quantification, i.e. quantification over absolutely everything there is, and a subsidiary desiderata is that we should be able to prove the existence of sets of the objects falling under the semantic concepts defined in our theory. Thus, for instance, we will have a set of all models. I also show that a Henkin-style proof of completeness is possible. To some extent the work presented has been preceded by Feferman (197?, unpublished) in his project of providing a foundation for category theory. I will clarify what is new in my approach.
2. Martin Kaså A completeness proof in experimental logic. We introduce a simple language with predicates corresponding to “classifying machines”, changing their extensions over time (but with a limit). The language is given a model-theoretic semantics (using omega-sequences of FO models) and a proof system. A completeness theorem is proved – Henkin style.

2011

28/1 (K333) Nicholas Asher Extended Speech Acts In this talk I will give an overview of Segmented Discourse Representation Theory, a theory of discourse structure and interpretation. I will show its similarities and differences with respect to standard dynamic semantics, and then talk about my recent work with colleagues on empirical testing of certain aspects of the theory.

4/2 Fredrik Engström Generalized quantifiers in dependence logic We introduce generalized quantifiers, as defined in Tarskian semantics by Mostowski and Lindström, in logics using the Hodges semantics, e.g., IF-logic and dependence logic. For this we introduce the multivalued dependence atom and observe the similarities with the newly introduced independence atom.

18/2 Helmut Schwichtenberg Minimal from classical proofs Classical and intuitionistic logic can be seen as fragments of minimal logic. A useful consequence of this point of view is the following observation. Geometric implications are formulas of the form all x1 .. xn(B -> ex y1 .. ym(B1 or .. or Bk)) with B, Bi conjunctions of prime formulas. A well-known theorem of Barr says that for geometric implications Gamma, G, classical derivability of G from Gamma implies intuitionistic derivability. Call a formula A an extended geometric implication (EGI) if A contains positive implications only.

A typical example of a formula which is not an EGI is the premise of the Peirce formula ((P -> Q) -> P) -> P. We show that Barr’s theorem holds for EGIs as well. Moreover, for EGIs Gamma, G without disjunctions classical derivability of G from Gamma implies minimal derivability. Such extensions of Barr’s theorem are needed in algebraic applications, e.g., the non Noetherian version of Swan’s theorem in [Coquand and Lombardi, A logical approach to abstract algebra, MSCS 2006]. The proof is by an analysis of possible occurrences of stability axioms in natural deduction proofs in normal form; it gives an explicit quadratic algorithm.

4/3 Martin Kaså Attempts to improve on two theorems on experimental logic Declaration of content and general warning: This is (partly) a “working seminar” on unfinished work in (some kind of) progress. The first part will be repetition for some of you, where I introduce “experimental logic” as a satisfaction relation between formulas in FO syntax and omega-sequences of FO models and then prove countable compactness and axiomatizability of a basic version of this kind of logic, which comes from some fairly natural “parameter setting”. In the second part, I will discuss what I am working on right now - attempts to improve on the results from part one. Basically, I want to: (i) be able to say something about (non-)compactness in the uncountable case, and (ii) give a concrete (and neat) axiomatization of the experimental consequence relation. I may also briefly mention some other related stuff.

18/3 Christina Thomsen Thörnqvist Receptionen av Aristoteles Analytica priora i det antika och medeltida Västeuropa Redan under antiken var Aristoteles (384-322 f Kr) Första analytik ett av den västerländska filosofins mest lästa och kommenterade verk. Från 1200-talet och framåt intog verket en självklar och framskjutande plats i den medeltida skolastiken och kom att i många avseenden utgöra navet i den formella logikens vidare utveckling. Övergången mellan antiken och medeltiden var dock problematisk av flera skäl: Analytiken var försvunnen i Västeuropa under nästan 600 år – mellan 500-talets början och tidigt 1100-tal – och hur det gick till när verket plötsligt åter blev tillgängligt är i dagsläget inte känt. Därutöver gick en mycket stor del av de grekiska kommentarerna till Första analytiken förlorade innan medeltidens början samtidigt som de bevarades indirekt i den latinska traditionen och därmed kom att utöva ett avgörande inflytande på den efterantika förståelsen av Analytiken. Seminariet ägnas åt en kartläggning av receptionen av Första analytiken i denna kritiska övergång bl a genom läsning av några nyckelpassager i verket tillsammans med motsvarande avsnitt i centrala grekiska och latinska kommentarer.

1/4 Paula Quinon Computational structuralism The objective of this talk is to present a view in philosophy of mathematics called ‘computational structuralism’ ([Halbach-Horsten 2005], [Quinon-Zdanowski 2007]). Computational structuralists claim that natural numbers are precisely the mathematical entities, which people use for counting and computing. Using Tennenbaum’s theorem they show that the computability assumption only is sufficient for singling out the class of recursive standard models of arithmetic (called the intended models). However, computational structuralism encounters several philosophical and formal difficulties. After a detailed presentation of the argument, we are going to address these issues, showing the possible ways out and pointing out the open problems.

15/4 Sean Walsh Comparing Peano Arithmetic, Basic Law V, and Hume’s Principle In this talk we present new constructions of models of Hume’s Principle and Basic Law V with restricted amounts of comprehension. The techniques used in these constructions are drawn from hyperarithmetic theory and the model theory of fields, and formalizing these techniques within various subsystems of second-order Peano arithmetic allows us to put upper and lower bounds on the interpretability strength of these theories and hence to compare these theories to the canonical subsystems of second-order arithmetic. [Slides in pdf]

29/4 Jakub Szymanik Characterizing Definability of Second-Order Generalized Quantifiers in Natural Language We present some results on the definability and complexity of the second-order generalized quantifiers and discuss how they relate to collective quantification in natural language. In particular, we show that the question whether a second-order generalized quantifier Q_1 is definable in terms of another quantifier Q_2 reduces to the question if for a certain first-order encoding of the quantifiers: Q_1* is definable in FO(Q^_2*,<,+, x). We use our characterization to show new definability and non-definability results for second-order generalized quantifiers. For example, we prove that the collective majority quantifier is not definable in second-order logic. Moreover, we introduce the second-order generalized quantifiers to the study of collective semantics and compare it with the type-shifting approach. We suggest that some collective quantifiers might not be realized in everyday language due to their high computational complexity. The talk is based on the joint work with Juha Kontinen.

13/5 Tommi Salo Defining Well orderings in model theoretic logics We will discuss the expressiveness of some extensions of first order logic, measured by the ability to define certain classes. We also introduce a partial ordering on logics, related to expressiveness. The central concepts are definability of classes of ordinals and the well-ordering number. Of great interrest related to this is a result by Lopez-Escobar about the non-definability of the class of well orderings in finite quantifier languages.

Logic related upcoming events:

8/6 Jörgen Sjögren Concept formation in mathematics PhD-thesis defend.

10/6–12/6 Filosofidagarna

13/6 Rasmus Blanck Metamathematical fixed points Licentiate thesis defend. The thesis. The defense will be at 10:15 in T219. Peter Dybjer will be opponent.

30/9 Fredrik Engström Logical constants as uniquely definable quantifiers Recently Feferman proposed a, what he calls, combined model theoretic and inferential criteria for logicality. I will try to give a bit of background and present his proposal.

14/10 Gunnar Adamsson Isomorphisms of diagonalizable Lindenbaum algebras Gunnar will present his thesis for the degree of Magister.

28/10 Symposium Ursi This is a symposium in honor of Björn Haglund on the day of his retirement. See the webpage of this event (only in Swedish).

11/11 Juha Kontinen Complexity results for dependence logic Dependence Logic is a new logic that incorporates the concept of dependence into first-order logic. The expressive power of dependence logic coincides with that of existential second-order logic, and the complexity class NP over finite structures. We review some recent results regarding the expressive power and complexity of certain fragments and extensions of dependence logic.

25/11 Fredrik Engström On numbers and games. Conway invented the surreal numbers in the beginning of the 70’s. These are numbers naturally evolving from an abstract notion of games. They were made popular in Knuth’s 1974 book “How Two Ex-Students Turned on to Pure Mathematics and Found Total Happiness”. It turns out that the field of surreal numbers include such different number systems such as the ordinals, the real numbers and infinitesimals. In this talk I will give a basic introduction to surreal numbers and games, more or less following Conway’s 1976 book “On numbers and games”.

9/12 Ulf Norell Agda for logic modelling. I will give a hands-on introduction to Agda, a dependently typed programming language/proof assistant. As an example we will model and play with some simple logics in Agda.

2010

29/1 Palle Leth Frege om predikatreferens Freges tes att predikattermer har Bedeutung anses allmänt vara djupt problematisk. De flesta anser att Freges grund för tesen var hans övertygelse om att relationen mellan predikat och begrepp är analog med relationen mellan egennamn och objekt. Jag hoppas visa på att Freges texter i frågan inte ger något stöd för uppfattningen att en sådan analogi ligger till grund för hans tes att predikat har Bedeutung.

12/2 Ulf Persson Platonism and Mathematics For some reason Platonism is considered something of a dirty word in philosophy, a symptom of rigid naivity, and something people rather distance themselves from even if they advocate ideas essentially congruent with it. In the seminar I intend to champion mathematical Platonism in its interpretation as mathematical realism and discuss how to distinguish between the transhuman and human elements in mathematics, the failure of which I believe is the basis for much confusion that characterizes the ongoing debate. The talk is going to be predominantly speculative and philosophical in nature.

26/2 Denis Bonnay Modeling Inexact Knowledge Perceptual indiscriminability is typically intransitive. Given three shades of color a, b and c, it can well be the case that I am not able to distinguish between a and b on the one hand, b and c on the other hand, even though I can distinguish between a and c. In this talk, I will discuss two issues regarding this basic fact. 1) How does intransitivity impact the logic of (perceptual) knowledge? If perceptual indiscriminability is directly taken to generate an accessiblity relation between epistemic alternatives, intransitivity will yield failure of positive introspection: my knowing that p is not sufficient for my knowing that I know p. 2) Where does intransitivity come from? Telling whether two shades or color are identical or categorizing a shade of color as orange or red can be construed as a decision task. Why does decision lead to intransitivity? Can we build psychologically plausible models of the inexactness of our perceptual knowledge. In connection with 1), I will argue that introspection can be recovered on intransitive models. In connection with 2), I will show how signal detection theory can provide the basis for fine-grained logical models. The talk is based on a series of papers co-authored with Paul Egré. In particular, “Knowing one’s limits”, to appear in Dynamic Epistemology: Contemporary Perspectives, O. Roy, P. Girard and M. Marion (eds) and Section 4 of “Vagueness, Uncertainty and Degrees of Clarity” forthcoming in Synthese

12/3 Jesper Carlström Formal logic in railway signalling applications. Prover Technology AB applies formal logic to design and verification of railway signalling systems. The main product is Prover iLock, a Windows program with a graphical user interface that allows a signalling engineer to define a railyard by drawing tracks with the mouse, and then automatically generate an interlocking system that can also be formally verified in the same tool, or by an independent tool. I will outline the process and discuss the problems encountered when academic ideas meet the down-to-earth demands of our customers. (Jesper doktorerade i matematik (logik) för Per Martin-Löf vid Stockholms universitet. Han disputerade 2005 och är nu utvecklingsledare på Prover för logikspråket PiSPEC. Detta används för att specificera logiken i ställverkssystem.

26/3 Jan Smith Hume, Kant, Darwin, and the rules of logic. Hume’s crucial observation that there is no direct evidence for causality opens up for an evolutionary understanding of causality. I will also argue that in an evolutionary perspective, the rules of logic play a similar role as causality.I will not rely on any result in biology, except that the gene-centered view of evolution has in general broadened the scope of evolutionary explanations. Rather, I will corroborate my claims by Kant’s view on causality and Aristotle’s on the rules of logic.

9/4 Dag Westerståhl Compositionality and Context Does the fact that linguistic communication is strongly context-dependent constitute a threat to the idea that natural languages are compositional? To many, it clearly does. But what exactly is at stake here? In this talk I try – after a brief introduction to compositionality – to sort out some of the issues by (a) distinguishing different kinds of context dependence, (b) distinguishing different kinds of semantic values (meaning, content, extension, etc.) for which the issue of compositionality may arise, (c) noting that for many of these values, the concept of compositionality has to be adapted to the presence of contextual arguments, and that there are at least two different ways of doing this, and (d) explain the logical relations between the resulting notions of compositionality. I will also sketch an approach to linguistic context dependence (this is joint work with Peter Pagin), and as an illustration explain how it can be used to give a straightforward account of pure quotation which is compositional in the relevant sense.

30/4 Dennis Bonnay The generality of logic and the problem of logical constants To account for our informal notion of logical consequence, it is not sufficient to provide a conceptually motivated definition of logical consequence. The definition of logical consequence has to be supplemented with a conceptually motivated division between logical symbols and extra-logical symbols. In connection with the problem of motivating this divide, the main aim of this talk is to investigate two related ideas. The first one is that being a possible interpretation for a logical constant amounts to satisfying some invariance criterion. The second one is that such a characterization can be vindicated by appealing to the generality of logic. I will present the first characterization of this kind given by Tarski himself in 1966, as a late follow-up to his 1936 paper on logical consequence. No matter how attractive the simplicity of Tarski’s proposal is, the analysis of generality in terms of invariance has proven to be more involved than Tarski had thought. So I will develop on an objection to Tarski’s analysis and recall an alternative characterization I have given which aims at fixing the problem. The corresponding invariance criterion has recently been challenged by Feferman in 2009. In the final part of the talk, I argue that Feferman’s criticisms can be met by redesigning the framework for invariance. This is shown to yield an invariance characterization of first-order definable operations, which can be justified in terms of generality.

7/5 Aarne Ranta Logic, Semantics, Translation, and Universal Grammar That languages have a common semantical foundation in logic is an old idea. In a letter to Mersenne in 1629, Descartes proposed a universal formal language that would serve as the basis of translation between languages; this idea was developed further by Leibniz in his “characteristica universalis”. In modern times, systems like UNL and SUMO are used as interlinguas for machine translation, much in the same spirit. On the other hand, critics like Sapir and Whorf have rejected the idea of a common semantical foundation of languages, and the main stream of machine translation is based on statistics on co-occurrences of words and phrases, with no reference to semantics; Google translate is an extremely successful example of this approach. In the talk, I will summarize the main arguments underlying the different approaches to translation. Then I will present an approach which, in a sense, builds on Descartes’s idea of a universal formal language, but takes into account the criticisms. The key idea is to distinguish between different levels of abstraction in language: on some levels, translation is clearly impossible, whereas on some other levels, it is clearly possible and the problems are technical rather than philosophical. The approach has been proven in several applications, and it is currently developed further in the European project MOLTO (Multilingual On-Line Translation).

21/5 Fredrik Engström Borelkvantorer och logiska konstanter Jag kommer att introducera Borelkvantorer och ge några tekniska resultat som kan ses om generaliseringar av Lopez-Escobars sats om invarianta Borelmängder. Jag kommer också koppla dessa resultat med den pågående debatten om logiska konstanter.

4/6 INSTÄLLT

10/9 Discussion Truth and provability II We will discuss the constructive/intuitionistic vs the classical views on the relation between truth and provability. This time we will focus on Panu Raatikainens paper “Conceptions of Truth in Intuitionism”, History and Philosophy of Logic 25 (2004).

The paper criticises the constructive/intuitionistic identification of truth and provability, and it is quite short. The interested reader may also consult: Per Martin-Löf, “On the Meanings of the Logical Constants and the Justifications of the Logical Laws”, Nordic Journal of Philosophical Logic, Vol. 1, No. 1, pp. 11-60. 1996. Online. (A thorough explanation from the constructivist/intuitionist side about the interpretation of the logical connectives.) and Cesare Cozzo (1994). What Can We Learn From the Paradox of Knowability? Topoi 13 (2):71–78 (A short paper claiming that Fitch’s paradox is based on a misinterpretation of the intuitionistic view, and suggests a more precise explanation of the relation between truth and provability, in order to avoid the paradox). If you cannot access the papers, please contact David Wahlstedt.

Monday 20/9 15:15 in T340: David Walhstedt Some Ramsey-like theorems in constructive logic and Brouwer’s thesis Please observe time, date and location. I am going to discuss some ideas about how to deal with Ramsey-like theorems in some constructive frameworks, and some aspects concerning Brouwer’s thesis on bars. I will present two different constructive interpretations of Ramsey’s theorem, by Theirry Coquand, and Vim Weldman and Marc Bezem, respectively. Using these ideas, we aim to reason constructively about termination of recursively defined programs.

8/10: Fredrik Engström Classification problems and models of arithmetic. I will introduce Borel reductions of equivalence relations. They are used to say how “hard” a certain classificaction problem is. This will then be used to prove theorems saying that the classification problems of countable models of arithmetic are hard indeed. The seminar will start from the very beginning of Borel reducability and end up in a recent paper by Coskey and Kossak.

22/10 (T307): Truth and provability III: Dag Prawitz Truth and proof: ontological or epistemic concepts? The talk will deal with how the concepts of truth and proof are to be conceived in a constructive or intuitionistic setting. I shall discuss in particular how this question has been answered by early intuitionism and by Martin-Löf in different phases of his work and shall conclude by sketching an alternative view.

29/10: Denis Bonnay Truth and dependence (joint work with F. van Vugt) Truth may yield paradoxes and Tarski showed how widespread the problem is by proving that no sufficiently rich classical language can contain its own truth definition on pain of inconsistency. In order to tackle with the semantic paradoxes, one should obviously try and understand which features of sentences are responsible, together with occurrences of the truth predicate, for the reported misbehavior. But the same question can be asked from a dual perspective. Some sentences, including sentences containing the truth predicate, are clearly unproblematic: why is it that they are immune to the semantic paradoxes? Following a widespread intuition, unproblematic sentences are such that their value ultimately depends on how the world is like.

The truth-value of (3) “Emily Dickinson was born in Amherst” directly depends on where Emily Dickinson was born. When evaluating (4) “The sentence `Emily Dickinson was born in Amherst’ is true”, we are led again to evaluate (3). Hence the truth-value of (4) depends, albeit indirectly, on where Emily Dickinson was born. To put it roughly, a sentence should considered grounded if its truth value can be established regardless of the truth or falsity of other sentences, or if its truth value can be established based on the truth or falsity of other sentences that are, themselves, grounded.

In the talk, I will compare two ways of making this precise: the “classical” account of groundedness, due to Kripke, and a more recent proposal by Leitgeb. These two accounts differ in the approach they choose. Kripke’s notion of groundedness is a by-product of the fixed-point construction aimed at characterizing the extension of the truth-predicate. By contrast, groundedness is Leitgeb’s primary target, which is to be attained by means of a fixed-point construction using a notion of dependence. However, one might hope that the two accounts are extensionnally equivalent, if there is one “right” notion of groundedness. But they are not. I will show that the difference is due to three parameters, some of which are extrinsic to the notion of groundedness, some of which are more intrinsic. By setting these parameters alike, one can show that the direct and the indirect route are, after all, equivalent.

19/11: Reiner Hähnle Abstract Interpretation of Symbolic Execution with Explicit State Updates. Systems for deductive software verication model the semantics of their target programming language with full precision. On the other hand, abstraction based approaches work with approximations of the semantics in order to be fully automatic. We designed a uniform framework for both fully precise and approximate reasoning about programs. Specifically, we present a sound dynamic logic calculus that integrates abstraction in the sense of abstract interpretation theory. Then we apply the approach to the analysis of secure information flow.

26/11 (T340): Thierry Coquand Ramsey’s Theorem in intuitionistic mathematics The usual infinite version of Ramsey’s Theorem is clearly not valid intuitionistically, since even in the simple case where we color the set of natural numbers in two colors in a recursive way, one cannot even decide which color will appear infinitely often. We present a method to analyse this situation from a constructive point of view, and possible constructive versions of this theorem, as well as its so-called clopen generalisation.

17/12 (T340): Gunnar Johansson Mereology, the basics. An introduction to mereology, by some seen as an ontologically neutral alternative to set theory, being the study of parts, wholes and their relation, some of its history, and some of the philosophy that goes along with it. I will try to say something of the benefits of different systems, and what some of the philosophical implications may be for having or not having atoms, arbitrary mereological sums and extensionality. In short, elementary mereology and an introduction to the subject.

2009

6/2 Claes Strannegård Reasoning Processes in Propositional Logic A computer-based experiment was conducted in which eight participants were asked to determine whether 80 randomly generated formulas of propositional logic were tautologies. The participants were all male in the age span 23-43 years and all of them had undergone training in propositional logic at university level. In each trial a propositional formula was presented to the participant. A time-limit of 45 seconds applied to each trial and no aids were allowed. For each trial, two aggregated psychological measures of difficulty were used: (i) the proportion of the participants who answered the trial correctly, and (ii) the average response time among the participants who gave correct answers. To model these psychological measures a cognitive architecture for propositional reasoning is defined. The cognitive resources are modeled according to the memory model of Atkinson and Shiffrin and features declarative memory, sensory memory, working memory, and procedural memory. Propositional reasoning is modeled on the basis of the state transition model of Newell and Simon. Specific proof systems for showing validity and non-validity with limited cognitive resources are defined. Our results indicate that the length of the shortest proofs in these proof systems is a substantially better predictor of both of the above psychological measures than is formula length.

6/3 Jens Allwood Feedback, coactivation and coconstruction in dialog

20/3 Jörgen Sjögren Explications, Abstract Objects, and Structuralism

27/3 Fredrik Engström Logiska operatorer i Dependence logic Jag kommer presentera ett förslag till ett allmänt ramverk för semantik av (logiska) operatorer i “Dependence Logic” (DL). Arbetet är pågående och de få resultat som kommer presenteras är som mest preliminära. Syftet är att ramverket sedan skall användas för en invariansanalys av (logiska) operatorer i DL. Ingen kunskap om DL förutsetts.

17/4 Denis Bonnay Definability and invariance in infinitary logic without equality I will present some strengthening of the connection between infinitary languages and invariance criteria for logical operations, as a generalization of an (old) result by Marc Krasner on definability in infinitary logic and groups of automorphisms. Krasner showed that, given a set M, there is a one-one correspondence between sets of operations on M which are closed under definability in L{\infty,\infty} and groups of permutations on M. Independently, Solomon Feferman asked in which logical language operations invariant under strong homomorphisms were definable (I will define precisely what a strong homomorphism is). I show that Feferman’s question can be answered by generalizing Krasner’s theorem, so as to get a one-one correspondence between sets of operations closed under definability in L{\infty,\infty} without equality and monoids of homomorphisms.

24/4 Thierry Coquand An introduction to constructive mathematics After a description of the historical background I will try to explain how constructive mathematics is thought of by constructive mathematicians (Bridges, Lombardi, Richman, …) as mathematics developed using intuitionistic logic. I will then try to survey some works in constructive algebra and analysis.

15/5 Anton Hedin Formell Topologi, Generaliserade Reella Tal, och Intervall-analys Jag kommer att ge en kort introduktion till formell topologi, vilket är en konstruktiv (och predikativ) presentation av Locale-teori, mer känt som punktfri topologi. Som ett exempel kommer vi se hur de reella talen R definieras som ett formellt rum. Genom att använda en typ av kompaktifiering kan man bädda in R i en utvidgning R_p som, förutom de reella talen, bland annat innehåller representationer av slutna intervall [a,b] (a,b reella tal). Vi kommer också att se ett utvidgningsresultat för kontinuerliga funktioner vilket öppnar för möjligheten att använda R_p som en domän för intervall-analys.

(29/5 Göran Sundholm Making sense of truth-values; Frege in mysterious circumstances Göran Sundholm kommer att hålla ett föredrag på datavetenskap på Chalmers. Tid 10:15 i EDIT-huset, sal ES51.)

5/6 Martin Kaså Palmé (OBS Nytt datum!) Experimental logics, mechanism and knowable consistency På detta arbetsseminarium vill jag ventilera och förbättra en av mina aktuella texter - ett (bitvis skissartat) utkast till en kort logisk-filosofisk artikel inom mitt avhandlingsområde. Som antyds av den preliminära titeln (rubriken ovan) anknyter det till den s.k. “Lucas-Penrose-tesen” (grovt sett: att Gödels (2:a) ofullständighetssats visar att det mänskliga medvetandet inte kan vara “mekaniskt” eller “algoritmiskt”). Dessa “gödelianska” argument är tämligen väl genomtröskade (och har övertygat mycket få) men här har vi en ny twist: jag kommenterar vilket eventuellt värde Jeroslows experimentella logiker kan ha för att kasta ljus över frågan - en tanke som finns hos Allen Hazen och Stewart Shapiro.

1/9 Johan Behrenfeldt Pumplemman: Hur naturliga språk kan klassificeras genom tillämpningen av pumplemman. Min magisteruppsats beskriver pumplemman från en lingvists perspektiv och hur de kan användas för att beskriva naturliga språk. I uppsatsen återfinns definitioner för och bevis av pumplemman för reguljära språk, kontextfria språk, trädfogande språk (tree adjoining languages) samt multipla kontextfria språk (multiple context-free languages). Grammatikerna som genererar dessa språkklasser beskrivs även kortfattat. Med hjälp av pumplemmana klassificeras ett antal formella språk. Den systematiseringen används för att beskriva de klassificeringar av naturliga språk som har hävdats av Chomsky (1957), Bar-Hillel and Shamir (1960), Postal (1964), Huybregts (1976), Manaster-Ramer (1987), Shieber (1985), Culy (1985) och Radzinski (1991). Motargumenten mot dessa påståenden presenteras även de. Uppsatsen visar på att det finns starka bevis för att placera naturliga språk utanför klassen av kontextfria språk och inuti klassen av milt kontextkänsliga språk.

25/9 Rasmus Blanck Some remarks on Reverse Mathematics as a partial realization of Hilbert’s Program Tillhörande text till seminariet finns som pdf

9/10 Peter Dybjer Program testing and constructive validity. I will discuss the connection between program testing and Martin-Löf’s meaning explanations for intuitionistic type theory. First I give a short overview of the historical development of the ideas behind the meaning explanations. Then I explain the connection with program testing. Finally, I will mention the possibility of pursuing the testing point of view for some other logical systems including impredicative ones.

23/10 John Cantwell Conditional and Possible Actuality I examine an argument recently put forward by Timothy Williamson that in the presence of an actuality operator (“It is actually the case that p”) the indicative conditional collpases into the material conditional. I provide two interpretations of the conditional where Williamson’s argument is shown to be invalid, an epistemic interpretation and an ontic interpretation. In the epistemic interpretation it becomes important to distinguish the de re interpretation from the di dicto interpretation of actuality. In the ontic interpretation I argue that if the world is indeterministic the definite description “the actual future” has an indeterminate reference in the sense that it is possible that the world will actually proceed in one way and possible that it will actually proceed in another way.

6/11 Sebastian Enqvist Interrogative belief revision in modal logic Belief revision theory is the study of rational theory changes with tools from formal logic. The standard framework for belief revision, called AGM, treats theory changes as functions defined, for a given input (a sentence to be learned or rejected), on epistemic states, traditionally represented as pairs (K,≤), where K is a logically closed set of sentences and ≤ is a preorder over K. The order ≤ represents the comparative degrees of entrenchment of members in K. Recently, in the paper “On the role of the research agenda in epistemic change” by Olsson & Westlund, 2006, this traditional model has been challenged. Olsson & Westlund argue that, in order to make certain crucial distinctions, we need to add a representation of the agent’s research agenda, and we need an account of how this agenda changes as our beliefs change.

Olsson & Westlund give a full treatment of agenda change in expansion (where only non-surprising information is received), while the problem of revision proper (with possibly surprising information) is left open. In earlier work, I have shown how to formalize Olsson & Westlund’s model in a modal object language, by extending known modal logics for belief revision (Krister Segerberg’s dynamic doxastic logic, and Giacomo Bonanno’s temporal logic of belief revision). In my talk, I will present this formalization. Also, I will present some work I have been doing since then, where I try to address the problem of proper revision and treat it once again in a modal logic.

20/11 Dag Westerståhl Back and forth between consequence relations and logical constants. The classical notion of logical consequence, in particular in Bolzano’s version with a given interpreted language, in fact defines a function from arbitrary sets of symbols to consequence relations (treating those symbols as constants). We look at the properties of this function, but also at functions that go in the other direction, extracting constants from a given consequence relation. The talk focuses on one such function, and the sense in which it can be seen as an inverse to Bolzano’s function. It is hoped that this sort of investigation will be relevant both for the abstract study of consequence relations and for our understanding of the notion of a logical constant. (Joint work with Denis Bonnay in the LINT project)

4/12 Sverker Lundin Hålet i pusslet Jag kommer att basera min presentation på en text med titeln: “The Missing Piece. An interpretation of Mathematics Education using some ideas from Žižek.” Här presenteras ett sätt att tänka kring relationen mellan matematikutbildning och matematik. Detta tänkesätt har, tror jag, relevans även för matematikfilosofi och logik men i vilken mån detta är sant är en öppen fråga som jag gärna vill ha hjälp från seminariedeltagarna att besvara.

18/12 David Wahlstedt Att rättfärdiga beräkningarna bakom konstruktiva bevis

I konstruktiv logik gör man distinktioner mellan begrepp som inte görs i klassisk logik. Ett godtyckligt påsteående kan inte bevisas konstruktivt endast genom att dess negation motbevisas. Istället kräver man en konstruktion som på ett direkt sätt övertygar om sanningen i påståendet. Ett konstruktivt bevis för att ett tal med en viss egenskap existerar, görs exempelvis genom att hitta ett sådant tal, eller genom att beskriva en beräkning som ger talet som resultat. För att konstruktivt bevisa en disjunktion, krävs att man har ett bevis för någon av dess delar. I konsekvens med detta, kan inte lagen om det uteslutna tredje bevisas konstruktivt.

Mitt kommande forskningsprojekt handlar om rättfärdigandet av konstruktiva bevis. Eftersom dessa bevis är algoritmer, måste det finnas ett argument för algoritmernas terminering. Om argumentet inte är konstruktivt, kan man ifrågasätta på vilket sätt det första beviset verkligen var konstruktivt. Man får en variant av konstruktivism besläktad med Markovs princip, där en obegränsad sökning med ett icke-konstruktivt termieringsbevis godtas som algoritm. I Martin-Löfs typteori låter man, i englighet med den s.k. Brouwer-Heyting-Kolmogorov tolkningen, typer representera påståenden, och element i typerna representera bevis.

Typteorin är ett funktionellt programspråk, baserat på typad lambdakalkyl och rekursiva datatyper, där härledningar liknar Gentzens naturliga deduktion, med introduktions- och eliminationsregler för datatyperna, som kan vara exempelvis naturliga tal. När man rättfärdigar Martin-Löfs typteori finns två icke-triviala termineringsrelaterade problem att handskas med. Det ena härrör från de rekursivt definierade reglerna, och behandlas traditionellt i Martin-Löfs typteori genom att man begränsar sig till primitiv strukturell rekursion. Det andra problemet härrör från den typade lambdakalkylen, och här brukar man använda metoden efter Tait/Gödel kallad “computability”. Riktigheten i denna metod vilar på vissa abstrakta objekt, så kallade reducerbarhetspredikat, som i sin tur måste rättfärdigas. Detta har aldrig gjorts fullt ut med konstruktiva metoder. Ett av mina mål är att undersöka hur detta skall göras, och vad det betyder när det inte görs.

2008

25/1 Minds, mechanical math and Hazen This talk aims to investigate the merits of a suggestion by philosopher A.P. Hazen that Jeroslow’s concept of an experimental logic is a better model for a computational mind doing mathematics than an ordinary formal system would be. Martin Kaså Palmé

8/2 Data mining-tekniker för concept description Jag kommer att prata om data mining-uppgiften concept description som syftar till att få fram tolkningsbara beskrivningar (modeller) av intressanta samband i en datamängd. En typisk situation är en datamängd där någon målvariabel (ofta kategorisk) skall förklaras i termer av ett stort antal attribut. Jag kommer att diskutera vilka kriterier en concept description-modell bör uppfylla och sedan göra en exposé över de studier vi utfört inom ämnet. Genomgången inkluderar de tekniker som använts, vilka problem som angripits, samt naturligtvis vilka resultat som uppnåtts. Särskilt fokus kommer att ligga på den egenutvecklade (enkla, men effektiva) algoritmen Chipper. Cecilia Sönströd (Borås Högsk)

22/2 Finite satisfiability of sentences of countably categorical theories I will discuss satisfiability in finite structures of sentences of countably categorical theories and how this is related to properties of “independence” and “amalgamation”, as considered in stability/simplicity theory of model theory. (For examples of notions of “independence”, the uninitiated reader can think of linear independence in vector spaces, or algebraic independence in algebraically closed fields.) Vera Koponen (Uppsala Univ)

14/3 Infinite time computations and infinite algoritms This paper is about infinite time Turing machines and the halting times of infinite time Turing machines with no input, that is, the clockable ordinals. It has a brief introduction to the two halting problems and to the oracle-concept. We examine the ordinals clockable by infinite time Turing machines with only one tape, and show that even more than was shown in (Hamkins and Seabold 2001) of the clockable ordinals, are clockable by a machine with only one tape. We also investigate the consequences of allowing the infinite time Turing machines to have an infinite amount of states in an infinite program. We show that the strength of such machines is the same as the strength of ‘ordinary’ infinite time Turing machines with real-oracles. (uppsatsseminarium) Anton Broberg

4/4 From consequence to constants, and back Bolzano, and later Tarski, defined a (logical) consequence relation =>_X from a set X of (logical) constants. In the opposite direction, I identify a set C^=> of constants from any given consequence relation =>, arguing that this is natural way to define (not necessarily logical) constancy. I investigate how these processes are related, in particular whether there is a Galois connection between them. Results so far are very tentative, and any comments or suggestions will be appreciated. (For those who know: The basic idea was presented in chapter 9.3 of Quantifiers in Language and Logic, but I now think the particular implementation suggested there was on the wrong track.) Dag Westerståhl

18/4 Introducerar “Dependence Logic” Seminariet har till syfte att introducera Dependence Logic som är en logik sprungen ur bland andra Hintikkas IF-logik. Jag kommer att presentera grundläggande definitioner och egenskaper hos logiken. Större delen av seminariet kommer att hållas på en grundläggande nivå. Fredrik Engström

9/5 Conditionals in Context Is everything you have learnt about formal semantics mistaken? Should notions such as “proposition”, “reference” and “possible worlds” be thrown out of formal semantics? I give a review of the book “Conditionals In Context” by Christopher Gauker, who proposes a radically novel basis for formal semantics. In the book, Gauker more specifically proposes a formal “context-logical” account of indicative and subjunctive sentences of English, which (in contrast to all existing accounts) yields correct judgements of validity for arguments involving conditionals.

The point of this is to show that Gauker’s “context-logical” account succeeds better than traditional possible worlds-semantics. He argue that the context-logical approach is better than the received view of semantics, both based on philosophical arguments and based on success of context-logical approach for describing the logic of conditionals. Staffan Larsson (Lingvistik)

23/5 Decomposing generalized quantifiers. This note explains the circumstances under which a type <1> quantifier can be decomposed into a type <1,1> quantifier and a set, by fixing the first argument of the former to the latter. The motivation comes from the semantics of noun phrases (also called determiner phrases) in natural languages, but here I focus on the logical facts. However, my examples are taken among quantifiers appearing in natural languages, and at the end I indicate two more principled linguistic applications. Dag Westerståhl

6/6 Terminsavslutning På självaste nationaldagen avslutar vi terminen med pompa och ståt. Vi firar med filmvisning, föreläsning, fika och (kanske) massa mer. Fredrik Engström

17/10 Some results on experimental logic The talk presents some results concerning compactness and axiomatizability of experimental consequence relations. Martin Kaså Palmé

3/11 (MÅNDAG!): Ickestandardbevis, en översikt Det är lätt att konstatera att ickestandardmodeller till PA innehåller ickestandardtal som (via någon gödelnumrering) kodar bevis i PA. Här ges en översikt av egenskaper hos dessa ickestandardbevis. Slutligen presenteras två artiklar av Hájek respektive Solovay, där två begränsningar av längden hos ickestandardbevis för inkonsistens visas med radikalt olika metoder. Rasmus Blanck

14/11 DialoGF: ISU-based dialogue systems in type theory In this talk I will present a type-theoretical dialogue manager. Ranta and Cooper have shown how to describe a simple form-based dialogue system as a type-theoretical proof editor. My PostDoc research has focussed on extending their ideas to cover more advanced dialogues. I have incorporated some ideas from Dynamic Syntax to be able to handle underspecified answers and sub-dialogues. I will show example dialogues which a type-theoretical dialogue manager can handle, and discuss how it relates with other Information State Update (ISU) approaches, such as the GoDiS dialogue manager. This seminar is about unfinished work, so I hope there will be lots of comments and a fruitful discussion… Peter Ljunglöf

28/11 A Contextualist Theory of Conditionals Indicative conditionals sometimes communicate that the consequent would follow causally or evidentially from the antecedent, and sometimes that it holds independently of the antecedent. On all standard accounts of indicatives, however, such relations of consequence and independence fall outside the content of conditionals. Instead, they are inferred pragmatically from the fact that a sentence with that content has been uttered.

This paper argues that this standard view is deeply problematic, and develops and defends relational contextualism, a view according to which indicative conditionals lack a complete literal content from which contents involving specific causal or evidential consequence or independence relations are pragmatically derived. Such specific contents are indeed pragmatically determined, but when they are, they constitute the primary communicative content of particular indicative conditionals. It is explained how relational contextualism not only does straightforward justice to our everyday understanding of indicatives and gives an attractive view of how we interpret them, but also, crucially, how it avoids various difficulties for contextualist theories of conditionals. Gunnar Björnsson

12/12 Consequence and constancy Every notion of (logical) consequence is tied to a notion of (logical) constant. For model-theoretic notions of consequence, which are just modern versions of Bolzano’s notion, essentially nothing more than identification of the constants is required. I look at two ways of doing that: the first — in terms of invariance — very briefly; the second — in terms of the consequence relation itself — in a little more detail. Dag Westerståhl

2007

2/2 On Explicating the Concept the Power of Arithmetical Theories Chaitin anger flera försök att explikera begreppet “the Power of Arithmetical Theories”. Dessa gås genom och det visas att inget av Chaitins förslag duger. En kortfattad redogörelse av det förslag jag konstruerade i lic-uppsatsen “Measuring the Power of Arithmetical Theories” ventileras också, samtidigt som några problem med detta förslag diskuteras. Slutsatsen är att det verkar vara omöjligt att konstruera en explikation av begreppet ifråga. Jörgen Sjögren

16/2 Om konstanta operatorer En universell operator u (av en viss typ) associerar med varje universum M ett objekt u*M (av denna typ). Typexempel är generaliserade kvantifikatorer. Fråga: Vad betyder det u är konstant över olika universa? Idé 1 (rigiditet): Det finns ett fixt objekt U sådant att u_M är begränsningen av U till M. Idé 2 (EXT): Om M delmängd av M’ så är u_M restriktionen av u*{M’} till M. Idé 3: Rigiditet och EXT är ungefär samma sak. Uppgift: Definiera och undersök dessa begrepp för operatorer av godtycklig typ. Problem: Definitionerna verkar vara något känsliga för vilket typsystem som används. Så det hela börjar med en presentation och jämförelse mellan (fyra) olika versioner av (enkel) typteori a la Church: relationell, funktionell, partiell, etc. Därefter en diskussion av hur ‘konstans’ lämpligen skall uppfattas. Dag Westerståhl

2/3 Beräkningsbarhet på topologiska rum via domänteori Domänteori ger en generell metod för att införa beräkningsstrukturer på godtyckliga topologiska rum. Jag kommer att försöka motivera varför domänteori är ett användbart och framgångsrikt verktyg inom beräkningsbar topologi, samt säga någonting om mitt eget arbete inom beräkningsbar distributionsteori. Fredrik Dahlgren

16/3 Deflationism and conservative truth theories

Conservativeness has been proposed as an important requirement for deflationary truth theories. This in turn gave rise to the so called ‘conservativeness argument’ against deflationism: a theory of truth which is conservative over its base theory S can’t be adequate, because it can’t prove that all theorems of S are true. Recently however Neil Tennant has argued, that some sort of a soundness claim can be incorporated in a deflationary theory in a legitimate way, so the conservativeness argument is not devastating. We will try to show that the problems confronting the deflationist are in fact more basic: even the observation that logic is true, or that truth is closed under provability, transcends the limits of a deflationary (i.e. conservative) truth theory. For that reason, Tennant’s argument turns out to be unsatisfactory. Our conclusion is that some version of the conservativeness argument still retains its force and presents a serious challenge, which hasn’t been met so far by the deflationists. Cezary Cieśliński

13/4 Reverse mathematics och dess filosofiska relevans Petter Johansson

27/4 Harel statecharts - teori och tillämpning Torbjörn Lager

11/5 En definierbar modell till ickestandardanalys Jag kommer att gå igenom Kanovei och Shelahs (2004) konstruktion av en definierbar modell till ickestandardanalys. All nödvändig bakgrund kommer att presenteras. Fredrik Engström

25/5 NF(U) - konsistens, ändlig axiomatisering och dess betydelse i semantiken för obegränsad kvantifiering

Ämnet för dagen är mängdteori, och närmare bestämt två system som i allmänhet anses vara en smula konstiga: Quines NF och Jensens NFU. Jag kommer mycket kort sätta in NF i ett historiskt perspektiv och säga något om välkända pro- och contraargument. NFU, dvs NF+urelement, är konsistent (Jensen 1969) och jag kommer uppehålla mig en stund vid beviset härav. Hailperin (1944) visade att NF är ändligt axiomatiserbar och detta gäller även för NFU. Jag presenterar en axiomatisering av NFU (har inte bestämt vilken ännu). Jag kommer också argumentera för att NFU bör ersätta ZF(C) i vissa sammanhang, nämligen när vi försöker göra reda för semantiken hos ett språk som tillåter absolut (icke begränsad) kvantifiering. Detta betyder att jag måste bemöta den kritik som finns, dels mot NFU och dels mot NFU som metateori. Martin Filin Karlsson

28/9 Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion

We present a variation of Martin-Löf’s logical framework with “beta-iota-equality”, extended with first-order parameterized algebraic data types and recursive pattern-matching definitions. Our contribution is a proof of normalization for the proposed system, from which we obtain decidable type-correctness. Our result holds under the assumption that the call relation of the recursive definitions is well-founded. Recursive definitions can be read as intuitive specifications, which makes it easier to understand their intended meaning, compared to definitions that use only pre-defined recursion operators, called elimination rules in type theory. Pattern-matching definitions can be seen as the underlying mechanism with which we describe elimination rules. The arguments used to justify recursively defined elimination rules are essentially the same as those justifying pattern-matching definitions. The use of pattern-matching takes the proof system closer to the look and feel of a programming language like Haskell or ML. We use the “Size-Change Principle for Program Termination” (C.S. Lee, N.D. Jones, A. Ben-Amram 2001) to establish that the recursive definitions have a well-founded call relation. The size-change criterion subsumes many known characterizations of terminating recursions, including primitive recursion and lexicographical ordering, but it also deals transparently with permuted arguments and mutual recursion. When instantiating the size-change relation for this criterion to be constructor decomposition, it corresponds closely to what we could call well-founded structural recursion. Davids avhandling. David Wahlstedt (Chalmers)

12/10 Easy and hard tautologies from the viewpoint of psychology Claes Strannegård (IT-uni)

26/10 Cryptography and the logical omniscience problem

An understanding of cryptographic protocols requires that we examine the knowledge of protocol participants and adversaries: When a participant receives a message, does she know who sent it? Does she know that the message is fresh, and not merely a replay of some old message? Does a network spy know who is talking to whom? Epistemic logic – the logic of “knowledge” – would therefore seem a natural framework for reasoning about the correctness of cryptographic protocols. However, any combination of epistemic logic and cryptography faces the so called logical omniscience problem: Cryptographic protocols concern knowledge in the sense of resource bounded knowledge, while in the standard semantics for epistemic logic, Kripke semantics, agents know all the logical consequences of what they know, including consequences that are infeasible to compute. In this talk, I show how it is possible to avoid logical omniscience through a rather small twist to standard Kripke semantics. I begin with some background on cryptographic protocols and the concrete (“grounded”) Kripke models for epistemic logic which are customary in computer science. Mika Cohen (KTH)

9/11 Logical Particularism

There is, traditionally, a presupposition of universalism in logic, noted already by Boole: “[…] the knowledge of the laws of mind does not require as its basis any extensive collection of observations. The general truth is seen in the particular instance, and it is not confirmed by the repetition of instances”. I aim in this paper to challenge this dogma, and instead argue that we should view particular inferences as the basic data of logic, and general logic laws as hypothetical generalizations of these, much as is done in empirical science. Because of this, I contend that formal languages, due to their inherent universality, may mislead us when we study logics, and that a partly lattice-theoretic and partly category-theoretic foundation would be preferable. Staffan Angere (Lund Uni)

23/11 Mathematical objects as figures of speech: On Yablo’s figuralism

The topic of this paper is a position in the philosophy of mathematics that has recently been put forward and defended by Stephen Yablo. The idea behind Yablo’s view, figuralism, is that mathematical language has many similarities with figurative or metaphorical language. If a metaphorical interpretation of mathematics can be plausibly argued for, it seems that this could be a way to account for the objectivity of mathematics without postulating a domain of abstract mathematical objects. Ebba Gullberg (Umeå Uni)

7/12 Is English really a formal language?

We propose a shift in perspective away from the view of natural languages as formal languages (encapsulated in the title of one of Richard Montague’s papers: “English as a Formal Language”). We propose that natural languages are instead to be seen as a collection of resources for constructing local languages for use in particular situations. This is suggested by the experience of constructing natural language grammars for particular applications using the Grammatical Framework developed by Aarne Ranta. It points to a research programme investigating how such resources play a role in linguistic innovation by agents constructing situation-specific local languages and how they can be made dynamic, modified by the linguistic agent’s exposure to innovative linguistic data. As an illustration of this we look at some cases of lexical innovation using coercion which have been discussed in the Generative Lexicon literature by Asher and Pustejovsky. Our approach uses type theory with records which appears to offer some conceptual advantages in the treatment of innovation. Is English really a formal language? The material for this talk will be drawn from two papers

• Natural languages as collections of resources
• Copredication, dynamic generalized quantification and lexical innovation by coercion

Robin Cooper (GU)

2006

3/2 Sanningssägare, fixpunkter och “riktig” självreferens Christian Bennet

17/2 Ett kontinuum av logiker mellan klassisk och intuitionistisk logik Petter R

3/3 Description Logic Björn Haglund

24/3 Hur nödvändig är matematiken vid förklaring av fenomen? Jörgen Sjögren

7/4 Om Jan Mycielskis pragmatiska mängdteori Christian Bennet

21/4 On the dispute between intuitionistic and classical mathematics Dag Westerståhl

5/5 Från typteori till stratifikation Martin Karlsson

19/5 Experimental compactness: some (hitherto) unsuccessful attempts. Martin Kaså Palmé

2/6 Kit Fines Class and membership - en Kopernikansk revolution? Martin Karlsson och Christian Bennet

1/9 On Rosser sentences and proof predicates It is a well known fact that the Gödel sentences of a theory T are all provably equivalent to the consistency statement of T, Con_T. This result is independent from choice of proof predicate. It has been proved by Guaspari and Solovay that this is not the case for Rosser sentences of T. There are proof predicates whose Rosser sentences are all provably equivalent and also proof predicates whose Rosser sentences are not all provably equivalent. This paper is an attempt to investigate the matter and explicitly define proof predicates of both kinds. Rasmus Blanck

15/9 Scottmängder, standardsystem och forcing Scotts problem handlar om att karakterisera standardsystem till modeller till FOA (Första Ordningens Aritmetik). Scott själv karakteriserade de uppräkneliga standardsystemen. Med en gränsövergång kan man också karakterisera alla standardsystem av kardinalitet \aleph_1. Eftersom standardsystem har högst kardinalitet kontinuum löser detta Scotts problem om vi antar kontinuumhypotesen. Vi skall presentera en ny infallsvinkel på problemet som använder sig av idéer från forcing. Fredrik Engström

6/10 Resource-bounded reasoning in first-order logic This paper presents a way of modeling human reasoning in first-order logic. Following a tradition in cognitive psychology, transition systems are used as the basic model for human reasoning. A proof system for first-order reasoning with bounded cognitive resources is presented. The system is a transition system and the proofs are computations in this transition system. Thus the proofs can be viewed as special kinds of reasoning processeses in a standard setting of cognitive psychology. It is shown how complexity measures that reflect the load on cognitive resources such as working memory and long-term memory can be defined on proofs. These complexity measures in turn generate relations of resource-bounded provability in a straight-forward fashion. Potential applications of such relations in the context of anthropomorphic theorem proving are described. The proofs of the system are both linear and local. Thus the system distinguishes itself, e.g., from Hilbert systems (in which proofs are linear but not local) and from Gentzen’s original systems of natural deduction (in which proofs are neither linear nor local). The system is shown to meet a number of desiderata pertaining to cognitive modeling. Claes Strannegård

20/10 Expansioner som undviker typer En modell M sägs vara rekursivt expanderbar om för varje teori T, i ett språk större än Ms språk, konsistent med Ms teori det finns en expansion av M som uppfyller T. Det visar sig att för en stor grupp modeller är rekursiv expanderbarhet samma sak som rekursiv mättning. Vi kommer att undersöka vad som händer med expanderbarhetsbegreppet när vi, förutom att uppfylla en teori, också undviker en typ. Fredrik Engström

3/11 Shavrukov: A note on diagonalizable algebras of PA and ZF Gunnar Adamsson

17/11 En generalisering av omega-regelnStudiet av expansioner som undviker typer leder på ett naturligt sätt till studiet av en logik som generaliserar omega-logik. Vi kommer att presentera denna logik, som vi kallar p-logik, och visa några enkla egenskaper. Seminariet kommer att hållas på en elementär nivå. Fredrik Engström

1/12 Temporala språk och formell verifiering Johan Mårtensson

15/12 Att bygga automorfier i modeller till FOA Ali Enayat har nyligen introducerat en ny teknik för att skapa automorfier till modeller till FOA. Vi kommer att presentera den nya tekniken, tillsammans med ett urval av de många satser som följer. Fredrik Engström

2005 Fall schedule

2/9 Negationsfritt bevis för Cantors sats, samt paradoxer ur ett kategoriteoretiskt perspektiv Christian Bennet

9/9 Orientering om kategoriteori och toposteori Christian Bennet

23/9 Boolos pluralsemantik för 2:a ordningens kvantifikation Martin Karlsson

7/10 Arbetsseminarium: Indispensability Jörgen Sjögren

21/10 Arbetsseminarium: Universell kvantifiering - relativism och absolutism Martin Karlsson

4/11 Arbetsseminarium: Experimentell kompakthet Martin Kaså Palmé

18/11 Data mining och ILP Björn Haglund

2/12 Arbetsseminarium: Fixpunkter och rossersatsers ekvivalens Rasmus Blanck

6/12 Aritmetikens modeller - en värld av möjligheter Fredrik Engström

9/12 Reflection principles and polynomial size proofs Joost Joosten

13/12 A guided tour of dynamic epistemic logic Barteld Kooi

16/1 Quine, Dummet and the grounds of deduction Tor Sandqvist

17/1 Logicality and invariance Denis Bonnay