Home Philosophy Advances in Proof-Theoretic Semantics

# Conclusion

The main conclusion is this: although the idea that the “grounds for asserting a proposition” are easily collected together as a unit is attractive, the different ways in which it can be done (disjunctive, conjunctive, with assumption discharge, with variable abstraction or parameterisation, …, recursion) generate (if the GE rules pattern is followed) many problems for the programme of mechanically generating one (or more) elimination rules for a logical constant, other than in simple cases. There are difficulties with the mechanical approach in [8]; there are similar difficulties in [13]. Without success of such a programme, it is hard to see what “GE harmony” can amount to, except as carried out in (e.g.) Coq [1] where strictly positive inductive type definitions lead automatically to rules for reasoning by induction and case analysis over objects of the types thus defined, and with strong normalisation results. A similar conclusion is to be found in [33].

# References

1. Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)

2. Dummett, M.A.E.: The Logical Basis of Metaphysics. Duckworth, London (1991)

3. Dyckhoff, R.: Implementing a simple proof assistant. In: Derrick, J., Lewis, H.A. (eds.) Work-

shop on Programming for Logic Teaching, Proceedings, vol. 23.88, pp. 49–59. Centre for Theoretical Computer Science, University of Leeds (1987). rd.host.cs.st-andrews.ac.uk/ publications/LeedsPaper.pdf

4. Dyckhoff, R.: Generalised elimination rules and harmony. In: Arché Seminar, St Andrews, 26

May 2009. rd.host.cs.st-andrews.ac.uk/talks/2009/GE.pdf

5. Dyckhoff, R., Pinto, L.: Cut-elimination and a permutation-free sequent calculus for intuition-

istic logic. Studia Logica 60, 107–118 (1998)

6. Dyckhoff, R., Pinto, L.: Proof search in constructive logics. In: Cooper, S.B., Truss, J.K. (eds.)

Proceedings of Logic Colloquium 97, i.e. Sets and Proofs, pp. 53–65. CUP (1999)

7. Ekman, J.: Propositions in propositional logic provable only by indirect proofs. Math. Log. Q.

44, 69–91 (1998)

8. Francez, N., Dyckhoff, R.: A note on harmony. J. Philos. Log. 41, 613–628 (2012)

9. Gentzen, G.: Untersuchungen über das logische Schließen. Math. Zeitschrift 39, 176–210

(1934)

10. Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)

11. Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge

(1989)

12. Joachimski, F., Matthes, R.: Short proofs of normalization for the simply-typed lambda-

calculus, permutative conversions and Gödel's T. Arch. Math. Log. 42, 59–87 (2003)

13. López-Escobar, E.G.K.: Standardizing the N systems of Gentzen. Models, Algebras, and

Proofs, pp. 411–434. Dekker, New York (1999)

14. Luo, Z.H.: Computation and Reasoning. Oxford University Press, New York (1994)

15. Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Naples (1986)

16. Martin-Löf, P.: On the meanings of the logical constants and the justifications of the logical

laws (the Siena Lectures). Nord. J. Philos. Log. 1, 11–60 (1996)

17. Matthes, R.: Interpolation for natural deduction with generalized eliminations. In: Kahle, R.,

Schroeder-Heister, P., Stärk, R. (eds.) Proof Theory in Computer Science. LNCS, vol. 2183, pp. 153–169. Springer, New York (2001)

18. Mendler, P.F. (Better known as Nax P. Mendler.): Inductive definition in type theory. Ph.D.

thesis, Cornell (1987). nuprl.org/documents/Mendler/InductiveDefinition.pdf

19. Moriconi, E., Tesconi, L.: On inversion principles. Hist. Philos. Log. 29, 103–113 (2008)

20. Negri, S., von Plato, J.: Structural Proof Theory. CUP, Cambridge (2000)

21. Olkhovikov, G.K., Schroeder-Heister, P.: On flattening elimination rules. Rev. Symb. Log. 13

pp. (2014). dx.doi.org/10.1017/S1755020313000385

22. Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Math. Struct. Comput.

Sci. 11, 511–540 (2001)

23. Pierce, B., et al.: Software Foundations. cis.upenn.edu/~bcpierce/sf/Logic.html 28

July 2013. Accessed 27 Jan 2014

24. Prawitz, D.: Natural Deduction. Almqvist and Wiksell, Stockholm (1965)

25. Prawitz, D.: Ideas and results in proof theory. In: Fenstad, J.E. (ed.) Second Scandinavian Logic

Symposium Proceedings, pp. 235–307. North-Holland, Amsterdam (1971)

26. Prawitz, D.: Proofs and the meaning and completeness of the logical constants. Essays on

Mathematical and Philosophical Logic. Reidel, Dordrecht (1979)

27. Prawitz, D.: Beweise und die Bedeutung und Vollständigkeit der logischen Konstanten. Con-

ceptus 16, 31–44 (1982) (Translation and revision of [26])

28. Read, S.L.: Harmony and autonomy in classical logic. J. Philos. Log. 29, 123–154 (2000)

29. Read, S.L.: General-elimination harmony and higher-level rules. In: Wansing, H. (ed.) Dag

Prawitz on Proofs and Meaning, pp. 293–312. Springer, New York (2015)

30. Schroeder-Heister, P.: A natural extension of natural deduction. J. Symb. Log. 49, 1284–1300 (1984)

31. Schroeder-Heister, P.: Generalized definitional reflection and the inversion principle. Log. Univ.

1, 355–376 (2007)

32. Schroeder-Heister, P.: Generalized elimination inferences, higher-level rules, and the implications-as-rules interpretation of the sequent calculus. In: Pereira, L.C., Haeusler, E.H., de Paiva, V. (eds.) Advances in Natural Deduction: A Celebration of Dag Prawitz's Work, pp. 1–29. Springer, New York (2014)

33. Schroeder-Heister, P.: Harmony in proof-theoretic semantics: a reductive analysis. In: Wansing,

H. (ed.) Dag Prawitz on Proofs and Meaning, pp. 329–358. Springer, New York (2015)

34. Schroeder-Heister, P., Tranchini, L.: Ekman's paradox (2014). Notre Dame Journal of Formal Logic (submitted)

35. Schwichtenberg, H., Wainer, S.: Proofs and Computations. Cambridge University Press, Cambridge (2012)

36. Tennant, N.: Ultimate normal forms for parallelized natural deductions. Log. J. IGPL 10, 299– 337 (2002)

37. Tesconi, L.: Strong normalization for natural deduction with general elimination rules. Ph.D. thesis, Pisa (2004)

38. von Kutschera, F.: Die Vollständigkeit des Operatorensystems für die intuitionistiche Aussagenlogik im Rahmen der Gentzensemantik. Archiv für mathematische Logik und Grundlagenforschung 11, 3–16 (1968)

39. von Plato, J.: Natural deduction with general elimination rules. Arch. Math. Log. 40, 541–567 (2001)

40. von Plato, J.: Explicit composition and its application in proofs of normalization (2015) (submitted)

41. von Plato, J., Siders, A.: Normal derivability in classical natural deduction. Rev. Symb. Log.

5, 205–211 (2012)

42. Zucker, J., Tragesser, R.S.: The adequacy problem for inferential logic. J. Philos. Log. 7, 501– 516 (1978)

Found a mistake? Please highlight the word and press Shift + Enter