הוכחת משפט אי השלימות הראשון של גדל - היסטוריית גרסאות

דביר654: /* הלמה של טרסקי (Diagonal lemma) */

2024-09-11T17:52:54Z

הלמה של טרסקי (Diagonal lemma)

→ הגרסה הקודמת		גרסה מ־17:52, 11 בספטמבר 2024
שורה 7:		שורה 7:

	===הלמה של טרסקי (Diagonal lemma)===		===הלמה של טרסקי (Diagonal lemma)===
	לכל פרדיקט עם משתנה מספרי אחד <math>P(x)</math> קיים בתאוריה משפט <math>s</math> עבורו:		לכל פרדיקט עם שניתן לכתוב ע"י לוגיקה מסדר ראשון משתנה מספרי אחד <math>P(x)</math> קיים בתאוריה משפט <math>s</math> עבורו:
	:<math>s\iff P([s])</math>		:<math>s\iff P([s])</math>

יהודה שמחה ב־08:41, 25 במרץ 2024

2024-03-25T08:41:23Z

→ הגרסה הקודמת		גרסה מ־08:41, 25 במרץ 2024
שורה 1:		שורה 1:
	חזרה ל[[משפטי אי השלימות של גדל (Gödel)]]		חזרה ל[[משפטי אי השלימות של גדל (Gödel)]]

	==הוכחת משפט ~~אי השלימות~~ הראשון של גדל==		==הוכחת משפט האי-שלימות הראשון של גדל==
			אוסף כל המשפטים בתאוריה הוא בן מנייה. על כן ניתן לתת לכל משפט בתאוריה מספר (הנקרא '''מספר גדל''') שאותו נסמן בסוגריים מרובעים.<br>
			לדוגמא: אם <math>''3 > 5''</math> הוא המשפט השלישי בתאוריה אזי <math>[''3>5'']=3</math>.<br>
			באופן דומה, נשתמש בסוגריים מסולסלים על מנת לחזור מהמספר אל המשפט. בדוגמא: <math>\{3\}=\,''\!3>5''</math>.

	~~מכיוון שאוסף כל המשפטים בתאורייה הוא בן מנייה ניתן לתת לכל משפט בתאוריה מספר~~ (~~הנקרא '''מספר גדל'''~~)~~, נסמן מספר זה בסוגריים מרובעים. לדוגמא: אם~~ <math>~~''3 > 5''~~</math> ~~הוא המשפט השלישי בתאורייה אזי~~ <math>~~[''3 > 5'']=3~~</math>~~. באופן דומה, נשתמש בסוגריים מסולסלים על מנת לחזור מהמספר אל המשפט. בדוגמא~~: <math>\~~{3\}=''3 > 5''~~</math>.		===הלמה של טרסקי (Diagonal lemma)===
			לכל פרדיקט עם משתנה מספרי אחד <math>P(x)</math> קיים בתאוריה משפט <math>s</math> עבורו:
			:<math>s\iff P([s])</math>

	~~===הלמה של טרצקי (Diagonal lemma)===~~
	~~::--לכל פרדיקט עם משתנה מספרי אחד <math>P(x)</math> קיים בתאוריה משפט s כך ש:~~

	~~::::::s אם"ם <math>P([s])</math>~~
	===הוכחה===		===הוכחה===
	נגדיר פונקציה <math>f:\~~mathbb{~~N}\~~rightarrow~~\~~mathbb{~~N}\cup\{0\}</math> באופן הבא:		נגדיר פונקציה <math>f:\N\to\N\cup\{0\}</math> באופן הבא:
	::אם <math>\{n\}</math> הוא נוסחא ~~עם משתנה~~ מספרי יחיד ~~<math>Q(x)=\{n\}</math>~~ אזי <math>f(n):=[Q(n)]</math>		:אם <math>\{n\}=Q(x)</math> הוא נוסחא במשתנה מספרי יחיד אזי <math>f(n):=[Q(n)]</math>.
	::אחרת, <math>f(n):=0</math>		:אחרת <math>f(n):=0</math>.
			*שימו לב כי <math>Q(n)</math> הוא הצבת <math>n</math> בנוסחא עם משתנה, ולכן גם מהווה נוסחא בתאוריה ולכן יש לו מספר גדל.
	*שימו לב ש<math>Q(n)</math> הוא הצבת n בנוסחא עם משתנה, ולכן גם מהווה נוסחא בתאוריה ולכן יש לו מספר גדל.
	*כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור. בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא.		*כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור. בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא.


	דוגמא:		דוגמא:
	נניח ~~והמשפט~~ השלישי בתאוריה הוא נוסחא מספרית <math>Q(x)=''x>2''</math>. במקרה זה <math>f(3)=[Q(3)]=[''3>2'']</math>		נניח כי המשפט השלישי בתאוריה הוא נוסחא מספרית <math>Q(x)=\,''\!x>2''</math>. במקרה זה <math>f(3)=[Q(3)]=[''3>2'']</math>.


	נגדיר כעת את הנוסחא הבאה <math>B(x)=P(f(x))</math>.		נגדיר כעת את הנוסחא הבאה <math>B(x)=P(f(x))</math>.

	:'''טענה''': <math>B([B])\iff P([B([B])])</math> לכל x		'''טענה''':
			<math>B([B])\iff P([B([B])])</math> לכל <math>x</math>.
	~~'''הוכחה''':~~
	~~נניח~~ <math>~~B([B])</math>. לכן <math>P(f([B]))</math>. נשים לב כי <math>f([B])=[B([B])]</math>. נובע כי <math>P([B([B])])~~</math> ~~כפי שרצינו~~.

			====הוכחה====
			כיוון אחד: נניח <math>B([B])</math>. לכן <math>P(f([B]))</math>. נשים לב כי <math>f([B])=[B([B])]</math>. נובע כי <math>P([B([B])])</math> כפי שרצינו.

	~~מצד~~ שני, נניח <math>P([B([B])])</math>. ~~כיוון ש~~<math>f([B])=[B([B])]</math> נובע כי <math>P(f([B])))</math> לכן לפי ההגדרה <math>B([B])</math>.		כיוון שני: נניח <math>P([B([B])])</math>. מהעובדה כי <math>f([B])=[B([B])]</math> נובע כי <math>P(f([B]))</math> לכן לפי ההגדרה <math>B([B])</math>.


	'''מסקנה''': המשפט <math>s=B([B])</math> מקיים:		'''מסקנה''': המשפט <math>s=B([B])</math> מקיים:
	::<math>P([s])~~\iff s~~</math>		:<math>s\iff P([s])</math>
	כפי שרצינו.		כפי שרצינו.

	===סיום הוכחת משפט ~~אי השלימות~~ הראשון של גדל בעזרת הלמה של ~~טרצקי~~===		===סיום הוכחת משפט האי-שלימות הראשון של גדל בעזרת הלמה של טרסקי===
	שימו לב ~~שמתוך~~ הלמה של ~~טרצקי~~ לא ניתן להגדיר את קבוצת כל המשפטים שהם 'אמת'. הרי אם ~~הייתה~~ קבוצה כזו, היה ~~ניתן~~ להגדיר נוסחא מספרית <math>=P(x)</math> "{x} אינו שייך לקבוצת המשפטים שהם 'אמת' ". לפי הלמה קיים משפט השקול לכך שאינו בקבוצת האמת, ולכן אם הוא אמת הוא אינו אמת, ואם הוא אינו אמת הוא אמת. (זו סתירה הדומה לפרדוקס של ראסל.)		שימו לב כי מתוך הלמה של טרסקי לא ניתן להגדיר את קבוצת כל המשפטים שהם 'אמת'. הרי אם היתה קבוצה כזו, אזי ניתן היה להגדיר נוסחא מספרית
			:<math>=P(x)</math> "<math>\{x\}</math> אינו שייך לקבוצת המשפטים שהם 'אמת'".
			לפי הלמה קיים משפט השקול לכך שאינו בקבוצת האמת, ולכן אם הוא אמת הוא אינו אמת, ואם הוא אינו אמת הוא אמת. (זו סתירה הדומה לפרדוקס של ראסל.)

	לעומת זאת, מכיוון שאוסף כל הטקסטים בשפה הוא בן מנייה, בפרט אוסף ההוכחות הוא בין מנייה, ולכן ניתן להגדיר את קבוצת כל המשפטים שניתן להוכיח (הם פשוט השורה האחרונה של כל הוכחה תקינה). נגדיר את הנוסחא <math>=P(x)</math> "{x} אינו שייך לקבוצת המשפטים הניתנים להוכחה ". כעת לפי הלמה של ~~טרוצקי~~ יש משפט השקול לכך שהוא אינו בקבוצת המשפטים הניתנים להוכחה. אם הוא היה שקר, סימן שהוא ניתן להוכחה ולכן הוא אמת וזו סתירה. אם הוא אמת, לעומת זאת, אין סתירה אך הוא אינו ניתן להוכחה.		לעומת זאת, מכיוון שאוסף כל הטקסטים בשפה הוא בן מנייה, בפרט אוסף ההוכחות הוא בין מנייה, ולכן ניתן להגדיר את קבוצת כל המשפטים שניתן להוכיח (הם פשוט השורה האחרונה של כל הוכחה תקינה). נגדיר את הנוסחא
			:<math>=P(x)</math> "<math>\{x\}</math> אינו שייך לקבוצת המשפטים הניתנים להוכחה".
			כעת לפי הלמה של טרסקי יש משפט השקול לכך שהוא אינו בקבוצת המשפטים הניתנים להוכחה. אם הוא היה שקר, סימן שהוא ניתן להוכחה ולכן הוא אמת וזו סתירה. אם הוא אמת, לעומת זאת, אין סתירה אך הוא אינו ניתן להוכחה.

	מכאן המשפט נובע באופן ישיר: או שהתאוריה אינה שלימה (~~היא מכילה סתירה~~) או שהיא אינה עקבית (~~קיים משפט שלא ניתן להוכיחו ולא ניתן להפריכו~~).		מכאן המשפט נובע באופן ישיר: או שהתאוריה אינה שלימה (קיים משפט שלא ניתן להוכיחו או להפריכו) או שהיא אינה עקבית (היא מכילה סתירה).

ארז שיינר ב־12:36, 28 באפריל 2020

2020-04-28T12:36:18Z

→ הגרסה הקודמת		גרסה מ־12:36, 28 באפריל 2020
שורה 11:		שורה 11:
	===הוכחה===		===הוכחה===
	נגדיר פונקציה <math>f:\mathbb{N}\rightarrow\mathbb{N}\cup\{0\}</math> באופן הבא:		נגדיר פונקציה <math>f:\mathbb{N}\rightarrow\mathbb{N}\cup\{0\}</math> באופן הבא:
	::אם <math>\{n\}</math> הוא נוסחא עם משתנה מספרי יחיד <math>P(x)=\{n\}</math> אזי <math>f(n):=[P(n)]</math>		::אם <math>\{n\}</math> הוא נוסחא עם משתנה מספרי יחיד <math>Q(x)=\{n\}</math> אזי <math>f(n):=[Q(n)]</math>
	::אחרת, <math>f(n):=0</math>		::אחרת, <math>f(n):=0</math>

	*שימו לב ש<math>P(n)</math> הוא הצבת n בנוסחא עם משתנה, ולכן גם מהווה ~~נוחסחא~~ בתאוריה ולכן יש לו מספר גדל.		*שימו לב ש<math>Q(n)</math> הוא הצבת n בנוסחא עם משתנה, ולכן גם מהווה נוסחא בתאוריה ולכן יש לו מספר גדל.
	*כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור. בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא.		*כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור. בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא.


	דוגמא:		דוגמא:
	נניח והמשפט השלישי בתאוריה הוא נוסחא מספרית <math>P(x)=''x>2''</math>. במקרה זה <math>f(3)=[P(3)]=[''3>2'']</math>		נניח והמשפט השלישי בתאוריה הוא נוסחא מספרית <math>Q(x)=''x>2''</math>. במקרה זה <math>f(3)=[Q(3)]=[''3>2'']</math>


	נגדיר כעת את הנוסחא הבאה <math>B(x)=~~\forall z:~~(z=f(x~~)\rightarrow P(z~~))</math>.		נגדיר כעת את הנוסחא הבאה <math>B(x)=P(f(x))</math>.

	:'''טענה''': <math>B([B])\iff P([B([B])])</math> לכל x		:'''טענה''': <math>B([B])\iff P([B([B])])</math> לכל x

	'''הוכחה''':		'''הוכחה''':
	נניח <math>B([B])</math>. לכן ~~עבור~~ <math>~~\forall z:~~(z=f([B]~~)\rightarrow P(z~~))</math>. נשים לב כי <math>f([B])=[B([B])]</math>. ~~בפרט, עבור <math>z=[B([B])]</math>~~ נובע כי <math>P([B([B])])</math> כפי שרצינו.		נניח <math>B([B])</math>. לכן <math>P(f([B]))</math>. נשים לב כי <math>f([B])=[B([B])]</math>. נובע כי <math>P([B([B])])</math> כפי שרצינו.


	מצד שני, נניח <math>P([B([B])])</math>. אם <math>~~z\neq[B~~([B])~~]</math> אזי שקר גורר כל דבר ובפרט את <math>P(z)</math>. אם <math>z~~=[B([B])]</math> ~~אזי~~ <math>~~z=[B~~([B])~~]\rightarrow P(z~~)</math> ~~שכן אמת גוררת אמת. ולכן סה"כ, הגרירה נכונה לכל <math>z</math> ולכן~~ <math>B([B])</math>.		מצד שני, נניח <math>P([B([B])])</math>. כיוון ש<math>f([B])=[B([B])]</math> נובע כי <math>P(f([B])))</math> לכן לפי ההגדרה <math>B([B])</math>.

ארז שיינר ב־12:31, 28 באפריל 2020

2020-04-28T12:31:22Z

→ הגרסה הקודמת		גרסה מ־12:31, 28 באפריל 2020
שורה 11:		שורה 11:
	===הוכחה===		===הוכחה===
	נגדיר פונקציה <math>f:\mathbb{N}\rightarrow\mathbb{N}\cup\{0\}</math> באופן הבא:		נגדיר פונקציה <math>f:\mathbb{N}\rightarrow\mathbb{N}\cup\{0\}</math> באופן הבא:
	::אם <math>\{n\}</math> הוא נוסחא עם משתנה מספרי יחיד <math>Q(x)=\{n\}</math> אזי <math>f(n):=[Q(n)]</math>		::אם <math>\{n\}</math> הוא נוסחא עם משתנה מספרי יחיד <math>P(x)=\{n\}</math> אזי <math>f(n):=[P(n)]</math>
	::אחרת, <math>f(n):=0</math>		::אחרת, <math>f(n):=0</math>

	*שימו לב ש<math>Q(n)</math> הוא הצבת n בנוסחא עם משתנה, ולכן גם מהווה ~~נוסחא~~ בתאוריה ולכן יש לו מספר גדל.		*שימו לב ש<math>P(n)</math> הוא הצבת n בנוסחא עם משתנה, ולכן גם מהווה נוחסחא בתאוריה ולכן יש לו מספר גדל.
	*כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור. בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא.		*כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור. בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא.


	דוגמא:		דוגמא:
	נניח והמשפט השלישי בתאוריה הוא נוסחא מספרית <math>Q(x)=''x>2''</math>. במקרה זה <math>f(3)=[Q(3)]=[''3>2'']</math>		נניח והמשפט השלישי בתאוריה הוא נוסחא מספרית <math>P(x)=''x>2''</math>. במקרה זה <math>f(3)=[P(3)]=[''3>2'']</math>


	נגדיר כעת את הנוסחא הבאה <math>B(x)=P(f(x))</math>.		נגדיר כעת את הנוסחא הבאה <math>B(x)=\forall z:(z=f(x)\rightarrow P(z))</math>.

	:'''טענה''': <math>B([B])\iff P([B([B])])</math> לכל x		:'''טענה''': <math>B([B])\iff P([B([B])])</math> לכל x

	'''הוכחה''':		'''הוכחה''':
	נניח <math>B([B])</math>. לכן <math>P(f([B]))</math>. נשים לב כי <math>f([B])=[B([B])]</math>. נובע כי <math>P([B([B])])</math> כפי שרצינו.		נניח <math>B([B])</math>. לכן עבור <math>\forall z:(z=f([B])\rightarrow P(z))</math>. נשים לב כי <math>f([B])=[B([B])]</math>. בפרט, עבור <math>z=[B([B])]</math> נובע כי <math>P([B([B])])</math> כפי שרצינו.

ארז שיינר: /* הוכחה */

2020-04-28T12:28:45Z

הוכחה

→ הגרסה הקודמת		גרסה מ־12:28, 28 באפריל 2020
שורה 22:		שורה 22:


	נגדיר כעת את הנוסחא הבאה <math>B(x)=~~\forall z:~~(z=f(x~~)\rightarrow P(z~~))</math>.		נגדיר כעת את הנוסחא הבאה <math>B(x)=P(f(x))</math>.

	:'''טענה''': <math>B([B])\iff P([B([B])])</math> לכל x		:'''טענה''': <math>B([B])\iff P([B([B])])</math> לכל x

	'''הוכחה''':		'''הוכחה''':
	נניח <math>B([B])</math>. לכן ~~עבור~~ <math>~~\forall z:~~(z=f([B]~~)\rightarrow P(z~~))</math>. נשים לב כי <math>f([B])=[B([B])]</math>. ~~בפרט, עבור <math>z=[B([B])]</math>~~ נובע כי <math>P([B([B])])</math> כפי שרצינו.		נניח <math>B([B])</math>. לכן <math>P(f([B]))</math>. נשים לב כי <math>f([B])=[B([B])]</math>. נובע כי <math>P([B([B])])</math> כפי שרצינו.

ארז שיינר: /* הוכחה */

2020-04-28T12:24:39Z

הוכחה

→ הגרסה הקודמת		גרסה מ־12:24, 28 באפריל 2020
שורה 11:		שורה 11:
	===הוכחה===		===הוכחה===
	נגדיר פונקציה <math>f:\mathbb{N}\rightarrow\mathbb{N}\cup\{0\}</math> באופן הבא:		נגדיר פונקציה <math>f:\mathbb{N}\rightarrow\mathbb{N}\cup\{0\}</math> באופן הבא:
	::אם <math>\{n\}</math> הוא נוסחא עם משתנה מספרי יחיד <math>P(x)=\{n\}</math> אזי <math>f(n):=[P(n)]</math>		::אם <math>\{n\}</math> הוא נוסחא עם משתנה מספרי יחיד <math>Q(x)=\{n\}</math> אזי <math>f(n):=[Q(n)]</math>
	::אחרת, <math>f(n):=0</math>		::אחרת, <math>f(n):=0</math>

	*שימו לב ש<math>P(n)</math> הוא הצבת n בנוסחא עם משתנה, ולכן גם מהווה ~~נוחסחא~~ בתאוריה ולכן יש לו מספר גדל.		*שימו לב ש<math>Q(n)</math> הוא הצבת n בנוסחא עם משתנה, ולכן גם מהווה נוסחא בתאוריה ולכן יש לו מספר גדל.
	*כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור. בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא.		*כמו כן, שימו לב כי שיטה זו דומה לשיטת האלכסון של קנטור. בכל נוסחא אנו מציבים את מספר הגדל של הנוסחא.


	דוגמא:		דוגמא:
	נניח והמשפט השלישי בתאוריה הוא נוסחא מספרית <math>P(x)=''x>2''</math>. במקרה זה <math>f(3)=[P(3)]=[''3>2'']</math>		נניח והמשפט השלישי בתאוריה הוא נוסחא מספרית <math>Q(x)=''x>2''</math>. במקרה זה <math>f(3)=[Q(3)]=[''3>2'']</math>

ארז שיינר: /* סיום הוכחת משפט אי השלימות הראשון של גדל בעזרת הלמה של טרצקי */

2011-10-13T08:37:14Z

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

→ הגרסה הקודמת		גרסה מ־08:37, 13 באוקטובר 2011
שורה 42:		שורה 42:
	לעומת זאת, מכיוון שאוסף כל הטקסטים בשפה הוא בן מנייה, בפרט אוסף ההוכחות הוא בין מנייה, ולכן ניתן להגדיר את קבוצת כל המשפטים שניתן להוכיח (הם פשוט השורה האחרונה של כל הוכחה תקינה). נגדיר את הנוסחא <math>=P(x)</math> "{x} אינו שייך לקבוצת המשפטים הניתנים להוכחה ". כעת לפי הלמה של טרוצקי יש משפט השקול לכך שהוא אינו בקבוצת המשפטים הניתנים להוכחה. אם הוא היה שקר, סימן שהוא ניתן להוכחה ולכן הוא אמת וזו סתירה. אם הוא אמת, לעומת זאת, אין סתירה אך הוא אינו ניתן להוכחה.		לעומת זאת, מכיוון שאוסף כל הטקסטים בשפה הוא בן מנייה, בפרט אוסף ההוכחות הוא בין מנייה, ולכן ניתן להגדיר את קבוצת כל המשפטים שניתן להוכיח (הם פשוט השורה האחרונה של כל הוכחה תקינה). נגדיר את הנוסחא <math>=P(x)</math> "{x} אינו שייך לקבוצת המשפטים הניתנים להוכחה ". כעת לפי הלמה של טרוצקי יש משפט השקול לכך שהוא אינו בקבוצת המשפטים הניתנים להוכחה. אם הוא היה שקר, סימן שהוא ניתן להוכחה ולכן הוא אמת וזו סתירה. אם הוא אמת, לעומת זאת, אין סתירה אך הוא אינו ניתן להוכחה.

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

ארז שיינר: /* הוכחת משפט אי השלימות הראשון של גדל */

2011-10-13T08:36:49Z

הוכחת משפט אי השלימות הראשון של גדל

→ הגרסה הקודמת		גרסה מ־08:36, 13 באוקטובר 2011
שורה 36:		שורה 36:
	::<math>P([s])\iff s</math>		::<math>P([s])\iff s</math>
	כפי שרצינו.		כפי שרצינו.

			===סיום הוכחת משפט אי השלימות הראשון של גדל בעזרת הלמה של טרצקי===
			שימו לב שמתוך הלמה של טרצקי לא ניתן להגדיר את קבוצת כל המשפטים שהם 'אמת'. הרי אם הייתה קבוצה כזו, היה ניתן להגדיר נוסחא מספרית <math>=P(x)</math> "{x} אינו שייך לקבוצת המשפטים שהם 'אמת' ". לפי הלמה קיים משפט השקול לכך שאינו בקבוצת האמת, ולכן אם הוא אמת הוא אינו אמת, ואם הוא אינו אמת הוא אמת. (זו סתירה הדומה לפרדוקס של ראסל.)

			לעומת זאת, מכיוון שאוסף כל הטקסטים בשפה הוא בן מנייה, בפרט אוסף ההוכחות הוא בין מנייה, ולכן ניתן להגדיר את קבוצת כל המשפטים שניתן להוכיח (הם פשוט השורה האחרונה של כל הוכחה תקינה). נגדיר את הנוסחא <math>=P(x)</math> "{x} אינו שייך לקבוצת המשפטים הניתנים להוכחה ". כעת לפי הלמה של טרוצקי יש משפט השקול לכך שהוא אינו בקבוצת המשפטים הניתנים להוכחה. אם הוא היה שקר, סימן שהוא ניתן להוכחה ולכן הוא אמת וזו סתירה. אם הוא אמת, לעומת זאת, אין סתירה אך הוא אינו ניתן להוכחה.

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

ארז שיינר: /* הוכחה */

2011-10-13T07:21:35Z

הוכחה

→ הגרסה הקודמת		גרסה מ־07:21, 13 באוקטובר 2011
שורה 33:		שורה 33:


	'''מסקנה''': המשפט <math>s=B([B])</math> מקיים		'''מסקנה''': המשפט <math>s=B([B])</math> מקיים:
	::--<math>P([s])\iff s</math> כפי שרצינו.		::<math>P([s])\iff s</math>
			כפי שרצינו.

ארז שיינר: /* הוכחת משפט אי השלימות הראשון של גדל */

2011-10-13T07:21:06Z

הוכחת משפט אי השלימות הראשון של גדל

→ הגרסה הקודמת		גרסה מ־07:21, 13 באוקטובר 2011
שורה 33:		שורה 33:


	'''מסקנה''': המשפט <math>s=B([B])</math> מקיים <math>~~s \iff~~ P([s])</math> כפי שרצינו.		'''מסקנה''': המשפט <math>s=B([B])</math> מקיים
			::--<math>P([s])\iff s</math> כפי שרצינו.