לוגיקה? מישהו?

[Shiberia]

לוגיקה? מישהו?

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

 

[yontanbn]

תגובה

למדתי לוגיקה, אני לא זוכר הרבה אבל אני יכול לנסות מותר לך להשתמש בסדר שני?

 

[Shiberia]

לוגיקה מסדר ראשון

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

 

[yontanbn]

או שאני לא מבין או שזה קל

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

 

[Shiberia]

דווקא נראה לי שאתה כן מבין

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

 

[yontanbn]

תגובה

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

 

[Shiberia]

סדר ראשון יכול לתאר גודל מבנה

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

 

[yontanbn]

הסבר

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

 

[Shiberia]

סדר שני

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

 

[yontanbn]

הסבר

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

 

[Shiberia]

אבל זה מה שמצחיק בלוגיקה

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

 

[yontanbn]

אבל זו כבר גלישה

לפילוסופיה ולמטאמתמטיקה....

 

[Shiberia]

הבה נגלוש

 

[yontanbn]

אם אנחנו גולשים

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

 

[Shiberia]

זה לא מוזר זה פשוט מצחיק

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

 

[yontanbn]

הדוגמא

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

 

[Shiberia]

דוגמא

אוקיי , אז בהתחלה היתה את הסמנטיקה וזה ממש תואם את האינטואציה , למשל אם A גורר B נכון ו A נכון אז B נכון , זה די ברור וגם עשינו זאת בהוכחות די פשוטות במתמטיקה אפילו בלי לשים לב. למשל צריך להוכיח ש אם A אז B נניח A וגם לא B ונגיע לסתירה. אוקיי , עכשיו המציאו מערכת הוכחה שנקראת HPC שיש לה כמובן אקיומות וכללי היסק כדי שתתאים אחד לאחד לסמנטיקה (כלומר ל T ו F). עכשיו נותר רק להוכיח את משפט השלמות שאומר ש A יכיח מתורה L אםם A נובע מתורה L. וזה הרי הדבר הכי ברור בעולם , למרות שהמשפט עצמו לוקח 4 עמודים הרי שכך הגדרתם את HPC , שהיא תתאים לסמנטיקה. אז אתה מבלה 3 שעות רק כדי להבין שבעצם לא היו שני כיוונים , הוכחות וסמנטיקה , אלא היה כיוון אחד , וממנו התפתחו. בכל מקרה ממשפט השלמות מקבלים הרבה מאוד דברים יפים - למשל קומפקטיות , שזה משפט אלמותי וכן הלאה.

 

[yontanbn]

תגובה

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

 

[Shiberia]

זה נראה לי כתהליך הגיוני לחלוטין

אבל אחר כך להוכיח משפטים בזה אחר זה משהו כמו 4 5 שעות זה די טיפשי. כי הרי זוהי ההגדרה...

 

[yontanbn]

יש משהו בדברייך

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