1，一阶逻辑系统
1.1，的定义
一阶逻辑系统也称为谓词系统或者量化理论。一阶形式系统可写为，其中：
的通用逻辑符号包括：连接词（），量词（），辅助符号（）。非逻辑符号包括：可数无穷多个个体/函数/命题/谓词变元。任意多个个体/函数/命题/谓词常元。可归纳定义如下：（1）若为个体变元或常元，则；（2）若为元函数常元或变元，为项，则为项；（3）任何项都可有限次应用（1）和（2）获得。由下列公式构成：设为元谓词常元或者变元，为项，则。可归纳定义如下：（1）；（2）若则；（3）若则；（4）若且是个体变元，则；（5）任何公式都可有限次应用规则（1）-（4）构造得到。
将称为语言，记为。
1.2，自由/约束出现
设为个体变元：
称在中形如或者的子公式的出现称为约束出现。变元的非约束的出现称为自由出现。若 在中有约束出现，则称为约束变元。若 在中有自由出现，则称为自由变元。若中无自由的个体，则称为闭公式。可能包括函数变元、命题变元、谓词变元。若中除约束个体变元外无其他变元，则称为句子。
1.3，代入操作
个体变元代入（对项的代入）：设是个体变元，是项，令：
若为个体常元，则；若为个体变元，则；若为函数常元，则；若为函数变元，则 ；
个体变元代入（对公式的代入）：设是个体变元，是项，令：
对原子公式，有；；；;
命题变元代入（对公式的代入）：设是命题变元，是公式，令：
；，为元谓词常元或者变元，不包含命题变元，不进行替换。；；。
1.4，可代入（自由）
项的可代入：称项对公式中的个体变元可代入（为自由的），如果对中的每个变元，变元在辖域内无自由出现。
公式的可代入：称公式对中的命题变元可代入（为自由的），如果对中的每个自由变元而言，不出现在辖域内。
原则：代入前后约束出现的次数不改变。
1.5，公理集和规则集
公理集：
，其中项对中的是自由的。，其中在中无自有出现。
规则集：
2，的定理与导出规则
2.1，无/有前提依赖证明
一阶系统有两类证明方式：无前提依赖与有前提依赖。
无前提依赖：不使用公设集中的公式，证明序列中仅出现公理以及通过应用规则得到的公式。带前提依赖：证明序列中可能包含公设集中的公式。
在前提依赖证明中，对规则增加了相应限制，并且还需要一条额外的规则。同时，还要区分公设集为有穷和无穷情况。
2.2，永真及P规则
称是永真的，如果存在中的永真式以及命题变元代入使得。
P-规则：
若是中的永真式，则；是的公式。若是永真的，则； 是 的公式。若且是永真的，则。
2.3，无前提依赖证明的协调性
取，定义映射如下：
若，则。
若则
关于无前提依赖证明满足绝对协调及关于否定协调。
2.4，肯定出现及否定出现
设，并将中的派生连接词、量词全部用原始符号替换，则：
若在中的某个指定出现位置位于偶数个的辖域中，则称的该次出现为正出现或者肯定的。若在中的某个指定出现位置位于奇数个的辖域中，则称的该次出现为负出现或者否定的。若在中的所有指定出现都是肯定的，则称在中为肯定的。若在中的所有指定出现都是否定的，则称在中为否定的。
：设，且为出现在和中的所有自由个体变元，则：
若在中为肯定的，则。若在中为否定的，则。若在中为肯定的，且，则。若在中为否定的，且，则。
：设，且为出现在和中的所有自由个体变元，则：
。若，则。若且，则。
证明：令为用替换在中所有肯定出现所得之公式；于是必然是用替换在中否定出现所得之公式。利用，可得及。
2.5，条件
设，不是的自由变元且对中的为自由的，则称和关于满足条件，记作：。
带入可逆性：换名等价性：规则：若，则若对中的是自由的，则若，则：若，且对中的是自由的，则：若且在中不自由，则：若，，且对中的是自由的，但在中不自由，则。：若，同时，，则。：若且则。
2.6，带前提依赖证明
给定有穷公式集，如果存在有穷序列，且对每个必有一下几种情况成立：
Hyp：；Ax：是公理；MP：存在，使得;Gen：存在，使得，其中在中不自由；：存在，公式，个体变元和满足，且 。
则称由可证，记作，并称是由导出的证明。
若是无穷集，则是指存在的一个有穷子集使得。
定理和派生规则：
：若，且是永真的，则。：若，在 中是肯定的（/否定的）且，则。：若且则。：若，在中不自由，对中的是可代入的，则。：若，在中不出现，对中的是可代入的，则。
3，的语义及前束范式
3.1，函数单点取代操作
设，则任取及，可以得到一个新的函数，其定义如下：
性质：
若，则。
3.2，解释和论域
给定二元偶为的一个解释，其中是一个非空集合，称为论域。为如下定义的一个映射：
若为个体常元，则；若为元函数常元，则；若为命题常元，则，其中；若 为元谓词常元，则。
给定解释，若映射满足：
若为个体变元，则；若为元函数变元，则；若为命题变元，则；若为元谓词变元，则。
则称为下的一个指派。用表示下所有指派构成的集合。
3.3，项和公式的语义
项的语义：设以及，对每个，可归纳定义其语义如下：
若为个体常元，则。若为个体变元，则。若，其中为元函数常元，则。若，其中为元函数变元，则。
公式的语义：设以及，对每个,可归纳定义其语义如下：
若，其中为元谓词常元，则。若，其中为元谓词变元，则若，则。若，则。若，则。
3.4，带入定理
设，项对中的可代入，公式对中的命题变元可代入。则对任意解释以及指派：
对任意的项有，其中。，其中。，其中。
若在中不自由，则对任意的，有。
推论：若为句子，则的真值只与解释有关，而与指派无关。
3.5，可满足和模型
可满足：给定公式，若存在解释以及使得，则称是可满足的，并记作。
模型：若对于公式，存在解释使得每个都有成立，则称是的模型，记作。
永真式：若每个解释都是的模型，就称是永真式或者有效的。
可满足：给定公式集合，若存在解释以及使得对每个都有，成立，则称是可满足的，此时记作。
模型：特别的，若对每个都有，就称是的一个模型，记作。
逻辑结果：若对每个解释及，若则，就称是的逻辑结果，记作。
3.6，前束范式
设为个体变元：
若为的子公式，且在中无自有出现，则称为空量词。若中无空量词，且量词均不出现在的辖域内，则称为前束范式。
因此，若为前束范式，当且仅当形如：。其中不含量词，，是彼此不同的个体变元。
若满足如下条件：
无空量词；中的自由变元与约束变元不同名；中不同的约束变元之间不同名；
则称是矫正的。
设是矫正的公式，并假设其中从左到右第个量词为，那么的前束范式为。其中：若肯定出现则不需要改变，否定改变取其对偶。
4，系统的元性质
4.1，可靠性
可靠性定理：
若则。若则。
推论：若公式集是可满足的，则必是协调的。
证明：若不协调，则且。由可靠性定理，有及。因为是可满足的，不妨设，则与矛盾。
4.2，协调性
一阶语言分层：分别令，为中的全体句子、闭公式和公式构成的集合。令为中全体闭项（不含变元的项）构成的集合。
协调性：设是一阶逻辑系统：
若，则称为绝对协调的。若，则或者，就称关于否定协调。若，则称是协调的。
设，若为协调的，则称与协调；否则称与不协调。特别的，若为有穷集时，则把与（不协调）称为与协调（不协调）。
协调集的性质：与不协调当且仅当。
推论：与不协调当且仅当。
4.3，独立性
独立性：
将全称量词的语义重新定义如下：
可以验证：除均为永真式，均保持永真性。但是，公理在该解释下永真，因此独立。
独立性：
选定某一个谓词常元，个体变元，以及命题常元。令为将中全部替换为所得之公式。考虑到前提为空的情形——若可不使用证出，则必然是永真式。
考虑公式，显然有，从而是永真式。但是不是永真式，从而独立
独立性：
考虑在中有成立，但是中任一公里的长度均大于的长度；和规则均不能减少已证定理的长度。因此规则独立。
规则独立性：
考虑新解释：对每个形如的公式有；同时对其他公司的定义不变（）。于是，若，则必然是的模型。但不是的模型，因此，从而独立。
规则独立性：
首先，。其次，设是在标准解释的基础上，将所有形如的值重赋为解释，则对任意若，则必为的模型。但是，不是的模型。因此独立。
4.4，完全性
完全集：设，若对每个，有或者有，则称是完全的。（与形式系统完全性不是一个概念）
极大协调集：若公式集即是完全的又是协调的，则称是极大协调集。
极大协调集性质：设为极大协调集，则：
对任意公式而言，与恰好有一个在中；若，则与不协调。
协调集的可容许性质：设是上的升链，且每个都是协的，则也是协调的。
协调集的可扩张性：若是协调集，则存在极大协调集使得。
形式系统的膨胀：设与是两个一阶形式系统：
若，则称是的膨胀，记作。若，则称是的真膨胀，记作。
形式系统的扩张：设与是两个一阶形式系统，：
若且，则称为的扩张，记作。若（偏序），且，则称为的保守扩张，记作。
若则为协调的当且仅当为协调的。
若，且两者的差别仅有个体常元，，则。
节省解释和节省模型：若解释满足，则称是节省的。若的模型是节省的，则称该模型为其节省模型。
语言保势扩张：给定两个一阶形式系统，若且，则。
协调集的可满足性：若是协调的，则必有节省解释满足。
完全性定理：
若，则。若，则。
4.5，紧致性
语法紧致性：一阶逻辑公式集是协调的当且仅当其每个有穷子集是协调的。
语义紧致性：一阶逻辑公式集是可满足的当且仅当其每个有穷子集是可满足的。
