# Intuitionistic fragments of classical logic

For what conditions on P and Q, does P ⊢ Q in classical logic imply P ⊢ Q in intuitonistic logic (for higher-order logic, though of course results for more restricted logics are relevant too)?

• There are many results of this form, usually restricting $P$ and $Q$ to "negative fragments" or restricting their complexity (to, say, $\Pi^0_2$ statements of arithmetic). Can you give more context about what kind of result you're interested in (and why)? – cody Feb 16 '17 at 22:26
• @cody I'm interested in generalizing cse.chalmers.se/~danr/papers/intuit.pdf (CEGAR loop for IPL satisfiability) to more powerful logics (using also profs.sci.univr.it/~bonacina/talks/MSR2016sggs-slides.pdf (DPLL-style procedure for first-order logic) and maybe a higher-order version of that). Basically, for (some?) intuitionistic fragments an intuitionistic validity procedure can just use a classical satisfiability procedure. – fread2281 Feb 16 '17 at 22:33
• For first order logic, the term you want to search for is “Glivenko classes”. Probably, similar characterizations and techniques apply for higher order logic. See: helsinki.fi/~negri/glivenko_classes.pdf – Ulrik Buchholtz Feb 16 '17 at 22:40
• @UlrikBuchholtz why don't you turn your comment into an answer? – cody Feb 17 '17 at 16:05
• @cody sure, done! – Ulrik Buchholtz Feb 17 '17 at 20:47