形式系统由{∑, TERM, FORMULA, AXIOM, RULE}等5个部分构成，其中 称为符号表，TERM 为项集；FORUMULA 为公式集；AIXIOM 为公理集；RULE 为推理规则集。
：1、 符号表∑为非空集合，其元素称为符号。
2、 设∑*为∑上全体字的组合构成的集合。
项集TERM 为∑*的子集，其元素称为项；项集TERM 有子集V ARIABLE 称为变量集合，其元素称为变量。
F(X) a, X,3、 设∑*为∑上全体字的组合构成的集合。
公式结FORMULA 为∑*的子集，其元素称为公式；公式集有子集ATOM ，其元素称为原子公式。
A(f(a,x1,y)), A →B4、 公理集AXIOM 是公式集FROMULA 的子集，其元素称为公理。
5、 推理规则集RULE 是公式集FORMULA 上的n 元关系集合，即RULE=)}2(|{n FORMULA r n n n r ⊆∧≥∧∃是正整数，其元素称为形式系统的推理规则。
其中公式集和项集之间没有交叉，即TERM ∩FORMULA =φ，公式和项统称为表达式。
由定义可知，符号表∑、项集TERM 、公式集FORMULA 是形式系统的语言部分。
而公理集AXIOM 、推理规则集RULE 为推理部分形式系统特性1、 符号表∑为非空、可数集合（有穷、无穷都可以）。
2、 项集TERM 、公式集FORMULA 、公理集AXIOM 和推理规则集RULE 是递归集合，即必须存在一个算法能够判定给定符号串是否属于集合（可判定的）。
3、 形式系统中的项是用来描述研究的对象，或者称为客观世界的。
而公式是用来描述这些研究对象的性质的。
这个语言被称为对象语言。
定义公式和项产生方法的规则称为词法。
公理：I))((A B A →→ II))()(())(((C A B A C B A →→→→→→ III ))())()(((A B B A →→⌝→⌝证明：A →A(1)A →(A →A)((A →(B →C))→((A →B)→(A →C))((A →(B →A))→((A →B)→(A →A))((A →((A →A)→A))→((A →(A →A))→(A →A))A →((A →A)→A))(A →(A →A))→(A →A)(A →(A →A))A →ABB A A →, 已知：R 是一个有关公式的性质证明：R 对于所有公式有效I. 对于)(FSPC Atom p ∈，则)(P RII. 假设公式A 和B 都具有RIII. )(FSPC Atom A ∈∀，且)(A R ，则)(A R ⌝IV. B A ,∀是公式，如果)(A R 且)(B R ，则)(B A R →根据：形式系统的联结词只有两个→⌝,，因为在命题逻辑的语义上，其他联结词可以有这两个联结词表示。
已知：A ⌝⌝求证：A 成立(1)A 是公式)(A A A →⌝⌝→A A →⌝⌝(2){A ⌝⌝，A ⌝}├A ⌝{A ⌝⌝，A ⌝}├A ⌝⌝A ⌝⌝├A反证(3)A ⌝⌝)(A A A ⌝⌝→⌝⌝⌝⌝→⌝⌝A A ⌝⌝→⌝⌝⌝⌝→⌝→⌝⌝⌝⌝)→⌝⌝)A⌝⌝⌝(A(AA→⌝A⌝⌝⌝A⌝⌝→→A→⌝⌝⌝⌝3)A()A(AA→⌝⌝AA公理代入原理：设A(P)为含有变元P的公理（定理同样适用），如果将公式A中的变元P 替换为命题变元B，则A(B)仍为公理（定理）；（公理填充）等价替换原理：设命题公式A含有子公式C（C为命题公式），如果C├│D，那么将A中子公式C提换为命题公式D（不一定全部），所得公式B满足A├│B。
紧致性：设∑为FSPC上的公式集合，A为FSPC的公式。
如果∑├A，则存在∑的有限子集∑0使得∑0├A。
已知：A→(B→C), B证明：A→C公理推演：A→(B→C)AB→CBC自然推演：f(B)=1,f(A)=0或者f(B→C)=1。
假设f(A)=0;则f(A→C)=1.假设f(A)=1,那么f(B→C)=1.f(B)=1,则f(C)=1.因此，f(A→C)=1.由此，命题成立。
给出一个形式系统，其公理定义如下：{A, (,), →,}{}{---}给出公理如下：A→AA →A →A(A →A)→(A →A)(A →A)→(A →A)(A-->A-->A)-->(A-->A)下列哪些是定理？A →A →(A →A)(A →A)→(A →A)→(A →A)(A →A →A)→(A →A →A)(A →B)→(A →B)→(A →B)语义构成结构：（有两个主要部分构成）*确定研究对象集合，论域或个体域*把形式系统中的变量到论域中的一组规则映射规则域值：指一组给公式赋值的规则根据这项规则将 －Atomic →Value 中语义的特殊公式1) 公式A 为永真式，重言式tautologies ，如果对一切赋值v ，1=VA . 2) 公式A 为永假式，矛盾式contradictions,如果对一切赋值v ，0=VA 3) A ，B 为逻辑等价的，如果对于一切赋值v ，VV B A =，记做A ╞B(A |=|B ) 4) 公式A 为可满足的，如果至少存在一个赋值v ，1=VA逻辑推论：设∑是一个FSPC 上的公式集合，A 是FSPC 上的任一公式。
A 为∑的逻辑结果，记做∑|=A ，当且仅当对任何赋值映射v ，如果v ∑＝1时，则1=v A 。
|=读作逻辑蕴涵。
逻辑等价：设公式A 和公式B 分别为FSPC 上的两个公式。
A 和B 为逻辑等价的，记做A|=|B 当且仅当A|=B 和B|=A 同时成立。
永真式：如果A 为永真式，则公式集合∑为空集，即|=A 。
演绎定理：设∑为FSPC 的公式集合，A 和B 分别为FSPC 上的公式。
∑|=B A →成立的充分必要条件是：A ,∑|=B 。
证明：从语义上：必要性：由于f1(∑)=1，则f1(A →B)=1;由于f1(A →B)=1,并且f1(A)=1，则f(B)=1充分性：对于映射f ，若f(∑)=1，假设f1(A)=0;f1(A →B)=1.假设f1(A)=1, 由于已知条件可以知道f(B)=1.因此，f(A →B)=1从形式上：必要性：v ∑＝1成立，则1)(=→v B A 成立。
对于1)(=→v B A 成立有两种情况，为了证明A ,∑╞B 成立，只需考虑，使v A ＝1的情况。
如果赋值映射v ，满足v ∑＝1，v A ＝1且1)(=→v B A ，则有v B ＝1。
因此，A ,∑╞B 成立。
充分性：任取赋值映射v ，满足1=∑v，则有：当v A ＝0时，,1)(=→v B A 有∑╞B A → 当v A ＝1时，由已知v B ＝1， 因此∑╞B A →联结词的完备集：联结词的集合为完备的，当且仅当对于其他的联结词都可以由这个联结词的集合中的元素来表示。
FSPC 中的完备集：},,{∨∧⌝、},{→⌝、},{↔⌝、},{∨⌝、},{∧⌝等。
如果引入异或，那么异或与⌝也构成一个完备集合。
形式化系统→语义结构→元理论→自动化语法构成语法构成研究形式系统语言构成规律。
主要研究推演（重写）规律；主要规律：（1）独立性：如果形式系统中每一个公理都是独立的，即把任一公里A 从形式系统中删除后，所得形式系统FS ˊ不满足├FS ′A （即A 不是FS ˊ的定理），则称形式系统为独立的；● 独立形式系统是简洁的；（2）一致性：形式系统FS 称为一致性，或相容的（consistent ）如果不存在FS 的公⌝同时成立；式A，使得├A，├A●所有形式系统都应该是一致的；（3）完全性：形式系统为完全的，如果对形式系统中任意公式A，或者├A成立，或者⌝成立；├A●完全性的形式系统，一切都是可知的；因此，几乎没有价值；（4）可判定性：形式系统FS称为可判定的，如果存在一个算法，对FS对的任一公式A，可确定├A是否成立，否则称FS是可判定的；如果上述算法对定理能作出判断，而对于非定理未必终止（作判断），称FS为半可判定的；●FS为可判定的，当且仅当定理集合为递归集；（5）公式集合一致性：称形式系统的公式集合Γ为一致的，如果形式系统是一致的，⌝同时成立。
且不存在公式A使Γ，├A ，├A语法和语义关系合理性（soundness）：称形式系统FS是合理的，FS的任意公式A有：├FS A，则|=M A，M为所有结构；完备性（Completeness）：称形式系统FS是完备的，如果对FS的任意公式A有：若|=M A，则├FS A，这里M为FS所讨论的一类结构；紧致性：称形式系FS是紧致的，如果对FS的任意公式集∑有：如果公式集∑的所有穷子集是可满足的，那么公式集∑也是可满足的；合理性证明：已知：A是定理求证：A是永真的由于A是定理，存在一个证明序列A1,A2,……An=A。
N=1时：A1=A。
由于A1或者为公理或者是前边的公式通过推理规则得到。
因此，A1是公理，也就是A是公理。
对于任意的赋值映射f，则f(A)=1。
假设：n<m时，命题成立：A是定理则A是永真的。
证明：当n=m时，命题成立。
A1,A2,……Am-1, Am=A v1, Am是公理：公理是永真的，因此命题成立。
2, Am是前边通过推理规则得到的。
推理分离规则，三段论。
假设Am是由Ai和Aj通过分离规则得到。
由于归纳假设，Ai和Aj都是永真的。
由于推理规则保真性，那么Am是永真的。
因此，命题成立。
自由变元：自由变元是真正的变元，可以将个体域中的任意个体代入到自由变元中。
类似于数学中的变元。
约束变元：约束变元并不是实际意义的变元（数学意义上的变元）。
约束变元是为表达某种想的辅助符号。
自由变元约束变元可代入不可代入不可改名可改名量词中的变元成为指导变元，指导 4变元是约束变元改名原理：在FSFC 中，称公式A ´为公式A 的改名式，如果将A 中至少一个量词的指导变元和相应的约束变元（如果有）都改为另一个相同名字的变元后得到的公式A ’。
在FSFC 中，如果A ’为公式A 的改命式，且A ’改用的变元在A 中无任何出现，那么A ├│A ’。
量词规则全称（∀）消去规则：如果∑├)(x xA ∀，且项t 对于公式)(x A 为可代入的，则∑├)(t A 。
全称（∀）引入规则：如果∑├)(t A ，t 不在∑中出现，则∑├)(x xA ∀。
存在（∃）销去规则：设∑为FSFC 的任意公式集合，A, B 为公式。
变元x 在∑和公式B 中无出现。
如果∑├)(x xA ∃，A ,∑├B 则∑├B 。
存在（∃）引入规则：设∑为FSFC 的任意公式集合，B 为公式。
变元x 在∑和公式B 中无出现。
如果∑├B ，则∑├)(x xB ∃。
形式语义基本概念1、 指称语义：语义是由语义结构和以及在这种结构下公式赋真值的规定构成的。