A cut-based tableau system with synthesising rules introducing complex formulas is the process of synthetic tableaux. In this paper, for Classical First-Order Logic, we present the method of synthetic tableaux, and we suggest a strategy to expand the system to first-order theories axiomatized by universal axioms. The method was influenced by the works of Negri and von Platon. We explain the approach with two examples: structures of synthetic tableaux for identity and partial order. Clearly, there is a connection between Frege and the ST system, which we believe should be further investigated. In fact, there is a question whether evidence heuristics functioning well in one system can be transferred to the other. Another issue is that a consequence of unregulated cut applications is the absence of a subformula property. Is there a way for a given formula to limit the class of formulas occurring in a proof tree?
Author(s) Details
Department of Logic and Cognitive Science, Faculty of Psychology and Cognitive Science, Adam Mickiewicz University, ul. Szamarzewskiego 89a, 60-568 Poznań,
Szymon Chlebowski
Department of Logic and Cognitive Science, Faculty of Psychology and Cognitive Science, Adam Mickiewicz University, ul. Szamarzewskiego 89a, 60-568 Poznań, Poland.
View Book :- https://bp.bookpi.org/index.php/bpi/catalog/book/339
