אינדוקציה שלמה ואינדוקציה רגילה

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

פותרים את SAT – אלגוריתם CDCL

בפוסט הקודם על פתרונות לבעיית SAT ראינו את אלגוריתם DPLL – זה היה פחות או יותר האלגוריתם הבסיסי שרוב פותרי ה-SAT המדוייקים (להבדיל מהסתברותיים) מבוססים עליו, אבל מן הסתם פותרים מודרניים הולכים רחוק יותר ממנו, ובפוסט הזה אני רוצה להציג אלגוריתם קצת יותר מודרני שמתבסס על DPLL אבל עושה עוד דברים מתוחכמים – אלגוריתם CDCL, …

פותרים את SAT – אלגוריתם DPLL

הגענו סוף סוף לדבר על האופן שבו פותרים את בעיית SAT במקרה הכללי. יש לנו פסוק CNF $latex \varphi$ ואין לו בהכרח צורה "נחמדה" כמו בבעיות 2SAT או HORNSAT שראינו בפוסט הקודם – מה עושים? ראשית כל ההסתייגות הבלתי נמנעת – אי אפשר להבטיח שמה שנעשה יהיה יעיל, כלומר ייגמר מהר יחסית לגודל הפסוק. SAT …

פותרים את SAT: המקרים של HORNSAT ו-2SAT

בפוסטים הקודמים דיברתי על בעיית SAT ועל השיטה שבה ניתן להוכיח שפסוק CNF אינו ספיק, אבל כל מה שעשיתי עד כה היה מאוד באוויר – עדיין לא הסברתי איך אפשר בפועל לקחת פסוק CNF ולקבוע אם הוא ספיק או לא. ובכן, באופן כללי הבעיה היא קשה, לפחות מבחינה תיאורטית, אבל יש מקרים פרטיים מסויימים של …

רזולוציה – איך אפשר להוכיח שאי אפשר?

בפוסט הקודם תיארתי את בעיית SAT וסיימתי בכך שהבטחתי להסביר איך אפשר להשתכנע בכך שפסוק CNF אינו ספיק, מבלי שיהיה צורך לבדוק את כל ההשמות האפשריות עבורו. בפוסט הזה אציג את השיטה הנפוצה ביותר לשימוש כדי להוכיח זאת – רזולוציה. מובטח לנו שאם $latex \varphi$ הוא פסוק CNF לא ספיק, אז קיימת הוכחה לכך המבוססת …

מה זו בעיית SAT ולמה חשוב לפתור אותה?

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

על P=NP מעל חבורות אבליות – סוף דבר

בשני הפוסטים האחרונים אני מכין את הקרקע לקראת הוכחה ש-$latex \mbox{P}\ne\mbox{NP}$ במודלים חישוביים שהם מעל חבורות אבליות אינסופיות. בפוסט הראשון הצגתי את הרעיון שמאחורי מודל חישובי שכזה והצגתי הוכחה לכך שעבור המקרה הקונקרטי של $latex G=\mathbb{Z}$ אנחנו אכן מקבלים ש-$latex \mbox{P}_{G}\ne\mbox{NP}_{G}$, ובפוסט שלאחריו הצגתי את המושג של על-מכפלה שבו נשתמש הפעם. ברשותכם ניגש הישר לעניינים. …

על על-מסננים ועל-מכפלות

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

על P=NP מעל חבורות אבליות – מבוא שלם

בואו נוכיח ש-$latex \mbox{P}\ne\mbox{NP}$. אה… מה? תיארתי בעבר בבלוג את בעיית $latex \mbox{P=NP}$ בתור הבעיה הפתוחה המרכזית במדעי המחשב ולא הרבה השתנה מאז – עדיין אין לנו הוכחה ש-$latex \mbox{P}\ne\mbox{NP}$ למרות שרוב מדעני המחשב חושבים שזה המצב. אז מן הסתם לא על הבעיה הזו אני רוצה לדבר. אני רוצה לדבר על $latex \mbox{P}\ne\mbox{NP}$ מעל מודל …

מכסחי הכמתים

בפוסטים שלי על לוגיקה הגעתי עד למשפטי השלמות והקומפקטיות של לוגיקה מסדר ראשון, וזה מביא אותנו אל הסף של מה שנקרא "תורת המודלים". הפעם אני רוצה לדבר על אחת מהטכניקות הבסיסיות שרואים כשמתחילים ללמוד את תורת המודלים – חילוץ כמתים. מכיוון שבאנגלית הטכניקה נקראת Quantifier Elimination ואני רוצה להשתעשע, אני אקרא לה כאן "חיסול כמתים". …

לוגיקה מסדר ראשון – כמה תוצאות של משפט השלמות

בפוסט הקודם שלי על לוגיקה סיימתי להציג את ההוכחה של משפט השלמות ללוגיקה מסדר ראשון. בפוסט הזה אני רוצה להציג כמה מסקנות ממנו שהן (לטעמי) מאוד לא מובנות מאליהן. נתחיל עם מה שקיבלנו באותו האופן גם בתחשיב הפסוקים: קומפקטיות. משפט הקומפקטיות ללוגיקה מסדר ראשון אומר שקבוצת פסוקים כלשהי $latex \Phi$ היא ספיקה – כלומר, קיים …

משפט השלמות של גדל, ההוכחה (חלק ב')

אנו ממשיכים בהוכחת משפט השלמות של גדל. כזכור, בפוסט הקודם הוכחנו שאם $latex \Phi$ היא תורה עקבית מקסימלית מעל מילון $latex \tau$ שבנוסף לכך קיימת עבורה קבוצת עדים $latex C$, אז קיים ל-$latex \Phi$ מודל. זה מספיק כדי לסיים את ההוכחה, בתנאי שנוכיח שכל תורה עקבית $latex \Phi$מעל מילון $latex \tau$ ניתן להרחיב לתורה עקבית …

משפט השלמות של גדל, ההוכחה (חלק א')

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

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

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

פרדוקס בוחן הפתע

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

הבעיה העשירית של הילברט – פונקציות דיופנטיות וחיות אחרות (רקורסיביות)

אנו ממשיכים בדרך שלנו אל ההוכחה שלא קיים אלגוריתם שפותר את הבעיה העשירית של הילברט. אני מניח שקראתם את פוסט המבוא ולכן קופץ ישר לעניינים הפעם. המושג המרכזי בפוסט הקודם היה קבוצה דיופנטית. זוהי קבוצה $latex S=\left\{ \left(a_{1},\dots,a_{n}\right)\right\} $ של $latex n$-יות של מספרים טבעיים חיוביים, כך שקיים פולינום $latex p\left(x_{1},\dots,x_{n},y_{1},\dots,y_{m}\right)$ בעל התכונה הבאה: למשוואה …

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

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

תחשיב הפסוקים – משפט הקומפקטיות ואיך משפט השלמות דומה למשפט טיכונוף

בפוסט הקודם על לוגיקה סיימתי להוכיח את משפט השלמות לתחשיב הפסוקים. לפני שנעבור הלאה, אני רוצה להתעכב טיפה על המסקנות מכל זה ולדבר עוד קצת על ההוכחה. בואו נתחיל ממסקנה לא טריוויאלית ממשפט השלמות: משפט הקומפטיות. משפט הקומפטיות אומר בפשטות שלתורה $latex \Phi$ יש מודל אם ורק אם לכל תת-תורה סופית $latex \Phi^{\prime}\subseteq\Phi$ יש מודל. …

משפט השלמות לתחשיב הפסוקים

בפוסט הקודם הצגתי מערכת הוכחה (חלקית, עוד לא גמרנו) לתחשיב הפסוקים והוכחתי שהיא מקיימת את משפט הדדוקציה: אם $latex \Phi\cup\left\{ \alpha\right\} \vdash\beta$ אז $latex \Phi\vdash\alpha\to\beta$. הפעם אני רוצה להמשיך לבנות את מערכת ההוכחה הזו ולהראות שהיא מקיימת את התכונה שלשמה היא קיימת: להוכיח כל מה ש"נכון", דהיינו אם $latex \Phi\models\varphi$ אז $latex \Phi\vdash\varphi$ (זכרו: $latex …

תחשיב הפסוקים – על נביעה לוגית והוכחות

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