Constructive semantics, admissibility of rules and the validity of Peirce's law

(jointly with Wagner de Campos Sanz and Thomas Piecha)

To appear in the Logic Journal of the IGPL. pdf

In his approach to proof-theoretic semantics, Sandqvist claims to provide a justification of classical logic without using the principle of bivalence. Following ideas by Prawitz, his semantics relies on the idea that logical systems extend atomic systems, so-called "bases", with respect to which the validity of logically complex formulas is defined. We relate this approach to admissibility-based semantics and show that the latter significantly differs from the former. We also relate it to semantics based on the notion of construction, in which case the results obtained are essentially the same as Sandqvist's. We argue that the form of rules admitted in atomic bases determines which logical rules are validated, as is the fact of whether bases are conceived as information states, which can be monotonely extended, or as non-extensible inductive definitions. This shows that the format of atomic bases is a highly relevant issue in proof-theoretic semantics.

Proof-Theoretic semantics, self-contradiction, and the format of deductive reasoning

To appear in: L. Tranchini (ed.), Anti-Realistic Notions of Truth, Special issue of Topoi vol. 31 no. 1, 2012. pdf

From the point of view of proof-theoretic semantics, it is argued that the sequent calculus with introduction rules on the assertion and on the assumption side represents deductive reasoning more appropriately than natural deduction. In taking consequence to be conceptually prior to truth, it can cope with non-wellfounded phenomena such as contradictory reasoning. The fact that in its typed variant, the sequent calculus has an explicit and separable substitution schema in form of the cut rule, is seen as a crucial advantage over natural deduction, where substitution is built into the general framework.

Implications as Rules in Dialogical Semantics

(jointly with Thomas Piecha)

To appear in: M. Peliš and V. Punčochář (eds.), The Logica Yearbook 2011, College Publications, London, 2012. Draft: pdf

The conception of implications as rules is interpreted in Lorenzen-style dialogical semantics. Implications-as-rules are given attack and defense principles, which are asymmetric between proponent and opponent. Whereas on the proponent's side, these principles have the usual form, on the opponent's side implications function as database entries that can be used by the proponent to defend assertions independent of their logical form. The resulting system, which also comprises a principle of cut, is equivalent to the sequent-style system for implications-as-rules. It is argued that the asymmetries arising in the dialogical setting are not deficiencies but reflect the `pre-logical' structural character of the notion of rule.

Proof-Theoretic Semantics (SEP Entry)

To appear as an entry of the Stanford Encyclopedia of Philosophy (Ed Zalta, ed.). pdf

The Categorical and the Hypothetical: A critique of some fundamental assumptions of standard semantics

To appear in: Sten Lindström, Erik Palmgren and Dag Westerståhl (eds.), The Philosophy of Logical Consequence and Inference. Special Issue of Synthese. pdf

The hypothetical notion of consequence is normally understood as the transmission of a categorical notion from premisses to conclusion. In model-theoretic semantics this categorical notion is `truth', in standard proof-theoretic semantics it is `canonical provability'. Three underlying dogmas, (1) the priority of the categorical over the hypothetical, (2) the transmission view of consequence, and (3) the identification of consequence and correctness of inference are criticized from an alternative view of proof-theoretic semantics. It is argued that consequence is a basic semantical concept which is directly governed by elementary reasoning principles such as definitional closure and definitional reflection, and not reduced to a canonical concept. This understanding of consequence allows in particular to deal with non-wellfounded phenomena as they arise from circular definitions.

Definitional Reasoning in Proof-Theoretic Semantics and the Square of Opposition

To appear in: J.-Y. Béziau and G. Payette (eds), New Perspectives on the Square of Opposition, Peter Lang, Bern, 2010. pdf

Within a framework of reasoning with respect to clausal definitions of atoms, four forms of judgement are distinguished: Direct and indirect assertion, and direct and indirect denial. Whereas direct assertion and direct denial are established by directly applying a definitional clause ("definitional closure"), indirect assertion and indirect denial result from showing that all possible premisses of the opposite judgement can be refuted ("definitional reflection"). The deductive relationships between these four forms of judgement correspond to those represented in the square of opposition, if direct assertion and direct denial are placed in the A and E corners, and indirect assertion and indirect denial in the I and O corners of the square.

An alternative implication-left schema for the sequent calculus

Abstract for the ASL Logic Colloquium 2010, Paris, 25-31 July. pdf

Implications-as-rules vs. implications-as-links: An alternative implication-left schema for the sequent calculus

Journal of Philosophical Logic 40 (2011), 95-101. Draft: pdf

The interpretation of implications as rules motivates a different left-introduction schema for implication in the sequent calculus, which is conceptually more basic than the implication-left schema proposed by Gentzen. Corresponding to results obtained for systems with higher-level rules, it enjoys the subformula property and cut elimination in a weak form.

Generalized elimination inferences, higher-level rules, and the implications-as-rules interpretation of the sequent calculus

Contribution to: Edward Hermann Haeusler, Luiz Carlos Pereira and Valeria de Paiva, editors, Advances in Natural Deduction. 2010. pdf

We investigate the significance of higher-level generalized elimination rules as proposed by the author in relation to standard-level generalized elimination rules as proposed by Dyckhoff, Tennant, López-Escobar and von Plato. Many of the results established for natural deduction with higher-level rules such as normalization and the subformula principle immediately translate to the standard-level case. The sequent-style interpretation of higher-level natural deduction as proposed by Avron and by the author leads to a system with a weak rule of cut, which enjoys the subformula property. The interpretation of implications as rules motivates a different left-introduction schema for implication in the ordinary (standard-level) sequent calculus, which conceptually is more basic than the implication-left schema proposed by Gentzen. Corresponding to the result for the higher-level system, it enjoys the subformula property and cut elimination in a weak form.

Definitional Reflection and Basic Logic

To appear in the APAL special issue "Advances in Constructive Topology and Logical Foundations" in honor of the 60th birthday of Giovanni Sambin (Maria Emilia Maietti, Erik Palmgren and Michael Rathjen, eds.). pdf

In their Basic Logic, Sambin, Battilotti and Faggian give a foundation of logical inference rules by reference to certain reflection principles. We investigate the relationship between these principles and the principle of Definitional Reflection proposed by Hallnäs and Schroeder-Heister.

Schluß und Umkehrschluß: Ein Beitrag zur Definitionstheorie

Erscheint in revidierter Form in: Carl Friedrich Gethmann (Hrsg.), Lebenswelt und Wissenschaft. Akten des XXI. Deutschen Kongresses für Philosophie (Essen, 15.-19. September 2008). Deutsches Jahrbuch Philosophie, Bd. 3, 2009. pdf

Diese Arbeit untersucht das Problem der Umkehrbarkeit von Schlüssen im definitorischen Kontext. Wenn eine induktive Definition in Form einer Liste von Klauseln gegeben ist, dann kann man aufgrund der Abgeschlossenheit dieser Definition ("Extremalklausel", "Nichts sonst ist ein A") definitorische Regeln umkehren. Im ersten Teil wird das Lorenzensche Inversionsprinzip als Prototyp der Umkehrung der Definitionsrichtung diskutiert. Der zweite Abschnitt untersucht die lokalisierte Fassung der Inversion in Form der definitorischen Reflexion. Abschnitt 3 zeigt, wie Umkehrbarkeit sich auch auf negative Kontexte erweitern läßt, wie sich Inversions- und Reflexionsprinzipien auch in bezug auf Negationen formulieren lassen. In Abschnitt 4 wird die Dualisierung von logischen Begrifflichkeiten erwähnt und insbesondere auf terminologische Probleme im Zusammenhang mit Theorien der Co-Implikation hingewiesen. Abschnitt 5 skizziert, wie sich Zulässigkeit und definitorische Reflexion selbst dualisieren lassen. In Abschnitt 6 wird kurz auf die Option verwiesen, Schluß und Umkehrschluß im Rahmen der Dialoglogik aus einem einheitlichen Prinzip zu gewinnen.

Sequent Calculi and Bidirectional Natural Deduction: On the Proper Basis of Proof-Theoretic Semantics

M. Peliš (ed.), The Logica Yearbook 2008, London: College Publications 2009. pdf

This paper argues that the sequent calculus or alternatively bidirectional natural deduction should be chosen as the basis for proof-theoretic semantics. Here "bidirectional natural deduction" is proposed as a term for a natural deduction system with generalized elimination inferences, in which major premisses of elimination inferences always occur in top position (i.e., are assumptions). It can be viewed as a sequent calculus in natural deduction format. When interpreted semantically, such systems promise to overcome certain shortcomings of proof-theoretic semantics in the Dummett-Prawitz tradition, which is based on the standard unidirectional model of natural deduction. In particular, they do more justice to the notion of "assumption". Assumptions are now treated on par with assertions, and open assumptions are no longer merely placeholders for closed proofs. Such an approach permits a smooth extension of proof-theoretic semantics beyond the realm of logical constants towards a general definitional theory of hypothetical reasoning.

Lorenzen's operative justification of intuitionistic logic

M. van Atten, P. Boldini, M. Bourdeau, G. Heinzmann (eds.), One Hundred Years of Intuitionism (1907-2007), Basel: Birkhäuser 2008. pdf

We analyse the logic-oriented part of Lorenzen's "Introduction to Operative Logic and Mathematics" (1955) and reconstruct his theory of implication. It turns out that his much criticized doctrine of iterated admissibility statements and meta-calculi can be given a sensible form. Furthermore, we compare Lorenzen's theory with proof-theoretic semantics in the Dummett-Prawitz tradition, and show that both approaches can be translated into one another. It is argued that, from the viewpoint of an epistemological approach to semantics, the Dummett-Prawitz approach (as well as Lorenzen's later 'dialogical' or game-theoretical semantics) has certain advantages over Lorenzen's operative theory, if it is expected that knowledge of meaning should manifest itself in observable behaviour.

Jürgen Mittelstraß and Peter Schroeder-Heister: Nicholas Rescher on Greek Philosophy and the Syllogism

R. Almeder (ed.), Rescher Studies (Festschrift 80th Birthday), Ontos Verlag. Draft: pdf

This paper comments on Rescher's Cosmos and Logos - Studies in Greek Philosophy and Galen and the Syllogism, pointing out the significance of Greek and Islamic sources for Rescher's approach to philosophy. In the more technical sections, it relates Rescher's edition of a manuscript of Al-Salah to corresponding work carried out by A.I. Sabra. Furthermore, it gives a critical evaluation of Rescher's systematic account of categorical syllogistics and especially of the relevance (or irrelevance) of the fourth figure. Finally, it attempts to reconstruct Rescher's interpretation of the ekthesis principles of Aristotle's modal syllogistics.

Proof-Theoretic versus Model-Theoretic Consequence

M. Peliš (ed.), The Logica Yearbook 2007, Prague: Filosofia 2008, 187-200. Draft: pdf

Both the model-theoretic notion of consequence in Tarski's sense and standard proof-theoretic notions of consequence in the BHK tradition and in the tradition of Dummett-Prawitz-style proof-theoretic semantics are defined in terms of a categorical concept (truth, validity, construction). It is argued that a proper proof-theoretic semantics should address the hypothetical concept of consequence directly, based on the sequent calculus as the formal model of reasoning. Inference rules are then justified by principles of definitional closure and definitional reflection with respect to a given clausal definition.

Generalized Definitional Reflection and the Inversion Principle

Logica Universalis 1 (2007), 355-376. Draft: pdf

The term inversion principle goes back to Lorenzen who coined it in the early 1950s. It was later used by Prawitz and others to describe the symmetric relationship between introduction and elimination inferences in natural deduction, sometimes also called harmony. Lorenzen's inversion principle has a much wider range than Prawitz's adaptation to natural deduction, dealing with the invertibility of rules of an arbitrary atomic production system. It is closely related to definitional reflection, which is a principle for reasoning on the basis of rule-based atomic definitions as well. After presenting definitional reflection and the inversion principle, it is shown that the inversion principle can be formally derived from definitional reflection, when the latter is viewed as a principle to establish admissibility. Furthermore, the relationship between defiitional reflection and the inversion principle is investigated on the background of a universalization principle, called the ω-principle, which allows one to pass from the set of all defined substitution instances of a sequent to the sequent itself.

Lorenzens operative Logik und moderne beweistheoretische Semantik

J. Mittelstraß (ed.), Der Konstruktivismus in der Philosophie im Ausgang von Wilhelm Kamlah und Paul Lorenzen. Paderborn: Mentis 2007, 167-196. Draft: pdf

Der Logik-Teil von Lorenzens "Einführung in die operative Logik und Mathematik" (1955) enthält Ansätze, die eine neue Diskussion, Einschätzung und Würdigung vom Standpunkt der modernen beweistheoretischen Semantik (seit 1971) verdienen. Es zeigt sich, daß Lorenzens Theorie einen signifikanten Schritt über die konstruktive Semantik vom BHK-Typ hinaus darstellt, der manche Ideen der beweistheoretischen Semantik vorwegnimmt. Außerdem enthält sie, aufgrund ihrer sehr allgemein gefaßten, auf beliebige Produktionssysteme ausgerichteten Konzeption Elemente, die auf dem Hintergrund der beweistheoretischen Semantik und der Anregungen aus der Theorie der Logikprogrammierung weiterentwickelt werden sollten. Anders als in Lorenzens eigener Einschätzung seiner konstruktiven Logikbegründung sollte sie also nicht nur als Zwischenstufe auf dem Weg zu einer dialogischen oder spieltheoretischen Semantik verstanden werden.

Für weitere Arbeiten (teilweise herunterladbar) siehe Publikationsliste