שאלה על מערכות הוכחה בלוגיקה

[קרמבו]

השאלה פונה לאנשים שעשו את קורס בלוגיקה ולא סתם זורקים תשובות לאוויר...

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


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

😣

 

[מר לטיסימוס]

תתבייש! אלכס יצלוב אותך!

 

[קרמבו]

אתה גם אמור לדעת את זה! אני זקוק לעזרה!

 

[מר לטיסימוס]

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

 

[קרמבו]

בגדול ההגדרה של מערכת שלמה זה

if e|= phi than e|- phi
כלומר כל מה שנכון ניתן להוכיח


של נאותה זה

if E|-phi than E|= phi

כלומר, כל מה שמוכיחים הוא נכון

 

[coldfire]

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

ושיזיינו את בר אילן עם המושגים המתמטיים בעברית.

לגבי לוגיקה מסדר ראשון, זה לא מעניין.

 

[מר לטיסימוס]

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

וזה then, יא דיסלקט.

 

[קרמבו]

נאותה = soundness
שלמה = completness

ולא עזרת לי... מדברים על מערכת מסדר ראשון.. :(

 

[מר לטיסימוס]

מצאתי לך משהו, אולי זה יעזור לך. יש שם כמה תיאורמות שהן נאותות אבל לא שלמות.

www.alcop.unibe.ch/downloads/Slides_T.Studer.pdf

 

[קרמבו]

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

סעיף א המערכת שימושית כי כל מה שניתן להוכיח הוא נכון, מהסאונדנס של המערכת, מצד שני בגלל שהיא לא שלמה אומר שלא כל מה שנכון ניתן להוכיח

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

---------- התגובה התווספה ב 17:48 ---------- התגובה הקודמת הייתה ב 17:46 ----------

Than, then

טומטו טומאטו!

 

[מר לטיסימוס]

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

 

[קרמבו]

לא נראה לי.

 

[מר לטיסימוס]

אז מי שכתב/ה את השאלה השנייה צריכ/ה כנראה לרענן את הלוגיקה שלו.

 

[קרמבו]

האמת שיצאתי טמבל בעצם. אתה יכול לקחת מערכת היסק כלשהי ולהוריד לה מהאקסיומות וליצור דברים אחרים... בקיצור כנראה שאני הדביל ולא המרצה..