Master Project: The format of reasoning systems and key concepts of proof-theoretic semantics

Individual Project 1: Proof and truth

Individual Project 2: The taxonomy of logical systems

Individual Project 3: General frameworks for hypothetical reasoning

 

---

 

First project phase:
Hypothetical Reasoning – Logical and Semantical Perspectives

Though the notion of "hypothesis" or "assumption" is central for deduction and inference, the logical systems to handle hypotheses are vastly different, both with respect to proof theory and with respect to semantics. The aim of this French/German research group is to bring together various approaches towards hypothetical reasoning and discuss them from a uniform perspective. The Master Project, to which all participants equally contribute, deals with the representation and basic laws of hypothetical reasoning. Here the intention of the group is to develop an intensional notion of hypothetical reasoning, which is both proof-theoretically (and therefore epistemologically) and semantically more adequate than existing notions. Four individual projects discuss this objective in relation to special areas: (1) The conceptual history of hypotheses-based logical systems in the 1920s and 1930s; (2) constructive approaches to hypothetical reasoning in modal logic; (3) the logic of conditionals, as this is the most natural place to apply and test any theory of hypothetical reasoning; (4) definitional reasoning and logical tomography, as these approaches lead to proof-theoretically grounded intensional notions of consequence.

Master Project

The way the human mind uses hypotheses has been discussed in philosophy since Plato's Meno, where it was characterized as the method used by geometers. Hypotheses play a crucial role in the natural sciences, where their status has been a matter of controversy for centuries. However, even without considering their application in geometrical or experimental research, the significance, status and role of hypotheses in reasoning is far from clear. Nowadays, when talking of hypothetical judgements (or "statements" or "propositions" or "sentences"), at least three different meanings can be distinguished:

1. (1) A hypothetical judgement is an assertion of an implication (conditional): If A, then B.
2. (2) A hypothetical judgement is an assertion made under a certain assumption: Assuming A, we can claim B.
3. (3) A hypothetical judgement expresses logical consequence: B follows logically from A.

In a logical formalism, we would express (1) by means of an implicative sentence "if A then B", (2) by a deduction starting with A as an assumption and ending with B, and (3) by means of a consequence statement such as "B follows from A". It is a standard topic of logic to distinguish between (1) and (3). Whereas the validity of (1) "if A, then B" hinges on the state of the world in which this judgement is made, the validity of (3) "B is a logical consequence of A" only depends on the logical form of A and B. Sometimes, following Russell, (1) is called the material conditional or material implication, whereas (3) expresses formal implication (although Russell used the term "formal implication" in a different sense). A judgement of form (2) can have either material or formal meaning, depending on the context, i.e., depending on whether A alone licenses the transition to B or whether further (non-logical) assumptions or rules are needed to arrive at B. The crucial difference between (1) and (2) is that (1) is an assertion of a single sentence (which has hypothetical form), whereas (2) is an assertion of a sentence with respect to another sentence (taken to be an assumption) and thus is inherently relational in character. (3) is a relational statement as well.

Gentzen. It was Gerhard Gentzen (1934/35) who, based on work by Paul Hertz, provided a paradigm shift in the representation of reasoning. In Gentzen-style systems, especially in his "sequent calculi", we find an explicit distinction between judgements of forms (1) and (2). In fact, the meaning of conditional sentences (1) is explained by reference to sentences of the form (2), the latter being expressed by means of the "sequent arrow". So in Gentzen-style systems we have a distinction between two levels: The structural level governed by an implication of type (2) and the sentential level with ordinary material implication (1). This distinction has lead to powerful systems and initiated many new developments in mathematical proof theory.

Consequence as transmission of truth: The primacy of the categorical over the hypothetical. According to model-theoretic semantics of the Tarski tradition, consequence is explained in terms of transmission of truth. According to the standard approach to proof-theoretic semantics developed mainly by Dummett and Prawitz (Dummett 1991, Prawitz 1985, 2006), the idea of truth is replaced with that of a canonical proof, but the picture is similar. This means that in both the model-theoretic and in the (standard) proof-theoretic approaches to semantics, a categorical concept is primary to the hypothetical one. Hypothetical consequence is explained by the transmission of a categorical concept (either "truth" or "canonical derivability") from the premisses to the conclusion of the consequence statement. Despite the fact that there is a clearcut formal difference between the assertion of a conditional and a hypothetical judgement, there is just a single primitive semantical concept, namely that of categorical truth or categorical provability. The basic tenet of the standard approach to semantics is the primacy of the categorical over the hypothetical (cf. Schroeder-Heister and Contu 2005, Schroeder-Heister 2008, 2009).

The idea that the categorical is primary to the hypothetical, and that the validity of the hypothetical concept of consequence is reduced to the transmission of the categorical concept of truth or verifiability from the hypothesis to the conclusion, will be called the transmission view of consequence.

Counterfactuals. Beside the general line of thought which goes from Frege to substructural and linear logic, through Gentzen’s sequent calculus and constructive type theory, there is another important path in the theory of hypothetical reasoning which is more specific: it examines a special case of hypothetical reasoning, namely the counterfactual one. What can we conclude from a hypothesis we know to be false? The logic of conditionals understood in this sense has received a strong impulsion from possible world semantics and has been a matter of intensive inquiry for half a century. However, its history is older, as its origin dates back at least to Ramsey (1929), where the motivation is more philosophical. As a matter of fact, one of the main goals of this line of thought is to clarify the notion of a law of nature. Modern logic taught us that a scientific law, that is a universal statement, is expressed as a conditional. However, not every universal statement is a law, and we must be able to distinguish a conditional which expresses a law of nature from a conditional which does not. As a consequence, the logic of conditionals is closer to the use of conditionals in ordinary life reasoning. It is a great challenge to synthesize these two approaches to hypothetical reasoning in a uniform framework.

Individual Project 1: Paul Hertz's Satzsysteme

The logical systems of Paul Hertz (1881 – 1940) were Gentzen’s starting point when developing his sequent calculus. Whereas the latter has become the formal proof-theoretic paradigm for hypothetical reasoning, Hertz’s work has been fairly neglected. In the 1920s Hertz (1922, 1923) developed a system of consequence logic, which, from the modern point of view, has two significant features: (i) It is based on a single notion of implication and, in this respect, is related to an approach already put forward by Frege. However, unlike Frege's, his notion of implication is a structural one – governed by principles later called "structural rules" by Gentzen. In this sense it is an exclusively structural approach. (ii) It has Cut as a basic primitive rule of inference which cannot (and should not) be eliminated as is done in the systems devised by Gentzen. Therefore, although Gentzen’s investigations into logical deduction originated from a close examination of Hertz's calculus – Gentzen’s first publication (1933) is devoted to Hertz’s "Satzsysteme" –, it is in many respects systematically opposed to Gentzen’s developments and nearer to systems as they appear, for example, within the framework of resolution proofs (see Schroeder-Heister 2002, Arndt 2008).

Individual Project 2: Hypothetical Reasoning and Modal Logic

The renewal of Gentzen’s ideas soon prompted the question: Are there sequent calculi for, at least, the main systems of modal logic? At the beginning of the 1980s, logicians started creating methods capable of generating extensions of the classical sequent calculus and, therefore, of providing modal logic with computational tools. These methods can be divided in two groups: (i) using purely syntactic sequent calculi; (ii) extending the standard sequent calculus by adding explicit semantic parameters, such as possible worlds or truth values. Unfortunately the results were rather unsatisfactory both from a philosophical and from a formal point of view. Therefore we are still facing a lack of suitable Gentzen calculi for the main systems of modal propositional logic (Blackburn et al. 2001). Using proof theoretical tools, modalities have been approached from another point of view. The constructive notion of a hypothetical judgement is absolutely fundamental to intuitionism (van Atten 2004, 2008). In this context, intuitionistic logic plays a crucial role, due to its close connection to modal logic and to constructive type theory. In 1990, P. Martin-Löf took an important step towards a general theory of hypothetical judgements. Preceded by his paper Mathematics of Infinity (Martin-Löf 1990), the 1990 Lectures on Choice Sequences (Martin-Löf 1991) introduce the concept of formal space. A formal space is a spread of contexts defined as progressive sequences of hypotheses related by refinement morphisms corresponding to a specification of the growth of knowledge. On top of such a space, the familiar type-theoretic judgements of proposition-formation and proof-introduction evolve continuously, like sets in the sheaves familiar to category-theorists, but in a predicative and effective way. In this framework, A. Ranta (1995) showed how to obtain constructive counterparts to possible-worlds semantics. Possible-worlds are not actual entities, but infinite streams, and thus fundamentally undetermined, or only partially determined.

Individual Project 3: Hypothetical Reasoning and Theories of Conditionals

The theory of conditionals is a natural context for considering hypothetical reasoning. It provides a fruitful framework for posing the question of whether we should distinguish between the categorical assertion of a conditional sentence and the assertion of a sentence under a hypothesis. According to the most famous of these theories (Lewis 1973, Stalnaker 1968, 1975), the conditional 'if it were to rain, the tennis game would be called off' is evaluated as true if, in the possible worlds which are most similar to our world and in which it does rain, the game is called off, – which is intuitively close to meaning (2) of hypothetical judgements. However, none of the theories, nor any of the theories proposed since, have been able to provide elucidation as to which similarity relation is to be used in the evaluation of conditionals. This holds despite the fact that they are by far the most widely-used theories of conditionals in philosophy and logic today.

Furthermore, some have raised doubts about the logical properties of these theories. The aim was to overcome the inadequacies of the account of behaviour of conditional sentences in natural language in terms of the material conditional: The falsity conditions of the material conditional are preserved, whilst some of the other logical properties are not. However, there are logical laws that hold of the material conditional and that seem intuitively correct, but which are lost under the Stalnaker-Lewis theory, such as: (i) the so-called law of import-export, (equivalence between "if P, then if Q, then R" and "if P and Q, then R") (McGee 1989); (ii) the schema of simplification of disjunctive antecedents, (inference from "if P or Q, then R" to "(if P, then R), and (if Q, then R)") (Fine 1975, Lewis 1981); (iii) even more dramatically, the disjunctive syllogism, (inference from "either P or Q" to "if not P then Q"). Some, such as Stalnaker, have argued that the apparent validity of these rules, in particular the rule of disjunctive syllogism, is due to pragmatic factors – for example, the similarity relation on worlds – rather than logical ones – how the conditional is evaluated assuming the similarity relation is given.

The epistemology of conditional reasoning is almost entirely focused on the famous Adams Thesis (Adams 1965, 1975) according to which rational belief in conditionals goes by conditional belief for their consequents on the assumption that their antecedent is true. As such, Adams Thesis is silent about the logic of conditionals. But it is clear that Adams Thesis has implications for logic: if Adams Thesis is right, then an adequate theory of the logic and semantics of conditionals should be compatible with it. Were it not the case, we would obtain a disturbing mismatch between logic and epistemology. However, Lewis (1976) has proven that no logical operator is compatible with Adams Thesis. It seems therefore that something has to be abandoned: either Adams Thesis, or the possibility of a logic and semantics for conditionals, i.e., the claim that conditionals have truth-conditions. The second option leads to the No Truth Value conception (Edgington, Gibbard) according to which conditionals have only acceptance conditions but no truth conditions. Adams Thesis and Lewis’s impossibility result thus strongly motivate a distinction between the categorical and the hypothetical; they also call for a better understanding of the relationship between them.

Individual Project 4: Definitional Reasoning, Logical Tomography and Intensional Consequence

Definitional reasoning is based on the idea that logical semantics should no longer only be concerned with logical constants, but that the semantics of logical constants is a special case of the reasoning with respect to a definition which gives the content of reasoning. General rules of hypothetical reasoning put this content into action by extracting assumption and assertion rules from this definition. Ideas of this kind go back to Lorenzen’s work in his operative logic (Lorenzen 1955) and to ideas put forward by Martin-Löf in his theory of (iterated) inductive definitions (Martin-Löf 1971). Similar ideas emerged from extensions of logic programming (see the papers in Schroeder-Heister 1991). They are also related to theories of cyclic updating truth valuations, as originally proposed in Kripke’s (1975) theory of truth and expanded by Gupta and Belnap (1993) and later research.

This idea was extended by Hallnäs & Schroeder-Heister (1990/91) to a general framework for hypothetical reasoning which allows for non-monotonic applications and includes, e.g., paradoxical reasoning. It is opposed to standard model-theoretic and proof-theoretic approaches in that it is strictly local in the sense that single reasoning steps rather than global behaviour of proofs are crucial. Philosophically, it can be viewed as a novel approach to analytical reasoning, which covers logical reasoning as a special case. From mathematics, it takes the inspiration that the fundamental type of definitions is the inductive one (of which the explicit one is a limiting case), and that the traditional philosophical preoccupation with explicit definitions has led to shortcomings in the reasoning paradigms developed. Logical tomography (Arndt 2008) further radicalizes the local approach to consequence by thoroughly separating content from structure. This leads to an intensional notion of proof, or more generally, to an appropriate representation of reasoning for which the form of proving is relevant.

References

• Arndt, M. (2008), Logical Tomography: Exposing the Structural Nature of Logic. Ph.D. thesis, Tübingen.
• Atten, v. M. (2004a), "Brouwer and the hypothetical judgement. Second thoughts on Jon Kuiper’s ideas and explorations. Brouwer’s road to intuitionism", Revue Internationale de Philosophie 230, 501–516.
• Atten, v. M. (2004b), On Brouwer, Belmont (CA): Wadsworth.
• Atten, v. M. (2008), "One Hundred Years of Intuitionism", Proceedings of the Cerisy Conference, Birkhäuser, Basel, to appear in july 2008 (with P. Boldini, M. Bourdeau and G. Heinzmann).
• Adams, E. W. (1965), "On the Logic of Conditionals", Inquiry 8: 166-97
• Adams, E. W. (1975), The Logic of Conditionals, D. Reidel Publishing Co., Dordrecht.
• Dummett, M. (1991), The Logical Basis of Metaphysics, London.
• Gentzen, G. (1933), "Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen", Mathematische Annalen 107, 329–350.
• Gentzen, G. (1934/35), "Untersuchungen über das logische Schließen". Mathematische Zeitschrift 39, 176–210, 405–431.
• Gupta, A. & Belnap, N. (1993), The Revision Theory of Truth. Cambridge Mass.: MIT Press.
• Hallnäs, L. & Schroeder-Heister, P. (1990/91), "A proof-theoretic approach to logic programming. I. Clauses as rules", Journal of Logic and Computation 1 (1990), 261–283. "II. Programs as definitions", ibid., 635–660.
• Hertz, P. (1922), "Über Axiomensysteme für beliebige Satzsysteme. I. Teil. Sätze ersten Grades". ("Über die Axiomensysteme von der kleinsten Satzzahl und den Begriff des idealen Elementes".) Mathematische Annalen, 87, 246–269.
• Hertz, P. (1923), "Über Axiomensysteme für beliebige Satzsysteme. II. Teil. Sätze höheren Grades", Mathematische Annalen, 89, 76–100. 246–269.
• Kripke S. (1975), "Outline of a theory of truth", Journal of Philosophy 72, 690–716.
• Lewis, D. K. (1973), Counterfactuals. Harvard University Press, Cambridge, Massachusetts.
• Lewis, D. K. (1976), "Probability of Conditionals and Conditional Probabilities", Philosophical Review 85, 297-315.
• Lewis, D. K. (1981), "Ordering semantics and premise semantics for conditionals", Journal of Philosophical Logic 10(2):217–234.
• Lorenzen, P. (1955), Einführung in die operative Logik und Mathematik. Berlin: Springer. 2nd ed. 1969.
• Martin-Löf, P. (1971), "Hauptsatz for the intuitionistic theory of iterated inductive definitions". In: J.E. Fenstad (ed.), Proceedings of the 2nd Scandinavian Logic Symposium (Oslo 1970), Amsterdam, 179–216.
• Martin-Löf, P. (1990), "Mathematics of Infinity", Lectures Notes in Computer Science 417, 146.
• Martin-Löf, P. (1991), Lectures on Choice Sequences, University of Stockholm.
• Prawitz, D. (1985), "Remarks on some approaches to the concept of logical consequence", Synthese 62, 152–171.
• Prawitz, D. (2006), "Meaning approached via proofs", Synthese 148, 507–524.
• Ranta, A. (1995), Type Theoretical Grammar, Oxford University Press, 1995.
• Schroeder-Heister, P. (ed.) (1991), "Extensions of Logic Programming. International Workshop", Tübingen, FRG, December 1989, Proceedings. Springer Lecture Notes in Artificial Intelligence, Vol. 475, Berlin.
• Schroeder-Heister, P. (2002), "Resolution and the origins of structural reasoning: Early proof-theoretic ideas of Hertz and Gentzen", Bulletin of Symbolic Logic 8, 246–265.
• Schroeder-Heister, P. & Contu, P. (2005), "Folgerung". In: W. Spohn et al. (eds.), Logik in der Philosophie, Heidelberg: Synchron Wissenschaftsverlag, 247–276.
• Schroeder-Heister, P. (2008), "Proof-theoretic versus model-theoretic consequence". In: M. Peliš (ed.), The Logica Yearbook 2007, Prague: Filosofia 2008, 187–200.
• Schroeder-Heister, P. (2009), "Sequent Calculi and Bidirectional Natural Deduction: On the Proper Basis of Proof-Theoretic Semantics". In: M. Peliš (ed.), The Logica Yearbook 2008, London: College Publications 2009.
• Stalnaker, R. C. (1968), "A theory of conditionals". In Rescher N., editor, Studies in Logical Theory, pages 98–112. Basil Blackwell Publishers, Oxford.
• Stalnaker, R. C. (1975), "Indicative conditionals", Philosophia 5:269–286.