Intuitionistic completeness of first-order logic |
| |
| Authors: | Robert Constable Mark Bickford |
| |
| Affiliation: | Cornell University, Department of Computer Science, Ithaca, NY 14853, United States |
| |
| Abstract: | We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator. |
| |
| Keywords: | 03 06 18 68 |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
