A Proof System for Fork Algebras and its Applications to Reasoning in Logics Based on Intuitionism

FRIAS, MARCELO FABIAN; ORLOWSKA, EWA

LOGIQUE ET ANALYSE

National Centre for Logical Investigations

Año: 1997 vol. 150 p. 239 - 284

0024-5836

Relational proof systems have been already proposed for certain modal, relevant and substructural logics. In this paper we present a general method for constructing Rasiowa-Sikorski-style deduction systems for nonclassical logics within the powerful relational framework of fork algebras. We apply the method to intuitionistic logic and a wide class of intermediate logics. The method consists in establishing interpretability of these logics in relational logics based on fork algebras (referred to as fork logics) and in developing a Rasiowa-Sikorski-like calculus for the respective fork logics. We prove soundness and completeness of the presented proof systems.