可靠性可理解为：如果语法层面（形式化层面）成立的结论，在现实系统中一定有这样的实例满足；
即形式化推导的正确性，如果实际系统该结论无法满足但存在这样的证明，则表示你的证明系统不可靠/正确。（与伪攻击falseattack不同-比如在proverif中伪攻击不是应用pi演算的证明系统不可靠，而是因为归结过程的问题导致的）。
完备性可理解为：如果现实系统中存在实例，则语法层面一定能够证明。
即如果实际系统中的安全属性显然满足，但你的证明系统无法证明，则表明你的证明系统不完备。
====以下为引文===============================================================================
2语法
我们首先从几个问题开始。
2.1语法是什么？
2.2命题逻辑中的语法是什么？
解释一下这些符号的含义，例如：φ∧ψ——∧e1φ其中的φ,ψ我们叫做公式。公式可以是以下这些形式：p,q,p∧q,q,(p∧q)∨p,…其中的∧e1，我们叫做规则。e的意思是消除(elimination).这条规则从φ∧ψ中消除了∧,只留下了前面的φ,e1中的1就是指φ,因为它排在第1个，对比一下∧e2就会明白了。规则中的i表示引入(introduction).规则的具体含义可参考1.至于其中的,→,…，我认为目前没有必要知道含义，你仅仅需要知道他们是一些推导规则就好了。虽然你们多半都知道含义，但是，现在把它们忘了吧。请再一次又一次地记住，这些推导规则从现实世界中剥离出来后，就有了他们的独立性，和具体的含义无关，例如：φ∧ψ–——∧e1φ我们只知道φ和ψ是命题，有真假，但是，不管他们是真是假，都不影响这条规则的成立。这一点请千万注意。例如：φ="我不喜欢计算机科学"(当然，这是假的）ψ="我喜欢数学"由上面的那条推导规则，可以推出φ,即"我不喜欢计算机科学",尽管这个结论是假的，但这和这条推导规则的成立无关。不能说，这规则得出假的结论，所以这条规则就是不正确的。2.3推理和推理的有效性
前面在引入自然推导规则时，我们举了一些例子，如自然语言中的对应形式，包括命题的真假，等等。这一切都是为了理解这些规则是怎么来的。那么，从现在开始，请忘掉那些例子，让你的知识保留在只知道图1所示的自然推导规则表.我们现在仅仅知道这张规则表，那么，这些规则用来做什么呢？这些规则可以用来推理。
2.3.1什么是推理看下面这种形式：φ1,φ2,…,φn|-ψ这就叫一次推理(sequent).其中φi叫做前提(premise),ψ叫做结论(conclusion).例如，下面这个形式就叫一次推理。p,(q∧r)|-p∧r
上面的证明过程，例如第6行，最右面的∧i3,5表示使用第3，5行的公式和规则∧i,得到第6行的公式。关于语法部分，现在只需要知道两件事：一：公式及自然推导规则表；二：推理和推理的有效性。下面开始语义部分。
3语义
3.1语义是什么？简单地说，语义就是语言所表达的含义。同样以自然语言为例：我吃饭你很容易知道这句话是什么意思。但是你想过为什么你能知道这句话是什么意思吗？原因在于，首先你知道“我”是什么意思，“饭”是什么意思，其次你知道“吃”是什么意思。最后，你明白“我吃饭”三个字连在一起是什么意思。你可能觉得这是一句废话，但是后面提到命题逻辑时，你可能就会明白为什么在这儿说了一句废话。关于这句话，还需要有两点要说明：一是，这句话是一个主谓宾的结构，但是即使你不知道这个句子的语法，你仍然可以知道它的含义。二是，在主谓宾结构中：主语和宾语可以取的值其实是一个集合：{我，你，饭，计算机，书,….},谓语可以取的值也是一个集合：{吃，看，打,….}.句子代表的含义也构成一个集合：{我吃饭的含义，我看书的含义,….}.同时，在“我吃饭”这个句子与“我吃饭的含义”之间存在着一种映射关系。语义中如果没有这种映射关系，那么你说“我吃饭”的时候，别人可能觉得你在看书。
有了真值表，我们才知道T∧F意味着什么，F→T意味着什么。至此，我们的语义系统就定义好了。
3.3语义蕴含(semanticentailment)及其有效性
看下面这种形式：φ1,φ2,…,φn|=ψ其中的|=即表示蕴含关系，从上面语法和语义的讨论中，你可能已经明白了，这只是一种语法层面的定义，那么蕴含的语义是什么呢？翻译为人话就是：当我说蕴含的时候，我是在说什么。蕴含就是在说，如果φ1,φ2,…,φn的取值都为T,那么ψ的取值一定为T.例如：p∧q,q,r|=p.当p∧q为T,q为T，r为T时，P一定为T.所以p∧q,q,r蕴含p.那么，什么是蕴含的有效性呢？
例如我问：p∨q,q,r|=p是有效的么？我其实是在问，p∨q为T,q为T,r为T时，p一定为T么？如果p一定为T,那么p∨q,q,r|=p是有效的。否则，p∨q,q,r|=p是无效的。所以，如果我说φ1,φ2,…,φn蕴含ψ,意思等同于：φ1,φ2,…,φn|=ψ是有效的。至此，语义部分就介绍到这里。下面，开始介绍可靠性与完备性。
4可靠性与完备性(SoundnessandCompleteness)
经过了前面冗长的关于语法和语义的介绍，终于可以开始介绍可靠性与完备性了。在此之前，请保证你可以正确区分|-和|=,知道推理的有效性和语义蕴含的有效性意味着什么。
在完成命题逻辑系统的定义后，我们想知道这个系统的一切性质，其中最重要的性质就是可靠性与完备性。这一节的两个定理告诉我们，命题逻辑系统满足可靠性和完备性。
4.1可靠性(Soundness)
4.1.1可靠性是指什么？
可靠性定理：令φ1,φ2,…,φn和ψ为命题逻辑中的公式，如果φ1,φ2,…,φn|-ψ是有效的，那么φ1,φ2,…,φn|=ψ是有效的。
这个定理是在说，我们为逻辑系统定义好语法和语义后，如果在语法上，我们可以利用推导规则，将φ1,φ2,…,φn转化为ψ，那么在语义上，如果φ1,φ2,…,φn都为T,那么ψ一定为T.
4.1.2为什么要引入可靠性的概念？首先，我们需要理解，可靠性是逻辑系统满足的一个性质。如果有一天，我们构造了另一个逻辑系统，自己定义了语法，定义了语义，那么，我们可能需要问一下自己：我定义的这个逻辑系统满足可靠性么？上面的可靠性定理是指在命题逻辑中，我们定义了语法：自然推导规则，推导及其有效性；我们定义了语义：真值表，语义蕴含及其有效性。在由这些定义构成的一个命题逻辑系统中，像可靠性定理描述的那样的性质是满足的。一旦我们证明了一个逻辑系统满足了可靠性，我们就可以利用这个好的性质来做一些事。4.1.3可靠性有什么用？现在我们明白了，之前定义的命题逻辑系统满足可靠性。现在，我们就可以利用这一点来做一点事了。我们可以利用逻辑系统的可靠性来确定：有一些证明是不存在的。例如：在命题逻辑系统中给定前提φ1,φ2,…,φn,能否证明ψ？这其实是在问：φ1,φ2,…,φn|-ψ是否是有效的。如果这个前提和结论非常复杂，那么你很可能证明不出来，因为证明通常是需要一点灵感的，而灵感通常是难得的。但是，你证明不出来不能说明这个证明不存在。那我们应该怎么做呢？有了可靠性定理，我们就可以将问题转化为：φ1,φ2,…,φn|=ψ是否是有效的。
而这个问题，我们完全可以用真值表来确定。假如我们用真值表确定了，φ1,φ2,…,φn|=ψ是无效的,那么，我们完全可以断言：φ1,φ2,…,φn|-ψ是无效的。即证明不存在。因为根据可靠性定理，如果φ1,φ2,…,φn|-ψ是有效的，那么φ1,φ2,…,φn|=ψ是有效的，与我们根据真值表得出的结论相矛盾。
5完备性(Completeness)
5.1完备性是指什么？
完备性定理：令φ1,φ2,…,φn和ψ为命题逻辑中的公式，如果φ1,φ2,…,φn|=ψ是有效的，那么φ1,φ2,…,φn|-ψ是有效的。可以看出，这和可靠性定理的定义正好相反。这其实是在说，在一个逻辑系统中，如果从语义上看，φ1,φ2,…,φn|=ψ是有效的，那么我们一定可以为φ1,φ2,…,φn|-ψ找到一个证明。在命题逻辑中，完备性定理也是成立的。具体的证明过程参考1。
5.2完备性有什么用？与可靠性一样，完备性也是逻辑系统的性质。那么完备性有什么用呢？在一个逻辑系统中，如果我们知道一些前提是真的，即φ1,φ2,…,φn都为真，那么，我们想知道在这样的条件下，结论ψ也一定是真吗？即我们想知道φ1,φ2,…,φn|=ψ是否是有效的。那么我们可能想找一个由φ1,φ2,…,φn到ψ的证明，即利用推导规则将φ1,φ2,…,φn转化为φ.这时候，完备性就会告诉我们，如果φ1,φ2,…,φn|=ψ是有效的，那么，这样的证明一定存在。假如你的逻辑系统不满足完备性，那么即使φ1,φ2,…,φn|=ψ是有效的，但是它的证明也可能不存在，那你的努力可能就是徒劳的。
6结束关于可靠性与完备性的讨论到这里就结束了，这只是我学习参考资料1第1章的一些体会，这本书相当不错，特别推荐给诸位。如果有什么问题，欢迎随时讨论。
参考:1MichaelHuth,MarkRyan.面向计算科学的数理逻辑——系统建模与推理.2005