LA1-1: 逻辑与证明补遗
no comments
Preview 01
问题一:什么是命题逻辑?与命题表达式真假有关的判断。
问题二:如何判定命题可满足?真值表与逻辑等价,范式与主范式。
逻辑
什么是逻辑?
- 形式化:研究某个形式语言的有效推理。如某个数学定理是否成立。
- 非形式化:研究自然语言中的论证。
逻辑的作用:逻辑用来做分析与论证,引导人们通过推理获得事物的本质,逻辑让描述变得严谨、无歧义。
命题
命题(proposition)一般采用如下解释:主要是指一些字或其他符号组合成的一种形式,这种形式所表达的为真或为假。(from 罗素)
命题指可以判断真假的陈述句。
命题变元:代表命题的变量,常用小写字母表示,取值范围为 ,显然 T 和 F 分别代表真(true)和假(false)。
原子命题和复合命题。复合命题是否为真取决于作为复合成分的子命题的真假和连词的语义。无法拆分的命题即原子命题。
一些连接词如下:
- 否定连接词:. 取值翻转。
- 合取连接词:. 为真当且仅当均为真。
- 析取连接词:. 为假当且仅当均为假。
- 蕴含连接词:. 为真当且仅当前假或后真。
- 双蕴含连接词:. 为真当且仅当同真同假。
真值表,如下由若干原子命题和复合命题取值构成的表格:
| F | F | T |
| T | F | F |
| F | T | T |
| T | T | T |
命题表达式(命题逻辑公式),递归定义如下:
- 命题变元是命题表达式。
- 若 是,则 是。
- 若 均是,则 均是。
- 只有有限次应用上述规则形成的符号串才是命题表达式。
- 运算符优先级:否定,合取,析取,蕴含,双蕴含。
将自然语言翻译成命题表达式。逻辑谜题。
命题表达式的真值确定:使得表达式为真的一种对式中命题变元的赋值称为该表达式的一种「成真指派」。真值表给出了该命题表达式的「所有指派」。
-
永真式(重言式):所有指派均为成真指派。
-
矛盾式:所有指派均为成假指派。
-
可能是:同时存在成真指派和成假指派。
逻辑等价
逻辑等价:再所有可能情况下两表达式 具有相同的真值,也就是 是永真式,记作 .
常用的逻辑等价:
-
双重否定律:.
-
幂等律:.
-
交换律:.
-
结合律:.
-
分配律:.
-
德摩根律:.
-
吸收律:.
-
支配律:.
-
恒等律:.
-
排中律(否定律之一):.
-
矛盾律(否定律之一):.
-
一些等价:.
-
假言易位:.
-
归谬论:.
逻辑等价的判定:通过上述逻辑等价变形式子。
通过逻辑等价进行推理。
命题的可满足性:一个复合命题是可满足的,则存在一个对其变元的赋值使其为真。Boolean satisfiability problem 即 SAT 问题,至今无高效的多项式算法能解决。
数独(Sudoku)也属于一种可满足性问题。
范式
命题表达式的范式:
-
命题变元或其否定称为文字。
-
有限个文字的析取式/合取式称为简单析取式/简单合取式。
-
由有限个简单合取式/简单析取式构成的析取式/合取式称为析取范式(DNF, disjunctive normal form)/合取范式(CNF, conjunctive normal form)。
-
一个文字既是一个析取范式,也是一个合取范式。
-
一个 DNF 为矛盾式当且仅当其每个简单析取式都是矛盾式;一个 CNF 是永真式,当且仅当其每个简单析取式都是永真式。
-
析取范式/合取范式的存在性:任一命题都存在着与之等价的析取范式与合取范式,但并不唯一。
-
主析取范式/主合取范式的唯一性:任一命题公式的主析取范式/主合取范式存在且唯一。
-
包含所有命题变元或其否定一次且仅一次的简单合取式/简单析取式称为极小项/极大项。
-
由有限个极小项/极大项组成的析取范式/合取范式称为主析取范式/主合取范式。
命题逻辑
命题逻辑就是涉及命题的逻辑领域。命题逻辑是逻辑学的一个分支,也被称为命题演算、句子演算、句子逻辑,有时也称为零阶逻辑。它涉及命题(真或假)和命题之间的关系,包括基于它们的论证的构建。
与一阶逻辑不同,命题逻辑不处理非逻辑对象、以及关于它们的谓词或量词。然而,命题逻辑的所有机制否包含在一阶逻辑和高阶逻辑中。从这个意义上说,命题逻辑是一阶逻辑和告诫逻辑的基础。
命题逻辑是一个形式系统,有可以由以逻辑运算符结合原子命题来代表「命题」的公式,以及允许某些公式建构成「定理」的一套形式「证明规则」。
Preview 02
问题一:如何基于命题逻辑进行推理?蕴含永真式与推理规则。
问题二:什么是(一阶)谓词逻辑?命题逻辑+谓词+量词;逻辑表达式。
问题三:如何基于谓词逻辑进行推理?命题逻辑的推理+全称/存在的例示/生成。
推理规则
- 前提:一组命题公式 .
- 结论:一个命题公式 .
- 「推理正确」当且仅当 为永真式。
此时 称为一个有效结论。对 中出现的命题变元的任一指派,若前提的合取式为真,则结论比为真。若前提的合取式为假,虽推理总是正确,但结论不一定正确。
常用的蕴含永真式导出的推理规则如下(请注意 则表明 是一个永真式,反之亦然):
- 附加律:.
- 化简律:.
- 假言推理:.
- 取拒式:.
- 析取三段论:.
- 假言三段论:.
- 等价三段论:.
- 构造性二难:. 特例:.
- 破坏性二难:.
论证。论证形式。
有效论证:从前提为真除法,推出结论为真的论证过程是一个表达式序列,该序列最后一个表达式应是要证明的结论,而其他任一表达式满足如下条件:
- 可为任一永真式。
- 可为前提中任一表达式。
- 可为序列中前面的任一表达式通过应用「替换规则」得到的表达式(适用于谓词逻辑)。
- 可谓前提中任一或若干表达式应用推理规则得到的新表达式。
用推理规则建立论证。
谓词(predicate)与量词(quantifier)
谓词: 可视为关于 的一个属性的取值,其值域是 .
量词:分为全称量词和存在量词:
- ,表示「对所有的 ,」,其中 是全称量词。
- ,表示「存在某个 ,」,其中 是存在量词。
量词必须指定论域。当论域元素可以一一列出式,量词(谓词公式)可以转化为命题公式的合取范式、析取范式。量词的优先级高于其他逻辑运算符。
量词的作用域。量化表达式中的变元:绑定、自由、作用域、替换。
量化表达式的逻辑等价:与逻辑表达式的逻辑等价类似,都有相同的真值而无论变量设定的论域和谓词的代入。e.g. .
量化表达式的否定式:.
嵌套量词:,但注意 和 不一定等价。
将自然语言翻译成逻辑表达式。
量化表达式的推理规则
- 全称例示:.
- 全称生成: for all .
- 存在例示: for some .
- 存在生成:for some .
用推理规则建立论证。
逻辑系统
逻辑系统具有下列性质:
- 有效性(validity):依系统的推理规则,若所有前提皆为真则结论必为真。
- 相容性(consistency):系统中任一定理都不与其他定理相矛盾。不存在命题 使得 和 皆可在系统中证明。
- 可靠性/正确性(soundness):系统中所有定理(有效且可证明的命题)均为真。和完备性互为逆命题。
- 完备性(completeness):系统中不存在无法证明或证否的有效命题。即系统中真命题皆可证明,称为定理,且假命题均可证否。
哥德尔证明了没有标准的算术形式系统可以同时满足相容性和完备性。
哥德尔不完备性第一定理:任意一个包含一阶谓词逻辑与初等数论的形式系统,都存在一个命题,其在这个系统中既不可证明为真,也不可证明为假。
语义蕴含(semantic entailment)
- 给定前提 ,结论 成立。
- .
- .
对于命题逻辑与一阶谓词逻辑而言,自然演绎规则是正确的,完备的,也即:
即基于自然演绎规则的推导和基于真值表的语义蕴含等价,这便是完备性。
哥德尔证明了任何一个假定得能作为数学基础的公理集都不可避免的不完备(即有相容性就无完备性)。
可判定性:是指存在一种算法能够在有限时间内对特定问题给出明确的是或否的判定结果。
- 命题逻辑是可判定的(decidable)。
- 一阶谓词逻辑是不可判定的(undecidable)。
- 经典的不可判定问题:停机问题:判断任意一个程序是否能在有限时间内结束运行。假设存在这样的判定程序
halt(),那么定义g()如下:
def g():
if halt(g):
loop_forever()
如果 halt(g) 停止则 g() 死循环,如果 halt(g) 死循环则 g() 停止,从而导出矛盾。
Preview 03
问题一:什么叫证明?表明定理为真的有效论证(演绎推理)。
问题二:常见的证明方法有哪些?见下文。
问题三:什么是猜想?有哪些有意思的猜想?尚未被证明的可能为真的陈述,见下文。
定理与证明
定理(theorem):能够被证明为真的陈述,通常比较重要。
证明(proof):表明陈述(定理)为真的有效论证。
定理证明中可以使用的陈述:
- 公理(不证自明的基本事实)。
- (当前)定理的前提。
- 已经证明的定理(推论、命题、引理)。
证明的本质是保证真实性,其涵义根据领域的不同有所差异。科学中的「证明」指利用「归纳推理」(inductive reasoning)去「证实」(prove)某个「假设」(hypothesis)。人们将大量特殊的信息收集(归纳)起来并根据自身的知识和经验去观察,并推断(推理)哪些是真实的。此类「证明」不产生「定论」(mathematical certainty)。
数学中的「证明」指利用「演绎推理」(deductive reasoning)和逻辑规则去推证某个命题。数学证明中每一步推理过程都根据某些「前提条件」(premise)展示出一个结论,称为逻辑推论。所有的证明过程必须是「严密的」(rigorous),每一步都必须提供确信的证据来支持中间结论,最终结论称为系统中的「定理」(theorem)。
用于数学的证明方式称为「形式化证明」或「推导」(derivation)。
定义(形式化证明):对一个命题的基于公理化系统的一系列逻辑演绎的有限过程。
证明方法
直接证明法:假设前提为真,得到结论为真。
间接证明法:证明逆否命题为真。
空证明法(前件假证明法):证明前提为矛盾式。
平凡证明法(后件真证明法):证明结论为永真式。
归谬法(反证法):证明前提且结论的否定为矛盾式。
广义归谬法:前提为多个命题的归谬法。
穷举法(分情形证明):前提为若干命题的或,分别证明。
等价性证明:,转而证明 .
存在性证明:对于 ,使用构造性证明找到一个 ;使用非构造性证明说明满足条件的 存在。
唯一性证明:证明唯一性。
构造性证明法。
反例法(命题为假的证明)。
证明中的错误。
猜想
猜想:被认为是真的(有意思的)陈述,还未证明其真假。
- 被证明为真:定理。包括庞加莱猜想、四色猜想、费马最后猜想。
- 被证明为假:推翻。费马数都是素数,假。
- 被证明为不可证明:连续统假设,其在集合论公理系统内不可证明/证伪。
费马大定理(费马最后猜想): 对于正整数 没有正整数解。由 Pierre de Fermat (1601-1665, France) 于 1637 年提出,最终由 Andrew Wiles (1953- , England) 于 1994/1995 年完成证明。
哥德巴赫猜想:任一大于 5 的整数都可写成三个质数之和(Goldbach Conjecture,1742 年提出),等价于欧拉表述的版本:任一大于 2 的偶数都可写成三个质数之和。弱化版本的「a+b 猜想」为:任一充分大的偶数都可表为一个素因子个数不超过 的数和另一个素因子不超过 的数之和。1966 年陈景润(1933-1996, China)证明了「1+2 猜想」。
四色定理(四色猜想):1852 年由 Francis Guthrie 提出,平面图均为 4 色可染。1890 年 Percy John Heawood (1861-1955, Britain) 证明五色猜想。1976 年 Kenneth Ira Appel (1932- , New York) 和 Wolfgang Haken (1928- , Berlin) 证明了四色定理。
世界数学难题:
- 希尔伯特二十三问:Hilbert’s problems (23), ICM’1900, Paris. 由希尔伯特在 1900 年在巴黎的 ICM 大会上提出。
- 七个千禧年问题:Millennium Prize Problems (7) by the Clay Mathematics Institute in 2000. 由克雷数学研究所在 2000 年提出。
七个千禧年问题包括:
- P 对 NP 问题。P versus NP problem.
- 霍奇猜想。Hodge conjecture.
- 庞加莱猜想。Poincaré conjecture (solved by Perelman).
- 黎曼猜想。Riemann hypothesis.
- 杨米尔斯方程解的存在性与质量间隙问题。Yang-Mills existence and mass gap.
- 纳维斯托克斯方程解的存在性和光滑性问题。Navier-Stokes existence and smoothness.
- BSD 猜想。Birth and Swinnerton-Dyer conjecture.
其中庞加莱猜想于 2002 年 11 月由 Grigori Perelman (1966- , Russian) 证明。
【希尔伯特二十三问如下】:
- 连续统假设。已证明 ZF 公理体系下不可证明。
- 算术公理系统的无矛盾性。Godel 于 1931 年证明无法在系统内部证明,G. Gentaen 于 1936 年使用超限归纳法证明。
- 只根据合同公理证明等底等高的两个四面体体积相等。M. Dehn 于 1900 年给出反例证否。
- 两点间直线最短。Pogleov 于 1973 年在对称距离情况下证明。
- 连续群的解析性。Gleason、Montgomery、Zippin 于 1952 年共同证明。山迈英彦 1953 年独立证明。
- 物理学公理化(数学化)。尚未解决。
- 超越数理论。尚在探索。非零一的代数数的无理代数数次方是超越数,由 Gelfond 于 1929 年、Schneider、Siegel 于 1935 年分别独立证明。
- 素数分布问题,特别是黎曼猜想、哥德巴赫猜想、孪生素数猜想。尚在探索。
- 一般互反律在任意数域中的证明。高木贞治于 1921 年、E. Artin 于 1927 年独立证明。相关的类域理论尚在发展。
- 丢番图方程可解性的判定。Matiyasevich 于 1970 年证明一般情况下不存在。
- 一般代数数域内的二次型论。H. Hasse 于 1920s-1930s 的工作已解决。
- 阿贝尔域上的克罗内克定理在任意代数有理域上的推广。尚未解决。
- 一般七次代数方程以二变量连续函数之组合求解的不可能性。接近解决。
- 某些完备函数系的有限的证明。永田雅宜于 1959 年给出反例证伪。
- 舒伯特计数演算的严格基础。Grothendiek 等于 1960s 发展的理论解决。
- 代数曲线和曲面的拓扑研究。尚在探索。
- 半正定形式的平方和表示。E. Artin 于 1927 年解决。
- 全等多面体构造空间。Bieberbach 于 1910 年,Reinhart 于 1928 年的工作解决。
- 正则变分问题的解是否总为解析函数。Bernstein 于 1904 年、Petrowsky 于 1939 年、De Giorgi 与 Nash 于 1956-1957 年的工作彻底解决。
- 研究一般边值问题。已解决,相关理论高度发展
- 具有给定奇点和单值群的Fuchs类的线性微分方程解的存在性证明。Hilbert 于 1905 年、H. Rohrl 于 1957 年、Deligne 于 1970 年解决。
- 用自守函数将解析函数单值化。简单情况已解决,更深的理论尚在探索。
- 发展变分学方法的研究。已解决,相关理论高度发展。