形式系统(formal system)
在逻辑中，指从一组公理出发，通过推理而产生的词项和内含关系的一种抽象的理论结构。每一个形式系统都有一形式语言，由基设符号（初始符号）及作用於这些符号的形成规则与形变规则（使我们能从一组公理进行推演）所组成。简要说，一个形式系统包括由基设符号藉有限组合而建立的许多公式；公式中合於某种组合形式者就是公理，我们依形变规则由公理进行推演工作。在任何公理系统中，基设符号都是不下定义的，其他所有符号都藉基设符号来界定。例如，在欧几里德几何中，「点」、「线」、「介於」都是基设名词。公式即基设符号所形成的一种良构表式，其中一部分被列为公理；推演规则被用来从一个或多个作为前提的公式推演出一个作为结论的公式。在这样的系统中，一条定理即是可以通过合式公式的有限序列加以证明的一个公式，这些合式公式中的每一个公式不是公理，就是从前面公式可以推得的公式。
English version：
formal system
In logic, a formal language together with a deductive apparatus by which some well-formed formulas can be derived from others. Each formal system has a formal language composed of primitive symbols that figure in certain rules of formation (statements concerning the expressions allowable in the system) and a set of theorems developed by inference from a set of axioms. In an axiomatic system, the primitive symbols are undefined and all other symbols are defined in terms of them. In Euclidean geometry, for example, such concepts as “point,” “line,” and “lies on” are usually posited as primitive terms. From the primitive symbols, certain formulas are defined as well formed, some of which are listed as axioms; and rules are stated for inferring one formula as a conclusion from one or more other formulas taken as premises. A theorem within such a system is a formula capable of proof through a finite sequence of well-formed formulas, each of which either is an axiom or is validly inferred from earlier formulas.