| Copyright | (c) Artem Mavrin 2021 |
|---|---|
| License | BSD3 |
| Maintainer | artemvmavrin@gmail.com |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | Safe |
| Language | Haskell2010 |
AutoProof.Internal.Classical.Proof.Glivenko
Description
Glivenko translation.
Synopsis
- glivenkoTranslate :: Ord a => Judgement a -> Judgement a
- isProvableGlivenko :: Ord a => Judgement a -> Bool
Documentation
glivenkoTranslate :: Ord a => Judgement a -> Judgement a Source #
Translate one judgement into another such that the first is classically provable if and only if the second is intuitionistically provable. Specifically, the Glivenko translation of a judgement \(g \vdash a\) is the judgement \(g, \lnot a \vdash \bot\).