The Problem of Natural Representation of Reasoning in the Lvov-Warsaw School

ABSTRACT

The problem of precise characterisation of traditional forms of reasoning applied in mathematics was independently investigated and successfully resolved by Jaśkowski and Gentzen in 1934. However, there are traces of earlier interests in this field exhibited by the members of the Lvov-Warsaw School. We focus on the results obtained by Jaśkowski and Leśniewski. Jaśkowski provided the first formal system of natural deduction in 1926. Leśniewski also demonstrated in some of his papers how to construct proofs in accordance with intuitively correct principles.

KEYWORDS:

• Jaśkowski
• Gentzen
• Leśniewski
• Tarski
• natural deduction

Notes

1 Since the problem of classification of forms of reasoning is not the subject of this paper we omit detailed references. Interested readers can consult e.g. Woleński 1989 or Indrzejczak 2009.

2 More on these demarcation problems in Indrzejczak 2010, 2015.

3 In fact, the first such proof was already provided by Gentzen but only for intuitionistic logic and presented in his dissertation; it was published with comments by Von Plato 2008.

4 See a readable introduction in Schroeder-Heister 2012.

5 Since trees better represent the structure of ready proofs and simplify their combinatorial transformations necessary for normalisation of proofs and consistency results.

6 See a comparison of Gentzen's and Jaśkowski's approach provided by Indrzejczak 2010.

7 One may find a detailed presentation of his achievements in Urbaniak 2014.

8 See vol I of Leśniewski 1992.

9 Note that in 1926 he was 20 years old.

10 Note that in Gentzen's system, this weaker form of indirect proof is sufficient for obtaining Heyting's intuitionistic logic but Gentzen is using ⊥ as a primitive constant (¬ is definable) and a rule of trivialisation $\mathrm{\perp }/\phi$, so deduction of q from $\mathrm{\neg }p$ and p is not a problem.

11 Cf. historical remarks in Bencivenga 1986 and Bencivenga 2014 and a survey of free logics provided by Nolt 2010.

12 The history of successive versions of Copi's ND (Copi 1954) with numerous mistaken formulations of this rule is particularly instructive.