Study on Synthetic Tableaux with Unrestricted Cut for First- Order Theories

The method of synthetic tableaux is a cut-based tableau system with synthesizing rules introducing complex
formulas. In this paper, we present the method of synthetic tableaux for Classical First-Order Logic, and we
propose a strategy of extending the system to first-order theories axiomatized by universal axioms. The strategy
was inspired by the works of Negri and von Plato. We illustrate the strategy with two examples: synthetic
tableaux systems for identity and for partial order. Clearly, there is a connection between Frege systems and ST
method, which we think should be further investigated. In particular, a question arises whether proof heuristics
working well in one system can be transferred to the other. Another problem pertains to the lack of a subformula
property being an effect of unrestricted cut applications. Is there a way to restrict the class of formulas appearing
in a proof tree for a given formula?