一个形式系统通常由四部分组成：

（1）各种初始符号.初始符号是一个形式系统使用的符号，经解释后其中一部分是初始概念.例如，命题演算中的“⇁”是一个初始符号，解释后它表示否定.

（2）一组形成规则.初始符号给定之后，它们可以组成各种各样的符号序列.形成规则规定，哪些符号序列是我们感兴趣的，因为这类符号序列经解释后是有意义的命题.因此，我们称这类符号序列为合式公式，简称公式.否则就不是合式公式.例如，在命题演算中，“p⇁”是没有意义的，因此它不是合式公式；而“⇁p”有意义，它表示命题p的否定命题，所以它是一个合式公式.

（3）公理.我们建立形式系统的最终目的是要把所有的重言式汇集成一个系统.为此，我们要把重言式演绎地排列出来，使得后面的总可以从前面“演绎”出，最前面的就是作为演绎出发点的“公理”.它可以演绎出其他“重言式”，但它却不能由别的“重言式”演绎出来.对公理的唯一要求是，每一公理都是形式系统中的公式.

（4）推理规则.推理规则充当演绎的角色.每一推理规则规定怎样从一个或一组公式通过符号变换得出另一个公式.用公理和推理规则推导出的公式叫做形式系统的内定理.

在形式系统中，初始符号和形成规则组成形式系统的语言，也叫形式语言.这种语言不是日常语言，而是只具有形状的语言，或者说是一种表意的符号语言.公理和推理规则组成演绎工具或称演绎基础，这种演绎工具仅仅是移动符号的规则.对这样的形式系统，我们要求它能够有一个机械的方法判定以下几点：

（1）任一符号是否为初始符号；(www.daowen.com)

（2）任一符号序列是否为合式公式；

（3）任一公式是否为公理；

（4）任一公式是否能从给定的公理根据推理规则得到；

（5）任一有穷长的公式序列是否为证明，即序列中每一公式是否为公理或是从先行的公式应用推理规则得到的.

这里，机械的方法是指：每一步都是按照某种事先给出的规则明确规定的而且在有穷步内完成的方法.这样做的目的是为了保证形式系统的严格性.

总之，一个形式系统是由它的初始符号、公式、公理和规则等完全确定的.有时我们也把形式系统看作一个完全形式化了的公理系统.命题演算是由命题逻辑的重言式组成的公理系统，是一个完全形式化的公理系统.