





Peter SchroederHeister Research
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 prooftheoretic 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, socalled "bases", with respect to which the validity of logically complex formulas is defined. We relate this approach to admissibilitybased 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 nonextensible inductive definitions. This shows that the format of atomic bases is a highly relevant issue in prooftheoretic semantics. ProofTheoretic semantics, selfcontradiction, and the format of deductive reasoningTo appear in: L. Tranchini (ed.), AntiRealistic Notions of Truth, Special issue of Topoi vol. 31 no. 1, 2012. pdf From the point of view of prooftheoretic 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 nonwellfounded 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 form 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 Lorenzenstyle dialogical semantics. Implicationsasrules 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 sequentstyle system for implicationsasrules. It is argued that the asymmetries arising in the dialogical setting are not deficiencies but reflect the `prelogical' structural character of the notion of rule. ProofTheoretic 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 semanticsTo 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 modeltheoretic semantics this categorical notion is `truth', in standard prooftheoretic 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 prooftheoretic 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 nonwellfounded phenomena as they arise from circular definitions. Definitional Reasoning in ProofTheoretic Semantics and the Square of OppositionTo 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 implicationleft schema for the sequent calculusAbstract for the ASL Logic Colloquium 2010, Paris, 2531 July. pdf Implicationsasrules vs. implicationsaslinks: An alternative implicationleft schema for the sequent calculusJournal of Philosophical Logic 40 (2011), 95101. Draft: pdf The interpretation of implications as rules motivates a different leftintroduction schema for implication in the sequent calculus, which is conceptually more basic than the implicationleft schema proposed by Gentzen. Corresponding to results obtained for systems with higherlevel rules, it enjoys the subformula property and cut elimination in a weak form. Generalized elimination inferences, higherlevel rules, and the implicationsasrules interpretation of the sequent calculusContribution to: Edward Hermann Haeusler, Luiz Carlos Pereira and Valeria de Paiva, editors, Advances in Natural Deduction. 2010. pdf We investigate the significance of higherlevel generalized elimination rules as proposed by the author in relation to standardlevel generalized elimination rules as proposed by Dyckhoff, Tennant, LópezEscobar and von Plato. Many of the results established for natural deduction with higherlevel rules such as normalization and the subformula principle immediately translate to the standardlevel case. The sequentstyle interpretation of higherlevel 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 leftintroduction schema for implication in the ordinary (standardlevel) sequent calculus, which conceptually is more basic than the implicationleft schema proposed by Gentzen. Corresponding to the result for the higherlevel system, it enjoys the subformula property and cut elimination in a weak form. Definitional Reflection and Basic LogicTo 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 SchroederHeister. Sequent Calculi and Bidirectional Natural Deduction: On the Proper Basis of ProofTheoretic SemanticsM. 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 prooftheoretic 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 prooftheoretic semantics in the DummettPrawitz 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 prooftheoretic semantics beyond the realm of logical constants towards a general definitional theory of hypothetical reasoning. Lorenzen's operative justification of intuitionistic logicM. van Atten, P. Boldini, M. Bourdeau, G. Heinzmann (eds.), One Hundred Years of Intuitionism (19072007), Basel: Birkhäuser 2008. pdf We analyse the logicoriented 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 metacalculi can be given a sensible form. Furthermore, we compare Lorenzen's theory with prooftheoretic semantics in the DummettPrawitz 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 DummettPrawitz approach (as well as Lorenzen's later 'dialogical' or gametheoretical 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 SchroederHeister: Nicholas Rescher on Greek Philosophy and the SyllogismR. 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 AlSalah 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. ProofTheoretic versus ModelTheoretic ConsequenceM. Peliš (ed.), The Logica Yearbook 2007, Prague: Filosofia 2008, 187200. Draft: pdf Both the modeltheoretic notion of consequence in Tarski's sense and standard prooftheoretic notions of consequence in the BHK tradition and in the tradition of DummettPrawitzstyle prooftheoretic semantics are defined in terms of a categorical concept (truth, validity, construction). It is argued that a proper prooftheoretic 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 PrincipleLogica Universalis 1 (2007), 355376. 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 rulebased 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 SemantikJ. Mittelstraß (ed.), Der Konstruktivismus in der Philosophie im Ausgang von Wilhelm Kamlah und Paul Lorenzen. Paderborn: Mentis 2007, 167196. Draft: pdf For further references (including downloadable items) see the list of publications 
