The announcements are posted to a seminar mailing list. All people interested in the seminar and not belonging yet to the list can send an e-mail to "sara dot negri at helsinki dot fi" to be included among the recipients.
The research seminar in logic is primarily intended for the presentation of original research in logic by junior and senior researchers and by international guests. The detailed schedule of the seminar, with titles and abstracts of the presentations will be posted on this web page (see below).
Credits are acquired through regular attendance, active participation in the discussions and, when possible, a presentation at the seminar. The presentation can be based either on existing literature, to be agreed with the docent, or on original research.
The study attainments will be registered with the code 4036311 (Ffi330), but the course can also be used as such for 405381 (Fte345a) and for doctoral studies.
Please use Web Oodi for the registration.
22.3.2013: Sara Negri "Proofs and countermodels in non-classical logics".
1.3.2013: Joseph Vidal-Rosset (Universite' de Lorraine Nancy, France ) "User-friendly decision methods for intuitionistic propositional logic".
Abstract: Even if one can always contest that a decision method for mathematical logic is easier than another one, because such a judgment depends on the education received, it should be possible to agree on criteria for recognizing that such and such a method is more "user-friendly" than others. In the first part of this talk, we begin by listing these criteria, and go on by showing the Trees Proof Method for intuitionistic propositional logic of Bell, DeVidi, and Solomon: "Logical Options: An Introduction to Classical and Alternative Logics" (2001). We explain why, according to these criteria, this method is truly both a pedagogical means to learn what is at stake in intuitionistic logic, and a user-friendly indirect test for formulas. The second part of this talk is a work in progress on a direct test for intuitionistic logic, one that is neither a natural deduction system, nor a sequent calculus. We have noticed this surprising fact: even if every rule of Quine's algorithm for classical propositional logic ["Methods of Logic," pp. 33-40] - another user-friendly logical test - is correct in intuitionistic logic, no intuitionistic method, similar to that of Quine, seems to have been invented to date. A correct explanation of this fact stands in Gödel's result: "No truth-functional, faithful n-valued logic, for any fixed finite n, can provide a semantics appropriate for intuitionistic propositional logic." Nevertheless, we show that it should be possible to define a Quinean algorithm for intuitionistic propositional logic, in assuming that every propositional variable receives a valuation in the set ⊥, ω, ⊤ where ⊥ and ⊤ are respectively minimal and maximal elements, and ω just stands for the indefinite progression of truth-values. We show that, if such a method can be proved to be sound, it could help to understand some very subtle points in intuitionistic mathematical logic, and therefore be considered as a user friendly direct test for intuitionistic semantics.
8.2.2013: Jan von Plato "R.L. Goodstein as a disciple of Wittgenstein and Gentzen".
Abstract: The recent discovery of eight dictations by Wittgenstein as well as the centenary two months ago have brought Ruben Louis Goodstein (1912-1985) again to actuality. He studied philosophy under Wittgenstein and mathematics under Littlewood in Cambridge and is known mainly for two great achievements. The first is a "logic-free" approach to mathematics, a strictly Wittgensteinian influence, the second an amazing result, known as "Goodstein's theorem." He defined in very simple steps sequences of natural numbers that grow to astronomical dimensions, but then showed that they eventually go to zero. For the proof, he needed Gentzen's principle of transfinite induction that by Gödel's theorem is unprovable in arithmetic. In both of these works, Goodstein was strongly influenced by the comments of Paul Bernays, as is shown by their war-time correspondence: Criticisms made him tone down the Wittgensteinian polemics and to suppress the claim that his theorem is a Gödelian sentence.
25.1.2013: Sergei Soloviev (IRIT, Toulouse) "Some Reflexions on Applicarions of Graphs and Graph Transformations in Proof Theory".
Abstract: The purpose of this talk is to look at promising applications of graph rewriting to proof theory. First we recall some cases where graphs more complex than trees are used to represent infromation about derivations, e.g., graphs obtained from proof-trees when sharing of premises and subderivations is permitted, graph structures of the "proof-net" type, "parallel" derivations of "clusters" of judgements etc. We consider possible interest of such structures in case when not only derivability, but also equivalence of derivatons is studied. We consider the notion of coherence graphs, illustrating it by example of coercive subtyping. In this context we turn our attention to graph transformations and their applications to proof theory.
The announcements are posted to a seminar mailing list. All people interested in the seminar and not belonging yet to the list can send an e-mail to "sara dot negri at helsinki dot fi" to be included among the recipients.
30.3.2012: Iryna Khomenko (Kiew University) "History of logic in Ukraine".
23.3.2012: Workshop on Proof Theory and Constructivism
17.2.2012: Andrea Strollo "Deflationary truth and conservativity"
Abstract: Deflationism is a typical approach to the notion of truth in analytical philosophy. Its basic inspiration is the (anti)metaphysical idea that there is nothing deep about 'truth'. We need a truth predicate just to serve harmless syntactical operations (like disquotation or expressing infinite conjunctions and disjunctions). Recently the alleged unsubstantiality of the property has been clarified with the formal notion of conservativity. However, once conservativity comes in play bad news follow from it. It has been argued that since deflationism is bound to conservativity it cannot be an adequate theory of truth. The identification unsubstantiliaty/conservativity is now taken for granted but I'll show that this is a big mistake. Despite appearances a deflationary theory cannot be conservative.
3.2.2012: Annika Siders "Gentzen's first consistency proof with bar induction".
Abstract: This talk gives a clarification of Gentzen's first consistency proof, explicitly using bar induction to show the termination of the reduction. For each sequent in PA, a reduction is defined. The reduction reduces the sequent into another sequent, thus forming a root-first proof search in ω-arithmetic and it is shown that each reduction branch terminates in a sequent in endform. The endform means that either the succedent of the sequent is a true numerical equation, or the antecedent contains a false numerical equation. The proof that the reduction terminates explicitly uses bar induction when proving a Hilfssatz that the conclusion of a cut on two reducible sequents also reduces to endform.
20.1.2012: Carlo Proietti "Pluralistic ignorance"
2.12.2011: Alberto Naibo "Towards a verificationist account of classical propositional logic"
Abstract: Intuitionistic logic is usually reckoned to be the maximal system of logical rules justifiable adopting a verificationist point of view. An age-old problem concerns the possibility of extending this set of justifiable rules beyond intuitionistic logic; in particular, the compatibility between classical and verificationist principles is here taken into account. Grounding on a distinction between potential and actual truth proposed by Per Martin-Löf, it is argued that if verificationism accepts a similar distinction at the level of hypothetical reasoning, then it can also accept a particular classical inference rule, namely the Peirce rule.
11.11.2011: Patrick Girard "Being flexible about ceteris paribus reasoning"
Abstract: Ceteris paribus clauses in reasoning are used to allow for defeaters of norms, rules or laws, such as in von Wright \cite{Wright63}'s example ``I prefer my raincoat over my umbrella, everything else being equal''. In \cite{Girard08thesis,benthem_girard_roy:CP}, a logical analysis is offered in which sets of formulas Gamma, embedded in modal operators, provide necessary and sufficient conditions for things to be equal in ceteris paribus clauses. For most laws, the set of things allowed to vary is small, often finite, and so Gamma is typically infinite. Yet the axiomatisation they provide is restricted to the special and atypical case in which Gamma is finite. We address this problem by being more flexible about ceteris paribus conditions, in two ways. The first is to offer an alternative, slightly more general semantics, in which the set of formulas are only give necessary but not (necessarily) sufficient conditions. This permits a simple axiomatisation. The second is to consider those sets of formulas which are sufficiently flexible to allow the construction of a satisfying model in which the stronger necessary-and-sufficient interpretation of \cite{Girard08thesis,benthem_girard_roy:CP} is maintained.
21.10.2011: Fausto Barbero, " Relevance of declarations of independence in IF logic. Part II"
7.10.2011: Fausto Barbero, " Relevance of declarations of independence in IF logic"
Abstract: Independence-friendly (IF) logic is an extension of first order logic which allows expressing independence between quantifiers by means of a syntactical device (slash operator). We can extend the game-theoretical semantics of first order logic to IF logic if we associate to the new formulas appropriate games of imperfect information. The resulting logic has strong links with the existential fragment of second-order logic, but it also codifies new phenomena of a game-theoretical nature (for example, the "dual negation", signalling,imperfect recall). IF logic can also be extended to a probabilistic semantics by means of the game-theoretical notion of equilibrium. It has been observed in literature that the intuitive reading of some IF sentences is in contrast with the decourse of values wich is prescribed by semantics. In some circumstances, declarations of independence are superfluous (they can be removed from an IF sentence without changing its truth value). What are these circumstances? I will give a partial answer to this question, by providing syntactical characterizations of some of these phenomena, for both the basic and the probabilistic semantics. As a corollary, these results yield deduction rules for some peculiar classes of IF sentences.
23.9.2011: Jan von Plato, "The intuitionistic insights of Bernays and Gentzen".
Summary: The antagonism of Hilbert and Brouwer is well known.
How systematic is the dispute between formalism and intuitionism? It is suggested that
the other Goettingen proof theorists understood well the basic insights of intuitionism
and put them into use in their work, mainly in the search for consistency proofs. A great
part of this assessment is based on manuscript sources.
The announcements are posted to a seminar mailing list. All people interested in the seminar and not belonging yet to the list can send an e-mail to "sara dot negri at helsinki dot fi" to be included among the recipients.
30.4.2010: Ole Hjortland (Department of Logic and Metaphysics, Univ. of St Andrews), Proof-theoretic semantics and categoricity.
16.4.2010: Sara Negri, "Syntax and semantics in logical calculi".
Reading Seminar on Formal Epistemology (29.1--26.3):
26.3.2010: Jonas Rogger, two papers on epistemic paradoxes.
"Dynamic Epistemic Logic," by Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi.
5.3.2010: Markus Pantsar, Chapter 5, Epistemic Actions.
19.2.2010: Igor Deraj, Chapter 4, Public announcements.
5.2.2010: Raul Halki, Chapter 3, Belief Revision.
29.1.2010: Paolo Maffezioli, Chapter 2, Epistemic Logic.
15.1.2010, Sergei Soloviev (IRIT, University of Toulouse), "Asymmetric Games and Game Semantics".
Abstract: Traditionally, in game semantics for logics, the idea is to construct a game for each formula such that the existence of winning strategy for one of the partners (often called "verifier" and "falsifier") corresponds to the truth value of this formula. We want to explore another idea: assume that there is a game related to a formula (we consider the games where the strategies are algorithms), and the truth value is derived from the result of this game. How an asymmetry in this game may influence the derived truth value? For example, there is an asymmetry of computational power of "verifier" and "falsifier", e.g. one can compute some universal function for the class of all strategies of its opponent. This is work in progress, based on some earlier theorems about algorithmic strategies in certain asymmetric games obtained by the author.
20.11.2009, Carlo Proietti, "Intuitionistic epistemic logic".
16.10.2009, Raul Hakli, "On the Role of Knowledge in Belief Revision".
Abstract: The theory of belief revision studies changing the epistemic state of a
rational agent upon receiving new information. Traditionally, new
information has taken to have priority over previous beliefs: If the new
information contradicts with what the agent believes, the previous
beliefs are revised so that the content of the new information can be
consistently believed. We study belief revision in a setting in which
the agent can have knowledge as well as beliefs. If the new information
contradicts with the agent's knowledge, it must be false and cannot be
accepted as such, but simply rejecting it may not be rational either for
something may still be learned from it. We suggest a method of
accommodative revision in which the incoming information is first
revised by the knowledge of the agent, and then the beliefs of the agent
are revised using this modified input. The properties of the method are
studied and examples of its use are given. We shall also briefly
consider what the agent should reply to the other agent who was the
source of the false information. This is joint work with Satu Eloranta,
Olli Niinivaara, and Matti Nykänen.
2.10.2009, Giuseppe Primiero (Ghent University): "Epistemic possibilities for constructive reasoning with open assumptions", abstract
25.9.2009
Giuseppina Ronzitti, "Counting, intuitionistically".
Brouwer [1918, 1925] introduced several "predicates of
countability". His notions are reviewed in Heyting [1929].
The classical definition of "countable set" as "embeddable into
the set of natural numbers" intuitionistically splits into several non-equivalent notions.
References:
L.E.J. Brouwer (1918) Begründung der Mengenlehre
unabhängig vom logischen Satz vom ausgeschlossenen Dritten.
Erster Teil: Allgemeine Mengenlehere. KNAW Verh. 1e sectie.
L.E.J. Brouwer (1925) Zur Begründung der intuitionistischen
Mathematik. I. Mathematische Annalen, 93.
A. Heyting (1929) De Telbaarheidspraedicaten van Prof. Brouwer,
Voordracht, gehouden voor het Wiskundig Genootschap.
G. Ronzitti (2002), On the cardinality of a spread, Ph.D. Thesis, University of Genoa.
G. Ronzitti (2005) On some difficulties concerning the definition of
an intuitionistic concept of countable set, The Logica Yearbook 2003.
11.9.2009 Jan von Plato, "The point of intuitionistic geometry".
The announcements are posted in the departmental mailing list. All people interested in the seminar and not belonging to the list can e-mail us to be included among the recipients.
24.4.2009 Jan von Plato "Gentzen's program", Discussion and comments by Roy Dyckhoff and Panu Raatikainen
27.3.2009 Annika Kanckos, "Gödel's Dialectica interpretation in natural deduction".
20.3.2009 Sara Negri, "Proof analysis in intermediate logics".
Abstract: Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by geometric implications. Each of these logics is embedded by the Goödel-McKinsey-Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the explanation of the rules. (Based on joint work with Roy Dyckhoff).
13.2.2009 Jan von Plato, "Proof analysis in Aristotle's deductive logic".
Summary: Aristotle's deductive logic, as presented in his book Prior Analytics, is a system of rules of proof. Formal proofs (derivations) in Aristotle's system are presented so that a complete command over their structure is gained. In particular, it is shown that derivations can be so transformed that steps of indirect proof are applied at most once as a last rule, the only way in which Aristotle used indirect proof.
30.1.2009 Roy Dyckhoff, "The correspondence between cut-elimination and normalisation".
Abstract: Zucker and Pottinger in the 1970s examined the question (posed by Kreisel) of the relationship between cut-elimination and normalisation for intuitionistic logic (using all the propositional connectives). Zucker observed that, when disjunction is considered, Gentzen's cut-reduction system is not even strongly normalising (SN) (and the reductions don't translate to normalisation steps); Pottinger showed that (for a sequent calculus without either a primitive, or even an admissible, contraction rule) every cut-reduction translated to zero or more normalisation steps, but left the issue for standard sequent calculi (such as G3i) unclear. We reconsider this issue, and present a complete and SN cut-reduction system for G3i, comprising reductions whose images under the standard translation to natural deduction consist of finite sequences of reductions. The proof of this latter fact has been formalised in Nominal-Isabelle by my student Peter Chapman (joint work with Christian Urban); formal proofs of the other claims are still being developed.
23.1.2009: Ryan Bissell-Siders, "On the Theory of Linear Order".
28.11.2008: Giuseppina Ronzitti, "Stenius on antinomies".
14.11.2008: Bianca Boretti, "Finitary and infinitary proofs for linear discrete time", abstract
26.9.2008: Jan von Plato, "Axiomatic logic".
12.9.2008: Gabriel Sandu, "Dependence and independence in logic: IF logic".
The announcements are posted in the departmental mailing list. All people interested in the seminar and not belonging to the list can e-mail us to be included among the recipients.
2.5.2008: Panu Kalliokoski, "Mutual consistence of inductive consequences".
25.4.2008: Ahti Pietarinen, "IF Epistemic Logic (part II)".
18.4.2008: Ahti Pietarinen, "IF Epistemic Logic".
14.3.2008: Rudolf Seising (Wien), "Fuzzy Sets and Systems in History and Philosˆ\ ophy of Science".
15.2.2008: Raul Hakli, "Does the deduction theorem fail for modal logic?"
1.2.2008: Sara Negri, "Kripke completeness revisited II".
18.1.2008: Sara Negri, "Kripke completeness revisited I".
7.12.2007: Bernard Linsky (Alberta), "A proposition occurs in a function only through its values: Extensionality in the Second Edition of Principia Mathematica".
16.11.2007: Mika Oksanen: "Logicism, Ontology and Tarski's Theory of Logical Truth"
2.11.2007: Gabriel Sandu, "Ceteris Paribus Modalities".
28.9.2007: Mirja Hartimo, "Husserl on Hilbert's 1902 "Memoir"" abstract.
14.9.2007: Jan von Plato "An application of proof analysis to the theory of order relations".
The logic seminar for the Academic Year 2006-2007 starts next Friday 15.9. It will meet usually every second week both during the Autumn and the Spring term. Time and place: Friday 12-14, Department of Philosophy, Siltavuorenpenger 20A, seminar room 222.
The announcements are posted in the departmental mailing list. s 1902 All people interested in the seminar and not belonging to the list can e-mail us to be included among the recipients.
The logic seminar is over and it will meet again in the autumn term.
8.6.2007: Sergei Soloviev "Axiomatics and evidence".
4.5.2007: Jan Wolenski, "An Analysis of Logical Determinism".
20.4.2007: Bianca Boretti, "Proof analysis in temporal logic".
13.4.2007: Annika Kanckos, "The consistency of Heyting arithmetic in natural deduction".
30.3.2007: Aapo Halko, "Finite model theory".
23.3.2007: Ahti Pietarinen, "A survey of diagrammatic logics II".
27.2-1.3-2.3: Alberto Zanardo "Logics of branching time: Semantics and deductive systems" (27.2 and 1.3 seminar room 303, 10-12, 2.3 seminar room 222, 12-14)
23.2.2007: Sara Negri, "Kripke semantics for modal and temporal logic".
16.2.2007: Tarja Knuuttila, "Models, representation, and mediation" Memoir
26.1.2007: Avril Styrman, "Finitist Set Theory FST"
24.11.2006: Jan von Plato, "Proof theory of elementary geometry".
Abstract: Systems of elementary geometry are presented as proof-theoretic rule systems. One system is in a multiple conclusion natural deduction style, another in sequent calculus style. The central result is decidability of derivability with these rules.
17.11.2006: Ahti Pietarinen, "A Survey of Diagrammatic Logics". Slides: print, view
10.11.2006: Tero Tulenheimo, "The (robust) decidability of modal logic: a survey".
Abstract: Basic modal logic -- and its numerous variants and extensions -- combine pleasant algorithmic properties with reasonable expressive power. In the present talk I survey recent discussion which has aimed to identify the formal features that allow modal logic to be computationally so well behaved.
27.10.2006: Laura Tesconi (University of Pisa), "On inversion principles".
13.10.2006: Michael von Boguslawski, "Oiva Ketonen on logic and epistemology".
Abstract: In this talk I plan to present the contents of a recently discovered manuscript by Oiva Ketonen entitled "Tietomme apriorisista aineksista" probably written during 1945- 1950. I will also spend some time discussing _Ketonen's time as a student at the university of Helsinki in the thirties and forties, by pooling resources from his unfinished autobiography, a study-diary, and a self-reflective talk entitled "Mitä filosofia minulle on?" - "What is philosophy for me?".
15.9.2006: Panu Raatikainen, "On intuitionistic logic and its philosophical foundations".
28.4.2006: Jack Stecher (Bergen): "Trade and communication under subjective information", abstract
21.4.2006: Michael von Boguslawski, "Oiva Ketonen's work on logic".
24.3.2006: Tarmo Uustalu (Tallinn), "Proof systems for bi-intuitionistic logic".
17.3.2006: Andrea Meinander, "A solution of the uniform word problem for ortholattices".
24.2.2006: Jan von Plato, "Skolem's forgotten work on the combinatorial analysis of deduction."
17.2.2006: Annika Kanckos, "A constructive proof of the consistency of arithmetic".
10.2.2006: Sara Negri, "Equality in the presence of apartness. A problem of Van Dalen and Statman reconsidered".
3.2.2006: Sami Paavola, "Interpretations of abductive inference".
27.1.2006: : Sergei Soloviev (IRIT, Toulouse) "Some global aspects of preservation and loss of digitalized information".
Abstract: This is rather popular talk based on several papers published by author in France and in Russia. There are considered mostly the middle- and long-term risks seriously underestimated in existing scientific publications. The primary source of these risks (in comparison with more traditional methods of representation of information) is that electronic media are necessary not only for writing but also for reading of the data. Due to this fact technical evolution and economic functioning of hard- and software has direct implications for accessibility of information.
2.12.2005: Petri Mäenpää, "Complete induction in Euclid's Elements".
25.11.2005: Fabio Acerbi, "Ways of analysis and synthesis in Hero of Alexandria".
18.11.2005: Jan von Plato, "Natural deduction. Part II: Applications to modal logic and Heyting arithmetic"
11.11.2005: Jan von Plato: "Natural deduction. Part I: Correspondence with sequent calculus"
. 21.10.2005: Risto Vilkko, "Kant's Influence on the Development of Modern Logic".
14.10.2005: Tero Tulenheimo, "A novel approach to Independence-friendly modal logic"
7.10.2005: Miira Tuominen, "On the Sorites-Argument in Ancient Medicine", NOTE exceptional location: U38 (Topelia) room F205.
23.9.2005: Dennis Bonnay and Benjamin Simmenauer (IHPST, Paris), "Tonk strikes back".
16.9.2005: Raul Hakli, "Developing a sequent calculus for the logic of common knowledge".