Dorota Leszczyńska-Jasion

The pivotal characteristic of erotetic calculi, as introduced by Wiśniewski, is that its construction serves both purely proof-theoretical purposes and more philosophical—erotetic—aims. Although this book focuses on proof-theoretical aspects of the method, the picture would certainly not be complete without the analysis of questions. The idea standing behind the method of Socratic proofs was to model reasoning in which a question concerning derivability in the underlying logic is answered by ‘pure questioning’, without the reference to an external source of information (see, first of all, the introductions to [21, 26]). Therefore, the construction of ‘Socratic’ calculi consists in a formalization of rules transforming questions concerning derivability in the underlying logic. One could ask: what is meant by ‘derivability’ here, but we shall not make an attempt to answer this question until Sect. 5.6. At the time being, we assume that some common intuitions concerning the notion are sufficient.

Our interest in the questioning process is a philosophical enterprise at least since SocratesSocrates. Today, the logic of questionsLogic of questions is a branch of philosophical logic that aims at formal models of questioning and the way questions play their roles in natural languages. The discipline is often called ‘erotetic logic’Erotetic logic from the Greek word ‘ε`ρωτεμα\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\grave{\varepsilon }\rho \omega \tau \varepsilon \mu \alpha $$\end{document}’ (erotema), which means ‘question’. On the other hand, proof theory is a well-established discipline studying mathematical proofs. In particular, proof theory models the process of argumentation, especially of proving, by means of formal systems in which proofs are constructed.

In this chapter, we present the method of Socratic proofs for a number of propositional modal logics called basic. In [11], the author presented erotetic calculi for the class of basic modal propositional logics. By basic modal logics, we mean K\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\textsf {K}$$\end{document} and all of its proper extensions, characterized by any combination of the following properties of the accessibility relation: seriality (also called ‘extendability’), reflexivity, transitivity, symmetry, and Euclideanness. These five semantic properties can be combined in 25=32\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$2^5=32$$\end{document} ways, including the empty one, but some combinations of properties entail others.

This chapter presents erotetic calculi for classical logic—both propositional and first-order. As explained in the first chapter, erotetic calculi are systems that transform questions of certain formal languages. The intuitive interpretation underlying this formalism is that the aim of such transformations is to solve the problem expressed by the initial question. Thus, the entire process of transforming one question into further questions can be viewed as a model of question processing, understood as a cognitive, problem-solving activity. In the previous chapter, we also referred to this process as inquiring, and we completed the picture by comparing this process against that of justifying, where the latter can be seen as the intuitive counterpart of a proof in more traditional proof systems, such as axiomatic systems, sequent systems, or natural deduction systems.

This book contains a systematic and formal attempt to model solutions to problems such as: Is it possible to prove a question? Is it possible to prove something by the use of questions? Do the existing paradigms in the logic of questions allow one to combine questions and proofs? What are the results in this field? In developing answers, the book focuses on the applications of the method of Socratic proofs, and goes beyond that. It starts out with an overview of the leading paradigms, issues, problems and ready solutions in the logic of questions, and places Inferential Erotetic Logic and the method of Socratic proofs against a wider background. It then introduces these two methods in more detail and explains how they can be used for classical logic, intuitionistic propositional logic and for basic modal logics. Next, the book deals with issues specific to the field of the logic of questions, introducing the tools of Minimal Erotetic Semantics (MiES). The final chapters describe the translations between proof systems: from a Socratic transformation, derived in an erotetic calculus, into a sequent system.

Inferential erotetic logic and inquisitive semantics give accounts of questions and model various aspects of questioning. In this paper we concentrate upon connections between inquisitiveness, being the core concept of INQ, and question raising, characterized in IEL by means of the concepts of question evocation and erotetic implication. We consider the basic system InqB of INQ, remain at the propositional level and show, inter alia, that: a disjunction of all the direct answers to an evoked question is always inquisitive; a formula is inquisitive if, and only if it evokes a yes–no question whose affirmative answer expresses a possibility for the formula; inquisitive formulas evoke questions whose direct answers express all the possibilities for the formulas, and each question erotetically implies a question whose direct answers express the possibilities for the direct answers to the implying question

Kooi and Tamminga's correspondence analysis is a technique for designing proof systems, mostly, natural deduction and sequent systems. In this paper it is used to generate sequent calculi with invertible rules, whose only branching rule is the rule of cut. The calculi pertain to classical propositional logic and any of its fragments that may be obtained from adding a set of rules characterizing a two-argument Boolean function to the negation fragment of classical propositional logic. The properties of soundness and completeness of the calculi are demonstrated. The proof of completeness is conducted by Kalmár's method. Most of the presented sequent-calculus rules have been obtained automatically, by a rule-generating algorithm implemented in Python. Correctness of the algorithm is demonstrated. This automated approach allowed us to analyse thousands of possible rules' schemes, hundreds of rules corresponding to Boolean functions, and to nd dozens of those invertible. Interestingly, the analysis revealed that the presented proof-theoretic framework provides a syntactic characteristics of such an important semantic property as functional completeness.

Our aim is to model the behaviour of a cognitive agent trying to solve a complex problem by dividing it into sub-problems, but failing to solve some of these sub-problems. We use the powerful framework of erotetic search scenarios combined with Kleene’s strong three-valued logic. ESS, defined on the grounds of Inferential Erotetic Logic, has appeared to be a useful logical tool for modelling cognitive goal-directed processes. Using the logical tools of ESS and the three-valued logic, we will show how an agent could solve the initial problem despite the fact that the sub-problems remain unsolved. Thus our model not only indicates missing information but also specifies the contexts in which the problem-solving process may end in success despite the lack of information. We will also show that this model of problem solving may find use in an analysis of natural language dialogues.

This paper presents Rasiowa–Sikorski deduction systems for logics \, \, \ and \. For each of the logics two systems are developed: an R–S system that can be supplemented with admissible cut rule, and a \-version of R–S system in which the non-admissible rule of cut is the only branching rule. The systems are presented in a Smullyan-like uniform notation, extended and adjusted to the aims of this paper. Completeness is proved by the use of abstract refutability properties which are dual to consistency properties used by Fitting. Also the notion of admissibility of a rule in an R–S-system is analysed.

An erotetic calculus for a given logic constitutes a sequent-style proof-theoretical formalization of the logic grounded in Inferential Erotetic Logic ). In this paper, a new erotetic calculus for Classical Propositional Logic ), dual with respect to the existing ones, is given. We modify the calculus to obtain complete proof systems for the propositional part of paraconsistent logic CLuN and its extensions CLuNs and mbC. The method is based on dual resolution. Moreover, the resolution rule is non-clausal. According to the authors knowledge, this is the first account of resolution for mbC. Last but not least, as the method is grounded in IEL, it constitutes an important tool for the so-called question-processing.

I consider two cognitive phenomena: inquiring and justifying, as complementary processes running in opposite directions. I explain on an example that the former process is driven by questions and the latter is a codification of the results of the first one. Traditionally, proof theory focuses on the latter process, and thus describes the former, at best, as an example of a backward proof search. I argue that this is not the best way to analyze cognitive processes driven by questions, and that proof-theoretical analysis of questions can bring mutual benefits for both proof theory and erotetic logic. In the second part of my paper (sect. 6.3) I introduce the structural rules of weakening and contraction. Results concerning their admissibility are discussed. I also sketch an erotetic interpretation of the rule of weakening as reducing information noise, and that of contraction as securing information.

The aim of the paper is to present a reconstruction of the constitutive theses of cognitive relativism. The reconstruction is based on some examples of well-known theses and statements that are conceived to be relativistic. I distinguish three constituents of cognitive relativism: 1) the thesis of constructive character of cognition, 2) the thesis of pluralism of cognitive schemes, 3) the thesis of incommensurability of cognitive schemes. The rest of the article aims at, first, proving that Quine's philosophical standpoint is not relativistic as it clashes with the third thesis of relativism. And, second, I try to argue that a relativist may avoid the consequence of agnosticism but, which is not surprising, he/she has to radically reject the idea of the objective truth as the purpose of our cognition

The method of Socratic proofs (SP-method) simulates the solving of logical problem by pure questioning. An outcome of an application of the SP-method is a sequence of questions, called a Socratic transformation. Our aim is to give a method of translation of Socratic transformations into trees. We address this issue both conceptually and by providing certain algorithms. We show that the trees which correspond to successful Socratic transformations—that is, to Socratic proofs—may be regarded, after a slight modification, as Gentzen-style proofs. Thus proof-search for some Gentzen-style calculi can be performed by means of the SP-method. At the same time the method seems promising as a foundation for automated deduction.

The goal of this paper is to propose correspondence analysis as a technique for generating the so-called erotetic calculi which constitute the method of Socratic proofs by Andrzej Wiśniewski. As we explain in the paper, in order to successfully design an erotetic calculus one needs invertible sequent-calculus-style rules. For this reason, the proposed correspondence analysis resulting in invertible rules can constitute a new foundation for the method of Socratic proofs. Correspondence analysis is Kooi and Tamminga's technique for designing proof systems. In this paper it is used to consider sequent calculi with non-branching, invertible rules for the negation fragment of classical propositional logic and its extensions by binary Boolean functions.