🚀 go-pugleaf

In article <1993Jan11.194737.11729@dcs.qmw.ac.uk> arodgers@dcs.qmw.ac.uk (Angus H Rodgers) writes:
>In <1993Jan10.005215.13278@CSD-NewsHost.Stanford.EDU>
>pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt) writes:
>>[...] double negation
>>served to retract a Heyting algebra onto a Boolean subalgebra of it
>
>Is this by any chance related to the construction of the regular open
>algebra of a topological space?

I haven't heard of that construction.  The retraction is the model
theoretic equivalent (i.e. the effect on the models) of the proof
theoretic statement that Boolean algebras can be axiomatized by adding
~~x = x to an axiomatization of Heyting algebras.  Any two distinct
elements x and ~~x of a given Heyting algebra are forced into
coincidence by this additional requirement.  The effect is to retract
that Heyting algebra (model of intuitionistic logic) H onto the largest
Boolean algebra (model of classical logic) embedded in H.

The result of the identification is to reduce the variety of truth
values in one's logic.  In intuitionistic logic not not x is in general
a weaker statement than x.  (It even *sounds* weaker, one respect in
which natural language seems to be intuitionistic rather than
classical.  This furnishes some evidence against two-valued logic,
necessarily Boolean, as the logic of natural language.)  That is, x
implies not not x but not necessarily the converse.  So if you
truthfully 'fess right up with "I broke the vase" then it cannot be
that you did not break the vase.  But if you say "I didn't not break
the vase" then while this tips us off to some degree of culpability on
your part it does not permit us to infer intuitionistically that you
actually broke the vase.

The passage from intuitionistic to classical logic erases this
distinction.

A common misconception is that eschewing the axiom ~~x = x deprives us
of part of mathematics.  As Goedel showed, every classically valid
theorem of mathematics has its intuitionistic counterpart, differing at
most in having a few double negatives sprinkled through it.  I like to
read "not not" as "surely."  All that adding ~~x=x to logic does to
mathematics then is to erase all instances of "surely" from theorems.
That is, the nuance expressed by the difference between the truth of
"x" and that of "not not x" is simply suppressed by Boolean logic,
which with only two truth values cannot "hear" the difference.
-- 
Vaughan Pratt			There's safety in large condition numbers.