백과

정형식의 규정

모든 표현은 원초적 기호들로부터 형성규칙(formation rules)이라고 하는 구문론적 문법규칙에 따라 구성된 것만이 정형식(well-formed formular/WFF)으로 인정된다.

편의상 명제논리체계에만 국한된 형성규칙의 예를 들면 다음과 같다.

첫째, 'P', 'Q', 'R', 'S'는 그 자체로 정형식이다. 둘째, 식의 왼쪽에 '~'를 붙여도 정형식이다. 셋째, 두 식 사이에 '⊃'를 넣고 그 두 식의 좌우에 괄호를 해도 정형식이다. 넷째, 이상의 규칙에 맞지 않는 어떤 것도 정형식이 아니다.

공리와 추론규칙의 제시

그 자체로서 공리이거나 또는 무한히 많은 사례들의 형식을 결정해주는 공리 도식들의 목록을 나열해줌으로써 공리들의 집합이 규정된다.

공리란 증명 없이 주장되는 문장을 말한다. 자연연역체계에서는 공리가 없고 그 대신에 추론규칙들에 의해서만 체계가 규정된다. 공리의 예를 들면 다음과 같다.

① (P⊃(Q⊃P))

② (((P⊃(Q⊃R))⊃((P⊃Q)⊃(P⊃R))

③ ((~P⊃~Q)⊃(Q⊃P))

추론규칙의 예에는 분리규칙, 대입규칙이 있다.

증명(연역)에 대한 정의

공리를 제외한 모든 식은 형식적 추론규칙에 의해 도출된다.

도출의 단계마다 비약이 허용되지 않으며, 오로지 표현들의 형식에 따라서만 도출이 허용되는 엄격한 체계여야 한다. 추론규칙들은 문장들에 대해서 구조적인 형태로 수행 가능한 조작(연산)을 규정해준다. 그러한 조작(연산)에 의해 다른 문장들로부터 얻어지는 문장을 그 다른 문장들의 귀결이라 한다.

단계 (3)과 (4)가 결합해서 정리들의 집합을 결정한다.

정리란 공리이거나 또는 공리들로부터 추론규칙들을 몇 차례 적용시켜서 도출한 문장을 말한다. 이중 후자는 증명 가능한 것이라고 불린다. 정리로 끝나는 일련의 연속적으로 도출된 문장들을 이 정리의 증명이라 한다. 만일 한 체계가 공리들 없이 구성되면 그 체계에 나오는 증명들은 가정들로부터의 증명이다. 지금까지 논의된 논리체계는 공리들에 기초해서 추론규칙들에 의해 정리들을 이끌어내는 체계이다. 반면에 공리들 없이 추론규칙들만을 유일한 연역수단으로 하는 체계를 구성할 수도 있다.

이러한 접근방식은 상당한 기술적 편리함이 있을 뿐더러 실제의 일상적 연역추론의 수행에 보다 근접한 방법이다. 이와 같은 종류의 최초의 체계는 1934년 겐첸(Gentzen)과 야스코프스키(Jaskowski)에 의해 각각 독자적으로 구성되었으며, 겐첸의 용어를 따라 자연연역체계라 불린다.

겐첸의 자연연역체계의 규칙은 다음과 같다.

모든 형식화된 이론은 하나의 논리체계를 전제로 한다.

만일 그 전제된 체계가, 술어변항은 없고 동일성 관계와 그에 관한 조작기호를 별도로 포함한 1차술어논리이면 그 이론을 기본이론 또는 표준형식이론이라고 부른다. 좁은 의미에서의 논리학이라는 개념은 이 기본이론이 전제하고 있는 1차술어논리의 체계로 환원된다. 1차술어논리는 모든 수학적 추론을 형식화하는 기초로서 충분하다. 1차술어논리가 자연언어나 그중에서도 특별히 철학적 논증에서의 모든 추론들을 형식화하는 데도 충분한지의 여부는 아직도 해결되지 않은 채로 남아 있다.