Socratic trees (Q383562)

The paper is concerned with proof-theoretic aspects of the method of Socratic transformations. It is founded on inferential erotetic logic developed by Wiśniewski and based on the idea of solving logical problems by questioning. A question in this framework is formulated as a finite list of sequents with one formula in the succedent. The key notion is that of a Socratic transformation of initial question into simpler ones by means of suitable rules. The method was already applied succesfully by Wiśniewski and his collaborators to many nonclassical logics, including modal and paraconsistent logics. In this paper, a system of Socratic proofs for classical logic is examined. Any Socratic transformation (a proof in particular) is similar to a proof tree in hypersequent calculi. However, the rules of the system are dual, i.e. whereas hypersequents are meant as metalogical disjunctions over sequents, questions are meant as conjunctions. Due to that, Socratic transformations avoid branching. In the paper, it is shown that every Socratic transformation may be translated into a proof tree of annotated sequents, called Socratic tree, where branching is present but we avoid rewriting of sequents which are not active in some deductive step. This leads to introduction of some form of cut-free sequent calculus for classical logic with rules introducing negated formulae, double negations and special rules for introduction of disjunction (negated conjunction) to succedent. All steps of the transformation are presented in detail and with formal algorithms, including an algorithm for reduction of the complexity of obtained trees. One may find this method an interesting alternative to other solutions applied in automated deduction. The paper clarifies the relationship of Socratic transformations to sequent calculus. It may be of interest for students in proof theory and automated deduction.