کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4661961 1633468 2014 35 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Intuitionistic completeness of first-order logic
ترجمه فارسی عنوان
کامل بودن شهودی از منطق مرتبه اول
کلمات کلیدی
معانی BHK؛ جامعیت، تئوری نوع ساختاری؛ معنای مدارک؛ نوع تقاطع؛ منطق شهودی
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

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.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the Nuprl proof assistant.Our result demonstrates the value of uniform validity as a semantic notion for studying logical theories, and it provides new techniques for showing that formulas are not intuitionistically provable. Here we demonstrate its value for minimal and intuitionistic first-order logic.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 165, Issue 1, January 2014, Pages 164–198
نویسندگان
, ,