[Agda] Classical Mathematics for a Constructive World

[wren ng thornton]

On 11/27/12 3:58 PM, Dan Licata wrote:
> Hi Martin,
>
> Thanks!  That makes more sense.
>
> I'm still a little confused about the difference between
>
>    Exists X : Type. ¬(X + ¬ X)
>
> which we cannot prove (it would be contradictory with the usual fact
> that Pi X:Type. ¬¬(X + ¬ X) holds) and
>
>    ¬Em = ¬(Pi X : Type. X + ¬X)
>
> which we can prove with univlanece.
>
> I guess this is just saying that classical logic is inconsistent with
> univalence, but it's a little surprising to me that a mere de Morgan
> will do us in.

I'm not sure I'd call this a "mere de Morgan"; of the four de Morgan's 
laws, this is precisely the one which always causes trouble. Indeed, in 
intuitionistic logic (a la Heyting) we get the schema:

     (exists X. ¬(P X)) -> ¬(forall X. P X)

However we do not get the converse. Indeed, the converse is precisely 
the generalized Markov's principle (GMP):

     ¬(forall X. P X) -> (exists X. ¬(P X))

GMP is accepted as an axiom by the Russian constructivists, and this can 
be somewhat justified by the fact that they were primarily looking at 
finite objects--- and hence if a property is not true everywhere, then 
one can exhaust the finite space in order to identify a counterexample.

On the other hand, Brouwer considered GMP to be false. And though 
Heyting's formalism of intuitionism cannot refute GMP, other 
formalizations of Brouwer's intuitionism can. This is part of what makes 
Brouwer's intuitionism anti-classical--- since, of course, GMP is 
inhabited in classical models.


> Do you have any intuition for this?  I want to say that it has something
> to do with continuity:   ¬Em is asserting the absence of a "continuous"
> proof of excluded middle.

If you consider the Russian constructivists to be correct ---i.e., that 
GMP is admissible when studying the sorts of objects they studied---, 
then the connection to continuity/compactness/etc is going to show up 
once you admit objects of study which cannot be exhaustively searched. 
Once you have such objects, the GMP begins to look rather dubious. It 
may be the case that for every proof p of (forall X. P X) we can 
construct some Y_p such that ¬(P Y_p). However, as indicated by the 
subscripting, the specific Y_p we come up with may depend on the exact 
structure of p. It need not be the case that, in the absence of the 
additional information that the content of p provides, we can identify 
some Y such that ¬(P Y).


You run into similar issues in separation logic. When using Hoare 
separation logic we get this nice frame rule:

     {P}   C {Q}
     -------------
     {P*R} C {Q*R}

(subject to some mild side conditions about R). People often focus on 
the fact that the addition of R is preserved from precondition to 
postcondition (i.e., parts of the heap which the program C does not 
touch, in fact remain the same and don't just magically change 
themselves); however, as Lindsey Kuper mentioned recently, one can also 
consider the important fact that the Q of the antecedent's postcondition 
is also preserved in the succedent's postcondition (i.e., the program C 
isn't going to change its side-effects when given a bigger heap). But 
there's an important caveat here, which Neel Krishnaswami mentions. If 
we desugar that rule and look at the actual conditions required to make 
a Hoare triple true, you end up with a similar sort of indexing issue as 
above. Just because we preserve the fact of there existing a heap which 
satisfies Q, that doesn't mean we preserve the *specific* heap that was 
used to witness the existence of a heap satisfying Q.

-- 
Live well,
~wren