בתשובה לדני גליק, 21/08/14 0:23
באיחור של עשור... מאמר יפה אבל התעלמת מטארסקי 639567
תודה, דני.

התעלמתי מהרבה התפתחויות בלוגיקה בשנים מאז 1936, כמובן. זה רק מאמרונצ׳יק.

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

בעזרת ההגדרה (המאוד טבעית) הזו אנו מסווגים פסוקים בשפה של האריתמטיקה לשתי מחלקות: פסוקי האמת ופסוקי השקר. מה שמשפט טרסקי אומר הוא שמחלקת פסוקי-האמת איננה arithmetically* definable*, כלומר אין *נוסחה* אריתמטית המתקיימת בדיוק עבור מספריהם הסידוריים של פסוקי-האמת.

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

- זה נכון שלארימתטיקה מסדר שני יש מודל יחיד, וזה נכון גם שזה לא סותר את משפט גדל מפני שתורות מסדר שני אינן אפקטיביות: אין דרך אלגוריתמית לבטא גרירה לוגית באמצעים סינטקטיים.
באיחור של עשור... מאמר יפה אבל התעלמת מטארסקי 639584
הבה נניח שניתן לנסח שפה מוגדרת היטב שאפשר לדבר בה על פילוסופיה, ואשר היא עקבית ואפקטיבית.
בין השאר השפה תכלול פסוקים כמו "בלה-בלה-בלה הוא אמת".
אפשר לתרגם את השפה לאריתמטיקה, למשל לכל משפט נכתוב את קוד ascii שלו וכך כל משפט ייוצג ע"י מספר. בתרגום, כללי המעבר בין משפטים בשפה יהפכו לכללים אריתמטיים. לפיכך קבוצת המשפטים המנוסחים היטב בשפה יתורגמו לקבוצת מספרים, וקבוצת המשפטים האמיתיים לקבוצת מספרים חלקית לזו הראשונה.
קל להראות שאם השפה המקורית היא אפקטיבית כך גם התורה האריתמטית שיצרנו.
המשפט "בלה-בלה-בלה הוא אמת" יהפוך לנוסחה אריתמטית א-לה-טארסקי. כלומר, אם המספר המתאים ל"בלה-בלה-בלה" הוא n, אז המשפט הטוען שמשפט זה הוא אמת יהיה מספר המתקבל מנוסחה אריתמטית על n.
תאאא"ט, זהו True(n‎) של טארסקי.
באיחור של עשור... מאמר יפה אבל התעלמת מטארסקי 639585
וגם - תודה על התשובה אחרי כל כך הרבה זמן!
שאלה - למה אתה מתכוון במשפט "אין דרך אלגוריתמית לבטא גרירה לוגית באמצעים סינטקטיים"?
האם אתה מתכוון שאי אפשר לדעת בלוגיקה מסדר שני אם משפט הוא valid?
למיטב הבנתי זו לא הדרישה של משפט אי-השלמות של גדל, אלא הדרישה היא: דרך אלגוריתמית לבדוק האם רצף של משפטים הוא הוכחה, וזו המשמעות של "אפקטיביות" בהקשר הזה.
באיחור של עשור... מאמר יפה אבל התעלמת מטארסקי 639586
סליחה - נראה לי ששכחתי כאן את הדרישה שיהיה אלגוריתם שייצר את כל המשפטים היכיחים, וזה אינו אפשרי בלוגיקה מסדר שני, נכון?
באיחור של עשור... מאמר יפה אבל התעלמת מטארסקי 639587
אני שוב מגיב לעצמי.
מה שבעצם התכוונתי הוא (בתקווה שאני לא שוב טועה או סתם מתבלבל) שאפשר לשכן (לא בטוח שזו המילה הנכונה) את תורת פיאנו בלוגיקה מסדר שני בתוך ZFC מסדר ראשון, ובהינתן שיכון כזה אפשר להוכיח ב-ZFC שיש לו מודל יחיד.
ההוכחה אפילו קלה, ליתר דיוק קל להוכיח שאם שתי קבוצות מקיימות את אקסיומות פיאנו מסדר שני כפי שאלה מתורגמות ל-ZFC, אז הן שוות.
עבור השיכון הרגיל שבד"כ עושים, המשפט הוא זה:
תהי A קבוצה, כך ש:
1) {} איבר ב-A (זה ה"אפס")
2) אם x איבר ב-A, אז {x,{x}} איבר ב-A (זה ה"עוקב")
3) לכל S תת-קבוצה של A, המקיימת את 1) ו-‏2), S=A (זה כמובן האקוויוולנט של אקסיומת האינדוקציה)
ותהי B קבוצה המקיימת את אותם תנאים כמו A.
אז A=B.

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

על אי שלמות של תורות מסדר שני 639903
תודה. גם הפנייה לספר היא תגובה מועילה :-)

חזרה לעמוד הראשי המאמר המלא

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