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

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

יכולת ביטוי

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

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

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

כללי הסקה

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

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

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

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

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

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