ארכיון התג: מערכות הוכחה

מערכת הוכחה ללוגיקה מסדר ראשון

פורסם בתאריך על ידי
3

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

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

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

  1. \(\alpha\to\left(\beta\to\alpha\right)\)
  2. \(\left[\alpha\to\left(\gamma\to\beta\right)\right]\to\left[\left(\alpha\to\gamma\right)\to\left(\alpha\to\beta\right)\right]\)
  3. \(\left(\neg\alpha\to\neg\beta\right)\to\left(\beta\to\alpha\right)\)

אלו "תבניות" כי במקום \(\alpha,\beta,\gamma\) אפשר להציב פסוקים כלשהם. באותו האופן התבניות הללו יהיו שייכות גם למערכת ההוכחה של לוגיקה מסדר ראשון, כאשר במקום \(\alpha,\beta,\gamma\) מציבים נוסחאות כלשהן בלוגיקה מסדר ראשון. תבנית כזו היא בעלת התכונה הסמנטית שלא חשוב מה נציב בה – בכל מבנה ובכל השמה, הפסוק שמתקבל מההצבות הללו יהיה בעל ערך אמת, ואפילו אם הנוסחאות שמציבים הן מורכבות וכללות כמתים ופונקציות ואקשן. הסיבה פשוטה: אם מחשבים את ערך האמת של הפסוק שמתקבל מההשמות, בסופו של דבר נקבל שכל מה שהצבנו במקום \(\alpha\) מתורגם לאחד משניים: או \(\mbox{T}\) או \(\mbox{F}\), וכך גם עבור \(\beta,\gamma\), מה שאומר שלא משנה איזו נוסחה מורכבת אפשר להציב במקום \(\alpha,\beta,\gamma\), עדיין תחת מבנה והשמה נתונים הם מתנהגים כמו משתנים בתחשיב הפסוקים, ולכן תבנית אקסיומה שהייתה טאוטולוגיה בתחשיב הפסוקים נותרת כזו גם כעת.

כלל ההיסק שלנו בתחשיב הפסוקים היה מודוס פוננס, \(\mbox{MP}\), שמתוך \(\alpha\) ו-\(\alpha\to\beta\) גזר את \(\beta\). נשתמש בו גם כעת. כפי שראינו, זה מספיק כדי לגזור כל טאוטולוגיה בתחשיב הפסוקים. הבעיה היא שבלוגיקה מסדר ראשון יש עוד דברים. מן הסתם יהיו אלה דברים שקשורים לכמתי ה"קיים" ו"לכל" שאין משהו דומה להם בתחשיב הפסוקים. בואו ניתן דוגמה:

\(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\)

זו נוסחה שמשתמשת בסימן יחס חד-מקומי \(R\), ויש בה משתנה קשור אחד \(x\) ומשתנה חופשי אחד \(y\). בכל מבנה \(\mathcal{M}\) ערך האמת של הרישא של הפסוק – \(\forall x\left(R\left(x\right)\right)\) – נקבע באופן יחיד, והוא יהיה \(\mbox{T}\) אם ורק אם \(R^{\mathcal{M}}=D^{\mathcal{M}}\), כלומר אם היחס \(R\) מתפרש ב-\(\mathcal{M}\) בתור "כל העולם". כעת, אם הערך של \(\forall x\left(R\left(x\right)\right)\) הוא \(\mbox{F}\) אז הנוסחה כולה היא תמיד בעל ערך אמת \(\mbox{T}\); ואילו אם ערך האמת שלו הוא \(\mbox{T}\) אז \(R^{\mathcal{M}}=D^{\mathcal{M}}\) ולכן לכל השמה אפשרית, לא משנה איזה ערך היא נותנת ל-\(y\), יתקיים ש-\(R\left(y\right)\) הוא \(\mbox{T}\) ולכן שוב הנוסחה כולה תהיה \(\mbox{T}\). במילים אחרות, הנוסחה \(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\)היא בעלת ערך האמת \(\mbox{T}\) בכל מבנה ובכל השמה אפשריים. לנוסחה בעלת התכונה הזו אני קורא אמת לוגית, ובכוונה אני לא קורא לה "טאוטולוגיה" כמו בתחשיב הפסוקים. במילה "טאוטולוגיה" בלוגיקה מסדר ראשון אני משתמש כדי לתאר את מה שמתקבל מלקיחת טאוטולוגיה בתחשיב הפסוקים ואז הצבת נוסחאות בתור המשתנים, ואילו \(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\) בבירור לא יכול להתקבל בצורה הזו. הדרך היחידה שבה הוא יכול להתקבל היא על ידי הצבה בפסוק \(X\to Y\), אבל הפסוק הזה כלל אינו טאוטולוגיה.

זה מראה לנו שהסיבות לכך ש-\(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\) היא אמת לוגית הן עמוקות יותר מאשר הסיבות לכך שנוסחה כמו \(\forall x\left(R\left(x\right)\right)\to\left(R\left(y\right)\to\forall x\left(R\left(x\right)\right)\right)\) היא אמת לוגית; השניה מתקבלת מהצבה בפסוק \(X\to\left(Y\to X\right)\) שהוא כן טאוטולוגיה של תחשיב הפסוקים, ולכן ערך האמת שלה נובע במובן מסויים רק מתכונות הקשרים (\(\to\) במקרה הזה), בעוד שערך האמת הלוגית של \(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\) נובע גם מתכונות הכמתים (שימו לב: אם נחליף את \(\forall\) ב-\(\exists\) נקבל משהו שאינו אמת לוגית). אני מקווה שזה עוזר להבין למה מה שעשינו בתחשיב הפסוקים רחוק מלהיות מספיק גם בתחשיב היחסים.

הנוסחה שלעיל מרמזת על סוג חדש של תבנית אקסיומה שנזדקק לו. אבל איך אפשר לפרמל אותה? בואו נראה עוד כמה דוגמאות לפני שנציג את המקרה הכללי. ראשית, הביטו בנוסחה הזו:

\(\forall x\left(\exists y\left(x+y>c\right)\right)\to \left(\exists y\left(z+y>c\right)\right)\)

כאן המשתנים \(x,y\) הם קשורים ואילו \(z\) הוא המשתנה החופשי; \(c\) הוא סימן קבוע, \(+\)הוא סימן פונקציה ו-\(>\) הוא סימן יחס. לא קשה לראות שגם הנוסחה הזו היא אמת לוגית. מה הדמיון בינה ובין הנוסחה הקודמת שהצגתי? בשתיהן יש "לכל \(x\) משהו עבור \(x\) גורר משהו עבור \(y\)". שם ה"משהו" היה \(R\left(x\right)\) וכאן ה"משהו" הוא \(\exists y\left(x+y>c\right)\) . באופן כללי "משהו" כזה יכול להיות כל נוסחה, אפילו נוסחאות שבהן \(x\) בכלל לא מופיע. אז לכאורה הצורה של האקסיומה צריכה להיות \(\forall x\varphi\to\varphi\), אבל הצורה הזו לא כללית מספיק. היא מסוגלת ליצור משהו כמו \(\forall x\left(R\left(x\right)\right)\to R\left(x\right)\), אבל הוא לא מסוגלת ליצור משהו כמו \(\forall x\left(R\left(x\right)\right)\to R\left(y\right)\).

אם כן, אולי אפשר לומר שהצורה של האקסיומה תהיה \(\forall x\varphi\to\psi\), כאשר \(\psi\) מתקבל מ-\(\varphi\) על ידי שינוי השם של המשתנה \(x\). זה כבר יותר בכיוון, אבל הנה נוסחה שהיא אמת לוגית ולא יכולה להתקבל כך:

\(\forall x\left(x\ge0\right)\to\left(1\ge0\right)\)

כאן \(0,1\) הם סימני קבועים של השפה ו-\(\ge\) הוא סימן יחס. כאן כבר לא סתם שינינו את השם של \(x\) אלא ממש החלפנו אותו בקבוע. ואפשר היה לעשות גם משהו כזה:

\(\forall x\left(x\ge0\right)\to\left(\left(1+z\right)^{2}\ge0\right)\)

כאשר כאן העלאה בריבוע היא סימן פונקציה, וגם חיבור הוא סימן פונקציה. מה שקרה הוא שהחלפנו את \(x\) בשם עצם: \(\left(1+z\right)^{2}\). אם כן, אפשר לומר שהצורה של האקסיומה תהיה \(\forall x\varphi\to\psi\) כאשר \(\psi\) מתקבל מ-\(\varphi\) על ידי החלפת כל מופע של \(x\) בשם עצם ספציפי כלשהו \(t\). זה בהחלט בכיוון, אבל זה כבר כללי יותר מדי. אם נעשה את זה, אנחנו עלולים לקבל נוסחאות שאינן אמיתות לוגיות. הנה דוגמה. ניקח את \(\varphi\) להיות \(\exists y\left(y>x\right)\) ואת \(t\) להיות \(y\) ונקבל:

\(\forall x\left(\exists y\left(y>x\right)\right)\to\exists y\left(y>y\right)\)

וזה בבירור לא פסוק שהוא אמת לוגית, כי קחו בתור מודל את המספרים הטבעיים – לכל מספר טבעי \(x\) קיים מספר גדול ממנו \(y\), אבל אין אף מספר טבעי שגדול מעצמו. מה השתבש? הבעיה היא שאנחנו משתמשים ב-\(y\) בתפקיד כפול: בתוך \(\varphi\) הוא משתנה מכומת, בעוד ש-\(x\) הוא משתנה חופשי בתוך \(\varphi\). בכך שאנחנו מציבים את \(y\) במקום \(x\) אנחנו הופכים משהו שלפני שניה היה חופשי (ולכן לא מושפע מהכמת \(\exists y\)) למשהו קשור (שכן מושפע מהכמת הזה). זה סוג שינוי שאנחנו חייבים למנוע. זה מוביל אותנו להגדרה שהיא קצת קשה לעיכול אם לא רואים לה קודם מוטיבציה: שם עצם \(t\) הוא חופשי להצבה במקום \(x\) בפסוק \(\varphi\) אם \(t\) לא מכיל אף משתנה \(y\) כך שיש מופע חופשי של \(x\) ב-\(\varphi\) שנופל תחת כמת עבור \(y\). זו הגדרה מסובכת מבחינה מילולית, אבל העיקרון ברור – אנחנו לא רוצים להחליף את \(x\) במשהו, ואז לגלות שבתוך המשהו היה משתנה שפתאום הופך להיות מכומת.

עוד נקודה שצריך לשים לב אליה היא ש-\(\varphi\) עשוי להכיל גם מופעים לא חופשיים של \(x\), ובהם אסור להציב. זה מקרה קצה מוזר למדי אבל עדיין יש להתחשב בו. הנה דוגמה: ניקח בתור \(\varphi\) את \(\exists x\left(x>0\right)\) ובתור \(t\) את הקבוע \(0\), ונקבל:

\(\forall x\left(\exists x\left(x>0\right)\right)\to\left(\exists x\left(0>0\right)\right)\)

שהוא כמובן לא נכון. הבעיה כאן היא הפוכה ביחס לבעיה הקודמת: קודם הפכנו מישהו לא מכומת למכומת, ואילו כאן אנחנו משתמשים בהצבה לתוך \(x\) כדי "להימלט" מהכמת \(\exists x\). הפתרון הוא פשוט למדי: לא מציבים את \(t\) בתוך מופעים מכומתים של \(x\) ב-\(\varphi\) אלא רק במופעים החופשיים שלו.

עכשיו אפשר סוף סוף לנסח את תבנית האקסיומה במפורש. התבנית היא:

  1. \(\forall x\varphi\to\psi\)

כאשר \(\psi\) מתקבל מ-\(\varphi\) על ידי הצבה בכל מופע חופשי של \(x\) ב-\(\varphi\) שם עצם \(t\) כלשהו שהוא חופשי להצבה במקום \(x\) ב-\(\varphi\).

צריך כמובן להוכיח שכל נוסחה כזו היא אכן אמת לוגית, מה שניתן לעשות באופן ישיר למדי הישר מהגדרות הסמנטיקה של לוגיקה מסדר ראשון ואוותר על כך כאן (ההוכחה דומה למה שעשיתי לעיל עבור \(\varphi=R\left(x\right)\)).

בואו נעבור להתבונן על נוסחה אחרת שעדיין אין לנו יכולת להוכיח במערכת שלנו:

\(\forall x\left(R\left(y\right)\to S\left(x\right)\right)\to\left(R\left(y\right)\to\forall xS\left(x\right)\right)\)

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

הפורמליזציה של תבנית האקסיומה הזו פשוטה:

  1. \(\forall x\left(\varphi\to\psi\right)\to\left(\varphi\to\forall x\psi\right)\)

כאשר הדרישה היא ש-\(x\) איננו משתנה חופשי ב-\(\varphi\). קל לראות שהדרישה הזו הכרחית כדי שהתבנית תגדיר נוסחאות אמיתיות לוגיות; בואו נביט על \(\forall x\left(x>0\to x>0\right)\to\left(x>0\to\forall x\left(x>0\right)\right)\) שהוא בבירור לא אמת לוגית – אגף ימין שלו בבירור מתקיים אבל אגף שמאל אומר שאם \(x\) ספציפי הוא גדול מאפס אז נובע מכך שכל \(x\) הוא גדול מאפס וזה בוודאי לא נכון.

האם באמת היה צריך להוסיף את תבנית האקסיומה החדשה הזו? האם אי אפשר לקבל אותה מהדברים הקיימים? לא ממש. התבנית הקודמת שהצגתי יודעת להסיר \(\forall\); היא לא יודעת להזיז אותו. זה מרמז גם על מה שעדיין חסר לנו – דרך לייצר \(\forall\). לצורך כך אוסיף כלל היסק חדש שנקרא \(\mbox{Gen}\) (מלשון Generalization – הכללה). הכלל מקבל פסוק \(\varphi\) ומייצר ממנו את \(\forall x\varphi\) עבור משתנה כלשהו \(x\), וניתן להשתמש בו גם כאשר \(x\) כן מופיע חופשי ב-\(\alpha\). עם זאת, יש עליו סייג קטן: אם \(\Phi\) היא קבוצת ההנחות שבה אנחנו משתמשים בהוכחה שלנו, אסור להשתש ב-Gen עבור אף משתנה \(x\) שמופיע חופשי בהנחה כלשהי ב-\(\Phi\). אצלנו ממילא אנחנו הולכים לדבר רק על קבוצת הנחות שהן פסוקים, כלומר נוסחאות בלי משתנים חופשיים, כך שהסייג הזה לא יהיה רלוונטי לנו ונוכל להשתמש ב-Gen בחופשיות.

תחת הסייג הזה פשוט למדי להוכיח ש-Gen עובד: נניח ש-\(\Phi\models\varphi\), כלומר כל מבנה \(\mathcal{M}\) והשמה \(z\) מקיימים שאם \(\mathcal{M}\models_{z}\Phi\) אז \(\mathcal{M}\models_{z}\varphi\). כדי להראות ש-\(\mathcal{M}\models_{z}\forall x\varphi\) צריך להראות שמתקיים \(\mathcal{M}\models_{z\left[x\leftarrow a\right]}\varphi\) לכל \(a\in D^{\mathcal{M}}\). כעת, מכיוון ש-\(x\) לא מופיע חופשי באף הנחה ב-\(\Phi\) הרי ש-\(\mathcal{M}\models_{z\left[x\leftarrow a\right]}\Phi\) (השינוי של הערך ש-\(x\) מקבל בהשמה \(z\) לא משפיע על ערך האמת ש-\(z\) נתנה לפסוקי \(\Phi\)) ולכן \(\mathcal{M}\models_{z\left[x\leftarrow a\right]}\varphi\).

האם סיימנו להציג את מערכת ההוכחה? תלוי. בהגדרות מסויימות של לוגיקה מסדר ראשון, כן; אבל אני הגדרתי לוגיקה מסדר ראשון כשהיא כוללת את סימן השוויון, והוא זקוק לטיפול מיוחד, מכיוון שהסמנטיקה שלו מיוחדת. הדרך הפשוטה ביותר להבין זאת היא להיות מודעים לכך שכרגע אין למערכת ההוכחה שלנו שום דרך להוכיח את הנוסחה הבאה:

\(x=x\)

די ברור שאפשר להוסיף אותה כתבנית אקסיומה, אבל זה עדיין לא מספיק. צריך עוד תבנית אקסיומה שתגיד לנו שאם שני משתנים הם שווים בערכם, אז כל שני שמות עצם שזהים פרט לאותם משתנים גם כן שווים בערכם, וכל שתי נוסחאות שזהות פרט לאותם משתנים הן שקולות. פורמלית, אז אלו האקסיומות שקשורות לשוויון (\(x,y\) מייצגים משתנים, \(t,s\) מייצגים שמות עצם, \(\varphi,\psi\) מייצגים נוסחאות):

  1. \(x=x\)
  2. \(x=y\to t=s\) כאשר \(s\) מתקבל מ-\(t\) על ידי החלפת מופע אחד או יותר של \(x\) ב-\(y\).
  3. \(x=y\to\left[\varphi\to\psi\right]\) כאשר \(\psi\) מתקבל מ-\(\varphi\) על ידי החלפת מופע אחד או יותר של \(x\) ב-\(y\).

האם סיימנו? באופן מפתיע למדי, התשובה היא כן! מסתבר שדי באקסיומות וכללי ההיסק שהראיתי כדי להוכיח כל פסוק בלוגיקה מסדר ראשון שנובע לוגית מקבוצת פסוקים של הנחות. כלומר, כעת אני יכול להוכיח את משפט השלמות והנאותות הבא: אם \(\Phi\) היא קבוצת פסוקים בלוגיקה מסדר ראשון ו-\(\varphi\) הוא פסוק כלשהו, אז \(\Phi\vdash\varphi\iff\Phi\models\varphi\). את ההוכחה אתחיל להציג בפוסט הבא.

אז מה זה IP=PSPACE?

פורסם בתאריך על ידי
2

מה היא הוכחה? מילון אבן-שושן מגדיר אותה כ"ראיה, אות לדבר כי אמנם כן הוא, הבאת מופת לאישור דבר". ויקיפדיה העברית מדברת על "סדרה סופית של טענות הנובעות זו מזו בעזרת כללי היסק, תוך שימוש בהגדרות, באקסיומות, ובידע קודם שהוכח קודם לכן, המראה שטענה מסוימת היא נכונה". מי צודק? ההגדרה של ויקיפדיה היא יותר קונקרטית, ומתאימה למושג הפורמלי של "הוכחה" שאותו לומדים בקורסים בלוגיקה; אולם ההגדרה שיותר מתאימה למשמעות היומיומית והכללית שאנו מייחסים למילה הוכחה היא כמובן זו של אבן-שושן. הוכחה, בראש ובראשונה, היא משהו שבא לשכנע אותנו שטענה כלשהי היא נכונה. האופן הספציפי שבו ההוכחה מבצעת הדבר הזה הוא מה שמבדיל בין סוגים שונים של הוכחות, וביניהן ההוכחה המתמטית שעליה ויקיפדיה העברית מדברת.

הוכחה במדעי הטבע לרוב תבוא בצורת נתונים אמפיריים התואמים לטענה מסויימת. כך זוכה מכניקת הקוונטים, שהניסוח המתמטי-פורמלי שלה והפרשנויות שמסבירות כיצד הוא מתיישב עם המציאות הם מאוד לא אינטואיטיביים, להילה של תורה מוכחת בגלל שהניבויים שהיא מספקת לניסויים אמפיריים מתגלים שוב ושוב כנכונים. כשהולכים למקומות אחרים במדעי הטבע מגלים שמושג ה"הוכחה" הוא עוד יותר מעורפל – מצד אחד תומכי האבולוציה טוענים שהיא הוכחה מעבר לכל ספק סביר – "האבולוציה היא עובדה", ומצד שני מתנגדיה טוענים שהכל בולשיט. אם ממשיכים לחפור עוד קצת נתקלים באנשים בעלי גישה קצת שונה למדעי הטבע, שטוענים טענות על קיום יצורים מסויימים – למשל, מפלצת ספגטי מעופפת – איך מוסיפים שקיום זה כלל לא ניתן להוכחה, או שהוכחה אינה נדרשת.

כל בלבול המוח הזה מוביל לכך שנהוג להגיד שבמדעי הטבע אין הוכחות בטוחות במאה אחוזים, אלא "רק במתמטיקה". המתמטיקה זוכה בציבור הרחב לעתים קרובות להילה של "התחום שבו אפשר לדעת בודאות אם דברים הם נכונים או לא". הכלי מספר 1 שבו המתמטיקה משתמשת למטרה זו הוא מושג ההוכחה שויקיפדיה הזכירה למעלה – סדרות סופיות של טענות, כך שכל טענה היא או אקסיומה, או נובעת מטענות קודמות בעזרת כללי היסק. אלא שכאן מתחילות הצרות – מי מבטיח לנו שהאקסיומות נכונות? מי מבטיח לנו שכללי ההיסק נכונים? ואפילו היו האקסיומות וכללי ההיסק נכונים, מי מבטיח לנו שהוכחה היא נכונה – כלומר, שמה שנכתב בה הוא אכן אקסיומה ושכל טענה נובעת מקודמותיה בעזרת כללי ההיסק?

התשובה היא ששום דבר לא מבטיח לנו את זה. ייתכן שיש שד מתעתע שגורם לנו להאמין באקסיומות וכללי היסק שגויים או לקרוא לא נכון הוכחות. אולי אנחנו חיים במטריקס ומיוצרת בנו אמונה לגבי דברים שגויים. אבל גם אם אין מטריקס ואין שדים מתעתעים, אין לנו דרך "להוכיח" שהאקסיומות וכללי ההיסק נכונים; איך נוכיח זאת? בשיטה המתמטית, עם אקסיומות וכללי היסק? יש כאן בעיה מעגלית, ואין שום דרך לצאת ממנה.

אם כן, לא הייתי אומר שהוכחה-של-ויקי-העברית "מראה" שטענה כלשהי היא נכונה; לדעתי יותר נכון לומר שהיא מהווה ראיה לכך שהטענה נכונה. כלומר, עוד גורם במכלול הגורמים שבאים לשכנע אותנו, קוראי ההוכחה, בנכונותה. בזאת ההוכחה המתמטית היא מקרה פרטי של ההוכחה של אבן-שושן, ולמרות הכבוד הרב שהיא זוכה לו כיום בציבור, צריך להיזהר ולא לתת לה מונופול.

בואו נביט שניה בהוכחה מתמטית "אמיתית" – הוכחת אוקלידס לקיום אינסוף ראשוניים. נניח שיש רק מספר סופי של ראשוניים, \(p_{1},\dots,p_{n}\). נתבונן במספר \(p_{1}\cdot p_{2}\cdots p_{n}+1\). הוא אינו מתחלק על ידי אף אחד מהראשוניים \(p_{1},\dots,p_{n}\) ולכן מתחלק על ידי ראשוני שונה מהם. זו כל ההוכחה, ועבור המתמטיקאים בקהל אני בטוח שהיא מספיקה, אבל האם זו הייתה "סדרה סופית של טענות הנובעות זו מזו בעזרת כללי היסק תוך שימוש באקסיומות"? היכן האקסיומות? מיהם כללי ההיסק? גרוע מכך – ההוכחה הזו מבצעת הרבה קפיצות לוגיות שעבור מתמטיקאי הן טריוויאליות אבל עבור מי שמעולם לא ראה אותן הן אסון. למה ש-\(p_{1}\cdots p_{n}+1\) לא יתחלק על ידי אף אחד מהראשוניים \(p_{1},\dots,p_{n}\)? ולמה שהוא כן יתחלק על ידי ראשוני שונה מהם? אלו דברים שדורשים הסבר – למעשה, הוכחה – בפני עצמם. ויקיפדיה העברית מכסה זאת בעזרת "ידע קודם שהוכח קודם לכן", אבל כשקוראים הוכחות אמיתיות לא תמיד ברור בכלל לאיזה ידע קודם ההוכחה מתייחסת. בהוכחות אמיתיות (כאלו שנמצאות בספרי לימוד מתקדמים; בספרי מבוא לרוב ההוכחות יותר ידידותיות) יש המון קפיצות מעל פרטים שרק קורא שבקיא בחומר מסוגל להשלים; קוראים אחרים נאלצים לפנות לעזרה לאתרים כמו MathOverflow ו-MathStackExchange.

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

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

בואו נעבור לדבר באופן טהור על גישתם של מדעי המחשב לכל העסק הזה. עבור מדעני המחשב, "טענה" היא בסך הכל סדרה סופית של תווים מעל א"ב כלשהו (למשל, כזה שבו יש רק שתי אותיות – 0 ו-1; שני אלו מספיקים כדי לקודד כל דבר וזה בדיוק מה שקורה במחשבים). לסדרה סופית כזו של תווים קוראים "מילה", ולקבוצה כלשהי של מילים קוראים "שפה" ומסמנים אותה ב-\(L\) לרוב. היעד של מערכות ההוכחה שלנו הוא להראות עבור מילה \(w\) כלשהי כי \(w\in L\). אם \(L\) היא אוסף כל המחרוזות אשר מקודדות טענות נכונות במתמטיקה ו-\(w\) היא המחרוזת "יש אינסוף זוגות ראשוניים שההפרש בין אברי הזוג הוא 2", הרי שלהראות \(w\in L\) במקרה הזה זה בעצם "להוכיח את השערת הראשוניים התאומים", כך שכל הדיבורים הללו על מילים ושפות לא באמת מגבילות את מה שאנחנו מסוגלים לדבר עליו, אלא רק נותנות לו פורמליזם שנוח עבורנו. לכל שפה תהיה מערכת הוכחה משל עצמה.

את המושג של "תהליך הבדיקה" ממדלים בצורה פורמלית בעזרת אלגוריתם, \(V\) – "המוודא" (מלשון Verifier). למי שהמושג אלגוריתם מעורפל מדי בשבילו, בדרך כלל דורשים ש-\(V\) הוא מודל חישוב קונקרטי מסויים, דוגמת מכונת טיורינג; אלו לא פרטים שיש צורך להיכנס אליהם כאן. \(V\) מקבל כקלט זוג \(\left(w,\pi\right)\), כש-\(w\) היא מילה כלשהי ו-\(\pi\) היא מחרוזת שמטרתה להוות הוכחה לכך ש-\(w\) שייך ל-\(L\). מ-\(V\) אנחנו דורשים שבהינתן קלט \(\left(w,\pi\right)\), \(V\) יסיים מתישהו את ריצתו על הזוג (אם הוא לא עוצר לעולם, כל העסק חסר ערך מבחינתנו), ויגיד "כן" או "לא". כדי שנוכל לומר שהאלגוריתם \(V\) פועל נכון, נצטרך שיקרו שני דברים:

  1. שלמות: אם \(w\in L\) אז קיימת הוכחה \(\pi\) כלשהי כך ש-\(V\) מסיים את ריצתו על \(\left(w,\pi\right)\) ואומר "כן".
  2. נאותות: אם \(w\notin L\) אז לכל \(\pi\) מתקיים ש-\(V\) מסיים את ריצתו על \(\left(w,\pi\right)\) ואומר "לא".

כלומר, אם \(V\) אומר "כן" הוא בעצם אומר "כן, \(w\in L\) וההוכחה \(\pi\) שכנעה אותי בכך", ואילו אם הוא אומר "לא", הוא בעצם אומר "\(\pi\) לא שכנעה אותי ש-\(w\in L\)" (שימו לב להבדל המהותי בין זה ובין לומר "\(w\notin L\), נקודה").

ההגדרה הזו נותנת המון חופש פעולה ל-\(V\); הוא רק צריך לעצור ולקיים את תנאי השלמות והנאותות, אבל אף אחד לא אומר לו איך בדיוק הוא צריך לבדוק ש-\(w\) נכון, איך הוא אמור להשתמש ב-\(\pi\), וכדומה. למעשה, הוא יכול גם להתעלם מ-\(\pi\) לחלוטין ולבצע בדיקה על \(w\) באופן בלתי תלוי. אם למשל \(L\) היא שפת המספרים הראשוניים, אז \(V\) יכול פשוט לבדוק את כל המחלקים האפשריים של \(w\) ואם לא התגלו מחלקים לא טריוויאליים – לעצור ולהגיד "כן", ואחרת לעצור ולהגיד "לא". בלי שהוא השתמש בכלל ב-\(\pi\) לשום מטרה שהיא.

אם כן, עולה השאלה הטבעית – האם השימוש ב-\(\pi\) – האם המעבר מ"\(V\) בודק דברים לבד" ל-"\(V\) מקבל הוכחה מהעולם החיצון ונעזר בה" – מוסיפה למערכת כוח חישובי? התשובה היא – בהחלט כן.

הבה וניקח כדוגמה את הבעיה העשירית של הילברט. בבעיה הזו נתונה משוואה דיופנטית (משוואה פולינומית במקדמים שלמים), והשאלה היא אם קיים לה פתרון במקדמים שלמים. הילברט ביקש למצוא אלגוריתם לפתרון הבעיה כבר ב-1900, אך רק בשנות השבעים של המאה ה-20 הוכח סופית כי אלגוריתם שכזה אינו קיים. הבה ונקבל כנתון את הטענה הזו (שתזכה יום אחד לפוסט – או סדרת פוסטים – משל עצמה) – זה אומר ש-\(V\) המסכן, אם קיבל \(w\) שמקודדת משוואה דיופנטית, לא יכול לבצע אף חישוב שגם יעצור תמיד וגם יחזיר תמיד את התשובה הנכונה. פורמלית אומרים על כך שהבעיה איננה במחלקה \(\mbox{R}\). מה הוא כן יכול לעשות? ובכן, אם קיים פתרון, אפשר בעזרת חיפוש ממצה למצוא אותו לבסוף, לעצור ולהחזיר אותו. רק מה? אם לא קיים פתרון, החישוב לא יסתיים לעולם (וזה, כזכור, מנוגד באופן חזק לדרישה הבסיסית שלנו מ-\(V\) שיעצור תמיד). על בעיות שניתנות ל"חצי פתרון" שכזה אומרים שהן במחלקה \(\mbox{RE}\).

כעת, לבעיה העשירית של הילברט יש מערכת הוכחה פשוטה למדי: אם \(w\) משוואה דיופנטית בעלת פתרון, אז \(\pi\) יקודד את הפתרון הזה – ההצבה הנדרשת למשתנים. אם \(V\) מקבל \(\left(w,\pi\right)\), הוא פשוט מציב את \(\pi\) לתוך המשוואה ובודק אם המשוואה מתקיימת או לא. אם כן – האח, \(V\) עוצר ומקבל; אחרת, \(V\) עוצר ודוחה. בכל מקרה \(V\) יעצור, ובכל מקרה הוא לא יטעה – אם ל-\(w\) יש פתרון, אז יש \(\pi\) שעבורו \(V\) יקבל (ההצבה ה"נכונה" למשוואה) ואם ל-\(w\) אין פתרון, ברור שלכל \(\pi\) הוא ידחה.

לא קשה להוכיח טענה כללית על מערכות הוכחה שכאלו – השפות שקיימת להן מערכת הוכחה שכזו הן בדיוק השפות שב-\(\mbox{RE}\). מכיוון ש-\(\mbox{RE}\) גדולה יותר מ-\(\mbox{R}\), זה מראה שמערכת ההוכחה שתיארנו מוסיפה כוח חישובי רב.

המחלקות \(\mbox{R}\) ו-\(\mbox{RE}\) שייכות לעולם המופלא של תורת החישוביות – לשאלה מה ניתן לחשב בכלל. העניינים נהיים סבוכים ומעניינים בהרבה כאשר עוברים לעולם המפלא של תורת הסיבוכיות – שבו השאלה היא מה ניתן לחשב ביעילות, כשכאן "יעילות" מזוהה עם "ריצה בזמן שהוא פולינומי בגודל הקלט". לכן אנחנו מדברים פה על מערכת הוכחה שזהה למה שתיארנו קודם פרט לדרישה ש-\(V\) ירוץ בזמן שהוא פולינומי בגודל של \(w\) (וכפועל יוצא מכך נובע ש-\(\pi\) אף הוא צריך להיות פולינומי בגודל \(w\) אחרת \(V\) לא יספיק לקרוא את כולו).

בעולם החדש הזה המחלקה \(\mbox{P}\) היא המקבילה של \(\mbox{R}\), ולמחלקת השפות שיש להן מערכת הוכחה מהסוג שתיארתי קוראים \(\mbox{NP}\). זו, אם כן, המקבילה של \(\mbox{RE}\) בעולם הסיבוכיותי, וכמו שאפשר להוכיח ש-\(\mbox{R}\ne\mbox{RE}\) ולכן הוכחות מוסיפות כוח באופן כללי, עולה השאלה האם \(\mbox{P}\ne\mbox{NP}\) ולכן הוכחות מוסיפות כוח בהקשר של חישובים יעילים. זו, אולי כבר שמעתם, הבעיה הפתוחה המרכזית במדעי המחשב, ואחת מהבעיות הפתוחות החשובות ביותר במתמטיקה באופן כללי. ההשערה היא שאכן \(\mbox{P}\ne\mbox{NP}\), אבל לכו תוכיחו – העולם הסיבוכיותי מאתגר הרבה יותר מהעולם החישוביותי וכבר נתתי דוגמה לכך בעבר.

אלא שכאן הכיף רק מתחיל. אם אנחנו כבר מכלילים את מושג ההוכחה, למה לעצור ב"מחרוזת כלשהי שאותה נותנים ל-\(V\) והוא נעזר בה כדי להכריע את הטענה בזמן יעיל"? את רעיון ההוכחה אפשר להכליל בשתי דרכים יחסית טבעיות – אינטראקציה, ואקראיות.

אינטראקציה אומרת כך – הבה ונניח שלמשחק שלנו מצטרף מתמודד נוסף, \(P\), "המוכיח" (מלשון Prover). בהינתן \(w\) \(P\) ו-\(V\) מנהלים ביניהם דיאלוג כלשהו – \(P\) שולח ל-\(V\) הודעה, ו-\(V\) יכול לענות לו, ו-\(P\) יכול לענות לתשובה, וכן הלאה. בסופו של דבר (ואחרי זמן פולינומי) \(V\) צריך לעצור ולקבל או לדחות את \(w\), ואותם תנאים של קודם תקפים: אם \(w\in L\) אז יש דרך התנהגות של \(P\) שגורמת ל-\(V\) לקבל, ואילו אם \(w\notin L\) אז לא משנה איך \(P\) יתנהג, \(V\) ידחה. בדרך כלל במערכות כאלו אנחנו לא מניחים ש-\(P\) מוגבל חישובית בכלל – כמו שקודם ההוכחה \(\pi\) הגיעה באורח קסום מהשמיים, כך גם כאן \(P\) הוא יצור שמיימי בעל כוח לא מוגבל (בעולם האמיתי הכוח של \(P\) ינבע לרוב מכך שיש לו כבר ידע קודם שאין ל-\(V\); למשל, \(P\) יכיר פירוק לגורמים של מספר \(n=pq\) מסויים בגלל שהוא עצמו הגריל מלכתחילה את \(p,q\) והכפיל אותם לקבלת \(n\)) .

טוב, אז מה נשתנה אם מרשים אינטראקציה? באופן מאכזב למדי, כלום. \(\mbox{NP}\) היא עדיין מחלקת הבעיות שקיימת להן הוכחה, גם עם מוכיח אינטראקטיבי שכזה. הסיבה לכך היא שאת כל מה ש-\(P\) עושה "אינטראקטיבית" אפשר היה לכתוב ב-\(\pi\) מראש, שכן ברור למוכיח בדיוק איך \(V\) הולך להגיב לכל דבר ש-\(P\) יאמר, כי \(V\) הוא דטרמיניסטי. אז ההוכחה תהיה בערך כך: "התשובה לשאלה הראשונה שלך היא: 42. התשובה לשאלה השניה שלך היא: 0. נכון שזה קריפי שאני יודע מה אתה הולך לשאול? נכון? נכון? נכון? טוב, בוא נמשיך, התשובה לשאלה השלישית היא: 42. וואו, השאלות שלך לא מקוריות. טוב, בוא נמשיך…".

איך אפשר להתקדם מכאן? בכמה דרכים. אחת מהדרכים היפות היא מערכת בוררות. במערכת שכזו אין מוכיח אחד אלא שני מוכיחים, שכל אחד מהם רוצה להוכיח משהו שונה. המטרה של אחד מהם היא להוכיח ש-\(w\in L\) והמטרה של השני – ש-\(w\notin L\). ברור שאחד מהם משקר, ולכן הם מנהלים מאבק כלשהו. בינתיים \(V\) יושב בצד ומאזין לויכוח שלהם (הוא לא צריך לשאול שאלות בעצמו כי, כמו קודם, המוכיחים יודעים בדיוק מה הוא הולך לשאול שכן הוא דטרמיניסטי). בסוף הויכוח (שצריך להימשך זמן פולינומי), \(V\) חורץ דין ומחליט האם \(w\in L\) או לא. כרגיל, ל-\(V\) אסור לטעות, בכלל.

האם המערכת הזו מוסיפה כוח? ככל הנראה כן. אפשר להוכיח שמחלקת השפות שיש להן מערכת בוררות שכזו היא \(\mbox{PSPACE}\) – מחלקת כל השפות שניתן להכריע בזכרון פולינומי. \(\mbox{PSPACE}\) היא מחלקה ענקית, שכוללת את \(\mbox{NP}\) וגם הרבה מעבר לכך; אתאר אותה בפוסט הבא יותר בפירוט. מצד שני, אין לנו מושג כיום אם \(\mbox{P}\ne\mbox{PSPACE}\).

הדרך השניה להתקדם מכאן היא להרשות אקראיות. נניח שאנחנו מרשים למוודא לעשות הגרלות שמכתיבות אילו שאלות הוא ישאל את המוכיח. האם שינינו משהו? ובכן, אם כל מה שעשינו הוא להרשות למוודא להגריל שאלות, לא ממש. כי איך תיראה כעת הוכחה \(\pi\) לנכונות טענה? היא תהיה מהצורה "אם היית מגריל 0, אז היית שואל כך וכך, והייתי עונה לך: 42! ואז, אם היית מגריל 1, היית שואל כך וכך והייתי עונה לך: 17! ואחר כך…". כלומר, ההוכחה מתארת מה קורה בסדרת בחירות אקראיות אחת של המוודא ומתעלמת מכל שאר האפשרויות. למה זה עובד? כי בסוף הדיאלוג הזה, התשובה של המוודא חייבת להיות התשובה הנכונה. אם \(w\in L\), כל מה שאנחנו רוצים הוא לראות סדרת בחירות אקראיות אחת שגורמת למוודא להשיב "כן". לא אכפת לנו מכך שיש אולי עוד המון דרכים לגרום לו להשיב כך.

אז כדי לפרוץ את גבולות \(\mbox{NP}\), אנחנו מכניסים לתמונה משהו שנראה כמו חילול הקודש כאשר מדובר על הוכחות – משהו שבאמת משנה לגמרי את התמונה: אנחנו מרשים למוודא לטעות. אנחנו עדיין דורשים שאם \(w\in L\) אז המוכיח יהיה מסוגל לשכנע אותו, ולא משנה מה המוודא שואל; אבל אם \(w\notin L\) אנחנו מרשים למוודא לענות בטעות "כן" בסוף הפרוטוקול. אנחנו רק דורשים שההסתברות לכך תהיה נמוכה. כמה נמוכה? ובכן, כמה שתרצו! אני ארחיב על כך בהמשך. הנקודה היא שלמוודא חייבת להיות הסתברות כלשהי, זניחה ככל שתהיה, לטעות.

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

כמה כוח הוסיפה לנו האפשרות הן לבצע אינטראקיציה והן האקראיות? כלומר, מהי המחלקה \(\mbox{IP}\) של כל השפות שיש להן הוכחה אינטראקטיבית הסתברותית? זו הייתה שאלה פתוחה במשך זמן מה מאז שהוצע המודל. היה ברור לכולם ש-\(\mbox{IP}\subseteq\mbox{PSPACE}\), אבל מה פרט לכך? כשהסתכלו על המחלקות \(\mbox{IP}\left[k\right]\) של מערכות הוכחה שבהן האינטראקציה היא של \(k\) סיבובים בדיוק, התגלה שלא משנה כמה \(k\) גדול – כל עוד הוא קבוע בגודלו ביחס לגודל הקלט, מתקבלת המחלקה \(\mbox{IP}\left[2\right]\). רק כשמרשים למספר הסיבובים בפרוטוקול להיות פולינומי בגודלו ביחס לגודל הקלט יש סיכוי לקבל משהו גדול יותר. מצד שני, אף אחד לא הכיר בעיות שדרשו זאת – כל מה שמצאו לו פרוטוקול הוכחה אינטראקטיבית (ונראה לכך דוגמאות בפוסט הבא) יכל להסתפק במספר קבוע של סיבובים. בנוסף, לא נראה היה שהסתברות אמורה להוסיף הרבה כוח למערכת ההוכחה; הסתברות לא מוסיפה הרבה כוח גם לחישוב רגיל (המחלקה \(\mbox{BPP}\), שהיא המקבילה ההסתברותית של \(\mbox{P}\), איננה גדולה מ-\(\mbox{P}\) בהרבה ויש החושדים ש-\(\mbox{P=BPP}\), ובניגוד ל-\(\mbox{P=NP}\) זה גם לא מופרך).

אם כן, האמונה הרווחת בקרב מדעני המחשב הייתה ש-\(\mbox{IP}\) היא מחלקה חלשה יחסית. ואז ב-1990 הוכיחו ש-\(\mbox{IP=PSPACE}\) (הוכיח את זה עדי שמיר, ה-S שב-RSA, ובאופן בלתי תלוי הוכיחה את זה עוד חבורה שלא אכתוב את כולה). זו באמת הייתה פצצה, בדיוק בגלל ש-PSPACE היא מחלקה כל כך גדולה ו"חזקה". זה היה גילוי מאוד מפתיע גם מבחינה רעיונית – האופן שבו הוכחה אינטראקטיבית היא הרבה, הרבה יותר מאשר הוכחה "קלאסית". וכמובן, ההוכחה של \(\mbox{IP=PSPACE}\) הייתה גם מבריקה בפני עצמה והשתמשה בטכניקות חדשות ביחס למה שהיה קיים אז.

בפוסטים הבאים אתן דוגמה למערכות הוכחה אינטראקטיביות קונקרטיות כדי שנבין על מה בכלל מדובר, אציג קצת יותר את המחלקה PSPACE כדי שנבין למה היא כל כך חזקה, ואז נעבור לאקשן – אוכיח בצורה מלאה כי ש-\(\mbox{IP=PSPACE}\), כולל כל הפרטים הטכניים. יהיה כיף.

משפט ה-PCP או: איך למדתי להפסיק לדאוג ולאהוב הוכחות הניתנות לבדיקה הסתברותית

פורסם בתאריך על ידי
6

אחד מהנושאים הלוהטים ביותר במדעי המחשב המודרניים הוא משפט ה-PCP, הרחבותיו והשלכותיו. אלא שכל הקשור ל-PCP עשוי להישמע מוזר מאוד כששומעים לראשונה מה ראשי התיבות הללו מסמלים: Probabilistically Checkable Proofs, הוכחות הניתנות לבדיקה הסתברותית. מה זה בכלל, ואיך אפשר לזהם מושג טהור כמו "הוכחה" שהיא תמיד ודאית ב-100 אחוז (לפחות כשמדובר על הוכחה "מתמטית") עם המושג הבזוי של "הסתברות"?

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

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

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

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

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

עכשיו, בהינתן גרף המילטוני, איך אפשר להשתכנע בכך שהוא אכן המילטוני? הבה ונקרא למי שמנסה להשתכנע "המוודא" (כי הוא מוודא שהטענה נכונה). המוודא יכול לנסות באופן שרירותי את כל המסלולים בגרף עד שימצא אחד המילטוני (או שלא ימצא, ואז ידע בודאות שהגרף אינו המילטוני). עם זאת, אפשר לעשות לו את החיים קלים יותר ולספק לו מראש תיאור של מסלול המילטוני בגרף – ואז כל מה שיישאר לו לעשות הוא לוודא שאכן התיאור הזה חוקי ומתאים לגרף. אם מישהו רמאי ייתן לו תיאור שקרי, המוודא יעלה על זה בקלות. זה מביא אותנו סוף סוף אל ההגדרה הפורמלית של "מערכת הוכחה עבור השפה \(L\)": היא מורכבת ממוודא \(V\), שאפשר לחשוב עליו בתור אלגוריתם מתוחכם (אבל עדיין אלגוריתם – כזה שכל צעד שלו מוגדר בצורה מדוייקת) שמקבל שני "קלטים" – טענה \(w\), והוכחה \(\pi\). הן הטענה והן ההוכחה הן פשוט מילים; המוודא רץ על שני הקלטים הללו ופולט לבסוף "מקבל" או "דוחה". פורמלית ניתן לכתוב זאת \(V\left(w,\pi\right)=\mbox{acc}\) ו-\(V\left(w,\pi\right)=\mbox{rej}\). הציפיות שלנו ממערכת הוכחה "טובה" (כלומר, ממוודא "טוב") הן שיתקיימו שלוש הדרישות הבאות:

  1. שלמות: לכל \(w\in L\) קיימת הוכחה \(\pi\) כך ש-\(V\left(w,\pi\right)=\mbox{acc}\).
  2. נאותות: לכל \(w\notin L\) ולכל הוכחה \(\pi\) מתקיים \(V\left(w,\pi\right)=\mbox{rej}\).
  3. יעילות: צריכת המשאבים של \(V\) על הקלטים \(w,\pi\) היא יעילה ביחס לגודל הייצוג של \(w\).

שתי הדרישות הראשונות הן מתמטיות "קלאסיות", בזמן שהשלישית היא מדעי-המחשבניקית "מודרנית". זו גם הדרישה הכי מעורפלת, ולכן אתמקד מעכשיו בפורמליזציה הסטנדרטית שלה- אנו דורשים כי זמן הריצה של \(V\) יהיה פולינומי בגודל \(w\). פולינומי, שכן זה מה שנחשב לזמן ריצה סביר בדרך כלל. כעת נשאלת השאלה מהן השפות שמקיימות את שלוש התכונות הללו. התשובה היא שאלו הן בדיוק השפות שבמחלקה המפורסמת \(\mbox{NP}\) שהזכרתי כאן לא אחת. אין כאן שום תובנה מחוכמת – ה"הוכחה" שמקבל \(V\) היא אותו דבר במהותו כמו ה"רמז" שבדרך כלל נהוג לומר שהמכונה לשפת ה-\(\mbox{NP}\) מקבלת (אם חושבים על \(\mbox{NP}\) כעל אוסף השפות שיש מכונה אי דטרמיניסטית שמכריעה אותן השקילות מעט פחות ברורה – ה"הוכחה" במקרה זה תהיה תיאור של הבחירות האי דטרמיניסטיות שהמכונה מבצעת עד לקבלת המילה השייכת לשפה).אם כן, במובן מסויים \(\mbox{NP}\) מסמלת עבורנו את מחלקת כל ה"תורות" שקיימת עבורן מערכת הוכחה יעילה. לאן ממשיכים מכאן?

כיוון אחד שניתן להמשיך אליו הוא הרחבה של מושג ה"הוכחה". במקום סתם הוכחה כתובה \(\pi\), אפשר לדבר על "מוכיח" \(P\) שמנהל שיחה מנומסת עם \(V\) ומנסה לשכנע אותו שהוא צודק. למערכת הוכחה כזו קוראים "מערכת הוכחה אינטראקטיבית". לרוע המזל, ניתן להוכיח כי השינוי הזה לא מוסיף כוח למערכת – גם מערכת הוכחה אינטראקטיבית מסוגלת להוכיח רק שפות ב-\(\mbox{NP}\). אם כן, צריך להקל איכשהו על אחת משלוש הדרישות שלנו. על יעילות לא רוצים לוותר בשום פנים ואופן, ולכן נותרו השלמות והנאותות. אם נלך לפי הגישה לפיה עדיפים עשרה פושעים מחוץ לכלא מאשר איש חף מפשע אחד בתוכו, הרי שעלינו לפגוע בנאותות, לא בשלמות; פגיעה בשלמות פירושה שייתכן שטענות נכונות לא יהיו ניתנות להוכחה; פגיעה בנאותות פירושה שיהיה אפשרי להשתכנע בטעות שטענה שגויה היא נכונה. החוכמה היא להגביל את ה"אפשרי" הזה ככל הניתן.

לא מזמן דיברתי על אלגוריתמים הסתברותיים. הדגשתי שם שהדבר החשוב באלגוריתם הסתברותי הוא שההסתברות תילקח על פני כל הריצות האפשריות של האלגוריתם על קלט מסויים, ולא על פני כל הקלטים. ההבדל מהותי: במקום שיהיו קלטים שעבורם האלגוריתם תמיד נכשל אבל "ההסתברות שהם יתקבלו" היא נמוכה (במרכאות, כי זה מושג מאוד בעייתי), האלגוריתם מבטיח הסתברות הצלחה כלשהי לכל הקלטים. כך גם במערכת הוכחה – אנחנו דורשים שלכל מילה \(w\notin L\) ולכל "הוכחה" \(\pi\) עבור \(w\) ("הוכחה" כזו היא בעצם נסיון להטעות את המוודא), ההסתברות שיתקיים \(V\left(w,\pi\right)=\mbox{rej}\) היא לפחות \(\frac{2}{3}\) או קבוע דומה (בפוסט על אלגוריתמים הסתברותיים הסברתי מדוע בחירת הקבוע אינה כה מהותית). כמובן שזה אומר, בפרט, שהמוודא פועל באופן הסתברותי.

אם מקבלים את ההקלה הזו של תנאי 2, פתאום מערכות ההוכחה שלנו מקבלות כוח רב הרבה יותר. אם הולכים בכיוון של מערכות הוכחה אינטראקטיביות, הרי שמתברר כי מערכת הוכחה אינטראקטיבית עם ההקלה ההסתברותית שהצגנו הופכת להיות חזקה כמו \(\mbox{PSPACE}\): כל בעיה שניתנת לפתרון בזכרון פולינומי, ניתנת להוכחה במערכת כזו. השלב הבא, והמשעשע עוד יותר, הוא הרחבת המערכת האינטראקטיבית כך שיהיו שני מוכיחים במקום אחד, כך שהמוודא מדבר עם כל אחד מהמוכיחים בנפרד, מבלי שהם יוכלו לתקשר זה עם זה. הדבר מזכיר קצת שני פושעים שנחקרים בנפרד והשקרים שהם מספרים אינם מתואמים, כך שקל לעלות עליהם. במדעי המחשב התחושה האינטואיטיבית הזו תורגמה לתוצאה מדוייקת – מערכות הוכחה שכאלו תופסות את כל \(\mbox{NEXP}\) – אוסף הבעיות שניתנות לפתרון אי דטרמיניסטי בזמן אקספוננציאלי. מחלקה זו גדולה לפחות כמו \(\mbox{PSPACE}\) (ככל שידוע לי, השאלה האם הן שוות או לא עודנה פתוחה).

עם זאת, הכיוון שאני רוצה לדבר עליו כעת אינו הכיוון האינטראקטיבי – נמשיך לדבר על הסיטואציה שבה המוודא מקבל הוכחה כתובה ותו לא. מכיוון שההסתברות מוסיפה לו כוח רב, מעניין לשאול איך אפשר "להצטמצם" כעת באופן אחר ועדיין לתפוס את מה שתפסה ההגדרה ה"קלאסית" להוכחה, כלומר את \(\mbox{NP}\). זה בדיוק המקום שבו נכנס משפט ה-\(\mbox{PCP}\) לתמונה.

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

זה גם בדיוק הרעיון שמנחה את ה-PCP: להגביל את כמות המידע שניתן לקרוא מתוך ההוכחה עצמה. זה גם מעלה את השאלה, שעד כה די הסתרתי, מה צריך להיות אורכה של ההוכחה. עד כה לא דרשתי שום דרישה על אורך ההוכחה, אבל כן דרשתי שהמוודא ירוץ בזמן פולינומי באורך \(w\); מכיוון שעד כה המוודא היה דטרמיניסטי, נבע מכך שגם מההוכחה עצמה הוא יוכל לקרוא מספר תווים שהוא לכל היותר פולינומי ב-\(w\), ולכן לא היה טעם לדבר על הוכחות ארוכות יותר; דה-פקטו, ההוכחת היו מאורך פולינומי ב-\(w\). לרוב בדיונים על \(\mbox{NP}\) הדרישה הזו מבוצעת במפורש.

אלא שכעת איננו חייבים לקרוא את כל ההוכחה – אנחנו יכולים לדגום תווים ממנה באקראי. למשל, להגריל את תו 13, תו 57 ותו 42,423 ולהחליט שרק אותם נקרא. גם כאן יש עניינים טכניים כלשהם של "איך קוראים את התו במקום ה-1,000,000,000 במהירות?" שלא אכנס אליהם (מה שעושים בפועל הוא להניח שההוכחה נתונה כ"קופסה שחורה" – בהינתן קלט של מקום בהוכחה, הקופסה מחזירה את התו שנמצא באותו מקום). מכאן שאנו מאפשרים להוכחות להיות ארוכות מאוד, אבל מרשים קריאה רק של חלק מצומצם מהן.

הדבר הנוסף שאותו ניתן להגביל הוא כמות האקראיות שבה מותר למוודא להשתמש (מספר ה"מטבעות" שיהיה מותר לו להטיל). שימו לב לקשר עדין ולא ברור מיידית בין נתון זה ובין גודל ההוכחה – אם לא ניתן להגריל יותר מדי ביטים, גם לא ניתן להגריל אינדקסים יותר מדי גדולים של מקומות בהוכחה; לכן מגבלה על מספר הביטים האקראיים שזמינים לנו כופה מגבלה דה-פקטו על הגודל האפקטיבי של ההוכחה.

וכעת מגיע הפאנץ'. נסמן ב-\(\mbox{PCP}\left(r\left(n\right),q\left(n\right)\right)\) את אוסף הבעיות שקיימת עבורן מערכת הוכחה מהסוג שתיארתי, שבה על קלט מאורך \(n\) ניתן להשתמש לכל היותר ב-\(O\left(r\left(n\right)\right)\) ביטים של אקראיות ולקרוא לכל היותר \(O\left(q\left(n\right)\right)\) ביטים מההוכחה. כך למשל \(\mbox{NP}=\mbox{PCP}\left(0,\mbox{poly}\left(n\right)\right)\) מתקיים בבירור (\(\mbox{poly}\) פירושו שאנו מרשים ל-\(q\left(n\right)\) להיות פולינום מכל חזקה שהיא; בפועל פירוש הדבר הוא גישה חופשית להוכחה כולה כל עוד עומדים במגבלות הזמן). התוצאה המפתיעה של משפט ה-\(\mbox{PCP}\) היא שמתקיים גם \(\mbox{NP}=\mbox{PCP}(\log(n),1)\).

במילים – אם מרשים שימוש ב-\(O\left(\log n\right)\) ביטים של אקראיות (וזה לא הרבה בכלל), אפשר להסתפק בקריאה של מספר קבוע של ביטים מההוכחה. קבוע, כלומר לא תלוי בכלל באורך \(w\). פירוש הדבר הוא, לדוגמה, שבבעיית המעגל ההמילטוני מספיק תמיד לקרוא 13 ביטים (שנבחרים באקראי) מההוכחה ואז לבצע כמה חישובים, ואין זה משנה כלל אם הגרף הנבדק הוא בעל 10 צמתים או בעל \(10^{100}\) צמתים. לטעמי האישי זוהי תוצאה מדהימה.

כמובן, יש דברים שמסתתרים כאן מאחורי הקלעים; בפרט, יש מספר גרסאות שונות למשפט (כולן אומרות כי \(\mbox{NP}=\mbox{PCP}\left(\log\left(n\right),1\right)\) אך נבדלות בקבועים ובפרמטרים נוספים שמאחורי הקלעים – למשל, דרישות השלמות והנאותות נפגעות בצורות שונות ומשונות). בגרסה שאני מתמקד בה, גודלה של ההוכחה יהיה עצום (אך כאמור, לא נצטרך לקרוא את כולה). בפוסטים הבאים אתאר (בעיקר בנפנופי ידיים, כי מדובר בנושא טכני למדי) את ההוכחה של גרסה מוחלשת של המשפט בכדי לתת תחושה של "מה הולך כאן בכלל", ולהציג את הנושא היפהפה בזכות עצמו שעליו ההוכחה מסתמכת – קודים לתיקון שגיאות. לעת עתה, אני מקווה שהתוצאה מצליחה להיות מעניינת בזכות עצמה.