用
形式化方法处理逻辑推理,特别是数学中所用推理。由于形式化了的推理过程与代数演算具有相似性,故也称之为逻辑演算。
这类推理的正确性仅依赖于它们的形式,而与内容无关,例如
三段论法。在这里,概念、推理等被分解为最基本的元素,推理过程被表示为由开始公式出发根据某些具体规则而做的形式变形。
逻辑演算的思想,也就是
数理逻辑最初的思想,首先由 G.W.莱布尼茨明确提出,又经 G.布尔、(F.L.)G.弗雷格、B.A.W.罗素和A.N.
怀特海等加以发展和完善。现代数理逻辑的研究已远远超出了逻辑演算的范围而发展成为四个主要分支──
模型论、
公理集合论、
递归论和
证明论。
由于形式推理在
公理化数学中用得最多,表达得也最精确,因此逻辑演算的主要内容就是数学
公理系统的形式化。形式化了的公理系统称为
形式系统。一般说,形式系统是由它的语言、公理和推理规则三部分构成。
形式系统的语言一般采用
人工语言。首先要规定语言的符号。符号的有穷序列(允许一个符号在序列中重复出现)称为一个表达式。正如
自然语言中并非所有字母的序列都是句子一样,并非所有的表达式都有意义。人们希望指出有意义的那部分表达式,称之为公式。但判别一个表达式是否为公式的标准,并不是根据它们的意义而是根据某些确定的形式规则,因此称之为形成规则。形成规则表明,语言中的符号依什么样的规律排列才形成公式,即语言中某一符号的序列是否为公式是可以依照形成规则机械地检查的。形式系统的语言也称为
形式语言。
形式系统中的公理需满足的惟一条件是它是该系统语言中的一个公式。推理规则(简称规则)陈述如何由有穷个确定的公式(称为规则的假设)得到某一确定的公式(称为规则的结论)。公理和推理规则一经确定,系统的全部定理就完全确定了。因为系统的定理通常是这样定义的:①所有公理是定理;②若形式系统推理规则的假设都是定理,则它的结论也是定理。因此,
形式系统的一个公式是否是它的定理也是可以机械地检查的。
由以上说明可知,一个形式系统是由它的符号、表达式及其排列规则等完全确定了的。虽然每个形式系统都有逻辑推理系统或数学
公理系统作为它的背景,即形式系统可以被解释为逻辑推理或某个数学结构,但是形式系统的解释或意义并不被认为是形式系统的一部分。这就使得形式系统本身成为一个纯语法的对象。把公理、定理等作为
形式语言中的公式、句子研究,称为公理系统的
语法研究。
形式系统的解释或意义称为语义。例如形式系统中的公式或句子在某个数学结构或模型中的真假性就是一个语义性质。
在
数理逻辑中,建立形式系统的主要目的在于将通常所说的“形式的”思维、
公理系统的“形式化”等概念精确化,使得数学中的语言、推理与数、形、方程式等一样成为数学研究的对象。对形式系统可以进行严格的数学处理,讨论其性质,包括语法与语义的性质,得出关于形式系统的一般结论。例如勒文海姆-斯科朗定理(见
模型论)。
哥德尔完备性定理(见
一阶逻辑)及
哥德尔不完备性定理等都是关于形式系统性质的定理。又如希尔伯特第 1问题即
连续统假设问题的研究就是在
集合论公理系统形式化的基础上才廓清了问题,并取得了进展。因此,
数理逻辑中对
形式系统的研究也给数学研究开辟了新的途径。
那种认为建立逻辑演算的形式系统是为了进行
形式思维,或者为了形式地证明数学定理的想法,是对于数理逻辑的研究对象和目的的一种误解。