פרדוקס בנך-טרסקי ומשפט אי השלמות.

פרדוקס בנך-טרסקי ומשפט אי השלמות.

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

מה עניין שמיטה להר סיני?

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

פרדוקס ב-ט משתמש באקסיומת הבחירה

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

למה לחפף מושגים בפורום מתמטיקה?

אם כאן לא נקפיד, מה יהיה בשאר המדינה? למה שלא תנסח את המשפט כהלכה? "כל תורה[0] עקבית[1], אפקטיבית[2] ואריתמטית[3] אינה שלמה[4]" [0] תורה = אוסף של הנחות יסוד וכללי היסק. [1] עקבית = שלא ניתן להוכיח בה היגד והיפוכו. [2] אפקטיבית = לכל סידרה סופית של אקסיומות וגרירות המנוסחות בה קיים אלגוריתם מכריע. [3] אריתמטית = שניתן לנסח בה טענות אריתמטיות מסויימות (אולי "אינדוקטיבית" מילה מתאימה יותר). [4] שלמה = שמסוגלת להכריע לגבי כל היגד המנוסח בה האם הוא אמת או שקר.

הבן אדם לא לקח קורס בלוגיקה.

לא אמרת לו כלום. זה למה חיפפתי.

תודה על ההבהרות,

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

לא נתתי את הניסוח הפורמלי

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

לגבי השרשור - אתה צודק

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

תודה לכולם!