Q0（数学逻辑）

Q0是彼得-安德鲁斯（PeterAndrews）对简单类型的羔羊皮微积分的表述，为数学提供了一个可与一阶逻辑加集合论相媲美的基础。它是高阶逻辑的一种形式，与HOL定理检验器家族的逻辑密切相关。定理证明系统TPS和ETPS是基于Q0的。2009年8月，TPS赢得了有史以来xxx次高阶定理证明系统的竞赛。

该系统只有五条公理，可以表述为。(公理2、3和4是公理模式–类似公理的家族。公理2和公理3的实例只因变量和常数的类型而不同，但公理4的实例可以有任何表达式来替代A和B。）下标的o是布尔值的类型符号，下标的i是单个（非布尔）值的类型符号。这些序列代表函数的类型，可以包括括号来区分不同的函数类型。下标的希腊字母如α和β是类型符号的句法变量。粗体大写字母如A、B、C是WFF的句法变量，粗体小写字母如x、y是变量的句法变量。S表示在所有自由出现处的句法替换。xxx的原始常数是Q((oα)α)，表示每个类型α的成员相等，以及℩(i(oi))，表示个体的描述操作符，即一个集合中恰好包含一个个体的xxx元素。符号λ和括号（[和]）是语言的语法。所有其他符号是包含这些术语的缩写，包括量词∀和∃。在公理4中，x对B中的A来说必须是自由的，也就是说，替换不会导致A的任何自由变量的出现在替换的结果中成为约束。

公理1表达了T和F是xxx的布尔值的想法。公理模式2α和3αβ表达了函数的基本属性。公理模式4定义了λ符号的性质。公理5说，选择算子是个体上平等函数的逆。(给定一个参数，Q将该个体映射到包含该个体的集合/谓词。在Q0中，x=y是Qxy的缩写，Qxy是(Qx)y的缩写)。这个算子也被称为_definitedescription_算子。在Andrews2002中，公理4被分成五个子部分来发展，这些子部分分解了置换的过程。这里给出的公理是作为一个替代方案来讨论的，并从这些子部分中得到证明。

安德鲁斯用所有类型的集合的选择操作符的定义扩展了这个逻辑，因此是一个定理（编号5309）。换句话说，所有类型都有一个确定的描述算子。这是一个保守的扩展，所以如果核心是一致的，扩展系统就是一致的。他还提出了一个额外的公理6，该公理指出有无限多的个体，同时还有等价的替代无限公理。与许多其他类型理论的表述和基于类型理论的证明助手不同，Q0没有规定o和i之外的基本类型，因此，例如有限心数被构造为服从通常的Peano公设的个体集合，而不是简单类型理论意义上的类型。

Q0有一个单一的推理规则。规则R.从C和Aα=Bα推断出用Bα的出现替换C中Aα的一次出现的结果，条件是C中Aα的出现不是紧接在λ前面的（一个变量的出现）。派生的推理规则R′可以从一组假设H进行推理。规则R′。如果H⊦Aα=Bα，而H⊦C，并且D是通过用Bα的出现替换Aα的一次出现而从C得到的，那么H⊦D。