ในตรรกศาสตร์ทางคณิตศาสตร์บทพิสูจน์แนวทแยง (หรือที่รู้จักกันในชื่อบทพิสูจน์การทำให้เป็นแนวทแยงบทพิสูจน์การอ้างอิงตนเองหรือทฤษฎีบทจุดตรึง ) พิสูจน์การมีอยู่ของ ประโยค ที่อ้างอิงตนเองในทฤษฎีเชิงรูปธรรมบางอย่าง

ตัวอย่างเฉพาะของบทพิสูจน์แนวทแยงถูกใช้โดยKurt Gödelในปี 1931 เพื่อสร้างการพิสูจน์ทฤษฎีบทความไม่สมบูรณ์ ของเขา เช่นเดียวกับที่Tarski ใช้ เพื่อพิสูจน์ทฤษฎีบทความไม่สามารถนิยามได้ ในปี 1933 ในปี 1934 Carnapเป็นคนแรกที่ตีพิมพ์บทพิสูจน์แนวทแยงในระดับทั่วไป^{[ 1 ]}บทพิสูจน์แนวทแยงได้รับการตั้งชื่อโดยอ้างอิงถึงการโต้แย้งแนวทแยงของ Cantorในทฤษฎีเซตและทฤษฎี จำนวน

บทพิสูจน์แนวทแยงใช้ได้กับทฤษฎีที่แข็งแกร่งเพียงพอใดๆ ที่สามารถแสดงฟังก์ชันแนวทแยงได้ ทฤษฎีดังกล่าวรวมถึงพีชคณิตพีอาโนลำดับที่หนึ่งพีชคณิตโรบินสันที่อ่อนกว่ารวมถึงทฤษฎีใดๆ ที่มี(เช่น ที่ตีความ) ^{[ 2 ]}ข้อความทั่วไปของบทพิสูจน์ (ดังที่แสดงด้านล่าง) ตั้งสมมติฐานที่แข็งแกร่งกว่าว่าทฤษฎีสามารถแสดงฟังก์ชันที่คำนวณได้ทั้งหมด (ทั้งหมด)แต่ทฤษฎีทั้งหมดที่กล่าวถึงก็มีศักยภาพนั้นเช่นกัน ${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {Q}}}$${\displaystyle {\mathsf {Q}}}$

บทพิสูจน์แนวทแยงยังต้องการการกำหนดหมายเลขแบบ Gödel ด้วย เราเขียนแทนรหัสที่กำหนดให้กับโดยการกำหนดหมายเลข สำหรับตัวเลขมาตรฐานของ(เช่นและ) ให้ เป็นตัวเลขมาตรฐานของรหัสของ(เช่นคือ) เราถือว่ามีการกำหนดหมายเลขแบบ Gödel มาตรฐาน${\displaystyle \alpha }$${\displaystyle \alpha (\varphi )}$${\displaystyle \varphi }$${\displaystyle {\overline {n}}}$${\displaystyle n}$${\displaystyle {\overline {0}}=_{df}{\mathsf {0}}}$${\displaystyle {\overline {n+1}}=_{df}{\mathsf {S}}({\overline {n}})}$${\displaystyle \ulcorner \varphi \urcorner }$${\displaystyle \varphi }$${\displaystyle \ulcorner \varphi \urcorner }$${\displaystyle {\overline {\alpha (\varphi )}}}$

ให้เป็นเซตของจำนวนธรรมชาติทฤษฎีอันดับแรกในภาษาเลขคณิตที่ประกอบด้วยแสดงถึงฟังก์ชัน ที่คำนวณได้ แบบn-ary (ทั้งหมด) ถ้ามีสูตรในภาษาของเช่นนั้น สำหรับทุกถ้าแล้ว${\displaystyle \mathbb {N} }$${\displaystyle T}$${\displaystyle {\mathsf {Q}}}$${\displaystyle k}$${\displaystyle f:\mathbb {N} ^{k}\rightarrow \mathbb {N} }$${\displaystyle \varphi _{f}(x_{1},\dots ,x_{k},y)}$${\displaystyle T}$${\displaystyle m_{1},\dots ,m_{k}\in \mathbb {N} }$${\displaystyle f(m_{1},\dots ,m_{k})=n}$${\displaystyle T\vdash \forall y(\varphi _{f}({\overline {m_{1}}},\dots ,{\overline {m_{k}}},y)\leftrightarrow y={\overline {n}})}$

ทฤษฎีบทการแสดงแทนเป็นจริง กล่าวคือ ฟังก์ชันที่คำนวณได้ทุกฟังก์ชันสามารถแสดงแทนได้ใน^{[ 3 ]}${\displaystyle T}$

ทฤษฎีบทแนวทแยง : ให้เป็นทฤษฎีลำดับที่หนึ่งที่ประกอบด้วย( เลขคณิตของโรบินสัน ) และให้เป็นสูตรใดๆ ในภาษาของโดยที่ เป็นตัวแปรอิสระเพียงตัวเดียวแล้วจะมีประโยคในภาษาของเช่นนั้น ${\displaystyle T}$${\displaystyle {\mathsf {Q}}}$${\displaystyle \psi (x)}$${\displaystyle T}$${\displaystyle x}$${\displaystyle \varphi }$${\displaystyle T}$${\displaystyle T\vdash \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner )}$

โดยสัญชาตญาณแล้ว ประโยค นี้เป็น ประโยค ที่อ้างอิงถึงตัวเองซึ่ง "กล่าวถึงตัวมันเองว่ามีคุณสมบัตินั้น" ${\displaystyle \varphi }$${\displaystyle \psi }$

บทพิสูจน์ : ให้เป็นฟังก์ชันที่คำนวณได้ ซึ่งเชื่อมโยงรหัสของแต่ละสูตรกับตัวแปรอิสระเพียงตัวเดียวในภาษาของกับรหัสของสูตรปิด(กล่าวคือ การแทนที่ลงในสำหรับ) และสำหรับอาร์กิวเมนต์อื่นๆ (ข้อเท็จจริงที่ว่าสามารถคำนวณได้นั้นขึ้นอยู่กับการเลือกหมายเลขของ Gödel ซึ่งในที่นี้คือหมายเลขมาตรฐาน ) ${\displaystyle diag_{T}:\mathbb {N} \to \mathbb {N} }$${\displaystyle \varphi (x)}$${\displaystyle x}$${\displaystyle T}$${\displaystyle \varphi (\ulcorner \varphi \urcorner )}$${\displaystyle \ulcorner \varphi \urcorner }$${\displaystyle \varphi }$${\displaystyle x}$${\displaystyle 0}$${\displaystyle diag_{T}}$

ตามทฤษฎีบทการ แทน ค่า แทนฟังก์ชันที่คำนวณได้ทุกฟังก์ชัน ดังนั้นจึงมีสูตรที่แทนโดยเฉพาะสำหรับแต่ละ${\displaystyle T}$${\displaystyle \delta (x,y)}$${\displaystyle diag_{T}}$${\displaystyle \varphi (x)}$${\displaystyle T\vdash \delta (\ulcorner \varphi \urcorner ,y)\leftrightarrow y=\ulcorner \varphi (\ulcorner \varphi \urcorner )\urcorner }$

ให้เป็นสูตรใดๆ ที่มีเพียงเป็นตัวแปรอิสระ ตอนนี้เรากำหนดให้ เป็นและให้เป็นแล้วความสมมูลต่อไปนี้สามารถพิสูจน์ได้ใน: ${\displaystyle \psi (x)}$${\displaystyle x}$${\displaystyle \chi (x)}$${\displaystyle \exists y(\delta (x,y)\land \psi (y))}$${\displaystyle \varphi }$${\displaystyle \chi (\ulcorner \chi \urcorner )}$${\displaystyle T}$

${\displaystyle \varphi \leftrightarrow \chi (\ulcorner \chi \urcorner )\leftrightarrow \exists y(\delta (\ulcorner \chi \urcorner ,y)\land \psi (y))\leftrightarrow \exists y(y=\ulcorner \chi (\ulcorner \chi \urcorner )\urcorner \land \psi (y))\leftrightarrow \exists y(y=\ulcorner \varphi \urcorner \land \psi (y))\leftrightarrow \psi (\ulcorner \varphi \urcorner )}$.

มีการสรุปทั่วไปต่างๆ ของบทพิสูจน์แนวทแยง เราจะนำเสนอเพียงบางส่วนเท่านั้น โดยเฉพาะอย่างยิ่ง การรวมกันของการสรุปทั่วไปสามประการแรกด้านล่างจะให้ผลลัพธ์เป็นการสรุปทั่วไปใหม่^{[ 4 ]}ให้เป็นทฤษฎีลำดับแรกที่มี( เลขคณิตโรบินสัน ) ${\displaystyle T}$${\displaystyle {\mathsf {Q}}}$

ให้เป็นสูตรใดๆ ที่มีตัวแปรอิสระ ${\displaystyle \psi (x,y_{1},\dots ,y_{n})}$${\displaystyle x,y_{1},\dots ,y_{n}}$

จากนั้นจะมีสูตรที่มีตัวแปรอิสระซึ่งทำให้. ${\displaystyle \varphi (y_{1},\dots y_{n})}$${\displaystyle y_{1},\dots ,y_{n}}$${\displaystyle T\vdash \varphi (y_{1},\dots ,y_{n})\leftrightarrow \psi (\ulcorner \varphi (y_{1},\dots ,y_{n})\urcorner ,y_{1},\dots ,y_{n})}$

ให้เป็นสูตรใดๆ ที่มีตัวแปรอิสระ ${\displaystyle \psi (x,y_{1},\dots ,y_{n})}$${\displaystyle x,y_{1},\dots ,y_{n}}$

จากนั้นจะมีสูตรที่มีตัวแปรอิสระซึ่งสำหรับทุก ๆ, . ${\displaystyle \varphi (y_{1},\dots y_{n})}$${\displaystyle y_{1},\dots ,y_{n}}$${\displaystyle m_{1},\dots ,m_{n}\in \mathbb {N} }$${\displaystyle T\vdash \varphi ({\overline {m_{1}}},\dots ,{\overline {m_{n}}})\leftrightarrow \psi (\ulcorner \varphi ({\overline {m_{1}}},\dots ,{\overline {m_{n}}})\urcorner ,{\overline {m_{1}}},\dots ,{\overline {m_{n}}})}$

ให้และเป็นสูตรที่มีตัวแปรอิสระและ ตามลำดับ ${\displaystyle \psi _{1}(x_{1},x_{2})}$${\displaystyle \psi _{2}(x_{1},x_{2})}$${\displaystyle x_{1}}$${\displaystyle x_{2}}$

จากนั้นก็มีประโยคและเช่นนั้น และ${\displaystyle \varphi _{1}}$${\displaystyle \varphi _{2}}$${\displaystyle T\vdash \varphi _{1}\leftrightarrow \psi _{1}(\ulcorner \varphi _{1}\urcorner ,\ulcorner \varphi _{2}\urcorner )}$${\displaystyle T\vdash \varphi _{2}\leftrightarrow \psi _{2}(\ulcorner \varphi _{1}\urcorner ,\ulcorner \varphi _{2}\urcorner )}$

กรณีของสูตรหลายๆ สูตรก็คล้ายคลึงกัน ${\displaystyle n}$

ให้เป็นสูตรใดๆ ในภาษาของโดยที่เป็นตัวแปรอิสระเพียงตัวเดียว แล้วจะมีพจน์ในภาษาของเช่นนั้น ${\displaystyle \psi (x)}$${\displaystyle T}$${\displaystyle x}$${\displaystyle t}$${\displaystyle T}$${\displaystyle T\vdash t=\ulcorner \psi (t)\urcorner }$

โดยทั่วไปแล้ว บทพิสูจน์แนวทแยงมุมเป็นผลมาจากบทพิสูจน์แนวทแยงมุมที่แข็งแกร่ง (ให้เป็น) อย่างไรก็ตาม โปรดทราบว่าบทพิสูจน์แนวทแยงมุมที่แข็งแกร่งนั้นขึ้นอยู่กับภาษาของ โดยเฉพาะอย่างยิ่งขึ้นอยู่กับว่ามีเทอมดังกล่าวหรือไม่โดยทั่วไป บทพิสูจน์แนวทแยงมุมที่แข็งแกร่งจะล้มเหลวสำหรับทฤษฎีในภาษาพื้นฐานของเลขคณิต (เช่น หรือ) แต่จะใช้ได้กับเลขคณิตแบบเรียกซ้ำดั้งเดิมซึ่งมีสัญลักษณ์ฟังก์ชันสำหรับแต่ละฟังก์ชันแบบเรียกซ้ำดั้งเดิม^{[ 5 ]}${\displaystyle \varphi (x)}$${\displaystyle \psi (t)}$${\displaystyle T}$${\displaystyle t}$${\displaystyle {\mathsf {Q}}}$${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {PRA}}}$

บทพิสูจน์นี้เรียกว่า "แนวทแยง" เพราะมีความคล้ายคลึงกับบทพิสูจน์แนวทแยงของแคนเตอร์ [ ^{6 ] คำ}ว่า "บทพิสูจน์แนวทแยง" หรือ "จุดคงที่" ไม่ปรากฏใน บทความของ เคิร์ท เกอเดลในปี 1931หรือใน บทความของ อัลเฟรด ทาร์สกีในปี 1936

ในปี พ.ศ. 2477 รูดอล์ฟ คาร์แนปเป็นคนแรกที่ตีพิมพ์เลมมาแนวทแยงในระดับทั่วไป ซึ่งกล่าวว่าสำหรับสูตรใดๆที่มีตัวแปรอิสระ (ในภาษาที่มีการแสดงออกเพียงพอ) จะมีประโยคที่เป็นจริง (ในแบบจำลองมาตรฐานบางอย่าง) ^{[ 7 ]}งานของคาร์แนปถูกกำหนดในแง่ของความจริงมากกว่าความสามารถในการพิสูจน์ (กล่าวคือในเชิงความหมายมากกว่าเชิงไวยากรณ์) ^{[ 8 ]}ยิ่งไปกว่านั้น แนวคิดของฟังก์ชันที่คำนวณได้ยังไม่ได้รับการพัฒนาในปี พ.ศ. 2477 ${\displaystyle \psi (x)}$${\displaystyle x}$${\displaystyle \varphi }$${\displaystyle \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner )}$

บทพิสูจน์แนวทแยงมีความเกี่ยวข้องอย่างใกล้ชิดกับทฤษฎีบทการเรียกซ้ำของ Kleeneในทฤษฎีความสามารถในการคำนวณและการพิสูจน์ของทั้งสองก็คล้ายคลึงกัน^{[ 9 ]}ในปี พ.ศ. 2495 Léon Henkinได้ตั้งคำถามว่าประโยคที่ระบุความสามารถในการพิสูจน์ของตัวเองนั้นสามารถพิสูจน์ได้หรือไม่ คำถามของเขานำไปสู่การวิเคราะห์บทพิสูจน์แนวทแยงในเชิงทั่วไปมากขึ้น โดยเฉพาะอย่างยิ่งกับทฤษฎีบทของ Löbและตรรกะความสามารถในการพิสูจน์^{[ 10 ]}

• การอ้างอิงตนเองทางอ้อม
• รายชื่อทฤษฎีบทจุดตรึง
• การอ้างอิงตนเอง
• ความขัดแย้งที่อ้างอิงถึงตนเอง