백과

용어나 명사 표현을 원자적 단위로 사용하는 술어계산과는 달리 분석되지 않은 단순명제를 원자적 단위로 사용한다. 또한 함수계산과는 달리 변항을 포함하지 않는 명제만 다룬다. 단순명제(원자명제)는 문자로 표현하고, 복합명제(분자명제)는 표준기호를 사용하여 만든다(·은 '그리고', ∨는 '또는', ⊃는 '만일 ……라면', ~는 '아니다'의 뜻).

형식체계인 명제계산은 어떤 명제형식(복합명제형식)이 공리로부터 증명될 수 있는가를 결정하는 일에 관여한다.

타당한 추론은 증명가능한 정식으로 재현된다. 왜냐하면 (모든 A와 B에 대해서) A⊃B는 B가 항상 A의 논리적 결과일 때만 증명가능하기 때문이다. 명제계산은 A와 ~A를 함께 증명할 수 있는 정식을 포함하지 않는다는 의미에서 무모순적이며, 어떤 증명불가능한 정식을 새로운 공리로서 부가할 경우 모순을 낳게 된다는 의미에서 완전하다. 명제계산체계에는 어떤 주어진 정식을 그 체계 안에서 증명할 수 있는가를 결정하는 효과적인 절차도 있다.→ 사유법칙, 술어계산