<p>As requested, I'm turning my comment into an answer:</p>

<p>For first order logic, the term you want to search for is “Glivenko classes”. Probably, very similar characterizations and techniques apply for higher order logic. See Sara Negri's <a href="http://www.helsinki.fi/~negri/glivenko_classes.pdf" rel="noreferrer" title="Glivenko sequent classes in the light of structural proof theory">Glivenko sequent classes in the light of structural proof theory</a>.</p>

CC BY-SA 3.0
2017-02-17T20:47:10.933Z
2017-02-17T20:47:10.933Z
Ulrik Buchholtz
<p>For what conditions on <code>P</code> and <code>Q</code>, does <code>P ⊢ Q</code> in classical logic imply <code>P ⊢ Q</code> in intuitonistic logic (for higher-order logic, though of course results for more restricted logics are relevant too)?</p>

CC BY-SA 3.0
2017-02-16T22:26:30.497Z
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
CC BY-SA 3.0
2017-02-16T22:33:52.540Z
@cody I'm interested in generalizing http://www.cse.chalmers.se/~danr/papers/intuit.pdf (CEGAR loop for IPL satisfiability) to more powerful logics (using also http://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
CC BY-SA 3.0
2017-02-16T22:40:22.430Z
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: http://www.helsinki.fi/~negri/glivenko_classes.pdf
Ulrik Buchholtz
CC BY-SA 3.0
2017-02-17T16:05:03.460Z
@UlrikBuchholtz why don't you turn your comment into an answer?
cody
CC BY-SA 3.0
2017-02-17T20:47:33.077Z
@cody sure, done!
Ulrik Buchholtz
<reference-request><lo.logic>
Intuitionistic fragments of classical logic
fread2281
# Intuitionistic fragments of classical logic

(Asked by: username_0 on 2017-02-16)

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)?

**Tags:** reference-request, lo.logic

> **Comments:**
> **username_1**: 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)?  
> **username_0**: @username_1 I'm interested in generalizing http://www.cse.chalmers.se/~danr/papers/intuit.pdf (CEGAR loop for IPL satisfiability) to more powerful logics (using also http://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.  
> **username_2**: 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: http://www.helsinki.fi/~negri/glivenko_classes.pdf  
> **username_1**: @UlrikBuchholtz why don't you turn your comment into an answer?  
> **username_2**: @username_1 sure, done!  

---

## 1 answers

### Answer by username_2 on 2017-02-17. Score: 8 | Accepted answer

As requested, I'm turning my comment into an answer:

For first order logic, the term you want to search for is “Glivenko classes”. Probably, very similar characterizations and techniques apply for higher order logic. See Sara Negri's [Glivenko sequent classes in the light of structural proof theory](http://www.helsinki.fi/~negri/glivenko_classes.pdf "Glivenko sequent classes in the light of structural proof theory").


---

