מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

5.1.4.4. משפט השלמות של H

אם $plot:$ \vDash \left\{ p \right\}S\left\{ q \right\}$$ אז $plot:${ \vdash _H}\left\{ p \right\}S\left\{ q \right\}$$

זוהי שלמות יחסית. נסביר מהי שלמות יחסית ומדוע השלמות של H היא כזו. השלמות אינה מתקיימת תמיד במקרה של H, עקב מספר נושאים:

לא תמיד ניתן לבטא את תנאי ההתחלה והסיום באמצעות לוגיקה כלשהי. (כוח הביטוי של הלוגיקה מוגבל). לפיכך יתכנו מקרים נכונים שפשוט אין לנו דרך לבטא אותם בכתב.
ידוע לפי משפט אי השלמות של גדל (משפט שחורג מתחום מסמך זה) שעבור המספרים השלמים אין מע' ההוכחה שלמה.

מכיוון שכך, אנו אומרים כי "אם אין בעיות בלוגיקה מסדר ראשון בה אנו משתמשים", אז מתקיימת שלמות. לכן אנחנו לא נדרשים להוכיח טענות לוגיקה מסדר ראשון בכלל CONS. כלומר, אנחנו עדיין צריכים להסתכל שהטענות ב-CONS נכונות, אבל אנחנו בודקים אותן בעזרת ידע מוקדם. לדוגמא – אנחנו מסתכלים על הטענות $plot:$x < 1 \to x < 10$$ ואומרים – "הטענה נכונה (ARITH) לפי ידע קודם ממתמטיקה".