基于构造性思想的直觉主义逻辑证明语义

程华清

1 直觉主义的构造性思想

20 世纪初，对数学基础的研究导致了直觉主义学派（intuitionistic school）的诞生，其代表人物是布劳威尔（L.E.J.Brouwer）。在布劳威尔看来，数学是一种心智的构造性的活动，数学定理表达的是纯粹经验的事实，数学不能建立在公理化方法基础之上，直觉（直观）就是数学可靠性的基础。直觉主义学派的座右铭是“存在即被构造”，这体现在它只接受心智可构造的数学对象（对于所考虑的数学对象来说，我们能够通过一定的方法能行地得到它们）和心智可构造的数学证明（对于一个数学命题所表达的内容来说，我们能够通过一定的方法能行地验证它）。在心智可构造的要求下，直觉主义学派拒斥实无穷而采纳潜无穷观。比如：在实无穷立场下，全体正整数能够构成一个作为独立对象的集合，它是一个完成了的整体；而在心智可构造的要求下，依赖于原始直觉，先构建正整数1，再根据布劳威尔所提出的二一原则（two-oneness）（[1]，第85 页），依次逐个地获得后继的正整数2,3,...，按照直觉主义的语言，这意味着“创造一个实体，接着再创造一个实体”，由此可构造正整数的无穷序列1,2,3,...,n,...，但这种建构过程是没有终止的，因此，正整数的无穷序列不能作为一个完成了的整体来看待。

在布劳威尔对数学的独特理解下，数学是不依赖于语言的。如果使用语言的话，那么语言就仅仅是记录完成了的数学构造的一种工具，通过语言这个媒介，不同个体可以交流他们所记录的数学构造。正如海廷（A.Heyting）所言：“直觉主义数学是一种心智的活动，正因如此，每种语言（包括形式语言）都只是交流的工具。原则上说，由于思想的可能性不能归约为预先设置的有限规则，因此我们不可能创建一个由公式组成的形式系统使之等价于直觉主义数学。”（[3]，第311页）逻辑作为在利用语言记录完成了的数学构造时所产生的形式规律，其有效性自然地依赖于数学的心智可构造性，数学便成为了逻辑的基础，而反之不然。

正是对数学的不同理解，使得直觉主义对“真”的理解有别于经典意义上的“真”。在经典意义上，对一个命题来说，它是非真即假的，一个命题的真独立于对它的证明；而在直觉主义看来，我们判定一个命题为真就必须要给出对它的构造性证明，否则就不能判定这个命题为真。直觉主义对基本的逻辑联结词（否定¬、合取∧、析取∨和蕴涵→）以及全称量词∀和存在量词∃的解释也是基于构造性立场的。接下来，我们遵循直觉主义构造性思想，来构建直觉主义逻辑的证明语义。由于构造性证明是一种基于直观理解的内涵概念，这使得本文所构建的直觉主义逻辑证明语义是一种内涵语义。我们构建证明语义的基本思路是：语义解释从具体命题、具体的可构造对象（个体）、具体的性质和关系等出发，采用对公式A作解释AI的方式，给出“直观有效”的定义；避免使用集合概念，尽量贴近直观。1在直觉主义逻辑中，对逻辑联结词、全称量词和存在量词的标准语义解释以布劳威尔、海廷和柯尔莫哥洛夫（A.N.Kolmogorov）的工作为基础，统称为BHK 解释。BHK 解释说明了：对于一个数学复合命题（包括全称命题和存在命题）来说，对它的具体构造性证明通过以何种方式从它的直接子命题的具体构造性证明而得到（参见[4]，第9 页）。本文构建的证明语义则是在对BHK 解释弱化后的基础上而建立的，体现在对否定词、蕴涵词、全称量词和存在量词的弱化解释。

2 直觉主义命题逻辑的证明语义

定义2.1(原子命题和联结词的证明解释).2参见[5]，第48–49 页，本文做了补充和改动。

1 对于一个原子命题φ来说，判定φ为真当且仅当给出φ的构造性证明。

2 对于一个否定命题¬φ（意为“并非φ”）来说，判定¬φ为真当且仅当从任意假设的对φ的构造性证明都将导致谬误3谬误作为初始概念，可以有多种表现形式，比如推出命题“B ∧¬B”这样的逻辑矛盾或推出如“0=1”这样的荒谬句。（这意味着φ没有构造性证明），这时我们亦称¬φ获得了构造性证明。

3 对于一个合取命题φ ∧ψ（意为“φ并且ψ”）来说，判定φ ∧ψ为真当且仅当同时给出对φ的构造性证明和对ψ的构造性证明，这时我们亦称φ ∧ψ获得了构造性证明。

4 对于一个析取命题φ ∨ψ（意为“φ或者ψ”）来说，判定φ ∨ψ为真当且仅当给出对φ的构造性证明或给出对ψ的构造性证明4另一种更强的对析取命题的证明解释是：判定φ ∨ψ 为真当且仅当可指明φ、ψ 中的哪一个析取支是正确的，并且给出该析取支的构造性证明。（参见[2]，第224 页），这时我们亦称φ ∨ψ获得了构造性证明。

5 对于一个蕴涵命题φ →ψ（意为“如果φ，那么ψ”）来说，判定φ →ψ为真当且仅当从任意假设的对φ的构造性证明都能够得到对ψ的构造性证明，若φ是谬误，不能获得构造性证明，亦判定φ →ψ为真。这时我们都称φ →ψ获得了构造性证明。

依赖于上述证明解释，我们可以进一步构建直觉主义命题逻辑的证明语义。下面，先给出直觉主义命题逻辑的形式语言L。

形式语言L由以下两个部分构成：

(1) 初始符号：

1 潜无穷个命题变元：p1,p2,...。

2 否定联结词¬、合取联结词∧、析取联结词∨和蕴涵联结词→。

3 左右括号：(、)。

(2) 形成规则（A,B是任意公式）：

1 任意的命题变元pi是公式。

2 如果A是公式，那么¬A是公式。

3 如果A,B是公式，那么(A ∧B),(A ∨B),(A →B)是公式。对一个公式A来说，A自身，以及作为A的组成部分的那些公式都被称为A的子公式。

定义2.2.L中的公式A的一个解释（记为AI）由以下方式获得：

1 将A中的每一个命题变元都解释为一个具体的（原子）命题，若A中含有不同的命题变元，那么不同的命题变元可以解释为不同的或相同的具体命题；

2 对联结词¬、∧、∨和→作证明解释（见定义2.12–5 ）。

对定义2.2 的说明：1 公式A的一个解释AI是一个确定的具体命题。2 若B是A的子公式并且AI是A的一个解释，那么在AI的解释下，B也获得了相应的解释（记为BI），即某一个确定的具体命题。3 公式A的两个解释是否相同仅取决于对A中的每个命题变元所作的解释是否相同。

定义2.3.称一个L中的公式A是直观有效的当且仅当对于A的任何解释AI，AI都被判定为真，即总能给出对AI的构造性证明。

定义2.1、定义2.2 和定义2.3 构成了直觉主义命题逻辑的证明语义。以下给出直觉主义命题逻辑公理系统IP，它建立在形式语言L的基础上，再加上以下两部分构成（[5]，第60–61 页）：

(1)IP的公理（A,B,C是任意公式）：

公理IP1：(A →(B →A))

公理IP2：((A →(B →C))→((A →B)→(A →C)))

公理IP3：(A →(B →(A ∧B)))

公理IP4：((A ∧B)→A)

公理IP5：((A ∧B)→B)

公理IP6：(A →(A ∨B))

公理IP7：(B →(A ∨B))

公理IP8：((A →C)→((B →C)→((A ∨B)→C)))

公理IP9：((A →B)→((A →¬B)→¬A))

公理IP10：(¬A →(A →B))

(2) 推理规则（A,B是任意公式）：

分离规则MP：由A和(A →B)可推出B。

若A是IP的公理，或者是由公理出发运用MP规则推出的公式，则称A是IP中的一个（内）定理，记为⊢IP A。

下面的工作是证明直觉主义命题逻辑系统IP的可靠性，证明由以下引理和定理构成。

引理2.1.系统IP的十条公理都是直观有效的。

公理IP1.(A →(B →A))

证明.先给定对公理IP1的任意的一个解释(A →(B →A))I。假设α是对AI的任意构造性证明，那么对任意假设的对BI的构造性证明β来说，总能得到对AI的构造性证明（即α），根据定义2.15 可知，(B →A)I获得了构造性证明，进而获得对(A →(B →A))I的构造性证明。再根据定义2.3 可知，公理IP1是直观有效的。

公理IP2.((A →(B →C))→((A →B)→(A →C)))

证明.先给定对公理IP2的任意的一个解释((A →(B →C))→((A →B)→(A →C)))I。假设α是对(A →(B →C))I的任意构造性证明、β是对(A →B)I的任意构造性证明、γ是对AI的任意构造性证明。根据定义2.15 可知，利用β，从γ能够得到对BI的构造性证明（记为γβ）；利用α，从γ能够得到对(B →C)I的构造性证明（记为γα）；利用γα，从γβ可以得到对CI的构造性证明。于是(A →C)I获得了构造性证明，进而((A →B)→(A →C))I和((A →(B →C))→((A →B)→(A →C)))I也获得了构造性证明。再根据定义2.3 可知，公理IP2是直观有效的。

公理IP3.(A →(B →(A ∧B)))

证明.先给定对公理IP3的任意的一个解释(A →(B →(A∧B)))I。假设α是对AI的任意构造性证明，假设β是对BI的任意构造性证明，根据定义2.13，(A∧B)I便获得了构造性证明。再根据定义2.15，(B →(A∧B))I和(A →(B →(A∧B)))I也获得了构造性证明。进而根据定义2.3 可知，公理IP3是直观有效的。

公理IP4.((A ∧B)→A)和公理IP5.((A ∧B)→B)

使用定义2.13、定义2.15 和定义2.3 即证，从略。

公理IP6.(A →(A ∨B))和公理IP7.(B →(A ∨B))

使用定义2.14、定义2.15 和定义2.3 即证，从略。

公理IP8.((A →C)→((B →C)→((A ∨B)→C)))

证明.先给定对公理IP8的任意的一个解释((A →C)→((B →C)→((A∨B)→C)))I。假设α是对(A →C)I的任意构造性证明、β是对(B →C)I的任意构造性证明、γ是对(A ∨B)I的任意构造性证明。根据定义2.14，或者给出对AI的构造性证明（记为γA）或者给出对BI的构造性证明（记为γB）。根据定义2.15，利用α，从γA能够得到对CI的构造性证明；利用β，从γB能够得到对CI的构造性证明。这样，根据定义2.15 可知，先后可获得((A ∨B)→C)I、((B →C)→((A ∨B)→C))I和((A →C)→((B →C)→((A ∨B)→C)))I的构造性证明。再根据定义2.3 可知，公理IP8是直观有效的。

公理IP9.(A →B)→((A →¬B)→¬A))

证明.先给定对公理IP9的任意的一个解释((A →B)→((A →¬B)→¬A))I。假设α是对AI的任意构造性证明、β是对(A →B)I的任意构造性证明、γ是对(A →¬B)I的任意构造性证明。根据定义2.15，利用β，从α能够得到对BI的构造性证明（记为αβ）；利用γ，从α能够得到对(¬B)I的构造性证明（记为αγ）。这样就导致了谬误。进而根据定义2.12，(¬A)I获得了构造性证明；由定义2.15，先后获得了((A →¬B)→¬A)I和((A →B)→((A →¬B)→¬A))I的构造性证明。再根据定义2.3 可知，公理IP9是直观有效的。

公理IP10.(¬A →(A →B))

证明.先给定对公理IP10的任意的一个解释(¬A →(A →B))I。假设α是对(¬A)I的任意构造性证明、β是对AI的任意构造性证明。利用α，从β将得到谬误，再根据定义2.15 可知，(A →B)I获得了构造性证明。进而(¬A →(A →B))I获得了构造性证明。再根据定义2.3 可知，公理IP10是直观有效的。

引理2.2.A,B是任意的L的公式，如果A和(A →B)都是直观有效的，那么B也是直观有效的。

证明.设BI是公式B的任意给定的一个解释，将BI扩展为公式(A →B)的解释(A →B)I，使得BI是(A →B)I解释下获得的相应解释，于是在(A →B)I解释下可获得公式A的解释AI。已知A和(A →B)都是直观有效的，由定义2.3 可知：AI和(A →B)I都被判定为真，再根据定义2.15 可知：BI被判定为真，所以B也是直观有效的。

定理2.3(系统IP的可靠性定理).任给一L的公式A，如果⊢IP A，那么A是直观有效的。

证明.根据引理2.1 和引理2.2，使用数学归纳法即证。

3 直觉主义谓词逻辑的证明语义

先构建直觉主义谓词逻辑的形式语言L∗。形式语言L∗由以下两部分构成：

(1) 初始符号：

1 潜无穷个个体变元：x1,x2,...。

2 个体常元：a1,a2,...。个体常元可以没有，也可以是有穷个或潜无穷个，个体常元可以被解释为特定的个体。

3 谓词符号：A11,A12,...（一元谓词符号）；A21,A22,...（二元谓词符号）；...；An1,An2,...（n元谓词符号）；...。谓词符号至少有一个，可以是有穷个或潜无穷个，对于任意的正整数m,n来说，Amn可以被解释为第n个m元谓词（一元谓词可以被解释为个体的性质，m元谓词（m ≥2）可以被解释为m个个体之间的关系）。

4 否定联结词¬、合取联结词∧、析取联结词∨、蕴涵联结词→、全称量词∀和存在量词∃。

5 左右括号：(、)。

个体变元和个体常元被统称为“项”。用t,t1,t2,...表示任意的项。

(2) 形成规则（A,B是任意公式）：

1 对于任意的m元谓词符号Amn和任意的项t1,t2,...,tm，Amn(t1,t2,...,tm)是公式（被称为原子公式）。

2 如果A是公式，那么¬A是公式。

3 如果A,B是公式，那么(A ∧B),(A ∨B),(A →B)都是公式。

4 如果A是公式，那么∀xiA和∃xiA（i是任意正整数）都是公式。

接下来，我们给出一些关于L∗的语型定义（[5]，第106–107 页、第162 页）：

1 对于任一公式A来说，如果A中有子公式∀xiB出现，那么称B是这个∀xi的辖域；如果A中有子公式∃xiC出现，那么称C是这个∃xi的辖域。

2 对于任一有个体变元出现的公式A来说，如果其中一个体变元xi（i是某个正整数）出现在∀xi或∃xi中，或者出现在∀xi或∃xi的辖域中，那么称xi的这一次出现为约束的；否则，称xi的这一次出现是自由的。如果xi在A中至少有一次自由出现，那么称xi是A中的自由变元。有自由变元的公式被称为开公式；没有自由变元的公式被称为闭公式。

对于公式A来说，无论个体变元xi1,xi2,...,xin（i1,i2,...,in是n个正整数）是否在A中出现，都可以将A记为A(xi1,xi2,...,xin)。

3 对于公式A(xi)来说，用A(t)表示：用项t替换A(xi)中xi的每一次自由出现而获得的公式；如果xi不是A中的自由变元，那么A(t)就是A(xi)。

4 若项t和个体变元xi满足下列条件之一，就称项t对于公式A中的xi是自由的：

1.xi在A中不出现或xi在A中仅有约束出现；

2.xi在A中有自由出现，并且项t是个体常元；

3.xi中有自由出现，项t是某一个体变元xj，并且每当xi在A中自由出现时，xi都不在∀xj或∃xj的辖域内。

以下，为了普遍性，我们把形式语言L∗的初始符号中的个体常元和谓词符号都选取为潜无穷个，在此基础上，我们建立直觉主义谓词逻辑的证明语义。5采用定义3.1 至定义3.5 以及引理3.1、引理3.2 的方式来构建直觉主义谓词逻辑证明语义的思想，是冯棉教授提出的。

定义3.1.L∗中的公式A的一个解释AI由以下七个部分构成：

1 先确定一个论域（对象域），含有有限个对象（不能没有对象）或潜无穷个对象。论域是个体变元和个体常元的取值范围。

2 将A中的每一个个体变元都解释为论域中的任意的对象。

3 对A中的每一个个体常元指定论域中的某一个对象（不同的个体常元可以指定论域中不同或相同的对象）。

4 将A中的每一个一元谓词符号都解释为论域中对象的某种性质（不同的一元谓词可以解释为不同或相同的性质）。

5 将A中每一个n(n ≥2)元谓词符号都解释为论域中n个对象之间的某种n元关系（不同的n元谓词符号可以解释为不同或相同的n元关系）。

6 联结词¬意为“并非”、∧意为“并且”、∨意为“或者”、→意为“如果……，那么……”。

7∀xi意为“对论域中的任意一个对象（都有……）”；∃xi意为“论域中至少有一个对象（有……）”。

对定义3.1 的说明：1 若A是一个闭公式，那么AI是一个具体命题；若A不是闭公式，那么AI不是一个具体的命题。2 若B是A的子公式，那么由AI可获得B的相应解释BI。

定义3.2.A是L∗的公式，AI是对A的一个解释，A中共有m个（m ≥0）不同的自由个体变元xi1,xi2,...,xim，对它们分别指定AI论域中的对象c1,c2,...,cm（这些对象可以相同也可以不同），则称其为“AI解释下全部自由变元的一个赋值”，记为AI(c1,c2,...,cm)。

对定义3.2 的说明：AI(c1,c2,...,cm)是具体命题，若A中没有自由变元（即m=0），那么AI(c1,c2,...,cm)就是AI。

定义3.3.A是L∗的公式，AI是A的一个解释，令φ′=AI(c1,c2,...,cm)（m ≥0）是“AI解释下全部自由变元的一个赋值”，它是一个具体命题，以下是“φ′被判定为真”的递归定义：

1 若A是原子公式，则φ′是原子命题，φ′被判定为真当且仅当给出φ′的构造性证明。（形式同定义2.11 ）

2 若A是¬B，则φ′是否定命题¬φ，同定义2.12 。

3 若A是(B ∧C)，则φ′是合取命题φ ∧ψ，同定义2.13 。

4 若A是(B ∨C)，则φ′是析取命题φ ∨ψ，同定义2.14 。

5 若A是(B →C)，则φ′是蕴涵命题φ →ψ，同定义2.15 。

6 若A是∀xiB，则φ′是全称命题∀xiφ，有两种情况：

(i)B中没有xi的自由出现，则A与B有同样的自由个体变元，这时φ=BI(c1,c2,...,cm)（它是“BI解释下全部自由变元的一个赋值”），则φ′被判定为真当且仅当φ被判定为真，这时亦称φ′获得了构造性证明。

(ii)B中有xi的自由出现，则φ′被判定为真当且仅当对AI论域中的任何一个对象c，都可以找到BI(c1,c2,...,cm,c)（它是“BI解释下全部自由变元的一个赋值”，其中xi指定对象c）的构造性证明，这时我们亦称φ′获得了构造性证明。

7 若A是∃xiB，则φ′是存在命题∃xiφ，有两种情况：

(i)B中没有xi的自由出现，表述方式同6 (i)。

(ii)B中有xi的自由出现，则φ′被判定为真当且仅当能够找到AI论域中的某一对象c，并给出BI(c1,c2,...,cm,c)（它是“BI解释下全部自由变元的一个赋值”，其中xi指定对象c）的构造性证明，这时亦称φ′获得了构造性证明。

定义3.4.A是L∗的任意公式，AI是对A的一个解释，则AI被判定为真当且仅当对于任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)（m ≥0），都可以获得对AI(c1,c2,...,cm)的构造性证明，这时我们亦称AI获得了构造性证明。

由定义3.3 和定义3.4 立即获得以下的引理3.1，它也可以视为“AI被判定为真”的递归定义：

引理3.1.A是L∗的公式，AI是对A的一个解释，则有：

1 如果A是原子公式Arn(t1,t2,...,tr)，则AI被判定为真当且仅当对于任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)（m ≤r），都可获得对AI(c1,c2,...,cm)的构造性证明。

2 如果A是公式¬B，那么AI被判定为真当且仅当对于任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)=¬BI(c1,c2,...,cm)，其中BI(c1,c2,...,cm)是“BI解释下全部自由变元的赋值”，从任意假设的对BI(c1,c2,...,cm)的构造性证明都将导致谬误。

3 如果A是公式(B∧C)，那么AI被判定为真当且仅当对于任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)=(BI(ci1,ci2,...,cik)∧CI(cj1,cj2,...,cjs))，其中BI(ci1,ci2,...,cik)是相应的“BI解释下全部自由变元的赋值”，CI(cj1,cj2,...,cjs)是相应的“CI解释下全部自由变元的赋值”，能同时给出对(BI(ci1,ci2,...,cik) 的构造性证明和对CI(cj1,cj2,...,cjs) 的构造性证明。

4 公式A是(B ∨C)，那么AI被判定为真当且仅当对于任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)=(BI(ci1,ci2,...,cik)∨CI(cj1,cj2,...,cjs))，其中BI(ci1,ci2,...,cik)是相应的“BI解释下全部自由变元的赋值”，CI(cj1,cj2,...,cjs)是相应的“CI解释下全部自由变元的赋值”，能给出对(BI(ci1,ci2,...,cik) 的构造性证明或者给出对CI(cj1,cj2,...,cjs) 的构造性证明。

5 如果A是公式(B →C)，那么AI被判定为真当且仅当对于任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)=(BI(ci1,ci2,...,cik)→CI(cj1,cj2,...,cjs))，其中BI(ci1,ci2,...,cik)是相应的“BI解释下全部自由变元的赋值”，CI(cj1,cj2,...,cjs)是相应的“CI解释下全部自由变元的赋值”，从任意假设的对BI(ci1,ci2,...,cik)的构造性证明都能够得到CI(cj1,cj2,...,cjs)的构造性证明；如果任何BI(ci1,ci2,...,cik)都是谬误，不能获得构造性证明，亦判定AI为真。

6 如果公式A是∀xiB，有两种情况：

(i)B中没有xi的自由出现，则AI被判定为真当且仅当对于任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)，都可以获得对BI(c1,c2,

...,cm)（它是“BI解释下全部自由变元的一个赋值”）的构造性证明。

(ii)B中有xi的自由出现，则AI被判定为真当且仅当对于任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)，对AI论域中的任何一个对象c，都可以找到BI(c1,c2,...,cm,c)（它是“BI解释下全部自由变元的一个赋值”，其中xi指定对象c）的构造性证明。

7 如果A是公式∃xiB，有两种情况：

(i)B中没有xi的自由出现，表述方式同6 (i)。

(ii)B中有xi的自由出现，则AI被判定为真当且仅当对于任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)，都能够找到AI论域中的某一对象c，并给出BI(c1,c2,...,cm,c)（它是“BI解释下全部自由变元的一个赋值”，其中xi指定对象c）的构造性证明。

定义3.5.称L∗的一个公式A是直观有效的当且仅当对A的任何解释AI，AI都被判定为真，即总能给出对AI的构造性证明。

由定义3.4 和定义3.5 立即获得以下的引理3.2：

引理3.2.L∗的一个公式A是直观有效的当且仅当对A的任何解释AI的任意一个“AI解释下全部自由变元的赋值”AI(c1,c2,...,cm)（m ≥0），都可以获得对AI(c1,c2,...,cm)的构造性证明。

定义3.1 至定义3.5 和引理3.1、引理3.2 构成了直觉主义谓词逻辑的证明语义，以下给出直觉主义谓词逻辑公理系统IQ，它建立在形式语言L∗的基础上，再加上以下两部分构成：6[5]，第169–170 页，表述有所改动。

(1)IQ的公理：首先，把IP1到IP10中形式语言L 的任意公式A、B、C解释成形式语言L∗的任意公式，所得到的十条公理IQ1到IQ10即为IQ的前十条公理。除此之外，增加如下涉及量词的公理（A,B是任意公式，i是任一正整数）：

公理IQ11：(∀xi(A →B)→(∀xiA →∀xiB))

公理IQ12：(∀xi(A →B)→(∃xiA →∃xiB))

公理IQ13：(A →∀xiA)，其中个体变元xi在A中不自由出现

公理IQ14：(∃xiA →A)，其中个体变元xi在A中不自由出现

公理IQ15：(∀xiA(xi)→A(t))，其中项t对于A中的个体变元xi是自由的，A(t)是用t替换A(xi)中xi的每一次自由出现而获得的公式。

公理IQ16：(A(t)→∃xiA(xi))，其中项t对于A中的个体变元xi是自由的，A(t)是用t替换A(xi)中xi的每一次自由出现而获得的公式。

(2) 推理规则（A,B是任意公式，i是任意正整数）：

分离规则MP：由A和(A →B)可推出B。

概括规则Gen：从A可推出∀xiA。

若A是IQ的公理，或者是由公理出发运用MP规则或Gen规则推出的公式，则称A是IQ中的一个（内）定理，记为⊢IQ An。

下面的工作是证明直觉主义谓词逻辑系统IQ的可靠性，证明由以下引理和定理构成。

引理3.3.系统IQ的16条公理都是直观有效的。

首先，IQ1到IQ10的证明方法参照引理2.1，并使用定义3.3 至定义3.5 或引理3.1、引理3.2，从略，这里仅给出对IQ11到IQ16的证明。

公理IQ11.(∀xi(A →B)→(∀xiA →∀xiB))

证明.给定对公理IQ11的任意的一个解释(∀xi(A →B)→(∀xiA →∀xiB))I，再给定任意一个“(∀xi(A →B)→(∀xiA →∀xiB))I解释下全部自由变元的赋值”(∀xi(A →B)→(∀xiA →∀xiB))I(c1,c2,...,cm)=(φ →(ψ →η))，其中φ=(∀xi(A →B))I(c1,c2,...,cm)是相应的“(∀xi(A →B))I解释下全部自由变元的赋值”，ψ=((∀xiA)I(ci1,ci2,...,cik)是相应的“(∀xiA)I解释下全部自由变元的赋值”，η=(∀xiB)I(cj1,cj2,...,cjs))是相应的“(∀xiB)I解释下全部自由变元的赋值”。假设α和β分别是φ和ψ的构造性证明，以下证η可获得构造性证明。分两种情况讨论：

(1) (A →B)中没有xi的自由出现（这时A和B中也没有xi的自由出现），根据定义3.36 (i)，利用α和β能够分别得到θ=(A →B)I(c1,c2,...,cm)（它是“(A →B)I解释下全部自由变元的一个赋值”）和δ=AI(ci1,ci2,...,cik)（它是“AI解释下全部自由变元的一个赋值”）的构造性证明，而θ=(δ →λ)，其中λ=BI(cj1,cj2,...,cjs)（它是“BI解释下全部自由变元的一个赋值”），再根据定义3.35，能够获得λ的构造性证明，进而根据定义3.36 (i)，η获得了构造性证明。

(2) (A →B)中有xi的自由出现，根据定义3.36 (ii)，对论域中的任一对象c，利用α能够得到θ=(A →B)I(c1,c2,...,cm,c)（它是“(A →B)I解释下全部自由变元的一个赋值”，其中xi指定对象c）的构造性证明，又有两种可能性：

(i) 当A中有xi的自由出现时，利用β能够得到δ=AI(ci1,ci2,...,cik,c)（它是“AI解释下全部自由变元的一个赋值”，其中xi指定对象c）的构造性证明，而θ=(δ →λ)，其中λ=BI(cj1,cj2,...,cjs)（若B中没有xi的自由出现）或λ=BI(cj1,cj2,...,cjs,c)（它是“BI解释下全部自由变元的一个赋值”，其中xi指定对象c，而B中有xi的自由出现），再根据定义3.35，能够获得λ的构造性证明，进而根据定义3.36，η获得了构造性证明。

(ii) 当A中没有xi的自由出现时，利用β能够得到δ=AI(ci1,ci2,...,cik)的构造性证明，而θ=(δ →λ)，其中λ=BI(cj1,cj2,...,cjs,c)，再根据定义3.35，能够获得λ的构造性证明，进而根据定义3.36 (ii)，η获得了构造性证明。

最后，利用α和β，从(1)(2)出发，根据定义3.35 可知(φ →(ψ →η))获得了构造性证明，再由引理3.2 推知公理IQ11是直观有效的。

公理IQ12.(∀xi(A →B)→(∃xiA →∃xiB))

参照公理IQ11的证明方法，并使用定义3.35、定义3.37 和引理3.2，从略。

公理IQ13.(A →∀xiA)，其中个体变元xi在A中不自由出现。

证明.给定对公理IQ13任意的一个解释(A →∀xiA)I，再给定任意一个“(A →∀xiA)I解释下全部自由变元的赋值”(A →∀xiA)I(c1,c2,...,cm)=(φ →ψ)，其中φ=AI(c1,c2,...,cm) 是相应的“AI解释下全部自由变元的赋值”，ψ=(∀xiA)I(c1,c2,...,cm)是相应的“(∀xiA)I解释下全部自由变元的赋值”。假设α是φ的任意构造性证明，根据定义3.36 (i)，ψ获得了构造性证明，再根据定义3.3 5，(φ →ψ)获得了构造性证明，进而根据引理3.2，公理IQ13是直观有效的。

公理IQ14.(∃xiA →A)，其中个体变元xi在A中不自由出现。

参照公理IQ13的证明方法，并使用定义3.35、定义3.37 (i) 和引理3.2，从略。

公理IQ15.(∀xiA(xi)→A(t))，其中项t对于A中的个体变元xi是自由的。

证明.给定对公理IQ15任意的一个解释(∀xiA(xi)→A(t))I，再给定任意一个“(∀xiA(xi)→A(t))I解释下全部自由变元的赋值”(∀xiA(xi)→A(t))I(c1,c2,...,cm)=(φ →ψ)。假设α是φ的构造性证明，以下证ψ可获得构造性证明，分三种情况讨论：

(1)xi不在A中自由出现，A(t)是A(xi)（即A）。这时φ=(∀xiA)I(c1,c2,...,cm)是相应的“(∀xiA(xi))I解释下全部自由变元的赋值”，ψ=AI(c1,c2,...,cm)是相应的“A(t)I解释下全部自由变元的赋值”。从α出发，根据定义3.36(i)，ψ获得了构造性证明。

(2)xi在A中有自由出现并且t是某一个体常元as，A(t)是A(as)。这时φ=(∀xiA(xi))I(c1,c2,...,cm),ψ=(A(as))I(c1,c2,...,cm)，设(∀xiA(xi)→A(t))I解释下对as指定的论域中的对象是c，根据定义3.36 (ii)，通过α能够得到(A(xi))I(c1,c2,...,cm,c)（它是“(A(xi))I解释下全部自由变元的一个赋值”，其中xi指定对象c）的构造性证明，而(A(xi))I(c1,c2,...,cm,c)=ψ，于是ψ获得了构造性证明。

(3)xi在A中有自由出现，t是某一个体变元xj，并且每当xi在A中自由出现时，xi都不在∀xj或∃xj的辖域内，A(t)是A(xj)。设(∀xiA(xi)→A(t))I解释下对xj指定的论域中的对象是ci（它是c1,c2,...,cm中的某一个对象），这时φ=(∀xiA(xi))I(c1,c2,...,ci−1,ci+1,...,cm)（若∀xiA(xi)中没有xj的自由出现）或φ=(∀xiA(xi))I(c1,c2,...,cm)（其中xj指定对象ci，而∀xiA(xi)中有xj的自由出现），ψ=(A(xj))I(c1,c2,...,cm)（它是“(A(xj))I解释下全部自由变元的赋值”，其中xj指定对象ci），根据定义3.36 (ii)，通过α能够得到(A(xi))I(c1,c2,...,cm)（它是“(A(xi))I解释下全部自由变元的一个赋值”，其中xi指定对象ci）的构造性证明，而(A(xi))I(c1,c2,...,cm)=ψ，于是ψ获得了构造性证明。

最后，利用α,从(1)(2)(3)出发，根据定义3.35 可知(φ →ψ)获得了构造性证明，再由引理3.2 推知公理IQ15是直观有效的。

公理IQ16.(A(t)→∃xiA(xi))，其中项t对于A中的个体变元xi是自由的。

参照公理IQ15的证明方法，并使用定义3.35、定义3.37 和引理3.2，从略。

引理3.4.A，B是任意的L∗的公式，如果A和(A →B)都是直观有效的，那么B也是直观有效的。

证明方法参照引理2.2，并使用定义3.3 至定义3.5 或引理3.1、引理3.2，从略。

引理3.5.A是L∗中任意公式，若A是直观有效的，则∀xiA也是直观有效的。

证明.给定∀xiA的任意一个解释(∀xiA)I，再给定任意一个“(∀xiA)I解释下全部自由变元的赋值”(∀xiA)I(c1,c2,...,cm)=φ。分两种情况讨论：

(1) 当xi在A中没有自由出现时，ψ=AI(c1,c2,...,cm)是相应的“AI解释下全部自由变元的赋值”，已知A是直观有效的，由引理3.2 知ψ可获得构造性证明，再由定义3.36 (i)，φ可获得构造性证明，进而由引理3.2 知∀xiA是直观有效的。

(2) 当xi是A中的自由变元时，设c是AI论域中的任意一个对象，已知A是直观有效的，由引理3.2 知AI(c1,c2,...,cm,c)（它是“AI解释下全部自由变元的一个赋值”，其中xi指定对象c）都能够获得构造性证明，再根据引理3.16 (ii)，φ可获得构造性证明，进而根据引理3.2 知∀xiA是直观有效的。

定理3.6(系统IQ的可靠性定理).任给一L∗的A，如果⊢IQ A，那么A是直观有效的。

证明.根据引理3.3、引理3.4 和引理3.5，使用数学归纳法即证。