Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
复制标题
关于直觉形式系统中 A→B ν C,A →(Ex)B(x) 类型的公式
DOI：
--
复制
发表时间：
1960
期刊：
影响因子：
--
通讯作者：
R. Harrop
中科院分区：
文献类型：
--
作者：
R. Harrop
在文献[1]中，证明了直觉初等数论N的闭析取可证当且仅当它的至少一个析取可证，（Ex）B（x）型闭公式在N中可证当且仅当B（n）对某个数n可证。证明的方法是表明，就封闭公式而言，N等价于结果是直接的微积分N1。证明的主要步骤在于证明N1的可证明公式集在肯定前件下是封闭的。这是通过获得集合的子集来完成的，该子集在肯定前件下是封闭的，并且包含原始集合的所有成员，因此它与原始集合相同。
In a previous paper [1] it was proved, among other results, that a closed disjunction of intuitionistic elementary number theory N can be proved if and only if at least one of its disjunctands is provable and that a closed formula of the type (Ex)B(x) is provable in N if and only if B(n) is provable for some numeral n. The method of proof was to show that, as far as closed formulas are concerned, N is equivalent to a calculus N1 for which the result is immediate. The main step in the proof consisted in showing that the set of provable formulas of N1 is closed under modus ponens. This was done by obtaining a subset of the set which is closed under modus ponens and contains all members of the original set, with which it is therefore identical.