1차언어에서는 predicate calculus라는 형식적인
작업을 통해 어떤 문장의 논리적 결과를 쉽게 도출 할 수
있습니다. 이는 우리가 일상적으로 사용하는 언어로
서술된 문장들 사이의 인과관계를 밝히는 일보다 명확합니다.
앞으로 일상언어로 서술된 문장을 N차문장이라,
1차 언어로 서술된 문장(formula)를 1차문장이라 부르겠
습니다.
N차문중 극히 일부는 1차문장으로 형식화 될 수 있습니다.
A를 1차문장으로 형식화 가능한 N차문장이라 가정하고
a를 A가 형식화 된 1차문장이라 가정해봅시다.
우리는 predicate calculs를 통해 기계적인 방식으로
a의 논리적결과 b를 도출해 낼 수 있습니다.
b에 대응하는 N차문장 B는 A의 논리적 결과 입니다.
(1차문장을 대응되는 N차문장으로 바꿔주는 작업을
deformalize라 합시다.)
일상언어를 이용해 A로부터 B를 도출해내는 과정보다
A를 1차 언어로 형식화 한 뒤 그 형식화 된 문장의 논리적 결과를 predicate calculus를 통해 찾아내고 그 결과를
deformalize해 줌으로써 N차문장 A의 논리적결과를
찾아내는것이 직관에 덜 의존하며 더 명확합니다.
집합 {(x,x): x is an element of a set X} 가
X에서 X로 가는 일대일 함수라는 것을 증명하는데
이 과정을 적용해봅시다.
이는 직관적으로 볼 때 매우 당연한 문장입니다.
직관적으로 당연한 문장은 언어를 통해 증명하는
것은 쉽지 않습니다.
하지만 이것을 형식화 하면 눈에 보이는 방식으로
매우 논리정연하게 증명해 낼 수 있습니다.
그 과정은 조만간 사진으로 보여드리겠습니다.