命题演算是最简单、最基本的形式系统，主要用来表示较为简单的逻辑推理的一种数学模型.其简单性表现为：当它把复合命题分解成简单命题后，就把简单命题视为最小考察对象，不再继续对简单命题进行分解.
定义1.1命题
具有确切真值的陈述句（或断言）称为命题（proposition）.
命题的真值非真即假，只有两种取值，这样的系统称为二值逻辑系统.
注意：
命题的类型：
命题通常用大写英文字母（可带下标）来表示.
命题通常可以通过一些联结词复合而构成新的命题，这些联结词被称为逻辑联结词.在命题演算中，这些联结词可以看作运算符，因此也叫作逻辑运算符.
定义1.2否定联结词
定义1.3合取联结词
定义1.4析取联结词
这里的“或”是“相容或”（“可兼或”）.
定义1.5蕴涵联结词
定义1.6等价联结词
一般约定：
定义1.7
原子命题在不指派真值时称为命题变元，而复合命题由原子命题和联结词构成，可以看作是命题变元的函数，且该函数的值仍为“真”或“假”，可以称为真值函数（truevaluefunction）或命题公式（propositionalformula）.
不是原子命题和联结词的任意组合都可以为命题公式.我们用递归的方法来定义命题公式.
定义1.8命题公式（合式公式、形式命题）
公式本身没有真值，只有在对其所有命题变元指定真值后才变成一个具有真值的命题.
定义1.9公式的解释
定义1.10公式的真值表
定义1.11
定义1.12
定理1.1
常用逻辑恒等式：
定义1.13
常用永真蕴涵式：
定理1.2代入定理
定理1.3替换定理
定义1.4对偶公式
定理1.4
定理1.6
首先考虑一元运算.
最多只能定义4种运算，但除了否定之外，永假、永真、恒等作为运算意义不大，所以一般不再定义其它一元运算.
考虑两变元在一个二元运算作用下可能的真值表.
为了叙述方便，引进下面四个联结词.
与非的性质：
或非的性质：
异或的性质：
定义1.15
同一个命题有不同的表达形式，这样给命题演算带来了一定的困难.为了使命题公式规范化，引入范式的概念.
定义1.16
性质：
定理1.7
任一命题公式都存在着与之等值的析取范式和合取范式.
证明：对于任一公式，可用下面的方法构造出与之等值的范式：
范式虽然为命题公式提供了一种统一的表达形式，但这种表达形式却不是唯一的，这种不唯一的表达形式给研究问题带来了不便，因此有必要引进更为标准的范式.
定义1.17
定理1.8
任何命题公式的主析取范式和主合取范式存在且唯一，即任何命题公式有且仅有一个与之等价的主析取范式和主合取范式.
求主析取范式和主合取范式的方法：
即，若
推理也称论证，它是指从前提出发推出结论的思维过程：前提是已知命题公式集合，结论是从前提出发应用推理规则推出的命题形式.
定义1.18
定理1.19
直接用等值演算来判断推理的形式结构是否是重言式.
将推理的形式结构转化为主析取范式，但仍判断其是否为重言式.
以上方法，当形式结构比较复杂，特别是所含的命题变元较多时，一般很不方便.
构造证明法是依据一些公认的推理规则，从前提出发，推导结论.它可以看作是公式的序列，其中每个公式都是按照事先规定的规则得到的，且可将所用的规则在公式后写明，该系列最后一个公式是所要证明的结论.
一些重要的永真蕴涵式：
由这9个定律中的8个可以得到8个推理规则：
意义：当推理的结论是蕴涵式时，可以将其前件作为附加前提引用，只要能推理出其后件，则原推理成立.
定义1.19
定理1.10
由上述定理得归谬法：
将结论的否定作为附加前提引入，公式序列的最后一行得到一矛盾式，则原结论成立.
形式系统一般由以下几个部分组成
对于一个形式系统，公理集和证明均可以为空.当两者皆为空时，系统仅仅为一个语句生成系统.在数理逻辑中，如果公理集非空，则称为公理系统；若公理集为空，则称为自然推理系统.
对于一个具体的实际系统，用形式系统来描述，有两个具体的问题必须解决，即语法推论和语义推论的一致性问题：
命题1
命题2
若一字母串是由两个公式并接而成，则并接的方式是唯一的.
确定任一给定字母串是否是公式的算法：
定义2（语法推论）
几点结论：
命题1（同一律）
命题3
定理（演绎定理）
命题1（否定肯定律）
推论（双重否定律）
定义1（真值函数）
定义1（赋值）
定义2（真值指派）
定理1
定义3（永真式）
定义4（永假公式与可满足公式）
定义5（语义推论）
由该定义立刻可得出以下结论：
命题4
定义1（公式集的完备性）
无矛盾公式集必有无矛盾的完备扩张.
定义1
命题4（De.Morgan律）
命题5（等值公式的性质）
下面讨论等值公式的替换问题.
命题6（等值公式的性质）
定理1（子公式等值可替换性）
在命题逻辑中，命题是具有真假意义的陈述句，从语法上分析，一个陈述句由主语和谓语两部分组成，若将句子分解为：主语+谓语，同时将相同的谓语部分抽取出来，则可以表示这一类的语句.因此，为了揭示命题内部结构以及命题的内部结构的关系，就按照这两部分对命题进行分析，分解成主语和谓语，并且把主语称为个体词或客体，而把谓语称为谓词.
在原子命题中，可以独立存在的客体（句子中的主语，宾语等）称为个体词（individual），而用以刻画个体词的性质或个体词之间的关系的词即是谓词（predicate）.
单纯的谓词或单纯的个体词都无法构成一个完整的逻辑含义，只有将它们结合起来才能构成一个完整的，独立的逻辑断言.
定义2
个体词和谓词根据其具有的抽象分为两种：
定义3
定义4
定义5
有必要对个体域进行统一，全部使用全总个体域，此时每一个句子中个体变量的变化范围用一个特性谓词来刻划.统一成全总个体域后，在公式中就不必特别说明.特性谓词在加入到命题函数中时遵循如下规则：
定义1（项的生成规则）
定义2（闭项）
只含有个体常元的项叫做闭项.
定义3（原子公式集）
原子公式集是指
定义1（谓词演算公式集）
字母表：
谓词演算公式的形成规则：
规则1（约束变元的改名规则）
规则2（自由变元的代替规则）
若公式中不含自由出现的变元，则称该公式为闭式.
“公理”：
“证明”：
定义2（命题演算型永真式）
推论1
定理3（反证律）
定理4（归谬律）
命题5
定义3（可证等性）
命题6
命题8
定理5（子公式的等价可替换性）
定义2（项解释）
定义3（项解释的变元变通）
定义1（公式的赋值函数）
定义1（公式在解释域中恒真与恒假）
结论：
判定问题：谓词逻辑的判定问题，指的是对任何一公式的有效性的判定，若说谓词逻辑是可判定的，就是要求给出一个可行的方法，使得对任一公式都能判断是否是有效的.所谓可行的方法，乃是一个机械方法，可一步一步做下去，并在有穷步内实现判断.一般来说，像数学定理的证明是不可行的.
常用的等价式：
常用的永真蕴涵式：
定理1（前束范式存在定理）
一阶逻辑中的任何公式都存在与之等值的前束范式.
（注：前束范式并不唯一.）
定理2
定义1（模型）
定义2（语义推论）
定义3（有效式与可满足公式）
(K1)、(K2)、(K3)三种模式的公理都是有效式.
一般情况下，总是假定相同的个体域（即全总个体域）下进行的.