שינויים
/* הוכחה */
::::::s אם"ם <math>P([s])</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>f(n):=10</math>
*שימו לב ש<math>P(n)</math> הוא הצבת n בנוסחא עם משתנה, ולכן גם מהווה נוחסחא בתאוריה ולכן יש לו מספר גדל.
דוגמא:
נניח והמשפט השלישי בתאוריה הוא נוסחא מספרית <math>P(x)=''x>2''</math>. במקרה זה <math>f(3)=[P(3)]=[''3>2'']</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])</math>. לכן עבור <math>\forall z:(z=f([B])\rightarrow P(z))</math>. בפרט, עבור <math>z=[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>s=B([B])</math> מקיים <math>s \iff P([s])</math> כפי שרצינו.
