خصائص الانفصال والوجود

يسرد راثجن  (2005) خمس خصائص قد تمتلكها النظرية. وتشمل هذه الخصائص خاصية الفصل ( DP )، وخاصية الوجود ( EP )، وثلاث خصائص إضافية:

• تنص خاصية الوجود العددي ( NEP ) على أنه إذا أثبتت النظرية${\displaystyle (\exists x\in \mathbb {N} )\varphi (x)}$إذا لم يكن لـ φ أي متغيرات حرة أخرى، فإن النظرية تثبت ذلك.${\displaystyle \varphi ({\bar {n}})}$بالنسبة للبعض${\displaystyle n\in \mathbb {N} {\text{.}}}$هنا${\displaystyle {\bar {n}}}$هو مصطلح في${\displaystyle T}$يمثل العدد ن .
• تنص قاعدة الكنيسة ( CR ) على أنه إذا ثبتت صحة النظرية${\displaystyle (\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)}$إذن يوجد عدد طبيعي e بحيث، لنفترض${\displaystyle f_{e}}$لتكن الدالة القابلة للحساب ذات الدليل e ، تثبت النظرية${\displaystyle (\forall x)\varphi (x,f_{e}(x))}$.
• ينص أحد أشكال قاعدة تشرش، CR ₁ ، على أنه إذا أثبتت النظرية${\displaystyle (\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)}$إذن يوجد عدد طبيعي e بحيث تثبت النظرية${\displaystyle f_{e}}$هو كامل ويثبت${\displaystyle \psi (f_{e})}$.

لا يمكن التعبير عن هذه الخصائص بشكل مباشر إلا للنظريات التي لديها القدرة على التكميم على الأعداد الطبيعية، وبالنسبة لـ CR ₁ ، التكميم على الدوال من${\displaystyle \mathbb {N} }$ل${\displaystyle \mathbb {N} }$. من الناحية العملية، يمكن للمرء أن يقول إن النظرية لها إحدى هذه الخصائص إذا كان للامتداد التعريفي للنظرية الخاصية المذكورة أعلاه (راثجين  2005).

بحكم التعريف تقريبًا، فإن النظرية التي تقبل قاعدة الوسط المرفوع مع وجود عبارات مستقلة لا تمتلك خاصية الفصل. لذا، فإن جميع النظريات الكلاسيكية التي تعبر عن حساب روبنسون لا تمتلكها. كما أن معظم النظريات الكلاسيكية، مثل حساب بيانو و ZFC، لا تثبت خاصية الوجود أيضًا، على سبيل المثال لأنها تثبت صحة ادعاء مبدأ أصغر عدد . لكن بعض النظريات الكلاسيكية، مثل ZFC بالإضافة إلى بديهية قابلية الإنشاء ، تمتلك شكلًا أضعف من خاصية الوجود (راثجن  2005).

تشتهر حسابات هيتينغ بامتلاكها خاصية الفصل وخاصية الوجود (العددية).

على الرغم من أن النتائج الأولى كانت متعلقة بنظريات الحساب البنّاءة، إلا أن العديد من النتائج معروفة أيضًا لنظريات المجموعات البنّاءة (راثجن 2005). بيّن جون مايهيل (1973) أن نظرية المجموعات البنّاءة (IZF) مع حذف بديهية التجميع لصالح بديهية الاستبدال تتمتع بخاصية الفصل، وخاصية الوجود العددي، وخاصية الوجود. أثبت مايكل راثجن (2005) أن نظرية المجموعات البنّاءة المترابطة (CZF) تتمتع بخاصية الفصل وخاصية الوجود العددي.  

لاحظ فريد وسيدروف  (1990) أن خاصية الفصل موجودة في جبر هيتينغ الحر والطوبولوجيا الحرة . من الناحية الفئوية ، في الطوبولوجيا الحرة ، يتوافق ذلك مع حقيقة أن الكائن النهائي ،${\displaystyle \mathbf {1} }$، ليس ضمّ كائنين فرعيين حقيقيين. إلى جانب خاصية الوجود، يُترجم ذلك إلى التأكيد على أن${\displaystyle \mathbf {1} }$هو كائن إسقاطي غير قابل للتحليل - الدالة التي يمثلها ( دالة المقطع العالمي) تحافظ على التشاكلات الفوقية والمنتجات المشتركة .

توجد عدة علاقات بين الخصائص الخمس المذكورة أعلاه.

في سياق الحساب، تستلزم خاصية الوجود العددي خاصية الفصل. ويستند البرهان إلى حقيقة أن الفصل يمكن إعادة كتابته كصيغة وجودية تُحدد كميًا على الأعداد الطبيعية.

${\displaystyle A\vee B\equiv (\exists n)[(n=0\to A)\wedge (n\neq 0\to B)]}$.

لذلك، إذا

${\displaystyle A\vee B}$هي نظرية من${\displaystyle T}$وكذلك${\displaystyle \exists n\colon (n=0\to A)\wedge (n\neq 0\to B)}$.

وبالتالي، بافتراض خاصية الوجود العددي، يوجد عدد ما${\displaystyle s}$بحيث

${\displaystyle ({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)}$

هي نظرية. بما أن${\displaystyle {\bar {s}}}$إذا كان رقمًا، فيمكن للمرء التحقق من قيمته بشكل ملموس.${\displaystyle s}$: لو${\displaystyle s=0}$ثم${\displaystyle A}$هي نظرية، وإذا${\displaystyle s\neq 0}$ثم${\displaystyle B}$هي نظرية.

Harvey Friedman (1974) proved that in any recursively enumerable extension of intuitionistic arithmetic, the disjunction property implies the numerical existence property. The proof uses self-referential sentences in way similar to the proof of Gödel's incompleteness theorems. The key step is to find a bound on the existential quantifier in a formula (∃x)A(x), producing a bounded existential formula (∃x<n)A(x). The bounded formula may then be written as a finite disjunction A(1)∨A(2)∨...∨A(n). Finally, disjunction elimination may be used to show that one of the disjuncts is provable.