תחשיב הפסוקים – הבדלי גרסאות

== התחשיב וגבולותיו ==

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

:א. '''אם''' החֶרֶק הוא נמלה, '''אזי''' הוא חי בתל נמלים.

:ב. החֶרֶק הנבדק '''הוא''' נמלה.

 

::'''אם א' - אזי ב''''.

 

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

 

:- נוכל להשאיר את א' כ''משתנה'', ובהתאם לכל ערך שהוא יקבל - בין אם הערך 'אמת' ובין אם 'שקר', נוכל לדעת על הערך ב'.

 

 

'''דוגמה לבדיקת תקפות טיעונים על פי הכללה''':

:הנחה א: '''א'''' כלשהו '''קיים''' בתוך '''ר''''

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

 

=== הצרנה (פורמליזציה) ===

 

 

הסמנטיקה (מבנה המשמעות) של תחשיב הפסוקים מורה לנו כיצד עלינו להבין את היחס בין הסמלים המייצגים פסוקים שונים, ובין הטענות שהם מייצגים. כאשר מעוניינים לנתח טיעון או הוכחה כלשהי באמצעות תחשיב הפסוקים, ראשית יש לערוך '''הצרנה''' להנחות ולטענות. בתהליך זה מסמנים כל [[משפט (בלשנות)|משפט]] בסיסי (למשל 'השמש תזרח מחר' או 'יוסי גר בלונדון') בסימן קבוע (בדרך כלל אות אנגלית גדולה כמו <math>P</math> או <math>Q</math>, או הסימן <math>P_i</math> עם האינדקס <math>i</math>, המייצג מספר מסוים). סימן זה מייצג את הטענה בכל מקום שתופיע בטיעון, והוא מכונה "פסוק יסודי", או "פסוק אטומי". גם הקָשַרים הלוגיים אינם נכתבים בתחשיב הפסוקים במילים אלא באמצעות סימונים מוסכמים, כפי שיוסבר להלן:

 

תחשיב פסוקים מסוים כולל קבוצה של '''פסוקים יסודיים''' או "פסוקים אטומיים", ומספר קָשַרים לוגיים סטנדרטיים. לדוגמה, נגדיר ש-<math>P</math> מייצג את הטענה "הגביע הוא שלנו", ו-<math>Q</math> מייצג את הטענה "אנחנו במפה"'. או אז ניתן להדגים את התחביר של חמשת הקשרים הלוגיים כך:

:'''הֵלחֵם''', או: '''קוֹנְיוּנְקְצִיָּה''' ("וגם"): <math>\land</math> או & - קשר בינארי, מקשר בין שני פסוקים. לדוגמה, הפסוק המורכב <math>P \land Q</math> מייצג את הטענה "הגביע הוא שלנו ואנחנו על המפה".

 

=== נוסחה בנויה כהלכה (נוסחה בנויה היטב) ===

* אם <math>A</math> ו-<math>B</math> נוסחאות בנויות היטב, אז לכל קשר <math>\Omega</math> כך ש <math>\Omega \in \{ \to,\land,\vee,\leftrightarrow \}</math>, הרי ש <math>(A \,\Omega\, B)</math> היא נוסחה בנויה היטב (דהיינו עבור כל שתי נוסחאות בנויות היטב, הצבתו של אחד מן הקשרים הבינריים ביניהן יוצרת נוסחה בנויה היטב).

* כל דבר אחר איננו נוסחה בנויה היטב.

 

 

אפשר לבנות סוגים שונים של תחשיבי פסוקים, באמצעות בחירה שונה של הקשרים המשתתפים. לדוגמה, אפשר להחליף את הקשר "אם <math>a</math> אז <math>b</math>" ב-"<math>b</math> או (לא <math>a</math>)", וכך להגדיר את הקשר 'אם-אז' באמצעות הקשרים "או" ו"לא". [[כללי דה-מורגן]] מאפשרים לוותר על אחד משני הקשרים "או" או "וגם".

=== תחשיב פסוקים שלם (קבוצת קשרים שלמה) ===

 

 

ישנם שני קשרים, שכל אחד מהם מהווה בעצמו "תחשיב פסוקים שלם", והם מכונים "הקשרים של שפר". קשרים אלו הם הקשרים "לא-וגם" ([[NAND לוגי|NAND]]) ו"לא-או" ([[NOR לוגי|NOR]]). התחביר הפורמלי של תחשיב הפסוקים המתמטי מתבסס על שני קשרים בלבד, "אם-אז" ו"לא" – כל שאר הקשרים מוגדרים כקיצורים של ביטויים הבנויים מקשרים בסיסיים אלו.

=== הנחות יסוד (אקסיומות) וכללי היסק ===

 

 

 

# <math>(p \to (q \to p))</math>

 

[[כלל היסק]] אחד, [[מודוס פוננס]] (קיומו של תנאי ונביעת טענה מקיומו של התנאי), המוגדר כך:

:ומ-<math>(p \to q)</math>

:הסק: <math>q</math>

 

:<math>a \land b</math> מוגדר כ- <math>\neg(a \to \neg b)</math>

:<math>a \leftrightarrow b</math> מוגדר כ- <math>\neg((a \to b) \to \neg (b \to a))</math>

'''דוגמה להוכחה'''. ניתן להוכיח מהמערכת הזו בקלות ש <math>a \to a</math>, כך:

 

::::::::::::::::::::::::אקסיומה 2 בו הצבנו <math>r=a, p=a</math> ו <math>q=(a\to a)</math>

::::::::::::::::::::::::אקסיומה 1 בו הצבנו <math>q=(a\to a), p=a</math>

::::::::::::::::::::::::[[מודוס פוננס]] על שורות 1 ו-2.

::::::::::::::::::::::::אקסיומה 1 בו הצבנו <math>p=a, q=a</math>

::::::::::::::::::::::::מודוס פוננס על שורות 3 ו-4: מש"ל.

 

{{הפניה לערך מורחב|טבלת אמת}}

 

 

לדוגמה, השלילה מחזירה פסוק שקרי עבור כל פסוק אמיתי אליו היא מקושרת, ומחזירה פסוק אמיתי עבור כל פסוק שקרי אליו היא מקושרת. נוח לייצג פונקציות אמת באמצעות [[טבלת אמת]], בהן T ו-F מייצגים את הערכים אמת ושקר (ב[[אלגברה בוליאנית]] יוחלפו אלו בערכים 1 עבור אמת ו-0 עבור שקר). בטורים הימניים של הטבלה אנו ממצים את כלל הצירופים האפשריים של ערכי האמת הניתנים לפסוקים היסודיים, ובטורים השמאליים אנו מציגים את ערך האמת המתקבל עבור הפסוק המורכב:

 

{|align="center" border="0" cellpadding="8"

 

|-align="center"

| F || T

|}

 

! | <math> P </math> || <math> Q </math> ||<math>P \to Q</math>

|-align="center"

 

|טבלת האמת של הקוניונקציה - ההֶלחֵם

! | <math> P </math> || <math> Q </math> ||<math>P \land Q</math>

|-align="center"

 

|טבלת האמת של הדיסיונקציה - הניתוק

! | <math> P </math> || <math> Q </math> ||<math>P \vee Q</math>

|-align="center"

|}

|טבלת האמת של התנאי הכפול

! | <math> P </math> || <math> Q </math> ||<math>P \leftrightarrow Q</math>

|-align="center"

 

=== טבלאות אמת ככלי לבדיקת תקפות טיעונים ===

 

לדוגמה, לבדיקת תקפות הטיעון:

# אם השמש זורחת האגם אינו קפוא

מסקנה: הברווזים לא עפים

 

יוצרנו הפסוקים האטומים על פי הלקסיקון (מילון תמציתי) הבא:

: <math>Q</math>: האגם קפוא

: <math>R</math>: הברווזים עפים

 

הטיעון המוצרן נכתב כך:

# <math>P \to \neg Q</math>

מסקנה: <math>\neg R</math>

 

וטבלת האמת שלו היא:

 

|-align="center"

|-align="center"

| 2 || T || T || F || F || F || T

|}

 

 

== מערכות הוכחה ==

 

 

 

 

=== דוגמאות למערכות הוכחה ===

דוגמה ל'''כלל הבאה''' (כלל הכנסה - אינטרודוקציה) להקשר של פסוק התנאי:

 

:: <math>\ Q</math>

––––––––––––––––––––––––

 

דוגמה ל'''כלל סילוק''' (כלל הוצאה - אלימינציה) להקשר של פסוק ההלחם (הקוניונקציה):

 

––––––––––––––––––––––––

 

* [[תחשיב הפרדיקטים]]

* [[שפה מסדר ראשון]]