불대수에 기반한 흔히 쓰는 논리 체계. 여러 가지 중요한 특징이 있지만 아마도 가장 중요한 특징은 모든 논리값이 참값이거나 거짓값이거나 둘 중 하나라는 공리를 대놓고 내세우고 있다는 것이다(the law of excluded middle). 만약 이 공리를 넣지 않으면 직관주의 논리계가 탄생한다.
\neg 연산자와 \rightarrow 접속사를 사용하는 다음 명제 논리계는 대표적인 완전하고 안전한 논리계이다. (\wedge, \vee 따위는 이들 연산자를 사용하여 구성된다고 치자.) 마지막 공리는 modus ponens(MP)라고 한다.
시퀀트 대수를 사용하는 자연 증명(natural proof) 체계는 쓰기 구찮다.1)