Abstract
We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two systems are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Beth, E. W., Semantic entailment and formal derivability, Mededelingen van de Koninklijke Nederlandes Akademie van Wetenschappen, Afdeling Letterkunde, N. R. Vol. 18, no. 13, Amsterdam, 1995, pp. 309–342. Reprinted in J. Hintikka (ed.), The Philosophy of Mathematics, Oxford readings in Philosophy, Oxford University Press, London, UK, 1969.
Beth E.W. (1959) The foundation of mathematics. North Holland, Amsterdam
Fitting, M., First-order Logic and Automated Theorem Proving, Springer-Verlag New York, 1990.
Gentzen, G., ‘Untersuchungen ber das logische Schliessen’, Mathematische Zeitschrift 39 (1934), 176–210, 405–431.
Düntsch I, Orłowska E. (2000) ‘A proof system for contact relation algebras’. Journal of Philosophical Logic 29, 241–262
Konikowska B. (2002) ‘Rasiowa-Sikorski Deduction Systems in Computer Science Applications’. Theoretical Computer Science 286, 323–366
MacCaull W., Orłowska E., (2002) ‘Correspondence results for relational proof systems with applications to the Lambek calculus’. Studia Logica 71, 279–304
Negri S., von Plato J. (2001) Structural Proof Theory. Cambridge University Press, Cambridge
Orłowska, E., Relational formalisation of nonclassical logics, in: C. Brink, W. Kahl, and G. Schmidt (eds), Relational Methods in Computer Science, Springer, Wien/New York, 1997, pp. 90–105.
Rasiowa H., Sikorski R., (1960) ‘On Gentzen theorem’. Fundamenta Mathematicae 48, 57–69
Rasiowa H., Sikorski R., (1963) Mathematics of Metamathematics. Polish Scientific Publishers, Warsaw
Schmidt, R., E. Orłowska, and U. Hustadt, Two proof systems for Peirce algebras, Proceedings of the 7th International Workshop on Relational Methods in Computer Science, Malente, Germany, 2003, Lecture Notes in Computer Science 3051, Springer, pp. 235–248.
Smullyan, R. M., First Order Logic, Springer, Berlin, Heidelberg, New York, 1971.
Wiśniewski, A., and V. Shagin, ‘Socratic Proofs for uantifiers’, Journal of Philosophical Logic 35, No. 2 (2006), 147–178.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Golińska-Pilarek, J., Orłowska, E. Tableaux and Dual Tableaux: Transformation of Proofs. Stud Logica 85, 283–302 (2007). https://doi.org/10.1007/s11225-007-9055-8
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-007-9055-8