לוגיקה מסדר שני

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

יכולת ביטוי

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

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

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

כללי הסקה

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

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

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

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

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

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

קשר למונים גדולים

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

מצד שני, אם $\kappa$ על-קומפקטי, אז לכל משפט בלוגיקה מסדר כלשהו שמתקיים במודל $M$ , כאשר $|M|\geq \kappa$ יש תת-מודל $N$ של $M$ , בו $|N|<\kappa$ , ו-$N$ מקיים את המשפט.

באופן דומה, מונה הוא קומפקטי-חלש אם ורק אם כל פסוק מסדר שני במבנה $<V_{\kappa },\in ,R>$ (עבור יחס $R$ המייצג תת-קבוצה כלשהי של $V_{\kappa }$), בו יש רק כמת כולל בודד על משתנה מסדר שני וכל שאר הכמתים הם מסדר ראשון משתקף, כלומר מתקיים גם במבנה $<V_{\alpha },\in ,R\cap V_{\alpha }>$ עבור סודר $\alpha <\kappa$ .