命题演算系统
在数理逻辑中，命题演算可以通过运用演算手段即建立形式系统进而把对重言式以及正确推理形式的研究，转变成对形式系统的研究。
形式系统就是没有任何语义内容的人工语言表示的系统，通常由五个部分构成：
1.初始符号：是一个形式系统使用的基本符号，是形式语言的语素。
2.形成规则：规定什么样的符号序列是形式语言的语句，即合式公式，简称公式。初始符号和形成规则共同组成了形式系统的语言，即形式语言。
3.公理：是某些被挑选出来、用作推导其他公式的出发点的公式，在一个系统中，公理是不加证明的，也是不可以证明的。
4.推理规则：是系统中使用的变形规则，每一个推理规则规定怎样从一个或一组公式通过符号变换得出另一个公式。
5.定理：是根据推理规则，由一定的公式推导出来的另一些公式。
建立和研究形式系统，需要用到两种语言：对象语言和语法语言。对象语言是用来构造公式、构成形式系统的语言。语法语言也称元语言，是人们讨论对象语言时所使用的另外一种语言，一般是使用人们日常说话时运用的自然语言，有时还需要增加一些特制的表意的语法符号。
另外，根据是否使用公理，可以把命题演算的形式系统分为两种：公理化命题演算系统和自然演算系统。