직관 논리

틀:위키데이터 속성 추적 논리학에서 직관 논리(直觀論理, 틀:Llang)는 수학적 직관주의에 근거하여 귀류법을 배척하는 논리 체계이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만 그 역은 일반적으로 성립하지 않는 특징이있다. 이처럼 직관주의 논리학은 이중부정의 일부법칙이 성립하지 않는다.

정의

직관 논리는 힐베르트 식으로 다음과 같이 서술되는 논리 체계이다.

통사론

직관 명제 논리에서, 명제 $\varphi ,\chi ,\dots$로부터 다음과 같은 새 명제들을 구성할 수 있다.

• 논리곱 $\varphi \wedge \chi$. 이는 "$\varphi$이며 또한 $\chi$"라고 읽는다.
• 논리합 $\varphi \vee \chi$. 이는 "$\varphi$이거나 또는 $\chi$"라고 읽는다.
• 함의 $\varphi ⟹\chi$. 이는 "만약 $\varphi$이라면 $\chi$ 또한 성립한다"라고 읽는다.
• 거짓 $\mathrm{\perp }$. 이는 거짓 명제로 읽는다.

이들로부터 다음과 같은 기호들을 정의한다.

• 부정 $\mathrm{\neg }\varphi$는 $\varphi ⟹\mathrm{\perp }$을 줄인 것이며, "$\varphi$가 아니다"라고 읽는다.
• 동치 $\varphi ⟺\chi$는 $(\varphi ⟹\chi )\wedge (\chi ⟹\varphi )$를 줄인 것이며, "$\varphi$와 $\chi$는 서로 동치이다"라고 읽는다.

직관 술어 논리에서는 명제 논리 연산자 밖에도, 자유 변수 $x$를 가지는 명제 $\varphi (x)$로부터 다음과 같은 새 명제들을 구성할 수 있다.

• (존재 술어) $\mathrm{\exists }x:\varphi (x)$. 이는 "$\varphi (x)$를 성립시키는 $x$가 존재한다"라고 읽는다.
• (보편 술어) $\mathrm{\forall }x:\varphi (x)$. 이는 "모든 $x$에 대하여, $\varphi (x)$가 성립한다"라고 읽는다.

추론

직관 명제 논리의 유일한 추론법은 전건 긍정의 형식이며, 이는 다음과 같다.

$\varphi ,\varphi ⟹\chi ⊢\chi$

직관 술어 논리에서는 다음과 같은 두 변수 일반화 규칙이 추가된다. 여기서, $x$는 $\varphi$에서 자유 변수가 아닌 변수(한정 변수이거나, 아니면 $\varphi$에 등장하지 않는 변수)이다.

• $\varphi ⟹\psi ⊢\varphi ⟹\mathrm{\forall }x:\psi$
• $\varphi ⟹\psi ⊢\varphi ⟹\mathrm{\exists }x:\psi$

공리

직관 명제 논리의 공리들은 다음과 같다. 임의의 명제 $\varphi ,\chi ,\psi$에 대하여,

• (함의 조건의 추가) $⊢\varphi ⟹(\chi ⟹\varphi )$
• (함의의 분배) $⊢(\varphi ⟹(\chi ⟹\psi ))⟹((\varphi ⟹\chi )⟹(\varphi ⟹\psi ))$
• (논리곱의 좌측 제거) $⊢\varphi \wedge \chi ⟹\chi$
• (논리곱의 우측 제거) $⊢\varphi \wedge \chi ⟹\varphi$
• (논리곱과 함의 조건의 추가) $⊢\varphi ⟹(\chi ⟹(\varphi \wedge \chi ))$
• (논리합의 좌측 추가) $⊢\chi ⟹\varphi \vee \chi$
• (논리합의 우측 추가) $⊢\varphi ⟹\varphi \vee \chi$
• (함의 조건들의 논리합) $⊢(\varphi ⟹\psi )⟹((\chi ⟹\psi )⟹(\varphi \vee \chi ⟹\psi ))$
• (거짓은 모든 명제를 함의) $⊢\mathrm{\perp }⟹\varphi$

직관 술어 논리에서는 다음 두 공리들이 추가로 성립한다. 여기서 $t$는 $\varphi (t)$에서 한정 변수가 아닌 변수이다.

• (보편 기호의 특수화) $⊢(\mathrm{\forall }x:\varphi (x))⟹\varphi (t)$
• (존재 기호의 추가) $⊢\varphi (t)⟹(\mathrm{\exists }x:\varphi (x))$

성질

명제의 격자

주어진 명제 $\varphi$로부터, 고전 명제 논리에서는 $\mathrm{\perp },\varphi ,\mathrm{\neg }\varphi ,\mathrm{\top }$ 네 개의 명제밖에 정의할 수 없지만, 직관 명제 논리에서는 이로부터 무한한 수의, 서로 동치이지 않는 명제들이 존재한다. 이를 리에게르-니시무라 사다리(틀:Llang)라고 하며, 라디슬라프 스반테 리에게르(틀:Llang)와 니시무라 이와오가 정의하였다.

고전 논리와의 관계

직관 논리는 고전 논리의 일부분이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만, 고전적으로 참이지만 직관 논리에서는 증명할 수 없는 명제들이 존재한다. 이러한 명제들은 다음을 들 수 있다.

• (배중률) $\varphi \vee \mathrm{\neg }\varphi$
• (이중 부정 삭제) $\mathrm{\neg }\mathrm{\neg }\varphi ⟹\varphi$
• (퍼스의 법칙) $(\varphi ⟹\chi )⟹\varphi )⟹\varphi$

의미론

직관 논리의 경우, 다양한 의미론이 존재한다. 이 가운데 하나로는 다음과 같은 위상수학적 의미론을 생각할 수 있다. 어떤 위상 공간 $X$에 대하여, 직관 논리를 다음과 같이 해석하자.

• 명제는 $X$의 열린 집합에 대응한다.
• 논리합 $\varphi \vee \chi$는 합집합 $\varphi \cup \chi$에 대응한다.
• 논리곱 $\varphi \wedge \chi$는 교집합 $\varphi \cap \chi$에 대응한다.
• 함의 $\varphi ⟹\chi$는 교집합 $\mathrm{int}((X\setminus \varphi )\cup \chi )$에 대응한다. 여기서 $\mathrm{int}$는 집합의 내부이다.
• 거짓 $\mathrm{\perp }$은 공집합 $\varnothing$이다.

이로부터 정의되는 부정과 동치는 다음과 같다.

• 부정 $\mathrm{\neg }\varphi$는 여집합의 내부 $\mathrm{int}(X\setminus \varphi )$에 대응한다.
• 동치 $\varphi ⟺\chi$는 $\mathrm{int}((\varphi \cap \chi )\cup (X\setminus (\varphi \cup \chi )))$에 대응한다.

일반적인 위상 공간에 대하여 증명할 수 있는 모든 명제들은 직관 논리에서 참임을 보일 수 있다.

이 밖에도, 양상 논리의 크립키 모형(틀:Llang)을 직관 논리에서도 사용할 수 있다.

역사

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

응용

직관 논리는 일반적인 토포스의 내부 논리(틀:Llang)로 등장한다. (표준적인) 집합의 토포스나, 이산 공간 위의 층의 토포스 등에서는 고전 논리가 성립하지만, 예를 들어 이산 공간이 아닌 위상 공간 위의 층의 토포스에서는 고전 논리가 성립하지 않고, 직관 논리를 사용해야만 한다.

각주

• 틀:서적 인용
• 틀:서적 인용
• (직관주의 논리,한국수학사학회지 = 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
• 틀:Eom
• 틀:웹 인용
• 틀:웹 인용
• 틀:웹 인용
• 틀:웹 인용

같이 보기

• 직관주의
• 초직관 논리