[Agda] Classical Mathematics for a Constructive World
wren ng thornton
wren at freegeek.org
Sun Dec 2 03:32:21 CET 2012
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
More information about the Agda
mailing list