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

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

יכולת ביטוי

בלוגיקה מסדר שני אנחנו יכולים לבטא משמעותית יותר מאשר בלוגיקה מסדר ראשון. כך למשל, ניתן לבטא כבר בלוגיקה מסדר ראשון את העובדה ששדה המספרים הממשיים הוא שדה סדור קווית (כיוון שכדי לנסח את העובדה הזו אנחנו צריכים רק להשתמש בכמתים על איברים במבנה), אבל לא ניתן לבטא בשפה מסדר ראשון את העובדה שלכל קבוצה חסומה יש חסם עליון מינימלי. עובדה זו ניתנת לביטוי על ידי לוגיקה מסדר שני, כיוון שהמשפט "לכל קבוצה 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$.