7
$\begingroup$

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

$\endgroup$
  • $\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$ – cody Feb 16 '17 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$ – fread2281 Feb 16 '17 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 Buchholtz Feb 16 '17 at 22:40
  • $\begingroup$ @UlrikBuchholtz why don't you turn your comment into an answer? $\endgroup$ – cody Feb 17 '17 at 16:05
  • $\begingroup$ @cody sure, done! $\endgroup$ – Ulrik Buchholtz Feb 17 '17 at 20:47
8
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.