תמונה: נוצרה בעזרת Google Gemini
המציאות היא מערכת פתוחה. רשומות מגיעות באיחור. עדים חוזרים בהם. חיישנים מכוילים מחדש. מדיניות משתנה. בשום שלב לא נוכל לומר שכל התצפית הרלוונטית כבר הגיעה, משום שאיננו יודעים אפילו מה עדיין לא התגלה.
הפעולה שונה. חיוב, תשלום, הענקת גישה, הפעלת אזעקה: כל אחת מהן דורשת תשובה סגורה. החלטה חייבת להסתיים גם כאשר המציאות אינה מסתיימת. בין עולם פתוח לבין פעולה סופית מתקיים פער מבני. עוד ביטחון של המודל, שרשרת מחשבה ארוכה יותר, או שכבה נוספת של סוכנים - אינם יכולים לסגור אותו.
השאלה הראשונה אם כן אינה “מה נכון?” אלא:
בעולם של claims ללא סוף ידוע, מי רשאי לקבוע את ההנחות עבור החלטה זו, ולפי אילו כללים?
מה שנכנס למערכת אינו האירוע עצמו. זהו חוזה, רשומת תשלום, יומן חיישן, סרטון, עדות, או הודעה: פרגמנט שהופק על ידי צופה, בזמן מסוים, דרך טרנספורמציה, בתוך היקף מסוים, עם מצבי כשל אפשריים. המערכת חייבת לקבל אלה כ-Claims, לא כעובדות.
אך שימור Claims אינו מספיק כדי לפעול. Claims עלולים להתנגש. רשומה חסרה עשויה להעיד שאירוע מעולם לא קרה, או פשוט שהאיסוף נכשל. ייתכן שיהיה צורך לשלב מספר Claims כדי לגזור הנחה אחת. אם ledger פתוח של Claims עובר ישירות למנוע שיפוט, האיסוף, בירור העובדות, ויישום הכללים מתמוטטים חזרה לכדי מעשה אטום אחד.
מה שדרוש לנו הוא הליך מפורש שבונה את המצב העובדתי המותר עבור החלטה מסוימת. אני קורא לאותו הליך Projection, ולתוצאתו Graph of Accepted Facts, או GAF.
Open Claims
│
▼
Projection
│ evaluation · conflict resolution · derivation · absence policy
▼
Graph of Accepted Facts (GAF)
│
▼
Closure
│ GAF · scope · policy · rules · runtime frozen
▼
Deterministic Verdict
│
▼
Authorized Action
│
└── new evidence · policy change · appeal · defect
│
▼
Reopen / Re-projection
הנקודה אינה לאסוף עוד עובדות. היא להפריד בין בניית הנחות השיפוט לבין החישוב על אותן הנחות.
קלט סופי עדיין אינו עולם סגור
קבוצת Claims סופית אינה הופכת לעולם סגור. אם תשלום אינו מופיע במסד נתונים, לא נוכל להסיק מיד שהתשלום לא בוצע. הרשומה עשויה להיות חסרה, מאוחרת, מנותבת לא נכון, או מוחזקת על ידי מוסד אחר.
לכן Projection חייב לקבוע את המשמעות של היעדרות, ולא רק את רשימת הקלט:
- איזה מקור נחשב שלם עבור נושא, פרדיקט, טווח, ותקופה נתונים?
- היכן ניתן להחיל הנחת עולם סגור?
- האם רשומה חסרה משמעה
falseאוunknown? - כיצד מבחינים בין שלילה מפורשת לבין נתונים חסרים?
- מה על המערכת להחזיר כאשר הראיות אינן מספיקות?
המאמר היסודי של Raymond Reiter, On Closed World Data Bases, ניסח באופן פורמלי את המהלך המכריע: תחת הנחת עולם סגור, כישלון להוכיח ליטרל חיובי בסיסי עשוי להתיר את שלילתו. מהלך זה שימושי בדיוק משום שהוא אינו בטוח באופן אוניברסלי. הוא דורש גבול מוצהר.
נניח שבנק מספק ledger תשלומים סופי עבור חשבון אחד ותקופה אחת, ומדיניות ה-Projection מקבלת את אותו ledger כשלם בתוך אותו היקף. היעדרות עשויה אז להיחשב כראיה לכך שאין שם עסקה תואמת. היעדרותה של אזכור תשלום בארכיון ההודעות של דייר אינה מוכיחה דבר כזה. מקור אחד סגור עבור שאילתה מוצהרת; האחר נותר פתוח.
Closure אינו ההצהרה “קראנו עד כאן”. זהו חוזה המגדיר היכן היעדרות עצמה הופכת למידע בר-חישוב.
Projection אינו כפתור שמקדם Claim לכדי עובדה
לא ניתן לצמצם את Projection לצירוף התווית accepted, rejected, או held ל-Claim שלם. Claims אמיתיים לרוב אינם נקיים כל כך.
- “שלחתי את שכר הדירה בחמישי” עשוי להיות בעל תאריך מאומת אך מטרה לא מאומתת.
- ייתכן שיידרשו שתי רשומות בלתי תלויות כדי לבסס תשלום אחד.
- Claim אחד עשוי לתמוך בטענה אחת ולהפריך אחרת.
- עובדה עשויה להיגזר גם אם אף מקור אינו מציין אותה במילים מדויקות.
- מקור אמין עדיין עשוי להיות לא פתור באשר לאיזה אירוע הרשומה שלו מתארת.
Evaluation הוא יחסי, לא דגל על Claim שלם. הוא מחבר Claim אחד או יותר, Proposition אטומי, ו-Projection מסוים. Derivation משלב אז Evaluations, הנחות שהתקבלו בעבר, וכללים מפורשים כדי להפיק Accepted Fact.
Claims ───────┐
Proposition ──┼── Evaluation ── accepted / rejected / unknown
Projection ───┘ │
▼
Derivation ── Claims · Facts · Rules
│
▼
Accepted Fact
Claim משמר מי טען או צפה במה. Proposition הוא ההצהרה הקטנה ביותר הנבחנת. Evaluation מתעד כיצד ה-Claims נוגעים ל-Proposition תחת Projection מסוים. Derivation הוא אובייקט ההוכחה המראה כיצד הופקה התוצאה. Accepted Fact הוא ההנחה שההליך מתיר לשיפוט זה להשתמש בה.
לכן אותו Claim עשוי להניב Accepted Fact שונה - או אף לא אחד - תחת מטרה אחרת, זמן חיתוך אחר, נטל הוכחה אחר, או סמכות אחרת. Accepted Fact אינו אמת מוחלטת על כל המציאות. זוהי הנחה המותרת לשימוש בתוך גבול החלטה מוצהר.
מדוע התוצאה היא גרף
הנחות השיפוט אינן משפטים מבודדים. מי שילם למי, מתי, כמה, לפי איזה חוזה, כלפי איזו התחייבות, ובעוד אותו חוזה בתוקף - הן הצהרות מקושרות.
Graph of Accepted Facts מכיל את אותן הנחות ואת היחסים הסמנטיים ביניהן, יחד עם ה-derivation וה-provenance שהפיקו אותן:
- ישויות, פעולות, זמנים, כמויות, ומצבים;
- Claims התומכים או מפריכים כל Proposition;
- מקורות מקוריים וגורמים אחראים;
- Evaluations וכללי derivation;
- חלופות שנדחו או לא נפתרו;
- יחסים טמפורליים, לוגיים, ויחסי החלפה.
מטרת הגרף אינה הסבר דקורטיבי. זוהי תלות הניתנת למעקב מכני.
החל מ-Verdict, מבקר חייב להיות מסוגל לרדת דרך ה-GAF וכלליו אל ה-Claims המקוריים. החל מ-Claim או מקור שבוטל, על המערכת להיות מסוגלת למצוא כל Accepted Fact, Closure, Verdict, ו-Action שעשויים לדרוש בדיקה חוזרת.
Provenance בלבד אינו מספיק. ניתוח השפעה מלא דורש גם תלויות derivation, תלויות שליליות, תנאים מצטברים, והיקף מדיניות. מסקנה עשויה להיות תלויה לא ב-Claim הקיים, אלא בהיעדרותו המוצהרת של כל Claim מתאים. תקן PROV-O: The PROV Ontology מסדיר provenance בר-פעולה הדדית סביב ישויות, פעילויות, סוכנים, ויחסים מוסמכים; הנטל הנוסף של GAF הוא לשמר את הקבלה הספציפית להחלטה ואת התלויות השליליות הדרושות כדי לפתוח מחדש שיפוטים.
זהו מודל נתונים לוגי, לא מנדט של מסד נתוני גרף. מסד נתונים יחסי, מאגר אובייקטים בכתובת-תוכן, יומן אירועים append-only, או מסד נתוני גרף - כל אחד מהם עשוי לממש אותו. האחסון הפיזי תקף אם הוא משמר את הצמתים, היחסים המוקלדים, ה-lineage, ושאילתות התלות ללא אובדן סמנטי.
Closure גדול מ-GAF
GAF משמר Accepted Facts ואת ה-Derivation וה-Provenance שלהם. Closure גדול מ-GAF: הוא מקפיא בדיוק איזה GAF שימש, עבור איזו שאלה, תחת אילו תנאים. זהו חוזה השחזור עבור ההחלטה.
Closure חייב להכיל לכל הפחות:
- את השאלה ואת מטרת השיפוט;
- את האירוע, הנושא, וההיקף הטמפורלי;
- את תמונת ה-GAF המדויקת ואת מזהה השלמות שלה;
- הצהרות שלמות והתייחסות להיעדרות, שלילה, ולא-ידוע;
- את מדיניות ה-Projection ואת גרסת המימוש;
- את כללי ה-Verdict ואת גרסת המנוע;
- תנאי זמן ריצה כגון דיוק מספרי, סדר, ושבירת תיקו;
- כללי קנוניזציה הדרושים כדי לזהות שוב את אותו הגרף.
אם אותו Closure שמופעל באותו זמן ריצה מניב Verdict שונה, שכבת החישוב לוקה בפגם. אם ה-Closures שונים, ניתן לאתר את אי-ההסכמה בקלט, במדיניות ה-Projection, ב-Accepted Facts, בכללים, או בזמן הריצה.
דטרמיניזם אינו אומר לדעת את המציאות באופן מושלם. הוא אומר שאותו עולם סגור חייב להיות מחושב באותו אופן.
מעקב אחר מקרה אחד עד הסוף
בעל בית טוען ששכר הדירה של יולי לא שולם. דייר טוען שהתשלום הועבר בחמישי. ה-ledger הבנקאי הסופי מראה שבעל הבית קיבל אלף דולר באותו יום, אך תזכיר ההעברה ריק. החוזה דורש אלף דולר עד החמישי בכל חודש.
ה-Open Claim Ledger משמר את כל ארבע הרשומות מבלי לאפשר לאחת לדרוס אחרת.
| Claim | תוכן | סטטוס מקור |
|---|---|---|
| Claim A | שכר הדירה של יולי לא שולם | טענת בעל הבית |
| Claim B | התשלום הועבר בחמישי | טענת הדייר |
| Claim C | חשבון בעל הבית קיבל אלף דולר בחמישי | ledger בנקאי סופי |
| Claim D | שכר הדירה החודשי הוא אלף דולר, לתשלום עד החמישי | חוזה תקף |
ה-Projection מצמצם את השאלה ל: “האם פיגור בתשלום שכר הדירה של יולי הוכח?” הוא מקבל את ה-ledger הבנקאי כשלם עבור החשבון והתקופה. הוא גם מיישם מדיניות שאינה מסיקה הקצאה לחוב מסוים ללא תזכיר או הסכם נפרד.
Claim C ו-Claim D תומכים ב-Propositions שהתקבלו. התאריך והסכום של Claim B נתמכים על ידי Claim C, אך הקצאתו לשכר הדירה של יולי נותרת לא ידועה. Claim A הוא טענת צד למסקנה הרצויה, לא ראיה בלתי תלויה לאי-תשלום, ולכן הוא אינו הופך ל-Accepted Fact על ידי חזרה.
ה-GAF רושם:
The contract required monthly payment by the fifth. [accepted]
The landlord received the contractual amount that day. [accepted]
Allocation of that payment to the July debt is unresolved.[unknown]
July rent delinquency has not been established. [not derived]
ה-Closure קושר את ה-GAF הזה למדיניות ה-Projection, להיקף השלמות של ה-ledger, לזמן החיתוך, ולמנוע ה-Verdict. ה-Verdict אינו delinquent; הוא undetermined. ה-Authorized Action לכן אינו מכתב דרישה, אלא בקשה לבסס את ההקצאה.
מאוחר יותר, מגיעה קבלת העברה מקורית הנושאת את התזכיר “שכר דירה יולי” כ-Claim חדש. ה-Closure הישן נשמר. אירוע Reopen מתחיל Projection חדש. אם התזכיר מתקבל, GAF חדש מקבל את ההקצאה, ו-Closure חדש מפיק paid כ-Verdict.
ה-Projection בדוגמה זו אינו הצבעה על מי מהצדדים נשמע אמין יותר. הוא קובע את השאלה, את גבול השלמות, את ה-Propositions האטומיים, את משמעות הנתונים החסרים, ואת כללי ה-derivation הדרושים לבניית מצב עובדתי הניתן להכרעה.
שימור ההחלטה כחוזה
הדוגמה עדיין מכילה צוואר בקבוק. אם כל תשלום ללא תזכיר מחייב את בעל הבית לאשר הקצאה, אי-הוודאות לא בוטלה; היא רק הועברה לתור אישור אנושי.
האישור הראשון אמור לפתור את המקרה. תבנית חוזרת אמורה לעשות יותר מכך: לשמר את ההחלטה כחוזה שיכול להפוך לקלט Projection עתידי.
נניח שבעל הבית מאשר את התשלום ושני הצדדים מאשרים כלל זה:
תשלום מוקצה לשכר הדירה של החודש הנוכחי כאשר הוא מגיע מהחשבון הרשום של הדייר עד למועד היעד, שווה לסכום החוזי, ואין חוב אחר בפיגור. מקרה המפר תנאי כלשהו דורש בדיקה.
זה מפיק ארבע רשומות נבדלות:
Case Decision ── this payment satisfied the July rent
Policy Candidate ── matching future payments may satisfy monthly rent
Ratified Contract── authorized conditions, exceptions, effective date, version
Policy Exception ── ambiguity outside the contract returns to human review
ה-Closure הבא מפנה לגרסת המדיניות המאושררת. Claims תואמים יכולים אז לעבור Projection מבלי לשאול את בעל הבית שוב את אותה שאלה; רק חריגה חדשה צורכת שיפוט אנושי. ההחלטה האנושית משמשת פעם אחת, בעוד המבנה המורשה שלה ממשיך לפעול.
אך החלטה אחת אינה עדיין מדיניות. מערכת אסור לה להפוך בשקט אישור אחד לתקדים. האדם בעל הסמכות חייב לאשרר את היקף הכלל, את החריגים, את תאריך התוקף, ואם הוא חל רטרואקטיבית. עד אז, רשומת המקרה היא רק Policy Candidate. אם חוזה חדש אינו רטרואקטיבי במפורש, הוא חל על Closures מאוחרים יותר ואינו כותב מחדש קודמים.
זה מוסיף לולאת שימור שנייה ל-GAF. Claims משמרים מה שנכנס מהעולם. GAF ו-Closure משמרים מה ששיפוט מסוים קיבל. מדיניות מאושררת משמרת כיצד אדם מוסמך פתר עמימות חוזרת, כך שה-Projection הבא מתחיל עם חוזה חזק יותר במקום אותו צוואר בקבוק.
שגיאות שונות דורשות תיקונים שונים
ברגע ש-Projection, Verdict, ו-Action מופרדים, “תוצאה שגויה” אחת מתפרקת לכשלים שונים:
- החמצת Claim רלוונטי היא שגיאת איסוף;
- הערכה שגויה של מקור או Proposition היא שגיאת Projection;
- יישום הכלל השגוי על Accepted Facts נכונים היא שגיאת חישוב;
- הצגת Verdict נכון באופן לא מדויק היא שגיאת תקשורת;
- ביצוע Verdict נכון כנגד יעד, מגבלה, או סמכות שגויים היא שגיאת Action.
טקסונומיה זו אינה מבטלת שגיאה. היא אומרת לנו מה לפתוח מחדש.
שגיאת איסוף דורשת Claim נוסף. שגיאת Projection דורשת בדיקה חוזרת של Evaluation ו-Derivation. שגיאת חישוב יכולה לשמר את ה-Closure תוך תיקון והשוואת המנוע. שגיאת Action אינה אמורה לכתוב מחדש את העובדות; היא דורשת ביטול, תיקון, או פיצוי בעולם החיצוני.
לקרוא לכל אלה “המודל טעה” מוחק את ההבחנה. ברגע שהסיבה אבדה, המערכת אינה יכולה להוכיח מה השתנה לאחר התיקון.
Accepted Fact אינו סמכות לפעול
Accepted Fact אינו מעניק כוח. “שכר הדירה בפיגור” ו"מערכת זו רשאית לשלוח מכתב דרישה" הן Propositions שונים.
מנוע ה-Verdict צורך Closure ומפיק שיפוט עם עקבת חישוב. Authorized Action חייב לבדוק בנפרד:
- מי אישר את האפקט;
- על איזה נושא ואובייקט הוא מכוון;
- מגבלות סכום ותדירות רלוונטיות;
- האם ניסיונות חוזרים הם אידמפוטנטיים;
- איזו קבלה מוכיחה ביצוע;
- כיצד ניתן לבטל או לפצות על אפקט שגוי.
הפקת עובדות, שיפוט, וביצוע נפרדים משום שכל אחד מפעיל סוג שונה של סמכות.
עולם סגור חייב להישאר ניתן לפתיחה מחדש
Closure חייב להיות בלתי ניתן לשינוי מבלי להעמיד פנים שהוא אמת נצחית. ראיות עשויות להגיע באיחור. מקור עשוי להתברר כמזויף. פגם במדיניות עשוי להתגלות. צד נפגע עשוי לערער.
כתיבה מחדש על התוצאה הישנה תהרוס את ההסבר לפעולה שננקטה באותו זמן. Reopen הוא לכן אירוע חדש, לא עריכה של ה-Closure הישן.
ראיה חדשה, שינוי מדיניות, ערעור, או דיווח על פגם נרשמים. גרף התלות מזהה Closures שעשויים להיות מושפעים. אם הליך מוסמך מתיר פתיחה מחדש, Projection חדש מפיק GAF, Closure, ו-Verdict חדשים. התוצאה החדשה מציינת מה היא מחליפה מבלי לכתוב מחדש את ההיסטוריה.
אם Action כבר שינה את העולם, חישוב מחדש אינו יכול להפוך אותו. ביטול, הודעות תיקון, החזרים, ופיצויים הם עצמם Actions חדשים עם הרשאה וקבלות משלהם.
יכולת הפתיחה מחדש אינה מחלישה את הסגירה. Closure הופך ללגיטימי בדיוק כאשר המערכת משמרת את מה שנקבע ומתירה החלפה רק דרך הליך מוצהר.
LLMs אינם יכולים להחליף את הגבול
רוב יישומי ה-LLM מקצה לקצה מערבבים פרשנות שאלה, אחזור, בחירת מקורות, בירור עובדות, יישום כללים, וביטוי - בייצור אחד. אם Claims שהתקבלו ונדחו אינם מוצאים החוצה, אותה תשובה אינה מוכיחה את אותן ההנחות. תשובה שהשתנתה אינה חושפת אם גבול הקלט או החישוב השתנו.
הסבר ארוך או עקבת נימוק שנוצרה אינם פותרים זאת. הסבר בדיעבד אינו רשומת ביצוע של הקלטים, הכללים, והסמכות שבפועל נעשה בהם שימוש.
LLMs נותרים שימושיים סביב הגבול. הם יכולים לחלץ מועמדי Claim ממקורות לא מובנים, להציע Propositions אטומיים, להסביר סתירות ולא-ידועים, לנסח מדיניות Projection, ולתרגם Verdict קבוע לשפה אנושית.
אך הצעה אינה אימוץ. Claim, מיפוי, Evaluation, או כלל שנוצרו על ידי LLM חייבים להפוך לקלט בעל גרסה עם provenance ולעבור הליך מוסמך. הסמכות הסופית עבור פעולה בעלת השלכות גבוהות אינה יכולה להישאר חבויה בתוך ייצור שפה טבעית.
התרומה היא השרשרת
הרכיבים אינם כולם חדשים. חשיבה על עולם סגור, provenance, מערכות truth-maintenance, event sourcing, מנועי כללים, בירור עובדות משפטי, וערעורים - כל אלה בעלי היסטוריה ארוכה. On Closed World Data Bases ביסס את ההבחנה בין עולם פתוח לסגור, בעוד PROV-O: The PROV Ontology הסדיר מודל גרף למעקב אחר ישויות דרך פעילויות וסוכנים אחראים.
התרומה היא השרשרת, המורכבת כפרוטוקול אחריות אחד:
Claims → Projection → GAF → Closure → Verdict → Action → Reopen
כל חץ הוא גבול של סמכות ושגיאה, לא רק טרנספורמציית נתונים. הגורם המשמר Claims, הסמכות המקבלת הנחות, המנוע המחשב Verdict, והשער המשנה את העולם - פועלים תחת חוזים שונים. הרשומות שלהם מתחברות, אך אף שלב אינו יורש בשקט את הסמכות של אחר.
GAF אינו המצאה של מסד נתונים נוסף. זוהי הצעה להפוך את המעבר כולו מ-claims פתוחים לעובדות ניתנות לפעולה לניתן לביקורת, לשחזור, ולערעור.
המטרה היא סגירה מבוקרת, לא אמת מושלמת
איננו יכולים לבנות מערכת היודעת את כל העולם הפתוח. אנו יכולים לבנות אחת המצהירה איזה מידע היא קיבלה כהנחה, ומדוע.
Open Claims משמרים אי-הסכמה ואי-ודאות. Projection קובע מטרה, היקף, נטל, ומשמעות ההיעדרות. GAF מחבר הנחות שהתקבלו ליחסים ולשושלת שלהן. Closure מקפיא את התנאים לשחזור. Verdict מחשב על הקלט הסגור. Action משנה את המציאות תחת סמכות נפרדת. Reopen מבקר מחדש את הגבול מבלי למחוק היסטוריה.
עם מחזור זה, שגיאה אינה נותרת עוד הזיה אטומה אחת. אנו יכולים להבחין בין מה שהמערכת החמיצה, מה שהיא קיבלה באופן שגוי, מה שהיא חישבה באופן שגוי מהנחות שהתקבלו, ומה שהיא ביצעה באופן שגוי לאחר שיפוט נכון.
הטלת Claims לתוך GAF אינה דרך להפוך מכונות לחסינות משגיאה. היא קובעת על מה המכונה שפטה כך שהשיפוט יוכל להיות משוחזר, מאותגר, ומתוקן.
האמרה “המתמטיקה נכונה משום שהיא מחשבת בתוך מערכת סגורה” מצביעה על עובדה צרה יותר, בת-הגנה. ברגע שאקסיומות, הגדרות, וכללי היסק נקבעים, ניתן לבדוק ולשחזר derivation בתוך אותו גבול פורמלי (Formalism in the Philosophy of Mathematics). זה אינו הופך כל אמת מתמטית לבת-חישוב, כל Proposition להכרעה, או כל מערכת אקסיומטית לשלמה. Closure מבטיח את השחזוריות של derivation שהתקבל, לא כל-ידיעה.
שיפוט בעולם האמיתי זקוק לאותו משמעת לפני החישוב. GAF אינו האמת עצמה. זהו העולם הסגור הקובע אילו הנחות התקבלו מהמציאות הפתוחה, כך שניתן לשחזר - ולערער - verdict בתוכו.
מאמרים קשורים
- האמת אינה מתגלה — הטיעון הפיזיקלי, המתמטי, והמשפטי לכך שהאמת מופיעה רק לאחר שעולם נסגר
- Triples הם Claims, לא עובדות — מדוע גרף ידע צריך לשמר claims מתחרים לפני חישוב שיפוט הקשרי
- toulmin — מנוע כללים המחשב חוזים — דוגמה אחת להפרדה בין הנחות שהתקבלו לבין חישוב כללים דטרמיניסטי
לקריאה נוספת (חיצוני)
- On Closed World Data Bases — התיאור המקורי של Raymond Reiter להערכת שאילתות בעולם פתוח וסגור
- PROV-O: The PROV Ontology — המלצת ה-W3C ל-provenance בר-פעולה הדדית
- Formalism in the Philosophy of Mathematics — התיאור הפורמליסטי של האמת המתמטית בתוך מערכת מונחית-כללים
מקורות
- Reiter, Raymond. On Closed World Data Bases. University of British Columbia, Technical Report.
- W3C. PROV-O: The PROV Ontology. W3C Recommendation.
- Stanford Encyclopedia of Philosophy. Formalism in the Philosophy of Mathematics.