논리학 에서 직관 논리 (直觀論理, 영어 : intuitionistic logic )는 수학적 직관주의 에 근거하여 귀류법 을 배척하는 논리 체계이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만 그 역은 일반적으로 성립하지 않는 특징이있다.
이처럼 직관주의 논리학은 이중부정의 일부법칙이 성립하지 않는다.
정의
직관 논리 는 힐베르트 식으로 다음과 같이 서술되는 논리 체계이다.
직관 명제 논리 에서, 명제
ϕ ϕ -->
,
χ χ -->
,
… … -->
{\displaystyle \phi ,\chi ,\dots }
로부터 다음과 같은 새 명제들을 구성할 수 있다.
논리곱
ϕ ϕ -->
∧ ∧ -->
χ χ -->
{\displaystyle \phi \land \chi }
. 이는 "
ϕ ϕ -->
{\displaystyle \phi }
이며 또한
χ χ -->
{\displaystyle \chi }
"라고 읽는다.
논리합
ϕ ϕ -->
∨ ∨ -->
χ χ -->
{\displaystyle \phi \lor \chi }
. 이는 "
ϕ ϕ -->
{\displaystyle \phi }
이거나 또는
χ χ -->
{\displaystyle \chi }
"라고 읽는다.
함의
ϕ ϕ -->
⟹ ⟹ -->
χ χ -->
{\displaystyle \phi \implies \chi }
. 이는 "만약
ϕ ϕ -->
{\displaystyle \phi }
이라면
χ χ -->
{\displaystyle \chi }
또한 성립한다"라고 읽는다.
거짓
⊥ ⊥ -->
{\displaystyle \bot }
. 이는 거짓 명제로 읽는다.
이들로부터 다음과 같은 기호들을 정의한다.
부정
¬ ¬ -->
ϕ ϕ -->
{\displaystyle \lnot \phi }
는
ϕ ϕ -->
⟹ ⟹ -->
⊥ ⊥ -->
{\displaystyle \phi \implies \bot }
을 줄인 것이며, "
ϕ ϕ -->
{\displaystyle \phi }
가 아니다"라고 읽는다.
동치
ϕ ϕ -->
⟺ ⟺ -->
χ χ -->
{\displaystyle \phi \iff \chi }
는
(
ϕ ϕ -->
⟹ ⟹ -->
χ χ -->
)
∧ ∧ -->
(
χ χ -->
⟹ ⟹ -->
ϕ ϕ -->
)
{\displaystyle (\phi \implies \chi )\land (\chi \implies \phi )}
를 줄인 것이며, "
ϕ ϕ -->
{\displaystyle \phi }
와
χ χ -->
{\displaystyle \chi }
는 서로 동치이다"라고 읽는다.
직관 술어 논리 에서는 명제 논리 연산자 밖에도, 자유 변수
x
{\displaystyle x}
를 가지는 명제
ϕ ϕ -->
(
x
)
{\displaystyle \phi (x)}
로부터 다음과 같은 새 명제들을 구성할 수 있다.
(존재 술어)
∃ ∃ -->
x
: : -->
ϕ ϕ -->
(
x
)
{\displaystyle \exists x\colon \phi (x)}
. 이는 "
ϕ ϕ -->
(
x
)
{\displaystyle \phi (x)}
를 성립시키는
x
{\displaystyle x}
가 존재한다"라고 읽는다.
(보편 술어)
∀ ∀ -->
x
: : -->
ϕ ϕ -->
(
x
)
{\displaystyle \forall x\colon \phi (x)}
. 이는 "모든
x
{\displaystyle x}
에 대하여,
ϕ ϕ -->
(
x
)
{\displaystyle \phi (x)}
가 성립한다"라고 읽는다.
추론
직관 명제 논리 의 유일한 추론법은 전건 긍정의 형식 이며, 이는 다음과 같다.
ϕ ϕ -->
,
ϕ ϕ -->
⟹ ⟹ -->
χ χ -->
⊢ ⊢ -->
χ χ -->
{\displaystyle \phi ,\phi \implies \chi \vdash \chi }
직관 술어 논리 에서는 다음과 같은 두 변수 일반화 규칙이 추가된다. 여기서,
x
{\displaystyle x}
는
ϕ ϕ -->
{\displaystyle \phi }
에서 자유 변수가 아닌 변수(한정 변수이거나, 아니면
ϕ ϕ -->
{\displaystyle \phi }
에 등장하지 않는 변수)이다.
ϕ ϕ -->
⟹ ⟹ -->
ψ ψ -->
⊢ ⊢ -->
ϕ ϕ -->
⟹ ⟹ -->
∀ ∀ -->
x
: : -->
ψ ψ -->
{\displaystyle \phi \implies \psi \vdash \phi \implies \forall x\colon \psi }
ϕ ϕ -->
⟹ ⟹ -->
ψ ψ -->
⊢ ⊢ -->
ϕ ϕ -->
⟹ ⟹ -->
∃ ∃ -->
x
: : -->
ψ ψ -->
{\displaystyle \phi \implies \psi \vdash \phi \implies \exists x\colon \psi }
공리
직관 명제 논리의 공리들은 다음과 같다. 임의의 명제
ϕ ϕ -->
,
χ χ -->
,
ψ ψ -->
{\displaystyle \phi ,\chi ,\psi }
에 대하여,
(함의 조건의 추가)
⊢ ⊢ -->
ϕ ϕ -->
⟹ ⟹ -->
(
χ χ -->
⟹ ⟹ -->
ϕ ϕ -->
)
{\displaystyle \vdash \phi \implies (\chi \implies \phi )}
(함의의 분배)
⊢ ⊢ -->
(
ϕ ϕ -->
⟹ ⟹ -->
(
χ χ -->
⟹ ⟹ -->
ψ ψ -->
)
)
⟹ ⟹ -->
(
(
ϕ ϕ -->
⟹ ⟹ -->
χ χ -->
)
⟹ ⟹ -->
(
ϕ ϕ -->
⟹ ⟹ -->
ψ ψ -->
)
)
{\displaystyle \vdash (\phi \implies (\chi \implies \psi ))\implies ((\phi \implies \chi )\implies (\phi \implies \psi ))}
(논리곱의 좌측 제거)
⊢ ⊢ -->
ϕ ϕ -->
∧ ∧ -->
χ χ -->
⟹ ⟹ -->
χ χ -->
{\displaystyle \vdash \phi \land \chi \implies \chi }
(논리곱의 우측 제거)
⊢ ⊢ -->
ϕ ϕ -->
∧ ∧ -->
χ χ -->
⟹ ⟹ -->
ϕ ϕ -->
{\displaystyle \vdash \phi \land \chi \implies \phi }
(논리곱과 함의 조건의 추가)
⊢ ⊢ -->
ϕ ϕ -->
⟹ ⟹ -->
(
χ χ -->
⟹ ⟹ -->
(
ϕ ϕ -->
∧ ∧ -->
χ χ -->
)
)
{\displaystyle \vdash \phi \implies (\chi \implies (\phi \land \chi ))}
(논리합의 좌측 추가)
⊢ ⊢ -->
χ χ -->
⟹ ⟹ -->
ϕ ϕ -->
∨ ∨ -->
χ χ -->
{\displaystyle \vdash \chi \implies \phi \lor \chi }
(논리합의 우측 추가)
⊢ ⊢ -->
ϕ ϕ -->
⟹ ⟹ -->
ϕ ϕ -->
∨ ∨ -->
χ χ -->
{\displaystyle \vdash \phi \implies \phi \lor \chi }
(함의 조건들의 논리합)
⊢ ⊢ -->
(
ϕ ϕ -->
⟹ ⟹ -->
ψ ψ -->
)
⟹ ⟹ -->
(
(
χ χ -->
⟹ ⟹ -->
ψ ψ -->
)
⟹ ⟹ -->
(
ϕ ϕ -->
∨ ∨ -->
χ χ -->
⟹ ⟹ -->
ψ ψ -->
)
)
{\displaystyle \vdash (\phi \implies \psi )\implies ((\chi \implies \psi )\implies (\phi \lor \chi \implies \psi ))}
(거짓은 모든 명제를 함의)
⊢ ⊢ -->
⊥ ⊥ -->
⟹ ⟹ -->
ϕ ϕ -->
{\displaystyle \vdash \bot \implies \phi }
직관 술어 논리에서는 다음 두 공리들이 추가로 성립한다. 여기서
t
{\displaystyle t}
는
ϕ ϕ -->
(
t
)
{\displaystyle \phi (t)}
에서 한정 변수가 아닌 변수이다.
(보편 기호의 특수화)
⊢ ⊢ -->
(
∀ ∀ -->
x
: : -->
ϕ ϕ -->
(
x
)
)
⟹ ⟹ -->
ϕ ϕ -->
(
t
)
{\displaystyle \vdash (\forall x\colon \phi (x))\implies \phi (t)}
(존재 기호의 추가)
⊢ ⊢ -->
ϕ ϕ -->
(
t
)
⟹ ⟹ -->
(
∃ ∃ -->
x
: : -->
ϕ ϕ -->
(
x
)
)
{\displaystyle \vdash \phi (t)\implies (\exists x\colon \phi (x))}
성질
명제의 격자
주어진 명제
ϕ ϕ -->
{\displaystyle \phi }
로부터, 고전 명제 논리에서는
⊥ ⊥ -->
,
ϕ ϕ -->
,
¬ ¬ -->
ϕ ϕ -->
,
⊤ ⊤ -->
{\displaystyle \bot ,\phi ,\lnot \phi ,\top }
네 개의 명제밖에 정의할 수 없지만, 직관 명제 논리에서는 이로부터 무한한 수의, 서로 동치이지 않는 명제들이 존재한다. 이를 리에게르-니시무라 사다리 (영어 : Rieger–Nishimura ladder )라고 하며, 라디슬라프 스반테 리에게르(체코어 : Ladislav Svante Rieger )[ 1] 와 니시무라 이와오[ 2] 가 정의하였다.
고전 논리와의 관계
직관 논리는 고전 논리 의 일부분이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만, 고전적으로 참이지만 직관 논리에서는 증명할 수 없는 명제들이 존재한다. 이러한 명제들은 다음을 들 수 있다.
(배중률 )
ϕ ϕ -->
∨ ∨ -->
¬ ¬ -->
ϕ ϕ -->
{\displaystyle \phi \lor \lnot \phi }
(이중 부정 삭제)
¬ ¬ -->
¬ ¬ -->
ϕ ϕ -->
⟹ ⟹ -->
ϕ ϕ -->
{\displaystyle \lnot \lnot \phi \implies \phi }
(퍼스 의 법칙)
(
ϕ ϕ -->
⟹ ⟹ -->
χ χ -->
)
⟹ ⟹ -->
ϕ ϕ -->
)
⟹ ⟹ -->
ϕ ϕ -->
{\displaystyle \left(\phi \implies \chi )\implies \phi \right)\implies \phi }
의미론
직관 논리의 경우, 다양한 의미론이 존재한다. 이 가운데 하나로는 다음과 같은 위상수학 적 의미론을 생각할 수 있다. 어떤 위상 공간
X
{\displaystyle X}
에 대하여, 직관 논리를 다음과 같이 해석하자.
명제는
X
{\displaystyle X}
의 열린 집합 에 대응한다.
논리합
ϕ ϕ -->
∨ ∨ -->
χ χ -->
{\displaystyle \phi \lor \chi }
는 합집합
ϕ ϕ -->
∪ ∪ -->
χ χ -->
{\displaystyle \phi \cup \chi }
에 대응한다.
논리곱
ϕ ϕ -->
∧ ∧ -->
χ χ -->
{\displaystyle \phi \land \chi }
는 교집합
ϕ ϕ -->
∩ ∩ -->
χ χ -->
{\displaystyle \phi \cap \chi }
에 대응한다.
함의
ϕ ϕ -->
⟹ ⟹ -->
χ χ -->
{\displaystyle \phi \implies \chi }
는 교집합
int
-->
(
(
X
∖ ∖ -->
ϕ ϕ -->
)
∪ ∪ -->
χ χ -->
)
{\displaystyle \operatorname {int} \left((X\setminus \phi )\cup \chi \right)}
에 대응한다. 여기서
int
{\displaystyle \operatorname {int} }
는 집합의 내부 이다.
거짓
⊥ ⊥ -->
{\displaystyle \bot }
은 공집합
∅ ∅ -->
{\displaystyle \varnothing }
이다.
이로부터 정의되는 부정과 동치는 다음과 같다.
부정
¬ ¬ -->
ϕ ϕ -->
{\displaystyle \lnot \phi }
는 여집합 의 내부
int
-->
(
X
∖ ∖ -->
ϕ ϕ -->
)
{\displaystyle \operatorname {int} (X\setminus \phi )}
에 대응한다.
동치
ϕ ϕ -->
⟺ ⟺ -->
χ χ -->
{\displaystyle \phi \iff \chi }
는
int
-->
(
(
ϕ ϕ -->
∩ ∩ -->
χ χ -->
)
∪ ∪ -->
(
X
∖ ∖ -->
(
ϕ ϕ -->
∪ ∪ -->
χ χ -->
)
)
)
{\displaystyle \operatorname {int} \left((\phi \cap \chi )\cup \left(X\setminus (\phi \cup \chi )\right)\right)}
에 대응한다.
일반적인 위상 공간에 대하여 증명할 수 있는 모든 명제들은 직관 논리에서 참임을 보일 수 있다.
이 밖에도, 양상 논리 의 크립키 모형 (영어 : Kripke model )을 직관 논리에서도 사용할 수 있다.
역사
라위트전 브라우어르 의 직관주의 수학을 형식화하기 위하여, 아런트 헤이팅 이 도입하였다.
응용
직관 논리는 일반적인 토포스 의 내부 논리(영어 : internal logic )로 등장한다.[ 3] (표준적인) 집합의 토포스 나, 이산 공간 위의 층 의 토포스 등에서는 고전 논리가 성립하지만, 예를 들어 이산 공간 이 아닌 위상 공간 위의 층의 토포스에서는 고전 논리가 성립하지 않고, 직관 논리를 사용해야만 한다.
각주
외부 링크
같이 보기