[音乐] 好，欢迎回来。
下面呢我们来介绍这个 一阶谓词演算的形式系统，叫做FC，因为这个First order是叫FC。
那么相比起这个命题演算的形式系统PC来说，
这个FC的这个符号系统呢要更为复杂一些， 因为呢我们在一阶谓词逻辑里面
引入了这个个体，个体常元，个体变元。
那这样呢，对于个体来说，它需要
再进一步地把个体组合成一些关于个体的一些公式，而不光光只是 对于真值的一些演算。
所以呢我们FC的符号系统，首先呢包含个体变元，
像x,y,z,然后u,v,w这些呢作为个体变元，然后个体常元呢就用a,b,c,d 这样的字母来表示。
那么还有呢个体间的这个运算符号 那么因为运算是千变万化千变万化万化的，所以呢我们用
这个函数符来表示它，用f,g,h这样的函数来表示它。
当然函数呢会有不同的元数，我们知道就是函数包含了多少个自变量的意思。
那么这个元数呢n就是一个正整数。
它表示呢是函数的元数，它可以是一元、 二元，或者更多元的这个函数。
那么接下来是谓词符号。
谓词符号呢用P，大写的P,Q,R,S来表示。
当然我们前面也知道，这个谓词呢也有这个元数， 单元谓词，二元、
三元这些谓词，所以呢， 它用右上角写一个这个数字，当然这个数字也是可以省略的。
它只是表示这个谓词的元数而已。
但是当n等于0的时候， 那么谓词公式呢就退化成一个命题常元，因为它没有任何的空位需要填。
那么接下来就是真值的联结词，否定联结词和蕴含。
那么这两个呢也是我们在PC当中所用到的。
它增加了一个量词，量词，就是
而我们不把这个存在量词引入呢，是因为 存在量词实际是可以用全称量词来表示的。
比如说存在x，那么它实际上是等价于
否定，然后呢全称量词，全称x，然后再否定，是
等价于这个的。
那么在 FC里边，还有一个高级的语言成分，就是关于如何把个体变元
和个体常元组合成一个个体项的问题。
那么这里就有一个新的一个概念，叫做个体项term，简称为项。
那么第一呢，个体变元和个体常元它是这个个体项，
第二呢，对于任何的正整数n，那么如果这个f(n)它是一个n元的函数符的话，
那么同时呢，t1,t2,一直到tn是项。
那么把这个t1,t2...tn填入到这个f 这个函数符的这个调用里边，那么它所
组成的一个运算，得到的也是一个项，也是一个项。
那么第三个呢，也是说，除了有限次地使用上述两个条款所确定的符号串之外， 没有别的东西是项。
这就说明这个项之间的 运算是可以嵌套的，是可以嵌套的，而且可以用不同的函数符， 来进行嵌套。
然后最终呢得到一个个体项，个体项。
然后接下来呢就是FC高级语言成分合式公式，就是谓词公式啊。
那么简称公式，那么它说第一呢，对于非负整数n，
如果P(n)呢是一个一元的谓词，t1,t2，一直到tn是项的话，
那么P(0)那就是命题常元了。
那么P(n)就是n等于1,2,3一直以上的，然后再加上
把它，把这个t1,t2,一直到tn，这个n个项的
填入到这个谓词里边去，也就是谓词填式， 它也是公式，也是公式。
第二说如果A，B是公式， v呢是任何一个个体变元，那么非A加括号，
A蕴含B加括号，这前面这两个都是PC里边定义的，命题公式里边定义的。
而第三个，任意的c，A 那么或者说任意的v，A(v)
也就是说这个A当中包含了v，或者不包含v，其实都无所谓，只要前面加了一个全称量词。
那么这些呢也都是公式。
那么最后，归纳 定义的最后，第三句也就是除了有限次地引用上述两个条款所确定的符号串之外，
没有别的东西是这个合式公式，是这个公式。
那么在介绍这个公理之前，
FC的公理之前，我们来先引入一个所谓的叫全称封闭式的 概念。
全称封闭式是说如果一个公式A当中有v1到vn，n个这个自由变元，
那么我们把这个n个自由变元全都用 全称量词来进行约束，然后放在A的前面。
那么这种的就称作为公式A的全称封闭式，全称封闭式。
如果A当中没有任何的这个自由变元的话，那么A的全称封闭式呢就是它自己， 就是它自己。
那么在这个全称封闭式下，我们再来介绍这个FC的公式， 啊，公理。
公理A1是A→(B→A)这样的蕴含， 公理A2呢是(A→(B→C))，然后(A→B)→(A→C)这样的蕴含。
A3呢是一个非A蕴含非B，然后再蕴含的B蕴含A。
A4呢它是一个
全称量词，任意x,A(x)，然后蕴含着A，然后呢把这个x
替换成一个t，替换成一个项，这个个体项呢就是我们前面所定义的
那个高级语言成分，个体项，所以呢它可以是个体变元，也可以是个体常元，以及
个体变元、 个体常元，进行这个函数符号，进行运算了以后得到的
这个项，对吧？那么所以呢它是用项来代入到这个
A里头，A里头替换这个自由变元， 啊，这样。
A5呢是一个 永真式，就是任意x，然后A(x)蕴含B(x)，然后再蕴含
任意xA(v)，然后蕴含着任意xB(x)， 那么x呢是任意一个自由变元。
A6呢是说A蕴含着任意xA， 而A当中并没有这个自由变元x。
那么A7呢是说从A1
到A6的所有的这些公理，它们的全称封闭式， 都是FC的公理。
那么A7呢实际上是一个 一个大总结，说A1到A6之间的这6条公理
里边只要任何一个公理它满足这个全称封闭式的话，
它只要有自由变元，把所有的自由变元都加上一个全称量词的约束， 然后放在公式的前面。
如果是这样的话，那么也都是公理。
那么我们看到FC当中的公理可以分成这几部分。
第一呢，A1-A3，它是命题逻辑，它是PC当中的公理，也是命题逻辑里边的重言式。
那么也是，同时呢，它也是这个谓词逻辑里边的永真式。
然后A4-A7则就是，单单是谓词演算当中的永真式，因为它们
都带着这个量词，都带着量词。
那么FC当中的推理规则，也跟PC一样，它只有一条规则。
A,B是任意公式，如果有A，如果有A蕴含B， 那么就可以写下B，在公式序列当中写下一个B。
这就是分离规则，这个呢是跟PC是一样的。
那当然FC也有一些重要的性质。
像合理性、 一致性、 完备性，这个呢跟
PC是一致的，它都是一样的，所谓的合理性就是说 FC当中的定理，同时呢也是我们的逻辑真理。
那么一致性呢是说FC当中呢不会 同时呢去证明或演绎出自相矛盾的两个
命题，对吧？然后完备性呢，只要是说逻辑当中的真理， 那么在FC里边都能够得到证明。
也同时呢，就是FC当中的定理。
这就是合理性、 一致性、 完备性。
当然在FC里边呢也有重要的一些 跟PC一样，它的重要的一些语言定理，这三个语言定理，在FC当中也是可以用的。
一个呢是演绎定理，一个是归谬定理，一个是穷举定理。
陈斌副教授
