The paper extends definitions and results of the method of tableaus, known for the classical logic, to intuitionistic logical systems. In particular, in classical proof theory (where a duality is available), it is easy to define dual tableaus and to prove their completeness. Within intuitionistic logic the tableaus (for signed formulas) were introduced by Fitting, who proved their completeness with respect to Kripke models. Here, we introduce dual intuitionistic tableaus (and dual Hintikka collections), and prove, following Fitting's method, their (adequacy and) completeness with respect to Kripke models
Duals of intuitionistic tableaus / Criscuolo, Giovanni; Tortora, Roberto. - In: RICERCHE DI MATEMATICA. - ISSN 0035-5038. - STAMPA. - 27:2(1978), pp. 355-365.
Duals of intuitionistic tableaus
CRISCUOLO, GIOVANNI;TORTORA, ROBERTO
1978
Abstract
The paper extends definitions and results of the method of tableaus, known for the classical logic, to intuitionistic logical systems. In particular, in classical proof theory (where a duality is available), it is easy to define dual tableaus and to prove their completeness. Within intuitionistic logic the tableaus (for signed formulas) were introduced by Fitting, who proved their completeness with respect to Kripke models. Here, we introduce dual intuitionistic tableaus (and dual Hintikka collections), and prove, following Fitting's method, their (adequacy and) completeness with respect to Kripke modelsI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.