In this paper we present two calculi for intuitionistic logic. The first one, IG, is characterized by the fact that every proof-search terminates and termination is reached without jeopardizing the subformula property. As to the second one, SIC, proof-search terminates, the subformula property is preserved and moreover proof-search is performed without any recourse to metarules, in particular there is no need to back-track. As a consequence, proof-search in the calculus SIC is accomplished by a single tree as in classical logic.
Intuitionistic logic freed of all metarules / G.Corsi; G.Tassi. - In: THE JOURNAL OF SYMBOLIC LOGIC. - ISSN 0022-4812. - STAMPA. - 72:(2007), pp. 1204-1218.
Intuitionistic logic freed of all metarules
CORSI, GIOVANNA;
2007
Abstract
In this paper we present two calculi for intuitionistic logic. The first one, IG, is characterized by the fact that every proof-search terminates and termination is reached without jeopardizing the subformula property. As to the second one, SIC, proof-search terminates, the subformula property is preserved and moreover proof-search is performed without any recourse to metarules, in particular there is no need to back-track. As a consequence, proof-search in the calculus SIC is accomplished by a single tree as in classical logic.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
