'not not A'에 해당되는 글 1건

  1. 2009.09.22 Constructive Logic (3)

Constructive Logic

공부 2009.09.22 14:57
일반적인 classical logic에서는 not not A가 A라는게 성립하는데

constructive logic에서는 그게 성립하지 않는다.

그러한 '사실' 은 알고있었는데 왜 그런지는 모르고 있다가

오늘 전산논리 수업덕분에 알게 되었다. 늦게라도 가길 잘한듯.


이유는 '∃'(어떤) 와 'V'(disjunction, or) 때문인데

constructive logic에서는 ∃x 가 존재하는것이 참임을 증명할때

그 x 를 명확히 지정해야하고

A or B 가 참이라는것을 증명하려면

A와 B중에 어떤게 참인지 지정해야 하기 때문이다.


예를들면 (not A) or A 는 classical logic에서는 항상 참이지만

constructive logic에서는 A를 모를 수도 있기 때문에 참이 아니다.


이런 설정은 기존의 classical logic에 비해 상당히 귀찮은 문제들을 만들어내는데,

그럼에도 불구하고 이렇게 하는 이유는

1. constructive logic을 이용한 proof으로부터 program을 추출할 수 있고

2. constructive logic이 classical logic보다 강력(포함)하기 때문이라네.


함수형 프로그래밍 언어에서 보여주는 독특하고 강력한 기능들이

전산논리 수업과 어떻게 연관이 되는지 조금씩 느낌이 오는것 같다.

'공부' 카테고리의 다른 글

Google Summer of Code2010 & CGAL  (0) 2010.03.30
O/R mapping  (0) 2010.02.26
Laplacian Pyramid on GPU  (1) 2010.01.13
Block-based Web Search  (0) 2009.12.06
오토 레포트  (3) 2009.11.04
Constructive Logic  (3) 2009.09.22
Posted by youknow04

댓글을 달아 주세요

  1. 희제 2009.09.22 21:59  댓글주소  수정/삭제  댓글쓰기

    그래서 왜 not not A = A(1)가 성립하지 않는건데?
    아래 설명은 전부 (not A) or A = true(2)가 성립하지 않는다는것에 대한 설명 아닌가?
    (1)과 (2)가 동치인가?

    • youknow04 2009.09.26 13:37  댓글주소  수정/삭제

      예를들어 A가 이방의 모든 사람은 한국인이다 일때
      not A는 이방의 어떤 사람은 한국인이 아니다 인데
      A가 거짓이더라도 not A가 참이 아닐 수도 있는게
      not A를 보이려면 '어떤' 사람이 한국인이 아닌지를 정해야하는데
      방에 사실 아무도 없거나 하면 그럴 수가 없잖아?

      이런식으로 '어떤'하고 'or' 때문에 A가 거짓이더라도 not A가 반드시 참이 되는게 아니라서, 클래시컬 로직에서처럼 not not A가 A가 아니라는 거였는데,

      지금보니까 너말데로 왜 not not A = A가 참인지는 본문에 설명이 없네...ㅎㅎ
      그리고 공부도 좀 더 해야겠다.
      댓글달면서 생각해보니 내가 제대로 알고있는건가 하는 생각이 드네.

  2. Euryale 2010.01.18 19:04  댓글주소  수정/삭제  댓글쓰기

    저도 대학에 들어가면 전산논리수업을 받아봐야겠네요