【数理逻辑】预备知识

元语言和对象语言：
对象语言：被讨论的语言
元语言：讨论对象语言时用的语言（解释说明）
语义
给形式语言以解释
真假赋值υ\upsilonυ给公式AAA指派的值记作AυA^\upsilonAυ

要证明一个公式是可满足的，只要找到一个模型（M,σ)（M,\sigma)（M,σ),即一个论域MMM,一个解释III,和一个赋值σ\sigmaσ,使集合内每一个公式为真就可以了。

可满足性和有效性
可满足性：存在一个赋值使公式为真
有效性：任意赋值公式为真
逻辑推论（语义关系）
是公式间的一种关系，相当于命题间的可推导性关系。
我们称公式A是公式集合Σ\SigmaΣ的逻辑结论，当且仅当对任意模型，如果此模型使Σ\SigmaΣ为真，那么它也使A为真。
设Σ⊆\Sigma\subseteqΣ⊆Form(Lp),A∈Form(\mathscr{L}^p),A\inForm(Lp),A∈Form(Lp)Form(\mathscr{L}^p)Form(Lp)
A是Σ\SigmaΣ中公式的逻辑推论，记作 Σ⊨\Sigma\vDashΣ⊨AAA

有效性：
例如问： p ∨ q , q, r ⊨\vDash⊨ p 是有效的么？
其实是在问， p ∨ q 为 T, q为T, r为T时， p一定为T么？
如果p一定为T, 那么 p ∨ q , q, r ⊨\vDash⊨ p 是有效的。否则，p ∨ q , q, r ⊨\vDash⊨ p 是无效的。
所以，如果说 φ1, φ2, … , φn 蕴含 ψ, 意思等同于：
φ1, φ2, …, φn ⊨\vDash⊨ ψ 是有效的。

形式推演（语法关系）
近代数理逻辑的思想追溯到很久以前，Leibniz力图建立一种精确的、普遍适用的科学语言，并寻求一种推理的演算，以便能用计算来解决辩论和意见不一致的问题，后来终于完成了，数理逻辑的历史由此开始。
形式推演的正确性是能够机械地检验的，而逻辑推论和可推导的证明都不能机械地检验。
用Σ⊢\Sigma\vdashΣ⊢AAA表示A是由Σ\SigmaΣ形式可推演的。Σ\SigmaΣ为推理的前提，A是待证明的命题，如果以Σ\SigmaΣ为前提，能证明A成立，那么称序贯Σ⊢\Sigma\vdashΣ⊢AAA可证，并称A是Σ\SigmaΣ的证明结论。

⊢和⊨\vdash和\vDash⊢和⊨都不是形式语言的符号，与→\rightarrow→不同。（→\rightarrow→是谓词符号集中的符号）
A⊨A\vDashA⊨BBB当且仅当∅⊨\emptyset\vDash∅⊨A→A\rightarrowA→BBB(即A→\rightarrow→B是重言式)
A⊢A\vdashA⊢BBB当且仅当∅⊢\emptyset\vdash∅⊢A→A\rightarrowA→BBB

推理系统的可靠性和完全性（命题逻辑）
可靠性：如果Σ⊢\Sigma\vdashΣ⊢AAA可证，那么Σ⊨\Sigma\vDashΣ⊨AAA成立（被证明的结论就是逻辑结论）
完全性：如果Σ⊨\Sigma\vDashΣ⊨AAA可证，那么Σ⊢\Sigma\vdashΣ⊢AAA成立（φ1, φ2, …, φn ⊨\vDash⊨ψ 是有效的，那么我们一定可以为φ1, φ2, …, φn ⊢\vdash⊢ ψ 找到一个证明。）

语法和语义，由完备性（语义解释得通，则一定有语法可以反映。
换言之，语法一定能反映语义的意思）和可靠性（语义一定能够用语法的验证得到。
换言之，语义的正确性可以由语法来保证）定理进行保证。
这样我们在使用逻辑推论和形式推演的时候，就有了理论依据。

语义：用来解释客观世界的现象。因为是解释，所以都是基于赋值的，因此我们在讨论语义的时候，都需要进行赋值。一般的赋值，是指真假（0/1）赋值。语义是在理解的基础上作出的，所以可能造成一些偏差，因为每个人理解不一样嘛，所以就需要有语法了。
语法：用来做形式化的推演。既然语义容易产生歧义，那么语法就是用来做规范地、机械地进行推演。基本思想是，如果 (i)第一步推演是正确的。 (ii)第n步推演是正确的，那么如果第n+1步是由第n步得到，那么也是正确的。以此类推得到归纳。

紧致性：
给定公式集合 Σ\SigmaΣ及公式 A ,若Σ⊢\Sigma\vdashΣ⊢AAA ,则存在有限的Γ⊆Σ\Gamma\subseteq\SigmaΓ⊆Σ 使得Γ⊢\Gamma\vdashΓ⊢AAA给定公式集合 Σ\SigmaΣ及公式 A ,若Σ⊢\Sigma\vdashΣ⊢AAA ,则存在有限的Γ⊆Σ\Gamma\subseteq\SigmaΓ⊆Σ 使得Γ⊢\Gamma\vdashΓ⊢AAA
这说明，即使序贯的前提Σ\SigmaΣ是公式的可数无穷集合，Σ⊢\Sigma\vdashΣ⊢AAA的形式证明也只与Σ\SigmaΣ所包含的有穷个公式有关。

假定有一个句集∑，其任意有限子集合∑’都有模型，则整个句集∑本身必有模型
或者说，一阶句子的（可能无限的）集合是可满足的（就是说有一个模型），当且仅当它的所有有限子集是可满足的

协调性：
命题逻辑公式集合Σ\SigmaΣ中不存在A，使得Σ⊢\Sigma\vdashΣ⊢AAA 且Σ⊢\Sigma\vdashΣ⊢¬\neg¬AAA
如果公式集合Γ\GammaΓ协调，那么存在公式A使Γ⊢A使\Gamma\vdashA使Γ⊢AAA不可证
数学定理的证明
形式化证明，CP过程，以待证明的序贯为根结点生成证明树，验证每个叶节点是否是公理的实例。
如果有穷步骤内停机并输出证明树，则序贯可证
如果不终止，则不可证
形式理论
定义：设Γ\GammaΓ是一阶语言的有穷或可数无穷的语句集合，如果Γ\GammaΓ协调（不存在相互矛盾的推论），则Γ\GammaΓ是一阶语言的形式理论（知识库就可以看作是一阶语言形式理论的实例）（初等算数理论是由9个语句组成的形式理论）

Γ\GammaΓ的理论闭包：指语句集合Th(Γ)={Th(\Gamma)=\lbraceTh(Γ)={A∣A是L的语句，且Γ⊢A|A是\mathscr{L}的语句，且\Gamma\vdashA∣A是L的语句，且Γ⊢AAA可证}\rbrace}
全体重言式的集合： Γ\GammaΓ是空集时， Γ\GammaΓ的理论闭包{\lbrace{A∣A是L的语句，且⊢A|A是\mathscr{L}的语句，且\vdashA∣A是L的语句，且⊢AAA可证}\rbrace}
演绎推理和归纳推理区别：
归纳推理是一种促成理论进化的推理，它涉及知识的增长，即使从正确的前提出发,使用归纳推理后,只能要求所得到的结论自身是协调的，或与前提是协调的，但不一定都是正确的，有些甚至可能是错误的。
演绎推理本质上是重言式的变换，即被推出的结论都蕴涵在前提之中，知识没有实质性的增长，演绎推理是可靠的，即从正确的前提出发，根据演绎推理规则得出的结论总是正确的（可靠性）
检验由归纳推理导出的结论是否正确，唯一的办法是看这个结论是否遇到“事实反驳”,也就是“反例”.当这个结论遇到“事实反驳” 时 ,它就是错误的。
极大缩减：
删除现有理论中导致与实验和观测结果相矛盾的原理和定律，使经删除后，理论的剩余部分成为与实验和观测结果相协调的现有理论的极大子集
R演算：形式理论的修正演算系统
当一个形式理论与事实产生矛盾时找出导致矛盾的前提，通过恰当地删去它们来获得一个协调的子理论
R演算=R公理+R逻辑连接词符号规则+R量词符号规则+R删除规则

R公理：A,Δ∣¬A,\Delta|\negA,Δ∣¬A,Γ⟹A,\Gamma\LongrightarrowA,Γ⟹A,Δ∣ΓA,\Delta|\GammaA,Δ∣Γ

即形式理论¬\neg¬A与左边的形式反驳A不协调，所以将其删除

R -∧\wedge∧规则：如果A被删除，那么A∧A\wedgeA∧BBB必须删除
R -∨\vee∨规则：如果A和B分别被删除，那么A∨A\veeA∨BBB必须删除
R -→\to→规则：如果¬\neg¬A和B分别被删除，那么A→A\toA→BBB必须删除
R -∀\forall∀规则：
演算规则：存在一个例子t使 A[t/x]被删除，那么 A[t/x]是∀xA(x) 的一个反例，所以∀xA(x)一定被删除。

如果存在一个反例，那么一般规律就不可能成立，因此必须被删除。

R -∃\exist∃规则：
演算规则:如果对任意新变量y，A[y/x]都将被删除，那么∃xA(x) 必须被删除。

如果一个原理，对每一种实验，都与实验结果不符，那么它的存在性不可能成立。

R -删除规则：如果现有理论 Γ1\Gamma_1Γ1，AAA，Γ2\Gamma_2Γ2的逻辑结论C与实验结果 Δ\DeltaΔ有矛盾，那么C的一个必要前提必须被删除

【数理逻辑】预备知识相关推荐

word2vec 中的数学原理详解（二）预备知识
版权声明:本文为博主原创文章,未经博主允许不得转载. https://blog.csdn.net/peghoty/article/details/37969635 https://blog.csdn. ...
计算机视觉预备知识,计算机视觉：泊松融合
Poisson Blending4:更多用途 Poisson Blending0:预备知识(图像的梯度.泊松方程) 进入正题之前,我们先补充一下基础知识.图像的梯度什么是图像的梯度?我们可以把图像看 ...
学习SLAM需要哪些预备知识？
点击上方"3D视觉工坊",选择"星标" 干货第一时间送达编辑:3D视觉工坊链接:https://www.zhihu.com/question/3518606 ...
[转]预备知识—程序的内存分配
因为经典,所以转发. 一.预备知识-程序的内存分配一个由C/C++编译的程序占用的内存分为以下几个部分栈区(stack) - 由编译器自动分配释放,存放函数的参数值,局部变量的值等.其操作方 ...
一步一步学Linq to sql（一）：预备知识
从今天起将推出新手讲堂,首先从linq开始详细讲解.一步一步学Linq to sql(一):预备知识什么是Linq to sql Linq to sql(或者叫DLINQ)是LINQ(.NET语言集 ...
用计算机语言编写的完成一定功能,C+的+预备知识.ppt
C的预备知识 * (顺序语句.选择语句.循环语句FOR及嵌套) C++讲义预知识:程序设计.算法和C++ 第一章:顺序结构 1.1标准数据类型和变量的定义 1.2 运算符.标准函数和表达式 1.4基 ...
微积分笔记（一）--预备知识
文章目录预备知识什么是微积分一. 直线 1.1 增量 1.2 直线的斜率 1.3 平行线和垂直线 1.4 直线的方程二.函数和图形 2.1 映射 2.2 逆映射与复合映射 2.3 函数 2.4 ...
基于python的nlp预备知识
基于python的nlp预备知识载入语料库 brown 语料库的导入分词 nltk的word_tokenize Stem抽取题干和Lemma 词形还原 NLTK实现Stemming三种方式 NLT ...
机器学习(三)——预备知识(学习率与激活函数)
预备知识 import tensorflow as tf import numpy as np # a = tf.constant([1,3,2,2,5]) # b = tf.constant([0, ...
C++Primer Plus （第六版）阅读笔记 + 源码分析【第一章：预备知识】
第一章:预备知识 C++简介 C++简史 C语言 C语言编程原理面向对象编程 C++和泛型编程 C++的起源可移植性和标准程序创建的技巧创建源代码文件编译和链接 UNIX Linux Win ...

【数理逻辑】预备知识

【数理逻辑】预备知识相关推荐

最新文章

热门文章