FOM: Interpreting double negation

[Todd Wilson]

Stephen Simpson:
> Second, we need to remember that the double negation transform is
> purely formal does not respect philosophical motivation.

Vaughan Pratt:
> I beg to contradict.  Double negation as a transformation is much more
> than formalism.  Look at the meanings of intuitionistic formulas, which
> form a Heyting algebra.  Double negation translates those meanings upwards
> to the nearest element of the Boolean algebra canonically embedded in
> that Heyting algebra.
> 
> A philosophically well motivated interpretation of this motion is that it
> carries the truth value of the proposition "A" to that of the proposition
> "surely A", where "surely" satisfies
> 
> 	surely surely = surely
> 	A -> surely A             (but not conversely) 
> 	surely not = not surely   (so this is a strong form of surely)
> 	etc.
> 
> To see the philosophical motivation here, think what "not not A" says:
> it says that the absurdity of A is absurd.  While this is not quite
> as strong as flatly asserting A, it is nevertheless a strong vote of
> confidence in A that can be succinctly put as "surely A".

An alternate way to read "not not A" is:  "A is globally consistent".
As you say, what is being asserted is the impossibility of refuting A,
which, classically, is the same as asserting that A is consistent.
However, compared with mere consistency, double negation asserts more,
since, because of the identity

	not not (A /\ B) = (not not A) /\ (not not B) ,

it follows (using Compactness) that any set of globally consistent
statements is, taken together, consistent in the usual sense that
adding them as axioms doesn't force true = false.  This is of course
much stronger than the usual notion of consistency, where two
statements can each be consistent with a common theory (like CH and
not-CH are with ZF) but are inconsistent when taken together.

-- 
Todd Wilson
Computer Science Department
California State University, Fresno