home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #18 / NN_1992_18.iso / spool / sci / logic / 1255 next >
Encoding:
Text File  |  1992-08-12  |  1.9 KB  |  44 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!mcsun!Germany.EU.net!ecrc!ecrc.de!sanjiva
  3. From: sanjiva@ecrc.de (Sanjiva Prasad)
  4. Subject: Question about Intuitionistic/Constructive logics
  5. Message-ID: <1992Aug12.110747.3850@ecrc.de>
  6. Sender: news@ecrc.de
  7. Reply-To: sanjiva@ecrc.de (Sanjiva Prasad)
  8. Organization: European Computer-Industry Research Centre, Munich
  9. Date: Wed, 12 Aug 1992 11:07:47 GMT
  10. Lines: 32
  11.  
  12.  
  13. Hi,  I have just started trying to learn about intuitionistic logic,
  14. and constructive logics in general, and am a little puzzled by some notions
  15. there, particularly of implication. Perhaps someone would be kind enough to
  16. help me. (By e-mail please, I don't read this newsgroup regularly).
  17.  
  18. From what I could understand from the book I was reading ("Intuitionism" by
  19. Heyting -- but I don't any more have access to the book ),  a mathematical 
  20. proposition demands a construction *with certain properties*  and can be 
  21. asserted when such a construction (in what seems to be an extremely general 
  22. sense of the term) is carried out.  
  23.  
  24. About implication: P->Q can be asserted iff there is a construction r such 
  25. that "joined to" any construction, say s, proving P, would automatically effect
  26. a construction proving Q. 
  27.  
  28. I am a little puzzled by what "joined to" exactly means.  In all the 
  29. examples I've seen, it has been juxtaposition of r and s -- which is
  30. okay for applications such as the type system for functional languages etc.
  31. (I think Heyting, in fact, says something to the effect of "by the definition 
  32. of  implication, the construction consists of simply the juxtaposition of
  33. r and s").
  34.  
  35. My first question is whether (and if so, what) constructions C[r,s] 
  36. more complicated than juxtaposition can be used for defining implication
  37. in an object language different from propositional intuitionistic logic. 
  38. That is, in general, what are these "certain properties" that the 
  39. constructions must have? 
  40.  
  41. Thanks,
  42.  
  43. Sanjiva Prasad            (sanjiva@ecrc.de)
  44.