On modal logics of partial recursive functions

被引：1
作者：
Naumov P. [1 ]
机构：
[1] Department of Mathematics and Computer Science, McDaniel College, Westminster, MD
来源：
Studia Logica | 2005年 / 81卷 / 3期
关键词：
Curry-Howard isomorphism; Modal logic; Recursive function;
D O I：
10.1007/s11225-005-4646-8
中图分类号：
学科分类号：
摘要：
The classical propositional logic is known to be sound and complete with respect to the set semantics that interprets connectives as set operations. The paper extends propositional language by a new binary modality that corresponds to partial recursive function type constructor under the above interpretation. The cases of deterministic and non-deterministic functions are considered and for both of them semantically complete modal logics are described and decidability of these logics is established. © Springer 2005.
引用
收藏
页码：295 / 309
页数：14
相关论文
共 17 条
  • [1] Constable R.L., Et al., Implementing Mathematics with Nuprl Proof Development System, (1986)
  • [2] Coquand T., Paulin Ch., Inductively defined types, COLOG-88 (Tallinn, 1988), pp. 50-66, (1990)
  • [3] Curry H.B., Functionality in combinatory logic, Proc. Nat. Acad. Sci. U. S. A., 20, pp. 584-590, (1934)
  • [4] Curry H.B., The combinatory foundations of mathematical logic, J. Symbolic Logic, 7, pp. 49-64, (1942)
  • [5] Curry H.B., Feys R., Combinatory Logic, Vol. I, 1, (1958)
  • [6] Fairtlough M., Mendler M., Prepositional lax logic, Inform, and Comput., 137, 1, pp. 1-33, (1997)
  • [7] Harel D., Kozen D., Tiuryn J., Dynamic Logic, (2000)
  • [8] Howard W.A., The formulae-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 480-490, (1980)
  • [9] Kopylov A., Nogin A., Markov's principle for prepositional type theory, Lecture Notes in Computer Science, 2142, pp. 570-584, (2001)
  • [10] McKinsey J.C.C., Tarski A., The algebra of topology, Ann. of Math. (2), 45, pp. 141-191, (1944)
12