Hypothetical reasoning: Its proof-theoretic analysis
Final Report Abstract
Hypothetical reasoning or reasoning under hypotheses is a key concept of logic. The project focussed on its proof-theoretic analysis. The Master Project, to which all participants equally contributed, dealt with the format of reasoning systems and key concepts of proof-theoretic semantics. Four Individual Projects extended this into different areas: (1) The relation between proof and truth, (2) the taxonomy of calculi for hypothetical reasoning from an epistemological point of view, (3) general frameworks for hypothetical reasoning to achieve a uniform treatment of philosophically relevant logical systems, and (4) historical investigations into the development of hypothetical reasoning. With the exception of (4), which did not receive funding, important contributions were made in all areas of the project. One of the main achievements is a clarification of the notion of “harmony” obtaining between logical rules, which is one of the central notions in proof-theoretic semantics. The clarification of this notion was obtained by using novel techniques, in particular employing second-order propositional logic, to model the notion. This lead to new results concerning the general form which logical rules must have in order to be in harmony. Another main achievement concerns the role of atomic, extra-logical rules in prooftheoretic semantics. Here several interesting, and even surprising, results have been obtained. Certain proof-theoretic semantics rely 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 have related this approach to admissibility-based semantics, and have shown that the latter significantly differs from the former. It could also be related to semantics based on the notion of construction, and it could be shown that the form of extra-logical rules admitted in atomic bases determines which logical rules are validated, as does the fact of whether bases are conceived as information states, which can be monotonely extended, or as non-extensible inductive definitions. We have been able to generalise these results: There are several proof-theoretic notions of validity which have been proposed in the literature, and for which completeness of intuitionistic logic has been conjectured. We have defined a notion of validity, which captures the common core of these notions, and we have refuted the completeness conjecture for it. This gives an answer to a long-standing question and raises several important issues, such as the relation between constructive and classical reasoning or the dependency of logical frameworks for hypothetical reasoning on the form of extra-logical rules which describe the specific domain that one is actually reasoning about. Overall, we now have a much better proof-theoretic understanding of what hypothetical reasoning is, how it is properly represented in logical frameworks and within proof-theoretic semantics, and what are the basic laws which govern hypothetical reasoning. This can also be a basis for a proof-theoretic analysis of hypothetical reasoning in areas beyond logic, for example in philosophy of science, informatics or law. A new project ("BeyondLogic") has been granted within the ANR-DFG programme, in which we apply our results on hypothetical reasoning in areas that lie beyond logic in the narrow sense. We have chosen philosophy of science as an application within philosophy, informatics as an application within the formal sciences, and law as an application within the field of social interaction. In each of these areas the idea of hypothetical reasoning plays a prominent role which can be used as a test case for our logical theories.
Publications
- (2013), “Constructive semantics, admissibility of rules and the validity of Peirce’s law” (with W. de Campos Sanz), Logic Journal of the IGPL 22, 297–308. First online: August 6, 2013
Piecha, T. & Schroeder-Heister, P.
- (2013), “Definitional Reflection and Basic Logic”, Annals of Pure and Applied Logic 164(4), 491–501
Schroeder-Heister, P.
- (2013), “From a single agent to multi-agent via hypersequents”, Logica Universalis 7, 147–166
Poggiolesi, F.
- (2014), “Are uniqueness and deducibility of identicals the same?”, Theoria
Naibo, A. & Petrolo, M.
(See online at https://dx.doi.org/10.1111/theo.12051) - (2014), “Failure of completeness in proof-theoretic semantics”, Journal of Philosophical Logic
Piecha, T. & Schroeder-Heister, P. (with W. de Campos Sanz)
(See online at https://dx.doi.org/10.1007/s10992-014-9322-x) - (2014), “On Flattening Elimination Rules”, Review of Symbolic Logic 7, 60–72
Olkhovikov, G. K. & Schroeder-Heister, P.
(See online at https://doi.org/10.1017/S1755020313000385) - (2014), “Proof theoretical semantics and feasibility”. In: M. Bourdeau & J. Dubucs (eds), Computability and Constructivity in Historical and Philosophical Perspective, pp. 135–157, Springer
Fichot, J.
- (2014), “The Calculus of Higher-Level Rules, Propositional Quantification, and the Foundational Approach to Proof-Theoretic Harmony”, Studia Logica 104, 1185–1216
Schroeder-Heister, P.
(See online at https://doi.org/10.1007/s11225-014-9562-3) - (2015), “Harmony in proof-theoretic semantics: A reductive analysis”. In: H. Wansing (ed.), Dag Prawitz on Proofs and Meaning, pp. 329-358, Springer
Schroeder-Heister, P.
