home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #1 / NN_1993_1.iso / spool / sci / logic / 2582 < prev    next >
Encoding:
Text File  |  1993-01-12  |  3.0 KB  |  57 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!stanford.edu!CSD-NewsHost.Stanford.EDU!Sunburn.Stanford.EDU!pratt
  3. From: pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt)
  4. Subject: Re: Multiple Truth Values
  5. Message-ID: <1993Jan12.083955.19685@CSD-NewsHost.Stanford.EDU>
  6. Sender: news@CSD-NewsHost.Stanford.EDU
  7. Organization: Computer Science Department,  Stanford University.
  8. References: <1993Jan9.191854.10303@dcs.qmw.ac.uk> <1993Jan10.005215.13278@CSD-NewsHost.Stanford.EDU> <1993Jan11.194737.11729@dcs.qmw.ac.uk>
  9. Date: Tue, 12 Jan 1993 08:39:55 GMT
  10. Lines: 45
  11.  
  12. In article <1993Jan11.194737.11729@dcs.qmw.ac.uk> arodgers@dcs.qmw.ac.uk (Angus H Rodgers) writes:
  13. >In <1993Jan10.005215.13278@CSD-NewsHost.Stanford.EDU>
  14. >pratt@Sunburn.Stanford.EDU (Vaughan R. Pratt) writes:
  15. >>[...] double negation
  16. >>served to retract a Heyting algebra onto a Boolean subalgebra of it
  17. >
  18. >Is this by any chance related to the construction of the regular open
  19. >algebra of a topological space?
  20.  
  21. I haven't heard of that construction.  The retraction is the model
  22. theoretic equivalent (i.e. the effect on the models) of the proof
  23. theoretic statement that Boolean algebras can be axiomatized by adding
  24. ~~x = x to an axiomatization of Heyting algebras.  Any two distinct
  25. elements x and ~~x of a given Heyting algebra are forced into
  26. coincidence by this additional requirement.  The effect is to retract
  27. that Heyting algebra (model of intuitionistic logic) H onto the largest
  28. Boolean algebra (model of classical logic) embedded in H.
  29.  
  30. The result of the identification is to reduce the variety of truth
  31. values in one's logic.  In intuitionistic logic not not x is in general
  32. a weaker statement than x.  (It even *sounds* weaker, one respect in
  33. which natural language seems to be intuitionistic rather than
  34. classical.  This furnishes some evidence against two-valued logic,
  35. necessarily Boolean, as the logic of natural language.)  That is, x
  36. implies not not x but not necessarily the converse.  So if you
  37. truthfully 'fess right up with "I broke the vase" then it cannot be
  38. that you did not break the vase.  But if you say "I didn't not break
  39. the vase" then while this tips us off to some degree of culpability on
  40. your part it does not permit us to infer intuitionistically that you
  41. actually broke the vase.
  42.  
  43. The passage from intuitionistic to classical logic erases this
  44. distinction.
  45.  
  46. A common misconception is that eschewing the axiom ~~x = x deprives us
  47. of part of mathematics.  As Goedel showed, every classically valid
  48. theorem of mathematics has its intuitionistic counterpart, differing at
  49. most in having a few double negatives sprinkled through it.  I like to
  50. read "not not" as "surely."  All that adding ~~x=x to logic does to
  51. mathematics then is to erase all instances of "surely" from theorems.
  52. That is, the nuance expressed by the difference between the truth of
  53. "x" and that of "not not x" is simply suppressed by Boolean logic,
  54. which with only two truth values cannot "hear" the difference.
  55. -- 
  56. Vaughan Pratt            There's safety in large condition numbers.
  57.