形式系统

形式系统是一个抽象的结构，用于根据一组规则从公理推断出定理。这些用于从公理进行推理的规则是形式系统的逻辑微积分。形式系统本质上是一个公理系统。1921年，大卫-希尔伯特提出用这样一个系统作为数学知识的基础。一个形式化系统可以代表一个定义明确的抽象思维系统。形式主义一词有时是形式系统的粗略同义词，但它也指一种特定的符号风格，例如，保罗-狄拉克的辫子符号。

每个形式化系统都由原始符号（它们共同构成一个字母表）来描述，通过推理形成的规则从一组公理中有限地构建一个形式化语言。因此，该系统由通过原始符号的有限组合建立起来的有效公式组成--这些组合是按照所述规则从公理中形成的。更正式地说，这可以表示为以下几点。一个有限的符号集，称为字母表，它将公式连接起来，因此一个公式只是从字母表中抽取的有限的符号串。一个由规则组成的语法，从更简单的公式中形成公式。如果一个公式可以用形式语法的规则来形成，那么这个公式就被称为形式良好。通常要求有一个决定程序来决定一个公式是否形式良好。一套公理，或公理图，由形式良好的公式组成。一套推理规则。一个可以从公理中推断出的形式良好的公式被称为形式化系统的定理。递归如果公理集和推理规则集分别是可判定集或半可判定集，那么一个形式化系统被称为是递归的（即有效的）或递归可列举的。

通过其逻辑基础对系统的尾随是形式化系统与其他可能在抽象模型中具有某种基础的系统的区别所在。通常，形式化系统将是一个更大的理论或领域（如欧几里得几何）的基础，甚至与模型理论等现代数学中的用法一致。

形式语言是一种由形式系统定义的语言。与语言学中的语言一样，形式语言一般有两个方面。语言的语法是语言的样子（更正式地说：语言中有效语词的可能表达的集合），在形式语言理论中进行研究。语言的语义是语言的语词的意思（根据有关语言的类型，以各种方式进行形式化）。形式语法是对一种形式语言的语法的精确描述：一组字符串。形式语法的两个主要类别是生成语法和分析语法，前者是关于如何生成语言中的字符串的一套规则，后者是关于如何分析一个字符串以确定它是否是语言的成员的一套规则。

简而言之，分析性语法描述了如何识别字符串是集合中的成员，而生成性语法则描述了如何只书写集合中的那些字符串。在数学中，形式语言通常不是由形式语法描述的，而是由（a）自然语言，如英语描述的。逻辑系统是由演绎系统和自然语言共同定义的。而演绎系统又只由自然语言来定义（见下文）。

一个演绎系统，也被称为演绎装置或逻辑，由公理（或公理图）和推理规则组成，可用于推导系统的定理。这样的演绎系统在系统所表达的公式中保留了演绎的品质。通常，我们所关注的品质是相对于虚假的真理。然而，其他的模式，比如说理由或信念，也可能被保留下来。为了维持其演绎的完整性，一个演绎工具必须是可定义的，而不需要参考语言的任何预期解释。其目的是确保推导的每一行仅仅是其前面几行的句法结果。对语言的任何解释都不应该涉及到系统的演绎性质。演绎系统的一个例子是一阶谓词逻辑。

一个逻辑系统或语言（不要与上面讨论的那种由形式化语法描述的形式化语言相混淆），是一个演绎系统（见上面一节；最常见的是一阶谓词逻辑），加上额外的（非逻辑的）公理。