طبوغرافيا فعالة

في الرياضيات، الطوبولوجيا الفعالةهـوو{\displaystyle {\mathsf {Eff}}}يجسد المفهوم الذي قدمه مارتن هايلاند ( 1982 ) الفكرة الرياضية للفعالية ضمن الإطار النظري للفئات . 

التصفيات

إمكانية تحقيق كلين

يعتمد هذا النموذج الطوبولوجي على الجبر التوافقي الجزئي الذي قدمه الجبر الأول لكلينك1{\displaystyle {\mathcal {K}}_{1}}في مفهوم كلين للتحقق التكراري ، يتم تخصيص أرقام تحقق لأي مسند ، أي مجموعة فرعية منشمال{\displaystyle {\mathbb {N} }}القضايا المتطرفة هي{\displaystyle \top }و{\displaystyle \bot }، تم تحقيقه بواسطةشمال{\displaystyle {\mathbb {N} }}و{}{\displaystyle \{\}}ومع ذلك، بشكل عام، فإن هذه العملية تُسند بيانات أكثر إلى القضية من مجرد قيمة حقيقة ثنائية .

تركيبة معك{\displaystyle k}ستؤدي المتغيرات الحرة إلى إنشاء خريطة في(Pشمال)شمالك{\displaystyle ({\mathcal {P}}{\mathbb {N} })^{{\mathbb {N} }^{k}}}قيمها هي مجموعات جزئية من الأعداد المحققة المقابلة.

موضوعات قابلية التحقيق

هـوو{\displaystyle {\mathsf {Eff}}}يُعدّ هذا مثالًا رئيسيًا على مفهوم قابلية التحقيق . وهي فئة من المفاهيم الأولية ذات منطق داخلي حدسي، وتُحقق شكلًا من أشكال الاختيار التابع . وهي عمومًا ليست مفاهيم غروتينديك.

على وجه الخصوص، فإن الطوبولوجيا الفعالة هيRتي(ك1){\displaystyle {\mathsf {RT}}({\mathcal {K}}_{1})}يمكن القول إن بعض بنى الطوبولوجيا القابلة للتحقيق الأخرى تجرد بعض الجوانب التي تلعبهاشمال{\displaystyle {\mathbb {N} }}هنا.

تعريف

توجد عدة طرق لبناء الطوبولوجيا الفعالة، على سبيل المثال، من خلال مفهوم الثلاثيات، أو كإكمالٍ من نوع ex/reg لفئة التجميعات . فيما يلي تعريف صريح ومفصل بالكامل. [ 1 ] : 115

كائن من كائنات الطوبولوجيا الفعالة هو مجموعةX{\displaystyle X}مزود بوظيفةهـ:X2P(شمال){\displaystyle E:X^{2}\to {\mathcal {P}}(\mathbb {N} )}تحقيق شروط معينة. نرمز إلىنهـ(x،y){\displaystyle n\in E(x,y)}بواسطةنx=y{\displaystyle n\Vdash x=y}(الترميز غير موحد؛ استخدام={\displaystyle =}يُحمّل الرمز معنىً يتجاوز معناه المعتاد، على غرار الترميزP(X=Y){\displaystyle P(X=Y)}(في نظرية الاحتمالات .) بشكل غير رسمي، هذا يعني أنن{\displaystyle n}هو شاهد حسابي، أو محقق للمساواةx=y{\displaystyle x=y}الشروط التي يجب استيفاؤها هي التالية:

  • يجب أن يكون هناك برنامجهـ{\displaystyle e}بحيث يكون ذلك لجميعنشمال{\displaystyle n\in \mathbb {N} }وx،yX{\displaystyle x,y\in X}، لونx=y{\displaystyle n\Vdash x=y}ثم مخرجاتهـ{\displaystyle e}علىن{\displaystyle n}، أي،ϕهـ(ن){\displaystyle \phi _{e}(n)}(أينϕهـ{\displaystyle \phi _{e}}هوهـ{\displaystyle e}تم تعريف الدالة الجزئية القابلة للحساب من الرتبة n ، وϕهـ(ن)y=x{\displaystyle \phi _{e}(n)\Vdash y=x}باختصار،هـ{\displaystyle e}يأخذ محققًاx=y{\displaystyle x=y}ويُخرج مُحققًا لـy=x{\displaystyle y=x}(للجميع)x،y{\displaystyle x,y}). (لاحظ أنهـ{\displaystyle e}لا يمكن الاعتماد علىx،y{\displaystyle x,y}ولا يتلقى إلا محقق ذلكx=y{\displaystyle x=y}كمدخلات، دون مزيد من المعلومات حولx{\displaystyle x}وy{\displaystyle y}.)
  • وبالمثل، يجب أن يكون هناك برنامج يأخذ مُحققًا لـx=y{\displaystyle x=y}ومحقق لـy=z{\displaystyle y=z}، ويُخرج مُحققًا لـx=z{\displaystyle x=z}(للجميع)x،y،z{\displaystyle x,y,z}).

مُحقق لـx=x{\displaystyle x=x}سيُطلق عليه ببساطة اسم مُحقق لـx{\displaystyle x}.

علاقة وظيفية من كائنX{\displaystyle X}إلى كائنY{\displaystyle Y}هي دالةو:X×YP(شمال){\displaystyle f:X\times Y\to {\mathcal {P}}(\mathbb {N} )}، مع استيفاء شروط معينة. نشير بشكل موحٍ إلىنو(x،y){\displaystyle n\in f(x,y)}بواسطةنو(x)=y{\displaystyle n\dash f(x)=y}(مرة أخرى، هذه صيغة خاصة؛و(x){\displaystyle f(x)}(ليس له معنى بحد ذاته). وهذا يعني بشكل غير رسمي أنن{\displaystyle n}يدرك حقيقة أنو{\displaystyle f}يرسلx{\displaystyle x}لy{\displaystyle y}أو "يدركو(x)=y{\displaystyle f(x)=y}الشروط هي كالتالي:

  • يوجد برنامج يأخذ مُحققًا لـو(x)=y{\displaystyle f(x)=y}ويُخرج مُحققًا لـx{\displaystyle x}ومحقق لـy{\displaystyle y}(للجميع)xX،yY{\displaystyle x\in X,y\in Y}).
  • يوجد برنامج يأخذ مُحققًا لـو(x)=y{\displaystyle f(x)=y}والمحققون لـx=x{\displaystyle x=x'}وy=y{\displaystyle y=y'}، ويُخرج مُحققًا لـو(x)=y{\displaystyle f(x')=y'}(للجميع)x،x،y،y{\displaystyle x,x',y,y'}).
  • يوجد برنامج يأخذ محققيو(x)=y{\displaystyle f(x)=y}وو(x)=y{\displaystyle f(x)=y'}، ويُخرج مُحققًا لـy=y{\displaystyle y=y'}(للجميع)x،y،y{\displaystyle x,y,y'}).
  • يوجد برنامجهـ{\displaystyle e}بحيث يكون ذلك لجميعxX{\displaystyle x\in X}ولجميع المحققينن{\displaystyle n}لx{\displaystyle x}يوجد بعضyY{\displaystyle y\in Y}بحيث يكون الناتجϕهـ(ن){\displaystyle \phi _{e}(n)}يدركو(x)=y{\displaystyle f(x)=y}.

يفترضو{\displaystyle f}هي علاقة وظيفية منX{\displaystyle X}لY{\displaystyle Y}وز{\displaystyle g}هي علاقة وظيفية منY{\displaystyle Y}لZ{\displaystyle Z}التركيبزو{\displaystyle g\circ f}العلاقة الوظيفية منX{\displaystyle X}لZ{\displaystyle Z}يتم تعريفها من خلال السماح للمحققين(زو)(x)=z{\displaystyle (g\circ f)(x)=z}لتكن رموز الأزواج(ر،s){\displaystyle (r,s)}بحيث يكون ذلك لبعضyY{\displaystyle y\in Y}لدينارو(x)=y{\displaystyle r\Vdash f(x)=y}وsز(y)=z{\displaystyle s\Vdash g(y)=z}العلاقة الوظيفية المطابقةبطاقة تعريف{\displaystyle \operatorname {id} }على جسمX{\displaystyle X}يتم تعريفها من خلال السماح للمحققينبطاقة تعريف(x)=y{\displaystyle \operatorname {id} (x)=y}كن مجرد محققين لـx=y{\displaystyle x=y}.

التشكلات منX{\displaystyle X}لY{\displaystyle Y}في الطوبولوجيا الفعالة توجد العلاقات الوظيفية منX{\displaystyle X}لY{\displaystyle Y}، مقسومة لتحديدو{\displaystyle f}وز{\displaystyle g}عندما يوجد برنامج يرسم خرائط لمنفذيو(x)=y{\displaystyle f(x)=y}إلى مُحققيز(x)=y{\displaystyle g(x)=y}(للجميع)x،y{\displaystyle x,y}وبرنامج آخر يرسم خرائط لمنفذيز(x)=y{\displaystyle g(x)=y}إلى مُحققيو(x)=y{\displaystyle f(x)=y}يتم استنباط تركيب التشكلات على الكسور عن طريق التركيب على مستوى العلاقات الوظيفية، وكذلك بالنسبة لتشكلات الهوية.

العلاقة بالتجمعات

ينشأ الموضوع الفعال كإكمال للفئة الأبسط من التجمعات .

التجميع هو مجموعةX{\displaystyle X}مزود بوظيفةR:XP(شمال){\displaystyle R:X\to {\mathcal {P}}(\mathbb {N} )}نرمز إلىنR(x){\displaystyle n\in R(x)}بواسطةنx{\displaystyle n\Vdash x}، يقرأ "ن{\displaystyle n}يدركx{\displaystyle x}كل اجتماعX{\displaystyle X}يمكن اعتبارها موضوعًا للمكان الفعال، من خلال الإعلان عن ذلك.ن{\displaystyle n}يدركx=y{\displaystyle x=y}متىx{\displaystyle x}وy{\displaystyle y}هما متساويان في الواقع ون{\displaystyle n}يدركون ذلك في الجمعيةX{\displaystyle X}(وهكذا، فإن محققيx{\displaystyle x}فيX{\displaystyle X}كموضوع للمكان الفعال، أي محققيx=x{\displaystyle x=x}هم بالضبط من يحققونx{\displaystyle x}فيX{\displaystyle X}(كمجموعة.)

تماثل التجمعاتو:XY{\displaystyle f:X\to Y}هي دالةو:XY{\displaystyle f:X\to Y}بين المجموعات الأساسية بحيث يوجد برنامج، مستقل عنxX{\displaystyle x\in X}، والتي تحدد محققيx{\displaystyle x}إلى مُحققيو(x){\displaystyle f(x)}يُؤدي هذا التشاكل إلى تشاكل في الطوبولوجيا الفعالة، ممثلاً بالعلاقة الوظيفية (التي لا تزال تُرمز إليها بـو{\displaystyle f}) أينو(x)=y{\displaystyle f(x)=y}يتحقق ذلك إذا وفقط إذاو(x){\displaystyle f(x)}يساوي في الواقعy{\displaystyle y}ثمّ مُحققوو(x)=y{\displaystyle f(x)=y}هي أزواج من مُحققx{\displaystyle x}ومحقق لـy{\displaystyle y}.

هذا التطابق يجعل فئة التجمعات فئة فرعية كاملة من الطوبولوجيا الفعالة.

تُعتبر فئة المجموعات فئة فرعية كاملة من فئة التجميعات، وذلك عبر الدالة.{\displaystyle \nabla }التي تحدد مجموعةX{\displaystyle X}إلى التجميع مع المجموعة الأساسيةX{\displaystyle X}حيث يُمثّل كل عنصر بكل عدد طبيعي. وعلى وجه الخصوص، تُعدّ فئة المجموعات أيضًا فئة فرعية كاملة من فئة الطوبولوجيا الفعّالة. [ 1 ] : 117

العمليات التصنيفية في الطوبولوجيا الفعالة

الطوبولوجيا الفعالة هي طوبولوجيا أولية تحتوي على كائنات الأعداد الطبيعية . وهذا يعني أنها تدعم عددًا من البنى الفئوية القياسية، والتي يتم تنفيذها بشكل صريح على النحو التالي.

  • الكائن الأولي هو التجميع الفارغ.
  • الكائن النهائي هو وحدة التجميع، وهو عنصر فريد حيث يتم تحقيق العنصر الفريد بواسطة كل عدد طبيعي.
  • كائن الأعداد الطبيعية هوشمال{\displaystyle \mathbb {N} }حيث لا يتحقق كل عدد طبيعي إلا بمفرده.
  • ناتج ضرب عنصرينX{\displaystyle X}وY{\displaystyle Y}هو حاصل الضرب الديكارتي للمجموعاتX×Y{\displaystyle X\times Y}حيث يكون محققًا لـ(x،y){\displaystyle (x,y)}فيX×Y{\displaystyle X\times Y}هو رمز زوج من مُحققx{\displaystyle x}ومحقق لـy{\displaystyle y}.
  • المنتج الثانوي لـX{\displaystyle X}وY{\displaystyle Y}هو نتاج مشترك للمجموعاتX+Y{\displaystyle X+Y}حيث يكون محققًا لـxX{\displaystyle x\in X}فيX+Y{\displaystyle X+Y}هو رمز زوج من 0 ومحقق لـx{\displaystyle x}فيX{\displaystyle X}ومحقق لـyY{\displaystyle y\in Y}فيX+Y{\displaystyle X+Y}هو رمز زوج من 1 ومحقق لـy{\displaystyle y}فيY{\displaystyle Y}.
  • مصنف الكائنات الفرعيةΩ{\displaystyle \Omega }يكونP(شمال){\displaystyle {\mathcal {P}}(\mathbb {N} )}حيث يكون محققًا لـP=سؤال{\displaystyle P=Q}هو زوج من برنامج يُرجع عنصرًا منسؤال{\displaystyle Q}بالنظر إلى عنصر منP{\displaystyle P}وبرنامج يُعيد عنصرًا منP{\displaystyle P}بالنظر إلى عنصر منسؤال{\displaystyle Q}. إنه ليس (متماثلًا مع) تجميعًا.

ملكيات

العلاقة بالمجموعات

تُظهر بعض الأشياء خاصية وجود تافهة تعتمد فقط على صحة علاقة المساواة.={\displaystyle =}"من المجموعات، بحيث يتم تعيين المساواة الصحيحة إلى المجموعة العلياشمال{\displaystyle \mathbb {N} }ورفضت خرائط المساواة لـ{}{\displaystyle \{\}}وهذا يؤدي إلى دالة كاملة وأمينة:Sهـتsهـوو{\displaystyle \nabla \colon {\mathsf {Sets}}\to {\mathsf {Eff}}}خارج فئة المجموعات ، والتي تحتوي على دالة المقاطع العالمية التي تحافظ على النهاية المحدودةΓ{\displaystyle \Gamma }باعتبارها مصفوفة المرافق الأيسر لها . ويؤثر هذا على عملية تضمين كاملة ودقيقة تحافظ على حدودها المحدودة.ω{\displaystyle \omega }-Sهـتsهـوو{\displaystyle {\mathsf {Sets}}\to {\mathsf {Eff}}}.

NNO

يحتوي الكائن الطوبولوجي على كائن أعداد طبيعيةشمال=شمال،هـشمال{\displaystyle N=\langle {\mathbb {N} },E_{\mathbb {N} }\rangle }ببساطةهـشمال(ن)={ن}{\displaystyle E_{\mathbb {N} }(n)=\{n\}}جمل صحيحة حولشمال{\displaystyle N}هي بالضبط الجمل التي يتم تحقيقها بشكل متكرر في حساب هيتينغحأ{\displaystyle {\mathsf {HA}}}.

الأسهم الآنشمالشمال{\displaystyle N\to N}يمكن فهمها على أنها الدوال التكرارية الكلية، وينطبق هذا أيضًا داخليًا علىشمالشمال{\displaystyle N^{N}}أما الأخير فهو الزوج المعطى بواسطة الدوال التكرارية الكليةتيR{\displaystyle \mathrm {TR} }وعلاقة بحيثهـتيR(و){\displaystyle E_{\mathrm {TR} }(f)}هي مجموعة الرموزهـشمال{\displaystyle e\in {\mathbb {N} }}لو{\displaystyle f}تُعدّ المجموعة الأخيرة مجموعةً فرعيةً من الأعداد الطبيعية، ولكنها ليست مجموعةً منفردةً تمامًا، إذ توجد عدة مؤشرات تحسب نفس الدالة التكرارية. لذا، يُمثّل المدخل الثاني للكائنات البيانات المُحقّقة.

معشمال{\displaystyle N}والدوال الصادرة والواردة إليها، بالإضافة إلى قواعد بسيطة لعلاقات المساواة عند تكوين المنتجات المحدودة×{\displaystyle \times }ويمكن الآن تعريف العمليات الفعالة وراثيًا بشكل أوسع. ومرة ​​أخرى، يمكن التفكير في الوظائف فيشمالشمال{\displaystyle N^{N}}كما هو موضح بواسطة المؤشرات، ويتم تحديد تساويها بواسطة الكائنات التي تحسب نفس الوظيفة. من الواضح أن هذا التساوي يفرض قيدًا علىشمال(شمالشمال){\displaystyle N^{(N^{N})}}لأن هذه الدوال لا تُعدّ إلا تلك الدوال القابلة للحساب التي تحترم المساواة المذكورة في نطاقها. وهكذا. الوضع بالنسبة للحالة العامةX،هـXY،هـY{\displaystyle \langle X,E_{X}\rangle \to \langle Y,E_{Y}\rangle }المساواة (بمعنىهـ{\displaystyle E}يجب احترام ('s) في المجال والصورة.

الخصائص والمبادئ

وبهذا، يمكن للمرء أن يثبت صحة مبدأ ماركوفمP{\displaystyle {\mathrm {MP} }}ومبدأ الكنيسة الموسعةهـجتي0{\displaystyle {\mathrm {ECT} }_{0}}(وصيغة من الدرجة الثانية منه)، والتي تُختزل إلى عبارة بسيطة حول كائن مثلشمالشمال{\displaystyle N^{N}}أو(1+1)شمال{\displaystyle (1+1)^{N}}وهذا يعنيجتي0{\displaystyle {\mathrm {CT} }_{0}}واستقلالية الفرضيةأناP0{\displaystyle {\mathrm {IP} }_{0}}.

مبدأ الاختيارشمالشمال{\displaystyle N^{N}}يرتبط هذا بفشل الاستمرارية الضعيفة لبروري . من أي كائن، يوجد عدد محدود من الأسهم إلىشمال{\displaystyle N}. Ωشمال{\displaystyle \Omega ^{N}}يحقق مبدأ التوحيد. شمال{\displaystyle N}ليس ناتجًا ثانويًا قابلًا للعد لنسخ من1{\displaystyle 1}هذا الموضوع ليس فئة من فئات الحزم.

تحليل

الشيءسؤالشمال،هـسؤالشمال{\displaystyle \langle {\mathbb {Q} }^{\mathbb {N} },E_{{\mathbb {Q} }^{\mathbb {N} }}\rangle }يُعدّ هذا المفهوم فعالاً من الناحية الشكلية، ومنه يُمكن تعريف متتابعات كوشي القابلة للحساب . ومن خلال عملية القسمة، يمتلك هذا الفضاء الطوبولوجي كائنًا من الأعداد الحقيقية لا يحتوي على أي كائن فرعي قابل للتقرير غير تافه . وباختيار الأعداد الحقيقية، يتطابق مفهوم أعداد ديديكيند الحقيقية مع مفهوم أعداد كوشي.

الخصائص والمبادئ

يتوافق التحليل هنا مع المدرسة التكرارية للبنائية. وهو يرفض الادعاء بأنx00x{\displaystyle x\leq 0\lor 0\leq x}وينطبق هذا على جميع العوالم الحقيقيةx{\displaystyle x}تفشل صياغات نظرية القيمة المتوسطة، وتُثبت أن جميع الدوال من الأعداد الحقيقية إلى الأعداد الحقيقية متصلة . توجد متتالية سبيكر، وبالتالي تفشل نظرية بولزانو-ويرستراس .

انظر أيضاً

مراجع

  1. 1 2 جاب فان أوستن (2008). إمكانية الواقعية: مقدمة لجانبها القاطع . إلسفير ساينس. رقم ISBN 9780444515841.