离散数学基本概念-电大同步上课进度更新

比眉伴天荒 2022-10-24 13:19 1502阅读 0赞

### **集合论基础** ###

**基数：集合的元素个数  
归纳法：可用归纳法表示集合，要求-基础，归纳，有限性  
递归指定：知道通项公式an，集合为a1 a2...  
外延性定理：元素相等，集合相等  
集合相等：元素相等  
集合个数：共n个元素，取m个个数为cmn，取n个个数为2的n次方  
幂集：集合的所有不同子集  
补集：上面有一杠  
差集：A-B，属于A不属于B  
对称差集：A⊕B，A-B并B-A  
等势：两个集合一一对应  
可数集合：和自然数集一一对应  
阿列夫零：可数集合元素个数  
不可数集合：和（0，1）一一对应  
阿列夫：不可数集合元素个数**

### **命题逻辑** ###

**命题：具有明确真值的陈述句  
真值：真或假  
不是命题：悖论和非陈述句  
原子命题：不能拆的命题  
复合命题：可以拆的命题  
联结词：语文的关联词  
否定：乛非；**否定的优先级最高  
**合取：∧并且  
析取：V或者  
蕴含：→若则**

*  Q→P：只有P，才Q
 *  乛P→乛Q：除非P，否则Q
 *  P的真值-Q的真值-P→Q的真值
 *  1-0-0
 *  1-1-1
 *  0-0/1-1

**等价：←→当且仅当**；同1，异0  
  
一致：真值表中存在一行的复合命题全为1

**命题变元（变量）：值 1（真）或 0（假）的变元**

**命题公式(合式公式)：将命题变元用联结词或圆括号按一定逻辑关系联结起来的符号串**

**赋值：值 1（真）或 0（假）**

**成真赋值：值 1（真）**

**成假赋值：值0（假）**

**真值函数：F（P,Q,R）**

**公式的一个解释（I）：给原子命题赋真值；n个命题变元，![2^n][2_n]个解释**

**真值表：由各个命题变元，和命题公式的真假组成的表格(按二进制来写)**

**重言式或永真式：真值表都为1**

**矛盾式或永假式：真值表都为0**

**可满足式：真值表为1，也可为0**

**公式等价：任意解释，G和H真值相同，即G<-->H为永真式**

**自反：G=G**

**对称：G=H H=G**

**传递：G=H H=I G=I**

**证明![G\_\{1\}][G_1]和![G\_\{2\}][G_2]逻辑等价：![G\_\{1\}][G_1]<-->![G\_\{2\}][G_2]真值表为1**

**等值式：**![A\\leftrightarrow B][A_leftrightarrow B]![A\\leftrightarrow B][A_leftrightarrow B]![A \\leftrightarrow B][A _leftrightarrow B]**为重言式**

**24个基本公式：最重要（G->H）=(乛G![\\vee][vee]H)**

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70][]

**代入定理：G（P,Q）永真，![G\{\}'(H,S)][G_H_S]永真      H(P,Q)，S(P,Q)**

**替换定理：![G\_\{1\}][G_1]是G的子公式，![H\_\{1\}][H_1]是和![G\_\{1\}][G_1]相等的任意命题，G中凡是出现![G\_\{1\}][G_1]的地方替换![H\_\{1\}][H_1]，替换后为H，则G=H**

**开括号：括号外面和括号里面的运算符号一致可以消去括号，不一致可以分配律消去括号**

# 公式的标准型-范式 #

**文字：命题变元及其否定**

**析取式（子句）：有限个文字取V，儿子多，析出蛋白质多**

**合取式（短语）：有限个文字取![\\Lambda][Lambda]，合二为一少，短**

**互补对：P和非P**

**析取范式：有限个短语析取**

**合取范式：有限个子句合取**

**没有括号：即是析取也是合取**

**极小项：每个短语其本身和否定不同时存在且二者之一出现一次，并各个短语出现次序一致**

**极大项：每个子句其本身和否定不同时存在且二者之一出现一次，并各个子句出现次序一致**

**等价定理：所有命题都有与之等价的析取范式，合取范式，主析取范式，主合取范式**

**P,Q对应的极小值真值表：每个解释对应一个取值为真都的极小项；没有等价（所有解释对应的真值相同）的两个极小项；从左上到右下为1**

**编码m：二进制下标，十进制下标，从0开始，顺序为     ┐P![\\Lambda][Lambda]┐Q           ┐P![\\Lambda][Lambda]Q         P![\\Lambda][Lambda]┐Q      P![\\Lambda][Lambda]Q **

**P,Q对应的极大值真值表：每个解释对应一个取值为0都的极大项；没有等价（所有解释对应的真值相同）的两个极大项；从左下到右上为0**

**编码M：二进制下标，十进制下标，从0开始，顺序为     ┐PV┐Q           ┐PVQ         PV┐Q      PVQ **

**极小![\\Lambda][Lambda]极小=0        极大V极大=1**

**V全部极小=永真公式    ![\\Lambda][Lambda]全部极大=永假公式**

**主析取范式：有限个极小项短语析取，无极小为空**

**主合取范式：有限个极大项子句合取，无极大为空**

**求主范式：**

**1.公式转换法：通过24个公式将其变为满足要求的式子**

**缺少命题：Q=（PV┐P）![\\Lambda][Lambda]Q    Q=（P![\\Lambda][Lambda]┐P）VQ  ，再用分配律**

**多余命题：PV┐P   P![\\Lambda][Lambda]┐P来消去**

**2.真值表法：**

**主析取范式**：写出真值表和m和1的排列方向**从左上到右下为1，不看真值表为0的一行，其它析取**

**主合取范式：**写出真值表和M和0的排列方向**从左下到右上为0，不看真值表为1的一行，其它合取**

**3.互补规则：**

**转换成编码后下标互补，为0-![2^n-1][2_n-1](n****为命题变元个数)**

**主析取范式为mVmVm....**

**主合取范式为M![\\Lambda][Lambda]M![\\Lambda][Lambda]M...**

**概念：描述问题的句子**

**判断：对概念的肯定与否定的判断**

**推理：从一个或多个前提推出结论的思维过程**

**推理有效：它的结论是它前提的合乎逻辑的结果，前提都为真，那么所得的结论也必然为真**

**蕴涵，逻辑结果：设G,H是公式，对任意解释I，如果I满足G，那么I满足H，则称H是G的逻辑结果(或称G蕴涵H),记为G![\\Rightarrow][Rightarrow]Ｈ，此时称G为前提，H为结论**

**永真定理：设G,H是公式，H是G的逻辑结果当且仅当G→Ｈ为永真公式**

**有效的：G1∧G2∧…∧Gn![\\Rightarrow][Rightarrow]Ｈ**

**一组前提：Г=\{G1,G2,…,Gn\}**

**永真定理推广：公式H是前提集合Г=\{G1,G2,…,Gn\}的逻辑结果当且仅当G1∧G2∧…∧Gn→Ｈ为永真公式。**

**“![\\Rightarrow][Rightarrow]”与“→”的不同：“→”仅是一般的蕴涵联结词，G→H的结果仍是一个公式，而“![\\Rightarrow][Rightarrow]”却描述了两个公式G，H之间的一种逻辑蕴涵关系，G ![\\Rightarrow][Rightarrow] H的“结果”，是非命题公式；用计算机来判断G Þ H是办不到的。然而计算机却可“计算”公式G→H是否为永真公式**

**判断有效结论的常用方法 ：G1∧G2∧…∧Gn→Ｈ为永真公式，真值表技术、演绎法和间接证明方法**

**真值表技术：取出所有G中的所有命题变元P，列包含P和G和H真值表，要求H为假时，至少一个G为假**

**推理定律：设G，H，I，J是任意的命题公式，则有：（小可推大）**

**G∧H![\\Rightarrow][Rightarrow]G　　　　　　(简化规则)**

**G∧H![\\Rightarrow][Rightarrow]H**

**G![\\Rightarrow][Rightarrow]G∨H　　　　　　(添加规则)**

**H![\\Rightarrow][Rightarrow]G∨H**

**┐G![\\Rightarrow][Rightarrow]G→H         =┐G∨H**

**H![\\Rightarrow][Rightarrow]G→H           =┐G∨H**

**┐(G→H)![\\Rightarrow][Rightarrow]G      ┐(G→H)=G∧ ┐H**

**┐(G→H)![\\Rightarrow][Rightarrow]┐H    ┐(G→H)=G∧ ┐H**

**G，H![\\Rightarrow][Rightarrow]G∧H**

**┐****G****，****G∨H****![\\Rightarrow][Rightarrow]****H**  **(****选言三段论)**  
**┐G，G  H****![\\Rightarrow][Rightarrow]****H**

**G****，****G→H****![\\Rightarrow][Rightarrow]****H**  **(****分离规则)**

**┐****H****，****G→H****![\\Rightarrow][Rightarrow]****┐G**  **(****否定后件式)**

**G→H****，****H→I****![\\Rightarrow][Rightarrow]****G→I**  **(****假言三段论)**

**G∨H****，****G→I****，****H→I****![\\Rightarrow][Rightarrow]****I**  **(****二难推论)**

**演绎法:****是从前提****(****假设****)****出发，依据公认的推理规则和推理定律，推导出一个结论来**

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 1][]

**推理规则**

*  ①**规则P（称为前提引用规则）：在推导的过程中，可随时引入前提集合中的任意一个前提；**
 *  ②**规则T（逻辑结果引用规则）：在推导的过程中，可以随时引入公式S，该公式S是由其前的一个或多个公式推导出来的逻辑结果。**
 *  ③**规则CP（附加前提规则）：如果能从给定的前提集合Г与公式P推导出S，则能从此前提集合Г推导出P→S。** P→(Ｑ→Ｒ)＝(P∧Ｑ)→Ｒ，P**![\\Rightarrow][Rightarrow]**(Ｑ→Ｒ)等价于(P∧Ｑ)**![\\Rightarrow][Rightarrow]**Ｒ

**例子：设前提Г=\{P∨Q，P![\\leftrightarrow][leftrightarrow]R，Q→S\}，G=S∨R。证明Г![\\Rightarrow][Rightarrow]G**

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 2][]![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 3][]

**例子：设Г=\{P→(Q→S)，┐R∨P，Q\}，G=R→S。证明：Г![\\Rightarrow][Rightarrow]G。**

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 4][]

**间接证明法（反证法） ：P![\\Rightarrow][Rightarrow]Q等价于┐Q![\\Rightarrow][Rightarrow]┐P，因此，为了间接地证明P![\\Rightarrow][Rightarrow]Q，可以假设Q为假(┐Q)，然后证明P为假(┐P)。**

**一致的，相容的：假设G1,G2,…,Gn是一组命题公式，P1,P2,…,Pn是出现在中的一切命题变元，若有解释I使G1∧G2∧…∧Gn取值为“真”，则称公式G1,G2,…,Gn是一致的，或者说是相容的。**

**矛盾式：G1∧G2∧…∧Gn是矛盾式当且仅当G1∧G2∧…∧Gn![\\Rightarrow][Rightarrow]Ｒ∧┐Ｒ，其中，R可为任意公式，R∧┐R为一矛盾式**

**将结论的否定加入到前提集合中构成一组新的前提，然后证明这组新的前提集合是不相容的，即蕴涵一个矛盾式。G1,G2,…,Gn,┐H![\\Rightarrow][Rightarrow] R∧┐R**

# **第四章 谓词逻辑** #

### **为什么要有****谓词逻辑？** ###

**命题逻辑能够解决的问题是有局限性的。只能进行命题间关系的推理，无法解决与命题的结构和成分有关的推理问题。**

### **谓词逻辑的目录** ###

**谓词逻辑中的基本概念**

**谓词的翻译原理**

**谓词的合式公式**

**谓词的标准型-范式**

**谓词逻辑的推理理论**

## **谓词逻辑中的基本概念** ##

**目录**

重点掌握

1 谓词逻辑符号化及真值

2 谓词公式的有效性和基本等价公式

3 掌握谓词逻辑的推理规则和公理

一般掌握

1 谓词公式的解释和真值

2 自由变元和约束变元

了解

前束范式与SKOLEM范式

### **谓词逻辑中的基本概念与表示** ###

**命题是具有真假意义的陈述句，从语法上分析，一个陈述句由****主语和谓语****两部分组成。**

### **个体词与谓词** ###

**在原子命题中，可以独立存在的客体（句子中的主语、宾语等），称为****个体词****(****Individual)****。而用以刻划客体的性质或客体之间的关系即是****谓词****(Predicate)****。**

1.**表示****具体的或特定****的个体词称为****个体常量****(Individual Constant)****，一般个体词常量用带或不带下标的小写英文字母****a, b, c****，****…****，****a****1****, b****1****, c****1****,****…****等表示；**

2.**表示****抽象的或泛指****的个体词称为****个体变量****(Individual Variable)****，一般用带或不带下标的小写英文字母****x, y, z,** **…****, x****1****, y****1****, z****1****,** **…****等表示。**

### **个体域** ###

*  ### **个体词的取值范围****称为****个体域****(****或****论域****) (Individual Field)****，常用****D****表示；** ###
 *  ### **宇宙间的所有个体域聚集****在一起所构成的个体域称为****全总个体域****(Universal Individual Field)****。** ###

### **n****元谓词** ###

**设D为非空的个体域，定义在Dn上取值于\{0,1\}上的n元函数，****称为n元命题函数或n元谓词**

**记为P(x1, x2, …, xn)。此时，个体变量x1, x2, …, xn的定义域都为D，P(x1, x2, …, xn)的值域为\{0, 1｝**

### **结论** ###

*  **谓词中****个体词的顺序是十分重要****的，不能随意变更。如命题****F(b, c)****为****“****真****”****，但命题****F(c, b)****为****“****假****”****；**
 *  **一元谓词****用以描述****某一个个体的某种特性****，而****n****元谓词****则用以描述****n****个个体之间的关系****。**
 *  **0****元谓词****(****不含个体词的****)****实际上就是一般的命题；**
 *  **具体命题的谓词表示形式****S(a)****有真值****和****n元命题函数****S(x)****却没有真值**
 *  **一个****n****元谓词不是一个命题****，但****将****n****元谓词中的个体变元都用个体域中具体的个体取代****后，就****成为一个命题****，有真值**

### 量词：任意，存在 ###

（1）对于全称量词(![\\forall][forall]x)，刻划其对应个体域的特性谓词作为**蕴涵式**之前件加入。

**所有的****老虎都要吃人；**

**解：设P(x)：x会吃人，U(x)：x是老虎,**

**则有：(**![\\forall][forall]**x)(U(x)→P(x))**

（2）对于存在量词(![\\exists][exists]x)，刻划其对应个体域的特性谓词作为**合取式**之合取项加入。

**有一些****人登上过月球**

**解：设S(x)：x登上过月球，R(x)：x是人,**

**则有：(**![\\exists][exists]**x)(S(x)∧R(x))**

## **谓词的翻译原理** ##

### **谓词的语言翻译** ###

**(**![\\forall][forall]**x)G(x)=G(x0)∧G(x1)∧...∧G(xn)**

**     (**![\\exists][exists]**x)G(x)=G(x0)∨G(x1)∨...∨G(xn)**

### **符号化下面一组语句** ###

**所有蜂鸟都五彩斑斓；没有大鸟以蜜为生；不以蜜为生的鸟都色彩单调；蜂鸟都是小鸟畅。**

**解****：设****P(x):x****是蜂鸟；****Q(x):x****是大鸟；****R(x)****：****x****是以蜜为生的鸟；****S(x)****：** **x****五彩斑斓。****假定所有鸟的集合为论域，则上述语句可符号化为****:**

**(****![\\forall][forall]****x)(P(x)→S(x))；** **(**![\\exists][exists]**x) (Q(x)∧****R(x))****；**

**(****![\\forall][forall]****x)(****┐****R(x)→** **┐****S(x))****；**  **(****![\\forall][forall]****x)(P(x)→** **┐****Q(x))**

## **谓词的合式公式** ##

**（****1****）****常量符号****：用带或不带下标的****小写英文字母****a, b, c,** **…****, a****1****, b****1****, c****1****,** **…****来表示。当个体域名称集合****D****给出时，它可以是****D****中的某个元素****；**

**（****2****）****变量符号****：用带或不带下标的****小写英文字母****x, y, z, ..., x****1****, y****1****, z****1****,...****来表示。当个体域名称集合****D****给出时，它可以是****D****中的任意元素****；**

**（****3****）****函数符号****：用带或不带下标的****小写英文字母****f, g, h, ..., f****1****, g****1****, h****1****, ...****来表示。当个体域名称集合****D****给出时，****n****元函数符号****f(x****1****, x****2****,** **…****,** **x****n****)****可以是****D****n****→D****的任意一个函数；**

**（****4****）****谓词符号****：用带或不带下标的****大写英文字母****P, Q, R,..., P****1****, Q****1****, R****1****...****来表示。当个体域名称集合****D****给出时，****n****元谓词符号****P(x****1****, x****2****,** **…****,** **x****n****)****可以是****D****n****→\{0****，****1\}****的任意一个谓词。**

### **项** ###

（1）任意的常量符号或任意的变量符号是项；

（2）若f(x1, x2, …, xn)是n 元函数符号，t1,t2,…,tn是项，则f(t1, t2, …, tn)是项；

（3）仅由有限次使用(1)，(2)产生的符号串才是项。

若P(x1,x2,…,xn)是n 元谓词，t1，t2，…，tn是项，则称P(t1,t2,…,tn)为**原子谓词公式**，简称**原子公式**。

### **量词辖域** ###

**   （1）若量词后有括号，则括号内的子公式就是该量词的辖域；**

**   （2）若量词后无括号，则与量词邻接的子公式为该量词的辖域。**

### **合式公式** ###

**（****1****）****原子公式****是合式公式；**

**（****2****）若****G****，****H****是合式公式，则****(****┐****G)****、****(****┐****H)****、****(G∨H)****、****(G∧H)****、****(G→H)****、****(G****«****H)****也是合式公式；**

**（****3****）若****G****是合式公式，****x****是个体变量，则** **(**![\\forall][forall]**x)****G****、(**![\\exists][exists]**x)G** **也是合式公式；**

**（****4****）仅仅由****(1)-(3)****产生的表达式才是合式公式。**

**例如**

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 5][]

### **自由变元和约束变元** ###

**给定一个合适公式****G****，若变元****x****出现在使用变元的量词的辖域之内，则称变元****x****的出现为****约束出现****，此时的变元****x****称为****约束变元**

**若****x****的出现不是约束出现，则称它为****自由出现****，此时的变元****x** **称为****自由变元**

### **两个规则** ###

**约束变元的改名规则****：对公式的一个子公式施行**

**自由变元的代入规则：****对整个公式施行**

**例子**

**（****1****）将公式(**![\\forall][forall]**x)(P(x)→Q(x, y))∧R(x, y)中的约束变元****x****进行改名；**

**(****![\\forall][forall]****z)(P(z)→Q(z, y))∧R(x, y)**

**（****2****）将公式(**![\\forall][forall]**x)(P(x)→Q(x, y))∧R(x, y)中的自由变元****y****进行代入。**

**  (![\\forall][forall]x)(P(x)→Q(x, z))∧R(x, z)**

### **闭式** ###

**设****G****是任意一个公式，若****G****中无自由出现的个体变元，则称****G****为****封闭的合适公式****，简称****闭式****。****闭式一定是命题。**

**例如(****![\\forall][forall]****x)(P(x)→(**![\\exists][exists]**y)R(x, y))****是一个闭式。**

### **谓词合式公式的解释** ###

**谓词逻辑中公式****G** **的每一个****解释****I(explanation)****由如下四部分组成：**

** （****1****）****非空的个体域****集合****D** **；**

** （****2****）****G** **中的每个****常量符号****，指定****D** **中的某个特定的元素；**

** （****3****）****G** **中的每个****n** **元****函数符号****，指定****D****n****到****D****中的某个特定的函数；**

** （****4****）****G** **中的每个****n** **元****谓词符号****，指定****D****n****到｛****0, 1****｝中的某个特定的谓词。**

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 6][]

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 7][]

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 8][]

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 9][]

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 10][]

**有效****公式****，****所有的解释****I****下都取值为****“****真****”**

**矛盾****公式****，****所有的解释****I****下都取值为****“****假****”**

**可满足****公式****，****至少有一种解释****I****使得****G****取值为****“****真****”**

### **谓词演算中的有效公式**  ###

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 11][]

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 12][]

![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 13][]

## ![watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 14][] ##

# #

## **谓词的标准型-范式** ##

## **谓词逻辑的推理理论** ##

to be continue2021.3.24

[2_n]: https://private.codecogs.com/gif.latex?2%5En
[G_1]: https://private.codecogs.com/gif.latex?G_%7B1%7D
[G_2]: https://private.codecogs.com/gif.latex?G_%7B2%7D
[A_leftrightarrow B]: https://private.codecogs.com/gif.latex?A%5Cleftrightarrow%20B
[A _leftrightarrow B]: https://private.codecogs.com/gif.latex?A%20%5Cleftrightarrow%20B
[vee]: https://private.codecogs.com/gif.latex?%5Cvee
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70]: /images/20221024/b6a362459b4f413281d4223b6be4327a.png
[G_H_S]: https://private.codecogs.com/gif.latex?G%7B%7D%27%28H%2CS%29
[H_1]: https://private.codecogs.com/gif.latex?H_%7B1%7D
[Lambda]: https://private.codecogs.com/gif.latex?%5CLambda
[2_n-1]: https://private.codecogs.com/gif.latex?2%5En-1
[Rightarrow]: https://private.codecogs.com/gif.latex?%5CRightarrow
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 1]: /images/20221024/11334be02bc0429b88f8d52d860d0db0.png
[leftrightarrow]: https://private.codecogs.com/gif.latex?%5Cleftrightarrow
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 2]: https://img-blog.csdnimg.cn/20210315164247563.png?x-oss-process=image/watermark,type_ZmFuZ3poZW5naGVpdGk,shadow_10,text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY=,size_16,color_FFFFFF,t_70
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 3]: /images/20221024/fb2eb0a245ec4643b65fc926a4d83a81.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 4]: /images/20221024/991d4d2076dd4bde94cb07bb76d94e62.png
[forall]: https://private.codecogs.com/gif.latex?%5Cforall
[exists]: https://private.codecogs.com/gif.latex?%5Cexists
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 5]: /images/20221024/b6bb3a06094f455582518b5660443f2e.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 6]: /images/20221024/362b0ee0e74c472ca5b5c4a84d0d5d4d.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 7]: /images/20221024/22aa62dd8147437390554286b4391541.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 8]: /images/20221024/c82ef577be574a958d74e7701b061e6c.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 9]: /images/20221024/3ff4e9e5045f426abd06da3f988f7a04.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 10]: /images/20221024/03fbcca6759447fb9b2435a065b9fd64.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 11]: /images/20221024/7419e00952b241f1b336c054d2fa515d.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 12]: /images/20221024/d299a9d0f7dc45b9914c32817b443104.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 13]: /images/20221024/ebfd63a221354917961cec3d2bb93c86.png
[watermark_type_ZmFuZ3poZW5naGVpdGk_shadow_10_text_aHR0cHM6Ly9ibG9nLmNzZG4ubmV0L2FpcXExMzY_size_16_color_FFFFFF_t_70 14]: /images/20221024/4bd0adaebb294979aa8abd6dba899eaf.png