形式证明

在逻辑学和数学中，形式证明或推导是一个有限的句子序列，其中每个句子都是一个公理，一个假设，或通过一个推理规则从序列中的前面的句子推导出来。它与自然语言论证的不同之处在于，它是严格的、不含糊的和可机械地验证的。如果假设集是空的，那么形式化证明中的最后一句话就被称为形式化系统的定理。定理的概念在一般情况下并不有效，因此可能没有任何方法可以让我们总能找到一个给定句子的证明或确定不存在。菲奇式证明、顺序计算和自然演绎的概念是对证明概念的概括。该定理是证明中它前面的所有形式良好的公式的语法结果。为了使一个形式良好的公式有资格成为证明的一部分，它必须是对证明序列中前面形式良好的公式应用演绎装置的规则的结果。形式化证明往往是在交互式定理证明的计算机帮助下构建的。重要的是，这些证明可以自动检查，也可以通过计算机检查。检查形式证明通常很简单，而寻找证明的问题通常在计算上是难以解决的和/或只是半可解的，这取决于使用的形式系统。

形式语言是一组有限的符号序列。这样的语言可以在不参考其任何表达的任何意义的情况下被定义；它可以在任何解释被分配给它之前就存在，也就是说，在它有任何意义之前。形式证明是用一些形式语言表达的。

形式语法（也叫形成规则）是对形式语言的良好形式公式的精确描述。它与形式语言的字母表上的字符串集合同义，这些字符串构成形式良好的公式。然而，它并不描述它们的语义（即它们的含义）。

形式系统（也叫逻辑微积分，或逻辑系统）由形式语言和演绎装置（也叫演绎系统）组成。演绎装置可以由一组转换规则（也叫推理规则）或一组公理组成，或者两者都有。形式系统被用来从一个或多个其他表达式中推导出一个表达式。

一个形式化系统的解释是对符号的意义的分配，以及对形式化系统的句子的真值。对解释的研究被称为形式语义学。给出一个解释与构造一个模型是同义的。