שפה מסדר ראשון

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

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

לאלף-בית של שפה מסדר ראשון יש כמה קבוצות סימנים: משתנים (כמו v0,v1,...), קבועים (כמו c0,c1,...), פונקציות ויחסים. פונקציה מאופיינת בעקביות על ידי המידות שלה: מספר הפרמטרים שהיא מקבלת (נקרא 'מקומיות' או אריות), התחום ממנו הפרמטרים נלקחים, וטווח התוצאה. גם סימני היחס מקבלים אריות. בדרך כלל סמל השוויון כלול בקבוצת היחסים.

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

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

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

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

ניתן להשוות בין שפה לממשק (Interface) בתכנות. הממשק מגדיר שמות ושיטות אך לא נותן להן פירוש. המחלקה (Class) שמממשת אותו נותנת פירוש וערכים. כך גם לשפה ולמודל: השפה מגדירה את המבנה, והמודל ממלא אותו בתוכן.

שפה מסדר ראשון היא דרך פורמלית לכתוב משפטים על אובייקטים. כימותים הם מילים כמו 'לכל' ו-'קיים' שמספרים על מספרים או פריטים.

השפה כוללת שמות למשתנים (כמו x), שמות לקבועים (כמו 0 ו-1), שמות לפונקציות (כמו חיבור) ושמות ליחסים (כמו 'קטן מ'). פונקציה היא פעולה שלוקחת כמה דברים ומחזירה תוצאה.

כדי שהמשפטים יהיו בעלי משמעות צריך לבחור מודל. מודל הוא קבוצה של פריטים ולתת פירושים לשמות. רק אז אפשר לבדוק אם משפט הוא אמיתי או לא.

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

לא תמיד אפשר לכתוב מספר כקיצור, למשל אם לא הוגדר קבוע בשם 5. אז כותבים אותו כ-1+1+1+1+1.

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