
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.
Mechanization of proofs and logical operations, sequent calculi, erotetic logic, Structure of proofs, Socratic transformations, proof theory, automated deduction
Mechanization of proofs and logical operations, sequent calculi, erotetic logic, Structure of proofs, Socratic transformations, proof theory, automated deduction
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 13 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
