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)?
$\begingroup$
$\endgroup$
5
-
$\begingroup$ 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)? $\endgroup$– codyFeb 16, 2017 at 22:26
-
$\begingroup$ @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. $\endgroup$– fread2281Feb 16, 2017 at 22:33
-
1$\begingroup$ 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 $\endgroup$– Ulrik BuchholtzFeb 16, 2017 at 22:40
-
$\begingroup$ @UlrikBuchholtz why don't you turn your comment into an answer? $\endgroup$– codyFeb 17, 2017 at 16:05
-
$\begingroup$ @cody sure, done! $\endgroup$– Ulrik BuchholtzFeb 17, 2017 at 20:47
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
