查看一阶逻辑的源代码
←
一阶逻辑
跳转至:
导航
、
搜索
因为以下原因,你没有权限编辑本页:
你刚才请求的操作只对属于该用户组的用户开放:
用户
您可以查看并复制此页面的源代码:
'''一阶逻辑''',是使用于[[数学]]、[[哲学]]、[[语言学]]及[[电脑科学]]中的一种[[形式系统]],也可以称为:'''一阶断言演算'''、'''低阶断言演算'''、'''量化理论'''或[[谓词逻辑]]。一阶逻辑和[[命题逻辑]]的不同之处在于,一阶逻辑包含[[量化 (数理逻辑)|量词]]。 [[高阶逻辑]]和一阶逻辑不同之处在于,高阶逻辑的断言符号可以有断言符号或函数符号当做引数,且容许断言量词或函数量词。在一阶逻辑的[[语义学|语义]]中,断言被解释为[[关系_(数学)|关系]]。而高阶逻辑的语义里,断言则会被解释为集合的集合。 在通常的语义下,一阶逻辑是[[可靠性定理|可靠]](所有可证的叙述皆为真)且[[完备性|完备]](所有为真的叙述皆可证)。虽然一阶逻辑的[[逻辑归结]]只是[[可判定性|半可判定性]]的,但还是有许多用于一阶逻辑上的[[自动定理证明]]。一阶逻辑也符合一些使其能通过[[证明论]]分析的[[元逻辑]]定理,如[[勒文海姆–斯科伦定理]]及[[紧致性定理]]。 一阶逻辑是[[数学基础]]中很重要的一部份。许多常见的公理系统,如一阶[[皮亚诺公理]]、[[冯诺伊曼-博内斯-哥德尔集合论]]和[[策梅洛-弗兰克尔集合论]]都是一阶理论。然而一阶逻辑不能控制其无穷模型的基数大小,因根据[[勒文海姆–斯科伦定理]]和[[康托尔定理]],可以构造出一种"病态"集合论模型,使整个模型可数,但模型内却会觉得自己有“不可数集”。类似地,可以证明实数系的普通一阶理论既有可数模型又有不可数模型。这类的悖论被称为[[斯科伦悖论]]。但一阶的[[直觉主义逻辑]]里,勒文海姆–斯科伦定理不可证明,故不会有以上之现象。 === 简介 === 在命题逻辑里,“苏格拉底是哲学家”、“柏拉图是哲学家”只能简单标记为 ''p'' 及 ''q'' 。 而一阶逻辑先将符号 Phil(''x'') 解释为 “ ''x'' 是哲学家”,然后以 ''s'' 代表苏格拉底;''b'' 代表柏拉图,则 Phil(''s'') 对应到 ''p'' ; Phil(''b'') 对应到 ''q'' 。也就是赋予'''断言符号'''“Phil(''x'') ”'''语意的解释''',而这个解释预设一个“所有人类的群体”(也就是语义解释的[[论域]]),将变数 ''x'' 解释为自群体取出来的某人。 其实断言符号可以包含一个以上的变数,像是把 Cp(''x'',''y'') 解释为“''x''与''y''是夫妻”,这样 : Cp(''s'',''y'') 就解释成“苏格拉底和''y''是夫妻”。 一阶逻辑和命题逻辑相同,断言符号和变数还能与逻辑符号组成更复杂的叙述:如将断言符号 Schol(''x'') 解释为 ''x'' 为学者。则“若''x''为哲学家,则''x''为学者”可表示为 : Phil ( ''x'' ) ⇒ Schol ( ''x'' ) 而“对所有''x'',若''x''为哲学家,则''x''为学者”则记为 : ∀ ''x'' ( Phil ( ''x'' ) ⇒ Schol ( ''x'' ) ) 也就是自左方开始阅读,以 ∀ ''x'' 代表“对所有''x''”;将之理解为“对所有的''x'', ∀ ''x'' 右方的叙述为真。”而 ∀ ''x'' 这个符号称为 ''x'' 的[[全称量词]]。 直观上还会有“若所有''x''是哲学家,那''x''的长子也会是哲学家”这样"合理"的叙述,为此将 Son(''x'') 解释为 “''x''的长子”,那这段"合理"叙述可记为 : ∀ ''x'' Phil ( ''x'' ) ⇒ Phil [ Son ( ''x'' ) ] 这种解释为成与 ''x'' 有唯一对应的那个对象的符号,称为'''函数符号'''。而事实上这段直观为真的叙述,经过适当的扩展以后就是一阶逻辑其中的一条[[公理模式|公理]]。 而对于“有''x''是哲学家”,则引入另一种量词表记为: : ∃ ''x'' ( Phil ( ''x'' ) ) 自左方开始阅读,以 ∃ ''x'' 代表“存在''x''”;也就是解释为“有''x''使 ∃ ''x'' 右方的叙述为真”。而 ∃ ''x'' 被称为 ''x'' 的[[存在量化|存在量词]]。全称量词和存在量词一起被简称为'''量词'''。 而直观上,“并非所有''x''不是哲学家”,和“有''x''是哲学家”是等价的;且“不存在''x''不是学者”也跟“所有的''x''是学者”在直观上也是等价的。所以只要有“否定”这个逻辑概念,那一阶逻辑就能以[[全称量词]]为基础,作以下的符号定义( ¬ 解释为 “否定”, 而 ''A'' 代表一段"叙述"): : ∃ ''x'' ''A'' := ¬ [ ∀ ''x'' ( ¬ ''A'' ) ] 而将存在量词定义为全称量词的衍伸。 === 形式理论 === 一阶逻辑的[[形式理论]]可分成几个部份: #语法:决定哪些符号组合是[[合式公式]]。(直观上的"语法无误的叙述") #推理规则:由合式公式符号组合出新合式公式的规则(直观上的"推理") #公理:一套合式公式(直观上的基本假设) === 标准语义 === 一阶逻辑的标准[[形式语义学|语义]]源于波兰逻辑学家Alfred Tarski所著[[真理的语义理论|《''On the Concept of Truth in Formal Languages''》]]。根据上面[[一阶逻辑#语法|语法]]一节,公式是由原子公式递回地添加逻辑连结词而来的,而原子公式是由断言符号与项所构成的。所以要检验一条公式在特定的论域下正不正确,就要规定'''项的取值''',然后检验这样的取值会不会落在断言符号所对应的[[关系_(数学)|关系]]里。由此延伸出所有公式的"真假值"。 也就是一套一阶逻辑的语义解释,要包含 #变数取值的论域 #如何解释函数符号(为论域中的某个函数)与常数符号(为论域中的某特定元素),以便从特定的变数取值得出项的取值。 #如何将断言符号与论域里的某关系做对应。 通常一套解释方法(简称为'''解释''')会以代号 ''M'' 表示。 === 一阶逻辑的元定理 === 下面列出了一些重要的元逻辑定理。 #不像[[命题演算]],一阶逻辑是不可判定性的。对于任意的公式P,可以证实没有[[判定过程]],判定P是否有效,(参见[[停机问题]])。(结论独立的来自于[[阿隆佐·邱奇|邱奇]]和[[图灵]]。) # [[有效性]]的判定问题是半可判定的。按[[哥德尔完备性定理]]所展示的,对于任何'''有效的'''公式P, P是可证明的。 # [[一元断言逻辑]](就是说,断言只有一个参数的断言逻辑)是可判定的。 === 转换自然语言到一阶逻辑 === 用自然语言表达的概念必须在一阶逻辑(FOL)可以为为其效力之前必须被转换到FOL,而在这种转换中可能有一些潜在的缺陷。在FOL中,<math>p \lor q</math>意味着“要么p要么q要么二者”,就是说它是“包容性”的。在英语中,单词“or”有时是包容性的(比如,“加牛奶或糖?”),有时是排斥性的(比如,“喝咖啡或茶?”,通常意味着取其中一个或另一个但非二者)。类似的,英语单词“some”可以意味着“至少一个,可能全部”,有时意味着“不是全部,可能没有”。英语单词“and”有时要按“or”转换(比如,“男人和女人可以申请”)。 === 参见 === * [[真值表]] * [[逻辑等价]] * [[逻辑条件]] * [[逻辑与非]] * [[逻辑或非]] * [[数理逻辑]] * [[零阶逻辑]] * [[布尔函数]] * [[哥德尔完备性定理]] * [[哥德尔不完备定理]] <span style="background:green; color:white; font-size:smaller">→ 学科目录:</span> '''[[哲学(目录)]]'''<br> [[Category:逻辑]] [[Category:逻辑学]] [[Category:哲学]] [[Category:中文词典]] [[Category:Y音词语]] [[Category:一]] [[Category:数理逻辑|Y]] [[Category:形式逻辑系统]]
返回
一阶逻辑
。
导航菜单
个人工具
创建账户
登录
名字空间
页面
讨论
变种
查看
阅读
查看源代码
查看历史
操作
搜索
导航
首页
最近更改
随机页面
工具箱
链入页面
相关更改
特殊页面
页面信息
扫描二维码可以用手机浏览词条