Open AccessProof-search of propositional intuitionistic logic sequents by means of classical logic calculus
Author(s) -
Romas Alonderis
Publication year - 2008
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.2008.18105
Subject(s) - sequent , intuitionistic logic , propositional calculus , propositional variable , sequent calculus , zeroth order logic , natural deduction , curry–howard correspondence , mathematics , calculus (dental) , cut elimination theorem , many valued logic , intermediate logic , proof calculus , well formed formula , classical logic , algebra over a field , discrete mathematics , computer science , pure mathematics , programming language , multimodal logic , mathematical proof , description logic , medicine , geometry , dentistry
In the paper, we define some classes of sequents of the propositional intuitionistic logic. These are classes of primarily and α-primarily reducible sequents. Then we show how derivability of these sequents in a propositional intuitionistic logic sequent calculus LJ0 can be checked by means of a propositional classical logic sequent calculus LK0.