직관 논리 문서 원본 보기

{{위키데이터 속성 추적}}
[[논리학]]에서 '''직관 논리'''(直觀論理, {{llang|en|intuitionistic logic}})는 수학적 [[직관주의]]에 근거하여 [[귀류법]]을 배척하는 논리 체계이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만 그 역은 일반적으로 성립하지 않는 특징이있다.
이처럼 직관주의 논리학은 이중부정의 일부법칙이 성립하지 않는다.
== 정의 ==
'''직관 논리'''는 힐베르트 식으로 다음과 같이 서술되는 논리 체계이다.

=== [[통사론]] ===
직관 [[명제 논리]]에서, 명제 <math>\phi,\chi,\dots</math>로부터 다음과 같은 새 명제들을 구성할 수 있다.
* [[논리곱]] <math>\phi\land\chi</math>. 이는 "<math>\phi</math>이며 또한 <math>\chi</math>"라고 읽는다.
* [[논리합]] <math>\phi\lor\chi</math>. 이는 "<math>\phi</math>이거나 또는 <math>\chi</math>"라고 읽는다.
* [[함의]] <math>\phi\implies\chi</math>. 이는 "만약 <math>\phi</math>이라면 <math>\chi</math> 또한 성립한다"라고 읽는다.
* [[거짓]] <math>\bot</math>. 이는 거짓 명제로 읽는다.
이들로부터 다음과 같은 기호들을 정의한다.
* [[부정]] <math>\lnot\phi</math>는 <math>\phi\implies\bot</math>을 줄인 것이며, "<math>\phi</math>가 아니다"라고 읽는다.
* [[동치]] <math>\phi\iff\chi</math>는 <math>(\phi\implies\chi)\land(\chi\implies\phi)</math>를 줄인 것이며, "<math>\phi</math>와 <math>\chi</math>는 서로 동치이다"라고 읽는다.
직관 [[술어 논리]]에서는 명제 논리 연산자 밖에도, 자유 변수 <math>x</math>를 가지는 명제 <math>\phi(x)</math>로부터 다음과 같은 새 명제들을 구성할 수 있다.
* (존재 술어) <math>\exists x\colon\phi(x)</math>. 이는 "<math>\phi(x)</math>를 성립시키는 <math>x</math>가 존재한다"라고 읽는다.
* (보편 술어) <math>\forall x\colon\phi(x)</math>. 이는 "모든 <math>x</math>에 대하여, <math>\phi(x)</math>가 성립한다"라고 읽는다.

=== 추론 ===
직관 [[명제 논리]]의 유일한 추론법은 [[전건 긍정의 형식]]이며, 이는 다음과 같다.
:<math>\phi,\phi\implies\chi\vdash\chi</math>
직관 [[술어 논리]]에서는 다음과 같은 두 변수 일반화 규칙이 추가된다. 여기서, <math>x</math>는 <math>\phi</math>에서 자유 변수가 아닌 변수(한정 변수이거나, 아니면 <math>\phi</math>에 등장하지 않는 변수)이다.
* <math>\phi\implies\psi\vdash\phi\implies\forall x\colon\psi</math>
* <math>\phi\implies\psi\vdash\phi\implies\exists x\colon\psi</math>

=== 공리 ===
직관 명제 논리의 공리들은 다음과 같다. 임의의 명제 <math>\phi,\chi,\psi</math>에 대하여,
* (함의 조건의 추가) <math>\vdash\phi \implies (\chi\implies\phi )</math>
* (함의의 분배) <math>\vdash(\phi \implies (\chi \implies \psi )) \implies ((\phi \implies \chi ) \implies (\phi \implies \psi ))</math>
* (논리곱의 좌측 제거) <math>\vdash\phi \land \chi \implies \chi </math>
* (논리곱의 우측 제거) <math>\vdash\phi \land \chi \implies \phi </math>
* (논리곱과 함의 조건의 추가) <math>\vdash\phi \implies (\chi \implies(\phi \land \chi ))</math>
* (논리합의 좌측 추가) <math>\vdash\chi \implies \phi \lor \chi </math>
* (논리합의 우측 추가) <math>\vdash\phi \implies \phi \lor \chi </math>
* (함의 조건들의 논리합) <math>\vdash(\phi \implies \psi ) \implies ((\chi \implies \psi ) \implies (\phi \lor \chi \implies \psi ))</math>
* (거짓은 모든 명제를 함의) <math>\vdash\bot \implies \phi </math>
직관 술어 논리에서는 다음 두 공리들이 추가로 성립한다. 여기서 <math>t</math>는 <math>\phi(t)</math>에서 한정 변수가 아닌 변수이다.
* (보편 기호의 특수화) <math>\vdash(\forall x\colon\phi(x))\implies\phi(t)</math>
* (존재 기호의 추가) <math>\vdash\phi(t)\implies(\exists x\colon\phi(x))</math>

== 성질 ==
=== 명제의 격자 ===
주어진 명제 <math>\phi</math>로부터, 고전 명제 논리에서는 <math>\bot,\phi,\lnot\phi,\top</math> 네 개의 명제밖에 정의할 수 없지만, 직관 명제 논리에서는 이로부터 무한한 수의, 서로 동치이지 않는 명제들이 존재한다. 이를 '''리에게르-니시무라 사다리'''({{llang|en|Rieger–Nishimura ladder}})라고 하며, 라디슬라프 스반테 리에게르({{llang|cs|Ladislav Svante Rieger}})<ref>{{저널 인용|성=Rieger|이름=L.|제목=On the lattice theory of Brouwerian propositional logics|저널=Spisy vydávané Přírodovědeckou fakultou University Karlovy|권=189|날짜=1949|쪽=1–40|mr=0040245|언어=en}}</ref>와 니시무라 이와오<ref>{{저널 인용|저널=The Journal of Symbolic Logic|권=25|호=4|날짜=1960-12|쪽=327-331|제목=On Formulas of One Variable in Intuitionistic Propositional Calculus|이름=Iwao|성=Nishimura|mr=142456|zbl=0108.00302|doi=10.2307/2963526|jstor=2963526|언어=en}}</ref>가 정의하였다.
:[[파일:Rieger-Nishimura.svg]]

=== 고전 논리와의 관계 ===
직관 논리는 [[고전 논리]]의 일부분이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만, 고전적으로 참이지만 직관 논리에서는 증명할 수 없는 명제들이 존재한다. 이러한 명제들은 다음을 들 수 있다.
* ([[배중률]]) <math>\phi\lor\lnot\phi</math>
* (이중 부정 삭제) <math>\lnot\lnot\phi\implies\phi</math>
* ([[찰스 샌더스 퍼스|퍼스]]의 법칙) <math>\left(\phi\implies\chi)\implies\phi\right)\implies\phi</math>

=== 의미론 ===
직관 논리의 경우, 다양한 의미론이 존재한다. 이 가운데 하나로는 다음과 같은 [[위상수학]]적 의미론을 생각할 수 있다. 어떤 [[위상 공간 (수학)|위상 공간]] <math>X</math>에 대하여, 직관 논리를 다음과 같이 해석하자.
* 명제는 <math>X</math>의 [[열린 집합]]에 대응한다.
* [[논리합]] <math>\phi\lor\chi</math>는 [[합집합]] <math>\phi\cup\chi</math>에 대응한다.
* [[논리곱]] <math>\phi\land\chi</math>는 [[교집합]] <math>\phi\cap\chi</math>에 대응한다.
* [[함의]] <math>\phi\implies\chi</math>는 [[교집합]] <math>\operatorname{int}\left((X\setminus\phi)\cup\chi\right)</math>에 대응한다. 여기서 <math>\operatorname{int}</math>는 집합의 [[내부 (위상수학)|내부]]이다.
* 거짓 <math>\bot</math>은 [[공집합]] <math>\varnothing</math>이다.
이로부터 정의되는 부정과 동치는 다음과 같다.
* [[부정]] <math>\lnot\phi</math>는 [[여집합]]의 [[내부 (위상수학)|내부]] <math>\operatorname{int}(X\setminus\phi)</math>에 대응한다.
* [[동치]] <math>\phi\iff\chi</math>는 <math>\operatorname{int}\left((\phi\cap\chi)\cup\left(X\setminus(\phi\cup\chi)\right)\right)</math>에 대응한다.
일반적인 위상 공간에 대하여 증명할 수 있는 모든 명제들은 직관 논리에서 참임을 보일 수 있다.

이 밖에도, [[양상 논리]]의 [[크립키 모형]]({{llang|en|Kripke model}})을 직관 논리에서도 사용할 수 있다.

== 역사 ==
[[라위트전 브라우어르]]의 [[직관주의]] 수학을 형식화하기 위하여, [[아런트 헤이팅]]이 도입하였다.

== 응용 ==
직관 논리는 일반적인 [[토포스]]의 내부 논리({{llang|en|internal logic}})로 등장한다.<ref>{{서적 인용|이름=Saunders|성=Mac Lane|저자링크=손더스 매클레인|공저자=Ieke Moerdijk|날짜=1992|제목=Sheaves in geometry and logic: a first introduction to topos theory|출판사=Springer|zbl=0822.18001|doi=10.1007/978-1-4612-0927-0|isbn=978-0-387-97710-2|총서=Universitext|issn=0172-5939|언어=en}}</ref> (표준적인) 집합의 [[토포스]]나, [[이산 공간]] 위의 [[층 (수학)|층]]의 토포스 등에서는 고전 논리가 성립하지만, 예를 들어 [[이산 공간]]이 아닌 [[위상 공간 (수학)|위상 공간]] 위의 층의 토포스에서는 고전 논리가 성립하지 않고, 직관 논리를 사용해야만 한다.

== 각주 ==
{{각주}}
* {{서적 인용|url=http://www.kupress.com/books/논리철학/|저자=여훈근|제목=논리철학|날짜=2000-06-17|isbn=89-7641-409-8|총서=인문사회과학총서|권=40|출판사=고려대학교 출판부|언어=ko|확인날짜=2020-01-21|보존url=https://web.archive.org/web/20160528164722/http://www.kupress.com/books/%eb%85%bc%eb%a6%ac%ec%b2%a0%ed%95%99/|보존날짜=2016-05-28|url-status=dead}}
* {{서적 인용|장url=http://www.phil.uu.nl/~dvdalen/articles/Blackwell%28Dalen%29.pdf|장=Intuitionistic logic|이름=Dirk|성=van Dalen|제목=The Blackwell guide to philosophical logic|url=http://www.wiley.com/WileyCDA/WileyTitle/productCd-0631206930.html|출판사=Blackwell|날짜=2001-08|쪽=224–257|doi=10.1111/b.9780631206934.2001.00014.x |isbn=978-0-631-20693-4|zbl=1002.03053|언어=en}}
*(직관주의 논리,한국수학사학회지 = The Korean journal for history of mathematics v.12 no.1 , 1999년, pp.32 - 44 이승온,  김혁수,, 박진원 ,  이병식  )https://scienceon.kisti.re.kr/commons/util/originalView.do?cn=JAKO199911921897668&oCn=JAKO199911921897668&dbt=JAKO&journal=NJOU00294661
*(논리연구14-2(2011)pp.39～75 - 직관주의적 유형론에서의 명제와 판단, 정인교-KRF-2007-327-A00159)http://logicalkorea.com/attach/paper/14-2-ChungIK.pdf

== 외부 링크 ==
* {{eom|title=Intuitionistic logic}}
* {{eom|title=Intuitionistic propositional calculus}}
* {{웹 인용|url=http://plato.stanford.edu/entries/logic-intuitionistic/|제목=Intuitionistic logic|웹사이트=Stanford Encyclopedia of Philosophy|날짜=2014-05-23|성=Moschovakis|이름=Joan|언어=en}}
* {{웹 인용|url=http://plato.stanford.edu/entries/intuitionistic-logic-development/|제목=The development of intuitionistic logic|웹사이트=Stanford Encyclopedia of Philosophy|날짜=2009-04-01|성=van Atten|이름=Mark|언어=en}}
* {{웹 인용|url=http://plato.stanford.edu/entries/intuitionism/|제목=Intuitionism in the Philosophy of Mathematics|웹사이트=Stanford Encyclopedia of Philosophy|날짜=2013-08-14|성=Iemhoff|이름=Rosalie|언어=en}}
* {{웹 인용|url=http://ncatlab.org/nlab/show/intuitionistic+logic|제목=Intuitionistic logic|웹사이트=nLab|언어=en}}

== 같이 보기 ==
* [[직관주의]]
* [[초직관 논리]]

{{논리학}}

{{전거 통제}}

[[분류:직관 논리| ]]