History is always difficult

This is a picture of Stanisław Jaśkowski (April 22, 1906, Warsaw – November 16, 1965, Warsaw) from Wikipedia, of course.
Jaśkowski is (as discussed in class)  one of the founders of natural deduction, which he described completely independently from Gerhard Gentzen in the 1930s.

Wikipedia  says that Gentzen's approach initially became more popular with logicians because it could be used to prove the cut-elimination theorem. But Jaśkowski's is closer to the way that proofs are done in practice.

This doesn't ring true to me (Valeria). I think only later logicians got interested in cut-elimination and that Jaśkowski's natural deduction system, which later came to be known as Fitch-style natural deduction,  is easier to typeset and hence more adaptable to textbooks.

But at least least his original paper is available from Wikipedia (On the Rules of Suppositions in Formal Logic Studia Logica 1, 1934 pp. 5–32; reprinted in: Storrs McCall (ed.), Polish logic 1920-1939, Oxford University Press, 1967 pp. 232–258) and young logicians can compare his article with Gentzen's.

Another major controversy in the earlier years of Natural Deduction was the one about the exact rules for the quantifiers in first-order logic. Much ink was spilled on that one too.

For my part I am much more interested in the issue of the trade-offs that one must make to extend Natural Deduction to Modal Logics and to substructural logics. Some incipient discussion can be found in Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic (G. Bellin, V. de Paiva and E. Ritter), In Methods for Modalities 2001, Amsterdam, November 2001. (pdf).

Need to add the reference to  Jaśkowski's paper and to von Neumann's discussion to our bibliography. Also need to read these, thanks for the historical insights Luiz Carlos. Here are the slides from the first lecture of the course.

References are Hard

Luiz Carlos and Hermann will produce cleaned up versions of the slides for the course, separated by days, i.e. Lecture 1,  Lecture 2, ..., Lecture 5.  Meanwhile here are some references that Luiz Carlos decided to add to his three classes.

(i) References for Prawitz' ecumenical system:
[1] Prawitz, Dag – Classical versus intuitionistic logic, in Why is this a proof, College Books, Tributes 27, 2015, pp. 15 – 32.
[2] Dowek, Gilles – On the definition of the classical connectives and quantifiers, in Why is this a proof, College Books, Tributes 27, 2015, pp. 228 - 238.
[3] Krauss, P.H. - A constructive interpretation of classical mathematics, Mathematische Schriften Kassel, preprint No. 5/92, 1992.

(ii) References for Ferreira's system Fat:
[1]  The faithfulness  of atomic polymorphism, Fernando Ferreira e Gilda Ferreira, Trends in Logic (2014)
[2]  Atomic polymorphism, Fernando Ferreira e Gilda Ferreira, JSL, vol. 76 (2013)
[3]  Commuting conversions vs. the standard conversions of the “good connectives", Fernando Ferreira e Gilda Ferreira, Studia Logica, vol. 92 (2009).

(iii) Reference for schematic rules:
Schröder-Heister, Peter – Generalized elimination inferences, higher-level rules,
and the implications-as- rules interpretation of the sequent calculus, in Advances in Natural Deduction – a celebration of Dag Prawitz’ work, (eds) Luiz Carlos
Pereira, Edward Hermann Haeusler and Valeria de Paiva, Springer, 2014, pp. 1–29.

(iv) Reference for D'Agostino's ND:
Marcello D’Agostino   Classical Natural Deduction. In: We Will Show Them! (1)  Edited by: Sergei N Artëmov, Howard Barringer, Artur S d’Avila Garcez, Luís C Lamb, John Woods.   429-468 College Publications isbn: 1-904987-11-7, (2005).

Wednesday Challenges

[1] We saw in the course two normalization strategies:

(a) Prawitz’ normalization strategy. This is based on the following result: in the fragment {conjunction, implication, negation, absurd, for all}, every application of the classical absurd rule can be restricted to atomic applications, i.e., to applications with atomic conclusions.

(b) Seldin’s normalization strategy. This is based on the following result: in the fragment {conjunction, implication, negation, for all, disjunction, existential}, every derivation  of Gamma proves A can be transformed into another derivation of Gamma proves A such that the new derivation has at most one application of the classical absurd rule. If this application occurs in the derivation, then it is the last rule applied.

Can these results be formulated for the sequent calculus LK?

[2] As a preparatory step for the proof of decidability of the propositional fragment of the intutionistic sequent calculus LJ, Gentzen proves the following result: A sequent Gamma proves A in this fragment is called reduced if no formula occurs in the sequent Gamma proves A, more than three times. If a reduced sequent Gamma proves A is provable in the fragment, then Gamma proves A has a reduced proof, i.e., a proof that contains only reduced sequents.

Question: Why “three times”??

Two courses in parallel, yay!!!

Greg Restall and  Shawn Standefer are teaching another course in Proof Theory at NASSLLI2016

Proof Theory: Logical and Philosophical Aspects

This already makes me happy,  as proof theory is usually the poor cousin of model theory. To have two proof theory courses in the same Summer School is a big win for us.

But more immediately, having the two courses in parallel has proved very useful.  Many in the audience are following both and this makes things easier.  We are concentrating on Natural Deduction, they are concentrating in Sequent Calculus  and we can point at things in their course, to complement observations in ours. and vice versa. Everybody wins.

I meant to have a picture of Greg and  Shawn teaching and writing on the board at the same time,  but I guess I've messed it up, as the picture is not on my phone, sigh... So I have to use this one of Luiz Carlos starting our course. it seems pretty much the only picture I have of the whole NASSLLI. Before we moved  to the Murray building, oh well.

Encyclopedia of Proof Systems

Some people have decided that there are so many different and interesting logics or proof systems in the world right now that it is worth having an encyclopedia where the entries are summarized versions of those logic systems.

They've created an open source project in GitHub that is not completely user driven. There is a manager, Bruno Woltzenlogel Paleo. Together with some friends, we are hoping to help  create the Encyclopedia of Logical Systems. Gentzen is the source of inspiration for this encyclopedia.

From the readme:
This is a collaborative and open Encyclopedia of Proof Systems. If you would like to contribute, please check the submission instructions.
 
(picture of David Hilbert, who had the original idea that proofs should be investigated as mathematical objects on their own)

Proof Theoretic Semantics?

Peter Schroeder-Heister has coined the slogan "proof theoretic semantics" in the late eighties.

It's one of the exercises in our list to read Peter's entry in the Stanford Encyclopedia of Philosophy and say what you think about the program.

A personal take is in "Proof-theoretic Semantics for Non Philosophers".

More Syllabus

 Subjects to discuss in the last two lectures

1. The relatives of Natural Deduction

2. Natural Deduction proving strategies

3. Introduction to Curry-Howard isomorphism

4. Subformula property and proving procedures complexity

5. On the size of Propositional proofs

First (easy, I promise) Exercise List for the Course

I bet the blackboard picture got you worried. Only 5 questions about the beginnings of Natural Deduction HERE.

We also would like to know more about you, you can send us email replying to this?

The slides are here!

We have a big number of slides HERE.

They're supposed to cover the first three lectures.

We also have a short exercise list and a questionnaire, if you're interested. in the next blog post.