home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #1 / NN_1993_1.iso / spool / sci / logic / 2583 < prev    next >
Encoding:
Text File  |  1993-01-12  |  1.9 KB  |  35 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!cs.utexas.edu!usc!howland.reston.ans.net!spool.mu.edu!agate!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.094423.20326@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> <1993Jan10.151351.19163@husc3.harvard.edu>
  9. Date: Tue, 12 Jan 1993 09:44:23 GMT
  10. Lines: 23
  11.  
  12. In article <1993Jan10.151351.19163@husc3.harvard.edu> zeleny@husc10.harvard.edu (Mikhail Zeleny) writes:
  13. >
  14. >To recapitulate the substance of past battles, Alfred Tarski, in his
  15. >article "On Extensions of Incomplete Systems of Sentential Calculus",
  16. >appeals to what has come to be known as Lindenbaum's Lemma, proving that
  17. >there exists but one (absolutely) complete and consistent extension of
  18. >incomplete sentential calculi, which contain as theorems certain
  19. >formulae (namely, CpCqp, CpCCpqq, and CCqrCCpqCpr), expressing naturally
  20. >evident properties of material implication.
  21.  
  22. It is worth mentioning that CpCCpqq (i.e. p->((p->q)->q)) is derivable
  23. from the other two (that is, from p->(q->p) (= K) and
  24. (q->r) -> ((p->q)->(p->r))) (= S) by modus ponens, mainly via the same
  25. derivation by which the lambda calculus combinator C (converse, Cfxy
  26. reduces to fyx) is derived from the combinators K and S by
  27. application.  This yields (p->(q->r)) -> (q->(p->r)), now substitute
  28. q->r for p and the rest is clear.  K and S as propositions constitute a
  29. complete axiomatization of the implicational fragment of intuitionistic
  30. logic.  Peirce's axiom ((p->q)->p)->p supplies an example of an
  31. implicational proposition that is in the classical theory but not the
  32. intuitionistic.
  33. -- 
  34. Vaughan Pratt            There's safety in large condition numbers.
  35.