ในตรรกศาสตร์ทางคณิตศาสตร์ทฤษฎีการพิสูจน์เชิงโครงสร้างเป็นสาขาย่อยของทฤษฎีการพิสูจน์ที่ศึกษาแคลคูลัสการพิสูจน์ที่สนับสนุนแนวคิดของการพิสูจน์เชิงวิเคราะห์ ซึ่ง เป็นการพิสูจน์ประเภทหนึ่งที่มีคุณสมบัติทางความหมายที่เปิดเผย เมื่อทฤษฎีบททั้งหมดของตรรกศาสตร์ที่เป็นทางการในแคลคูลัสการพิสูจน์มีการพิสูจน์เชิงวิเคราะห์แล้ว แคลคูลัสการพิสูจน์นั้นสามารถใช้เพื่อแสดงสิ่งต่างๆ เช่นความสอดคล้อง ให้ขั้นตอนการตัดสินใจและอนุญาตให้ดึงพยานทางคณิตศาสตร์หรือการคำนวณออกมาเป็นคู่ตรงข้ามของทฤษฎีบท ซึ่งเป็นงานประเภทที่มักจะมอบหมายให้กับทฤษฎีแบบจำลอง^{[ 1 ]}

แนวคิดเรื่องการพิสูจน์เชิงวิเคราะห์ถูกนำมาใช้ในทฤษฎีการพิสูจน์โดยGerhard Gentzenสำหรับแคลคูลัสลำดับ (sequent calculus ) การพิสูจน์เชิงวิเคราะห์คือการพิสูจน์ที่ปราศจากการตัด (cut-free ) แคลคูลัสการหักล้างตามธรรมชาติ (natural deduction calculus ) ของเขายังสนับสนุนแนวคิดเรื่องการพิสูจน์เชิงวิเคราะห์ด้วย ดังที่Dag Prawitz ได้แสดงให้เห็น นิยามนั้นซับซ้อนกว่าเล็กน้อย—การพิสูจน์เชิงวิเคราะห์คือรูปแบบปกติ (normal forms ) ซึ่งเกี่ยวข้องกับแนวคิดของรูปแบบปกติใน การเขียนเทอมใหม่ ( term rewriting )

คำว่า"โครงสร้าง"ในทฤษฎีการพิสูจน์เชิงโครงสร้าง มาจากแนวคิดทางเทคนิคที่นำเสนอในแคลคูลัสลำดับ (sequent calculus): แคลคูลัสลำดับแสดงถึงการยืนยันที่ทำขึ้นในขั้นตอนใด ๆ ของการอนุมานโดยใช้ตัวดำเนินการพิเศษนอกเหนือจากตรรกะที่เรียกว่าตัวดำเนินการเชิงโครงสร้าง: ในเครื่องหมายจุลภาคทางด้านซ้ายของ สัญลักษณ์ "turnstile"เป็นตัวดำเนินการที่โดยปกติแล้วตีความว่าเป็นการเชื่อม (conjunction) เครื่องหมายจุลภาคทางด้านขวาเป็นการเชื่อมแบบเลือก (disjunction) ในขณะที่สัญลักษณ์ "turnstile" เองนั้นตีความว่าเป็นการบ่งชี้ (implication) อย่างไรก็ตาม สิ่งสำคัญที่ควรทราบคือ มีความแตกต่างพื้นฐานในพฤติกรรมระหว่างตัวดำเนินการเหล่านี้กับตัวเชื่อมทางตรรกะที่ใช้ในการตีความในแคลคูลัสลำดับ: ตัวดำเนินการเชิงโครงสร้างถูกใช้ในทุกกฎของแคลคูลัส และจะไม่ถูกนำมาพิจารณาเมื่อถามว่าคุณสมบัติของสูตรย่อย (subformula property) ใช้ได้หรือไม่ ยิ่งไปกว่านั้น กฎทางตรรกะมีทิศทางเดียวเท่านั้น: โครงสร้างทางตรรกะถูกนำมาใช้โดยกฎทางตรรกะ และไม่สามารถกำจัดได้เมื่อสร้างขึ้นแล้ว ในขณะที่ตัวดำเนินการเชิงโครงสร้างสามารถนำมาใช้และกำจัดได้ในระหว่างการอนุมาน ${\displaystyle A_{1},\dots ,A_{m}\vdash B_{1},\dots ,B_{n}}$

แนวคิดในการมองคุณลักษณะทางไวยากรณ์ของลำดับเป็นตัวดำเนินการพิเศษที่ไม่ใช่ตรรกะไม่ใช่เรื่องเก่า และถูกผลักดันโดยนวัตกรรมในทฤษฎีการพิสูจน์: เมื่อตัวดำเนินการเชิงโครงสร้างนั้นเรียบง่ายเหมือนในแคลคูลัสลำดับดั้งเดิมของ Getzen ก็ไม่จำเป็นต้องวิเคราะห์มากนัก แต่แคลคูลัสการพิสูจน์ของการอนุมานเชิงลึกเช่นตรรกะการแสดงผล (แนะนำโดยNuel Belnapในปี 1982) ^{[ 2 ]}รองรับตัวดำเนินการเชิงโครงสร้างที่ซับซ้อนเท่ากับตัวเชื่อมตรรกะ และต้องการการจัดการที่ซับซ้อน

ทฤษฎีบทการกำจัดส่วนตัด (Hauptsatz)เป็นผลลัพธ์สำคัญสำหรับแคลคูลัสลำดับ ทฤษฎีบทนี้กล่าวว่า ลำดับใดๆ ที่สามารถอนุมานได้โดยใช้กฎส่วนตัด สามารถอนุมานได้โดยไม่ต้องใช้กฎส่วนตัด กฎส่วนตัดซึ่งเป็นการขยายหลักการทางตรรกะของ modus ponensนั้นถูกกำหนดไว้ดังนี้

${\displaystyle {\frac {\Gamma \vdash \Delta ,A\quad A,\Pi \vdash \Sigma }{\Gamma ,\Pi \vdash \Delta ,\Sigma }}\quad ({\text{Cut}}),}$

โดยที่และเป็นลำดับของสูตร สูตรตัดนั้นถูกใช้เสมือนเป็นบทพิสูจน์ย่อยขั้นกลางที่ถูกนำเสนอแล้วกำจัดออกไป ความสำคัญของการกำจัดกฎนี้คือ การพิสูจน์ที่ปราศจากการตัดจะมีคุณสมบัติสูตรย่อย ซึ่งรับประกันว่าทุกสูตรที่ปรากฏที่ใดก็ตามในการพิสูจน์ที่ปราศจากการตัดนั้นเป็นสูตรย่อยของสูตรในลำดับสุดท้ายที่สรุป ดังนั้น การพิสูจน์จึงเป็นการวิเคราะห์โดยสมบูรณ์ เนื่องจากไม่จำเป็นต้องนำเสนอแนวคิดภายนอกใดๆ นอกเหนือจากแนวคิดที่มีอยู่แล้วในข้อความที่กำลังพิสูจน์ คุณสมบัติการตัดนี้ใช้เพื่อแสดงให้เห็นถึงความสอดคล้องของ ตรรกะ แบบคลาสสิกและแบบสัญชาตญาณและใช้ในความหมายเชิงทฤษฎีการพิสูจน์ ${\displaystyle \Gamma ,\Delta ,\Pi ,}$${\displaystyle \Sigma }$${\displaystyle A}$

การอนุมานเชิงธรรมชาติเป็นระบบที่เป็นทางการสำหรับการสรุปเชิงตรรกะจากข้อสมมติโดยอาศัยชุดของกฎการอนุมานที่สะท้อนการใช้เหตุผลโดยสัญชาตญาณของมนุษย์อย่างใกล้ชิด ความเชื่อมโยงโดยตรงระหว่างตรรกะและการคำนวณเกิดขึ้นผ่านความสัมพันธ์แบบ Curry–Howard ซึ่งสร้าง ความสัมพันธ์แบบไอโซมอร์ฟิซึมโดยตรงระหว่างสูตรในตรรกะเชิงสัญชาตญาณและประเภทในแคลคูลัสแลมบ์ดาแบบมี ประเภท ในความสัมพันธ์นี้ ทุกประพจน์สามารถมองได้ว่าเป็นประเภทและการพิสูจน์ประพจน์นั้นเปรียบได้กับโปรแกรมของประเภทที่สอดคล้องกันนั้น โดยพื้นฐานแล้ว การพิสูจน์คือการสร้างที่แสดงให้เห็นถึงการมีอยู่ของประเภท ตัวอย่างเช่น การพิสูจน์การบ่งชี้สอดคล้องกับฟังก์ชันที่รับเทอมประเภทเป็นอินพุตและสร้างเทอมประเภทเป็นเอาต์พุต ในทำนองเดียวกัน การพิสูจน์การเชื่อมโยง( ประเภทผลคูณ ) สอดคล้องกับคู่ที่ประกอบด้วยเทอมประเภทและเทอมประเภทความสัมพันธ์นี้ไม่ใช่เพียงแค่ผิวเผิน กระบวนการทำให้การพิสูจน์เป็นมาตรฐาน (proof normalization) ซึ่งเป็นการกำจัดขั้นตอนเชิงตรรกะที่ซ้ำซ้อนออกไปเพื่อทำให้การพิสูจน์ง่ายขึ้นนั้น สอดคล้องโดยตรงกับกระบวนการประมวลผลโปรแกรม หรือก็คือ การลดรูปเบต้า (beta-reduction) ในแคลคูลัสแลมบ์ดาแบบมีชนิดข้อมูล (typed lambda calculus) ความเหมือนกัน นี้ เชื่อมโยงเนื้อหาการคำนวณของการพิสูจน์เชิงตรรกะ ทฤษฎีชนิดข้อมูลสมัยใหม่ และเป็นแนวทางในการออกแบบตัวช่วยในการพิสูจน์ แผนภาพต่อไปนี้แสดงให้เห็นถึงความสอดคล้องกันนี้ ${\displaystyle A\to B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\land B}$${\displaystyle A}$${\displaystyle B}$

ความเป็นคู่และความกลมกลืนเชิงตรรกะเชื่อมโยงกันผ่านสมมาตรของแคลคูลัสลำดับสถาปัตยกรรมของ ลำดับ โดยที่คือเซตย่อยจำกัดของสูตร สร้างความเป็นคู่พื้นฐานระหว่างส่วนนำ (ซ้าย) และส่วนตาม (ขวา) ความเป็นคู่นี้ปรากฏให้เห็นอย่างชัดเจนโดยกฎการแนะนำด้านซ้ายและด้านขวาสำหรับตัวเชื่อมเชิงตรรกะแต่ละตัว ตัวอย่างเช่น กฎสำหรับการเชื่อม ( ) และการแยก ( ) เป็นกฎคู่กัน: ${\displaystyle \Gamma \vdash \Delta }$${\displaystyle \Gamma ,\Delta }$${\displaystyle \land }$${\displaystyle \lor }$

${\displaystyle {\begin{array}{ccc}{\text{(}}{\land }{\text{L)}}&{\dfrac {A,B,\Gamma \vdash \Delta }{A\land B,\Gamma \vdash \Delta }}&{\text{(}}{\land }{\text{R)}}&{\dfrac {\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}{\Gamma \vdash \Delta ,A\land B}}\\\\{\text{(}}{\lor }{\text{L)}}&{\dfrac {A,\Gamma \vdash \Delta \qquad B,\Gamma \vdash \Delta }{A\lor B,\Gamma \vdash \Delta }}&{\text{(}}{\lor }{\text{R)}}&{\dfrac {\Gamma \vdash \Delta ,A,B}{\Gamma \vdash \Delta ,A\lor B}}\end{array}}}$

ความสมมาตรซ้าย-ขวานี้สะท้อนถึงความกลมกลืนที่ลึกซึ้งยิ่งขึ้นระหว่างความหมายทางไวยากรณ์ของตัวเชื่อม ซึ่งกำหนดโดยกฎการแนะนำเท่านั้น ผ่านหลักการผกผัน และพฤติกรรมการกำจัดของมัน ทฤษฎีบทการตัดและการกำจัดรับประกันความกลมกลืนเชิงอภิปรัชญานี้ กฎการตัด แสดงถึงรูปแบบหนึ่งของการเชื่อมต่อความหมาย การยอมรับได้ของกฎนี้แสดงให้เห็นว่าระบบการพิสูจน์มีความสอดคล้องกันภายในและเป็นแบบวิเคราะห์ กล่าวคือ การพิสูจน์ไม่จำเป็นต้องอ้างอิงถึงแนวคิดภายนอก เช่น สูตร ที่ไม่มีอยู่ในข้อสรุป การลดการตัดบนสูตรที่ซับซ้อนให้เหลือการตัดบนสูตรย่อย ผ่านการลดกรณีสำคัญระหว่างกฎซ้ายและขวา เช่น การลดการตัดบนที่แนะนำโดยทั้ง ( R) และ ( L) เป็นการแสดงออกเชิงคำนวณของความสมดุลที่สมบูรณ์แบบระหว่างศักยภาพในการแนะนำและการกำจัดของตัวเชื่อม ดังนั้น การตัดและการกำจัดจึงตรวจสอบว่ากฎการดำเนินการมีความกลมกลืนกัน ทำให้มั่นใจได้ว่าระบบตรรกะมีความสอดคล้องกัน และการพิสูจน์มีคุณสมบัติการทำให้เป็นมาตรฐานที่ดี ${\displaystyle {\text{(Cut)}}\quad {\dfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Lambda }{\Gamma ,\Sigma \vdash \Delta ,\Lambda }},}$${\displaystyle A}$${\displaystyle A\land B}$${\displaystyle \land }$${\displaystyle \land }$

กฎการอนุมานบางอย่างเป็นแบบเฉพาะที่ซึ่งเป็นคุณสมบัติที่ต้องการ^{[ 3 ]}ตัวอย่างเช่น พิจารณากฎ ! ในตรรกะเชิงเส้น : เพื่อตรวจสอบว่ากฎ ! ถูกนำไปใช้อย่างถูกต้องกับขั้นตอนการคำนวณลำดับที่แน่นอนไม่เพียงแต่จำเป็นต้องตรวจสอบว่าแต่ยังจำเป็นต้องตรวจสอบว่าแต่ละมี ! เป็นตัวเชื่อมตรรกะภายนอกสุด ในแง่นี้ กฎนี้ไม่ใช่แบบเฉพาะที่เนื่องจากในการใช้กฎนี้ จะต้องตรวจสอบสูตรจำนวนไม่จำกัด $${\displaystyle {\frac {\vdash A,?B_{1},\dots ,?B_{n}}{\vdash !A,?B_{1},\dots ,?B_{n}}}}$$${\displaystyle {\frac {\vdash A,B_{1},\dots ,B_{n}}{\vdash A',B_{1},\dots ,B_{n}}}}$${\displaystyle A'=?A}$${\displaystyle B_{i}}$

ตัวอย่างที่คุ้นเคยกว่าคือ ในแคลคูลัสลำดับคลาสสิก LK กฎการอนุมานสำหรับ OR คือกฎนี้ไม่ใช่กฎเฉพาะที่ เนื่องจากในการตรวจสอบว่ากฎนี้ถูกนำไปใช้อย่างถูกต้องในขั้นตอนใดขั้นตอนหนึ่ง จะต้องตรวจสอบไม่เพียงแค่ว่าแต่ยัง ต้องตรวจสอบด้วยว่า กฎเหล่านี้เป็นกฎเฉพาะที่^{[ 4 ]}$${\displaystyle {\frac {A,\Gamma \vdash \Delta \quad B,\Gamma \vdash \Delta }{A\lor B,\Gamma \vdash \Delta }}(\lor \vdash ),\quad {\frac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}(\vdash \lor _{1}),\quad {\frac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}(\vdash \lor _{2})}$$${\displaystyle \lor \vdash }$$${\displaystyle {\frac {A,\Gamma \vdash \Delta \quad B,\Gamma '\vdash \Delta '}{C,\Gamma \vdash \Delta }}}$$${\displaystyle C=A\lor B}$${\displaystyle \Gamma =\Gamma ',\Delta =\Delta '}$${\displaystyle \vdash \lor _{1},\vdash \lor _{2}}$

แนวคิดเรื่องความเป็นท้องถิ่น (Locality) เกิดขึ้นจากข้อพิจารณาในการเขียนโปรแกรมเชิงตรรกะแบบขนาน แนวคิดมีดังนี้: ลำดับขนาดใหญ่อาจถูกจัดเก็บในลักษณะกระจายไปทั่วโปรเซสเซอร์หลายตัวและตำแหน่งหน่วยความจำหลายแห่ง ขั้นตอนการอนุมานแบบท้องถิ่นสามารถดำเนินการได้ด้วยปริมาณการโต้ตอบที่จำกัด ในขณะที่ขั้นตอนการอนุมานแบบไม่ท้องถิ่นสามารถดำเนินการได้ด้วยปริมาณการโต้ตอบที่มากอย่างไม่จำกัด ตัวอย่างเช่น โดยเฉพาะอย่างยิ่ง ในการดำเนินการโปรเซสเซอร์จำเป็นต้องสร้างลำดับใหม่โดยที่ชี้ไปยังที่อยู่หน่วยความจำเดียวกันกับและชี้ไปยัง ตามด้วยที่อยู่หน่วยความจำที่สองของในทางตรงกันข้าม การใช้กฎจำเป็นต้องตรวจสอบว่าลำดับสองลำดับนั้นเหมือนกัน ซึ่งต้องใช้การดำเนินการ โดยที่คือจำนวนสูตรในลำดับ ${\displaystyle \Gamma \vdash \Delta }$${\displaystyle {\frac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}}$${\displaystyle \Gamma '\vdash \Delta '}$${\displaystyle \Gamma '}$${\displaystyle \Gamma }$${\displaystyle \Delta '}$${\displaystyle A\lor B}$${\displaystyle B,\Delta }$${\displaystyle \lor \vdash }$${\displaystyle O(n)}$${\displaystyle n}$

กรอบงานไฮเปอร์ซีเควนต์ขยายโครงสร้างซีเควนต์ ธรรมดา ไปเป็นมัลติเซตของซีเควนต์ โดยใช้ตัวเชื่อมโครงสร้างเพิ่มเติม | (เรียกว่าแถบไฮเปอร์ซีเควนต์ ) เพื่อแยกซีเควนต์ที่แตกต่างกัน มีการนำไปใช้เพื่อสร้างแคลคูลัสเชิงวิเคราะห์สำหรับตรรกะโมดอ ล ตรรกะ ระดับกลางและตรรกะโครงสร้างย่อย^{[ 5 ] [ 6 ] [ 7 ]}ไฮเปอร์ซีเควนต์เป็นโครงสร้าง

${\displaystyle \Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}$

โดยแต่ละอันเป็นลำดับปกติ เรียกว่าส่วนประกอบของไฮเปอร์ลำดับ เช่นเดียวกับลำดับทั่วไป ไฮเปอร์ลำดับสามารถสร้างขึ้นจากเซต มัลติเซต หรือลำดับ และส่วนประกอบสามารถเป็นลำดับที่ มีข้อสรุปเดียวหรือหลายข้อสรุป ก็ได้การตีความสูตรของไฮเปอร์ลำดับขึ้นอยู่กับตรรกะที่กำลังพิจารณา แต่เกือบทุกครั้งจะเป็นรูปแบบของการแยกแบบใดแบบหนึ่ง การตีความที่พบบ่อยที่สุดคือการแยกแบบง่ายๆ ${\displaystyle \Gamma _{i}\vdash \Delta _{i}}$

${\displaystyle (\bigwedge \Gamma _{1}\rightarrow \bigvee \Delta _{1})\lor \dots \lor (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

สำหรับตรรกะระดับกลาง หรือเป็นการเชื่อมโยงแบบเลือกของกล่อง

${\displaystyle \Box (\bigwedge \Gamma _{1}\rightarrow \bigvee \Delta _{1})\lor \dots \lor \Box (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

สำหรับตรรกะเชิงโมดอล

ตามการตีความแบบแยกส่วนของแท่งไฮเปอร์ซีเควนต์ โดยพื้นฐานแล้วแคลคูลัสไฮเปอร์ซีเควนต์ทั้งหมดจะรวมกฎโครงสร้างภายนอกโดยเฉพาะอย่างยิ่งกฎการลดทอนภายนอก

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma \vdash \Pi }}}$

และกฎการหดตัวภายนอก

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}}}$

ความสามารถในการแสดงออกเพิ่มเติมของกรอบไฮเปอร์ซีเควนต์นั้นมาจากกฎที่จัดการโครงสร้างไฮเปอร์ซีเควนต์ ตัวอย่างที่สำคัญคือกฎการแบ่งแบบโมดัล^{[ 6 ]}

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma ,\Omega \vdash \Box \Pi ,\Theta }{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \Sigma \vdash \Box \Pi \mid \Omega \vdash \Theta }}}$

สำหรับตรรกะโมดอลS5ซึ่งหมายความว่าสูตรทุกสูตรในนั้นมีรูปแบบ ${\displaystyle \Box \Sigma }$${\displaystyle \Box \Sigma }$${\displaystyle \Box A}$

ตัวอย่างอื่นแสดงโดยกฎการสื่อสารสำหรับตรรกะระดับกลางLC ^{[ 6 ]}

${\displaystyle {\frac {\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Omega \vdash A\qquad \Sigma _{1}\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m}\mid \Theta \vdash B}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma _{1}\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m}\mid \Omega \vdash B\mid \Theta \vdash A}}}$

โปรดทราบว่าในกฎการสื่อสาร ส่วนประกอบต่างๆ เป็นลำดับที่มีข้อสรุปเดียว

แคลคูลัสลำดับซ้อนเป็นรูปแบบที่เป็นทางการซึ่งคล้ายกับแคลคูลัส โครงสร้าง แบบสองด้าน