yu.pdf Justification logic is an explicit version of modal logic. In justification logic, instead of []3, we have t:3, with a intuitive meaning that t is a justification of 3, where t is a term with its structure. After a glance of its history, we will present the logic formally, and talk about two indispensible features, "Fitting completeness" and "Realization". Some selected topics will also be mentioned, including mixed-systems of modal and justification logics, self-referentiality in realizations, possible philosophical applications, etc..
Q：表示提问 A：表示回答 S：表示补充
王彦晶Q：对不同的出现可能有不同的翻译是吧？
俞珺华A：就是到这一步，realizer其实是任意的，你如果给的比较聪明，那就可以，你要是乱给的话，当然就不行。同样，一个S4定理，我们由很多种不同的办法去做这种，主要不同LP都得是定理。做法通常实际上是证明对证明。
王彦晶Q：能有一个统一的realizer，根据证明的，能从S4推出一个公式来，根据证明的不同选不同的翻译。
俞珺华A：有一种比较流行的就是给定一个算法，算法借助于S4的证明，如果你非要用这种算法，S4的证明不一样，那边结果就不一样。
赵晓玉Q：这个不是算术语言中的乘法吧？
俞珺华A：不是。这是定义我们PL语言当中，有项有公式，项中有常元有变元，这是其中一个operator。后面那个加号也不是算术的加。
苏兴池Q：冒号就是表示前面一个是后面的证明的意思吗？有多少个常元？
俞珺华A：这么说吧，有可数无穷多个序列，每个序列里面有常元。
王彦晶Q：这就像是必然化规则类似这么办，任何是内定理的我就可以加n个这样，如果我想像必然化规则那样生给。
俞珺华A：你要说原定理一定通这个我不敢说，它的毛病在，假如说在这个逻辑中证出来这么一个內定理，我们只要通过观察t的形式，就能把这个证明给复原出来，如果是这样的话，大概是有这个问题。而且还有一个就是如果这样一个规则允许它在证明中任何地方出现的话，很有可能你这边用一个那边用一个等你需要两边一样的时候它还要改。
王彦晶Q：问号上面一横这个为什么是个操作，这就很奇怪。
俞珺华A：他就是把它理解为一个操作看它怎么样，并没有说它一定是个操作，如果真的照算法这个角度考虑的话其实5这里就已经出了毛病了，在4里面，如果t是phi的证明，这个叹号有一个对应递归函数是我们能找到的，但这里t不是phi的证明，那就已经不是一个能行的算法了，所以这个LP或者以下的这些很多性质至少能够接受，再往上有些东西确实技术上的痕迹有点重。
王彦晶Q：就不能有可证性的解释，这就有点奇怪，如果ox不能用可证或者justify去解释。
俞珺华A：如果从这个角度说哪一个自然不自然，其实模态逻辑也一样，我要刻画信念什么的那个模态逻辑合适，justification这边也可能有类似的问题，至少我个人我还是把它当作技术上的一个办法来看的，是一个很新奇的做法，在哲学逻辑的角度看有多么直观我也难说。
王彦晶Q：语言里头只有一个常元？
俞珺华A：常元不再分析的一个序列，还是那么多个。
王彦晶Q：不需要不同序列之间的叠加是吗？
俞珺华A：我们序列不写或者在同一个序列，c1假设是一个公理，我们前面那个应该是c2，如果没有叹号的话我们实际上可以用它来，我们不用必然化规则代两层，弄一层然后用MP，相当于这两个就会对应，大概是这么一个意思。
王彦晶Q：刚才说的好像就是从系统那儿说的，就换了一种说法，不是很语义。
俞珺华A：这个确实是这一类justification logic都会有的问题，语义和语法太近了。
王彦晶Q：S5就不管那个极大可及世界了对吧，那就一个点就够了。
俞珺华A：是的。问题是它那个全通是可及关系全通，就是说我猜这个是出在对于S5这个等价关系我们找不到一个合适的类似于这样的条件。其实说起来这也不奇怪。我们先说一下完全性。
徐 超Q：我了解到Justification Logic 是在那个08年的有一篇文章，我一直以为它是从那儿来的，因为他要把普通的知识没有直接体现，只是说true belief，就是没有说justify，把它引进来之后首先他在98年就已经用到的Justification Logic这个词了吗？还是说他从08年才开始用的？
俞珺华A：如果不是08年的话就往前不会太早了。最开始是只有LP的，后来很多逻辑都是在S5出现以前剩下的都是S4那些子逻辑，都是同一个方法其实，所以人们可能认为那时候是可证逻辑的奠基，之前甚至有这样的记法LPK4对应像LP这样的东西，现在不再这样写了。
徐 超Q：他在那篇文章里说justification，他也用到了evidence，他对知识的定义是我们知道F就意味着我们知道F的一个evidence，他这个evidence一般地我们怎么去理解它，它不像在 LP里面它是一个证明，它的结构都清晰，他只是在里面做了一个假设，justification解释为有结构的抽象实体，然后他就把LP的所有的组合全用进去了，就像您刚才讲的，evidence是proof吗？它的结构是什么？
俞珺华A：那篇文章我的理解是他想用已有的成套的方法去看它在认知逻辑里面能不能有一些应用，并不认为他在试图通过这个逻辑给知识下一个什么定义。他做过一些报告，所谓的Justification Logic并不是要justification怎么样去定义它，而是要贡献在于说把justification引入到关于epistemic logic研究中来，他只是说提供了一个我们在逻辑上去说它的一个办法。在01年的时候他出过一个文章是关于justification的本体论的，可能会更不喜欢，他的处理大概是这样的：t可以是phi的证据，也可以是一些别的东西，他把t理解成一个公式集，就是它所justify的那些公式的集合，他给了一个一个argument，我们如果看模态逻辑，我们说一个在模型当中命题变元什么的，命题变元不就是那些满足它的那些点的集合嘛，那我这个justification就在公式里面。
王彦晶Q：他这个setting里面我觉得他如果想说他这个东西对知识逻辑知识论可能有一点用的话，我的conceptual的一个问题就是他的语义里头t那个term只是在当前世界上去check，因为语义其实没变，在所有世界上phi都为真，而且在当前世界上t是phi为真的justification，但是在知识逻辑里就搞不清楚哪个是当前世界，你凭什么就只用当前世界的t作为justification的check，就是为什么不是对所有不可取分的点上都是同一个t去做phi的justification，而且phi在哪个点上都为真，如果那么定义的话会有什么样的区别。
俞珺华A：您说的那个对现有做法其实是特例，他这个是随便取的。
王彦晶S：不，我说的是他语义限制更多，因为现在就只是说在当前世界上t是一个justification，然后在所有不可区分的世界上phi都真，那我现在说的是第二个条件是不变的，第一个条件变成在所有不可区分的世界上t都是phi的justification，那个好像更符合我们对认知的理解。因为如果说（t，phi）是一个知识的公式的话那你在语义里有假设分不清哪一个是真实世界，那term只在当前世界check，这个是我不太明白的。
俞珺华A：我猜他会这么说，在克里普克模型中既然你不知道自己是在哪一个世界上，那你的valuation怎么给。
王彦晶S：是，它的valuation是可以变的，我不见得知道这个valuation，其实说（t，phi）是说普通的知识要更强的justified true belief，那不应该能够identify当前世界，如果语义改成我说的那样的话是不是逻辑性质也会有不一样，因为你不止check当前世界上的情况。
周北海Q：你的完全性证明里头只是用到了典范模型的完全性，没有讲到框架完全性是吗？
俞珺华A：这个没有。现在的这个完全性都是在模型上去证，框架的话你的evidence function怎么办。
王彦晶S：其实不是关系怎么样，而是那个evidence到底算在框架里还是不算在框架里。
俞珺华A：首先我也没有试过，我也没见过有拿出来过的。
周北海S：对于justification这个词，现在有两种翻译，一个是证成，还有一个是核证，这在台湾用的比较多。
王彦晶Q：证成是说去justify phi的那个东西。
周北海Q：只说翻译成证成，这个什么意思自己琢磨。我们到底在谈论什么东西，一开始我们要证明这个东西我要给它一个性质刻画，后来谈论justification这个事情，核证也好，证成也好，它跟证明有什么关系？
俞珺华A：他只是把形式证明看成了其中一种justification。
周北海Q：那它除了证明以外还有什么？
俞珺华A：这就看怎么挑了。就像模态逻辑，我们说logic about beliefs，我们可以挑不同的系统，这里就也是。
周北海Q：这里就是用justification这个词覆盖了一些东西，证明是它的一种，还有某种东西也是它的一种，这个某种东西是什么，哪一些？比如说法律上经常提供证据，你也用到了evidence这个词，那证据这个词是不是也可以作为justification的一些材料或什么，谈各种各样的evidence，证明是一种evidence，比如到了现场，指纹也是一种evidence，它有那么广吗？指纹这些东西都可以justify他到现场去了，把他到现场看作一个句子，它为真，为什么呢？因为有很多证据在里面。会不会你的justification覆盖了我们现在谈的，你的包括这些吗？
俞珺华A：我个人认为应该是的。
周北海Q：我希望有结构的没结构的都可以在这个justification里面谈，justified某一个东西，证据也好，证明也好，等等，都justify这个东西，最广义上去看。
俞珺华A：我们充一个这样的架子出来，现在有一个方法，然后不同的setting出来的性质可能是不一样的。
周北海Q：我把所有的justification，比如说叫核证吧，都给它提供一个统一的、一般的理论，所有的东西都可以在我这个底下用，最基本的框架都是这样，是不是这么个想法？
俞珺华A：他可能是把最小的J当作一个最广泛的逻辑，然后再往上面加。但未必是直观上所有的justification都可以包含，他不会说这样的话。
周北海Q：你们现在想做的是冲着什么目的去做的，大体上分，我们把证明也看作一个justification，数学证明算是一种先天的justification吧，还有一种算是经验上的证据比如指纹、血迹等，属于经验事实，这两种有先天的不同，当你做justification的时候会不会区分这两种不同的东西，是只谈先天的可证性还是扩展到经验上的证据，这是有本质区别的。你要做知识逻辑的话为什么非要搭在S4、S5这些正规模态逻辑上，本来它们作为知识逻辑我认为不是很好，我总认为会陷入逻辑全知这个问题中，能不能自己独立做出来一套，总有一种技术上的惯性，要从一个套路来做，还是都是知识的共性。
俞珺华A：我个人的话是的，我只是把它当作技术上的一个方法，而不是当作哲学逻辑，或者哲学上的一些讨论，如果是Artmov的话，可能确实会说到这个问题，他14年出过一个文章讨论过逻辑全知的问题，他会用像复杂性这样去刻画，他确实考虑过这个问题。
王彦晶S：上次王仁俊老师就是用这个思想去处理全知问题。他加入时间的概念。
俞珺华S：我个人更多的还是把它当作一个版本的模态逻辑去看，至于说它是不是有那么大哲学上意义什么的我倒不是特别关心。
程莹莹 整理
