A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
Antonio Piccolomini d'Aragona
我处理了两种证明理论语义的方法:一种基于论证结构和理由,我称之为可还原性语义,一种基于原子基(集)公式之间的后果,称为基础语义。 后者反过来分裂为标准读数,以及Sandqvist提出的变体。 我证明一些结果,当满足适当的条件时,允许一个人从一种方法转向另一种方法,我得出这些结果相对于(递归)逻辑系统在有效性的证明理论概念方面的完整性问题的一些后果。 这将导致我专注于一个基本完整性的概念,我将讨论关于直觉逻辑的已知完整性结果。 拟议方法的一般兴趣源于这样一个事实,即可还原性语义可以理解为基础语义的标签,其基础语义与基础语义产生关系(成集)的公式中键入的证明对象,并且见证了这一事实。 反之亦然,基础语义可以理解为通过删除这种关系所持有的事实的见证而获得的可还原语义结果关系的类型抽象,并且仅仅关注相关证明对象的输入和输出类型。
I deal with two approaches to proof-theoretic semantics: one based on argument structures and justifications, which I call reducibility semantics, and one based on consequence among (sets of) formulas over atomic bases, called base semantics. The latter splits in turn into a standard reading, and a variant of it put forward by Sandqvist. I prove some results which, when suitable conditions are met, permit one to shift from one approach to the other, and I draw some of the consequences of these r...
