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

${\displaystyle \Gamma _{1}\Rightarrow \Delta _{1}\mid \cdots \mid \Gamma _{n}\Rightarrow \Delta _{n}}$

ลำดับที่ประกอบกันเป็นไฮเปอร์ซีเควนต์เรียกว่าคอมโพเนนต์ ความสามารถในการแสดงออกที่เพิ่มขึ้นของกรอบงานไฮเปอร์ซีเควนต์นั้นมาจากการใช้กฎในการจัดการคอมโพเนนต์ต่างๆ เช่น กฎการสื่อสารสำหรับตรรกะระดับกลาง LC ( ตรรกะเกอเดล-ดัมเมตต์ )

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

หรือกฎการแบ่งโมดอลสำหรับตรรกะโมดอลS5 : ^{[ 1 ]}

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

แคลคูลัสไฮเปอร์ซีเควนต์ถูกนำมาใช้ในการแก้ปัญหาตรรกะเชิงโมดอลตรรกะเชิงกลางและตรรกะเชิงโครงสร้างย่อยโดยทั่วไปแล้ว ไฮเปอร์ซีเควนต์จะมีรูปแบบการตีความแบบสูตร กล่าวคือ ถูกตีความโดยสูตรในภาษาเป้าหมาย ซึ่งเกือบทุกครั้งจะเป็นการเชื่อมโยงแบบ "หรือ" รูปแบบการตีความแบบสูตรที่แน่นอนนั้นขึ้นอยู่กับตรรกะที่พิจารณา

ในทางทฤษฎีแล้ว ไฮเปอร์ซีเควนต์มักถูกมองว่าเป็นมัลติเซต จำกัดของ ซีเควนต์ธรรมดาซึ่งเขียนแทนด้วย

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

ลำดับที่ประกอบกันเป็นไฮเปอร์ซีเควนต์นั้นประกอบด้วยคู่ของมัลติเซตของสูตร และเรียกว่าส่วนประกอบของไฮเปอร์ซีเควนต์ นอกจากนี้ยังมีการพิจารณารูปแบบต่างๆ ที่กำหนดไฮเปอร์ซีเควนต์และซีเควนต์ในแง่ของเซตหรือรายการแทนที่จะเป็นมัลติเซต และขึ้นอยู่กับตรรกะที่พิจารณา ซีเควนต์อาจเป็นแบบคลาสสิกหรือแบบสัญชาตญาณกฎสำหรับตัวเชื่อมเชิงประพจน์มักเป็นการดัดแปลงกฎซีเควนต์มาตรฐานที่สอดคล้องกัน โดยมีไฮเปอร์ซีเควนต์ด้านข้างเพิ่มเติม หรือเรียกว่าบริบทไฮเปอร์ซีเควนต์ ตัวอย่างเช่น ชุดกฎทั่วไปสำหรับชุดตัวเชื่อมที่สมบูรณ์เชิง ฟังก์ชัน สำหรับตรรกะเชิงประพจน์แบบคลาสสิกนั้นกำหนดโดยกฎสี่ข้อต่อไปนี้: ${\displaystyle \{\bot ,\to \}}$

${\displaystyle {\frac {}{{\mathcal {G}}\mid \Gamma ,p\Rightarrow p,\Delta }}}$

${\displaystyle {\frac {}{{\mathcal {G}}\mid \Gamma ,\bot \Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,B\Rightarrow \Delta \qquad {\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }{{\mathcal {G}}\mid \Gamma ,A\to B\Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,A\Rightarrow B,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A\to B,\Delta }}}$

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

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,\Sigma \Rightarrow \Delta ,\Pi }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,A,A\Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,A\Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma \Rightarrow A,A,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }}}$

กฎการลดทอนภายนอกและการหดตัวภายนอกเป็นกฎที่สอดคล้องกันในระดับของส่วนประกอบไฮเปอร์ซีเควนซ์แทนที่จะเป็นสูตร:

${\displaystyle {\frac {\mathcal {G}}{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta \mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}}$

ความถูกต้องของกฎเหล่านี้มีความเชื่อมโยงอย่างใกล้ชิดกับการตีความสูตรของโครงสร้างไฮเปอร์ซีเควนต์ ซึ่งเกือบทุกครั้งจะเป็นรูปแบบของการเชื่อมแบบ "หรือ" การตีความสูตรที่แม่นยำนั้นขึ้นอยู่กับตรรกะที่พิจารณา ดูตัวอย่างบางส่วนด้านล่าง

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

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

คือสูตร

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

ถ้าในที่นี้คือมัลติเซตที่เราเขียนสำหรับผลลัพธ์ของการนำสูตรทุกสูตรในมาใส่ไว้ข้างหน้านั่นคือมัลติเซตโปรดทราบว่าส่วนประกอบเดี่ยวจะถูกตีความโดยใช้การตีความสูตรมาตรฐานสำหรับซีเควนต์ และแถบไฮเปอร์ซีเควนต์จะถูกตีความว่าเป็นการเชื่อมกล่องแบบแยก ตัวอย่างหลักของตรรกะโมดอลที่ไฮเปอร์ซีเควนต์ให้แคลคูลัสเชิงวิเคราะห์คือตรรกะS5ในแคลคูลัสไฮเปอร์ซีเควนต์มาตรฐานสำหรับตรรกะนี้^{[ 1 ]}การตีความสูตรจะเป็นดังข้างต้น และกฎเชิงประพจน์และเชิงโครงสร้างคือกฎจากส่วนก่อนหน้า นอกจากนี้ แคลคูลัสยังประกอบด้วยกฎโมดอล ${\displaystyle \Gamma }$${\displaystyle A_{1},\dots ,A_{n}}$${\displaystyle \Box \Gamma }$${\displaystyle \Gamma }$${\displaystyle \Box }$${\displaystyle \Box A_{1},\dots ,\Box A_{n}}$${\displaystyle \mid }$

${\displaystyle {\frac {{\mathcal {G}}\mid \Box \Gamma \Rightarrow A}{{\mathcal {G}}\mid \Box \Gamma \Rightarrow \Box A}}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Gamma ,A\Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,\Box A\Rightarrow \Delta }}}$

${\displaystyle {\frac {{\mathcal {G}}\mid \Box \Gamma ,\Sigma \Rightarrow \Box \Delta ,\Pi }{{\mathcal {G}}\mid \Box \Gamma \Rightarrow \Box \Delta \mid \Sigma \Rightarrow \Pi }}}$

การยอมรับกฎการตัดในรูปแบบที่เหมาะสมสามารถแสดงได้โดยใช้ข้อโต้แย้งทางไวยากรณ์เกี่ยวกับโครงสร้างของการอนุมาน หรือโดยการแสดงความสมบูรณ์ของแคลคูลัสโดยไม่ต้องใช้กฎการตัดโดยตรงโดยใช้ความหมายของ S5 สอดคล้องกับความสำคัญของตรรกะโมดอล S5 จึงมีการกำหนดแคลคูลัสทางเลือกจำนวนหนึ่ง^{[ 2 ] [ 3 ] [ 1 ] [ 4 ] [ 5 ] [ 6 ] [ 7 ] นอกจากนี้ยังมีการเสนอแคลคูลัสไฮเปอร์ซีเค วน}ต์สำหรับตรรกะโมดอลอื่นๆ อีก^{มากมาย[ 6 ] [ 7 ] [ 8 ] [ 9 ]}

แคลคูลัสไฮเปอร์ซีเควนต์ที่อิงตามซีเควนต์แบบสัญชาตญาณหรือซีเควนต์แบบตัวสืบทอดเดี่ยวได้ถูกนำมาใช้ประสบความสำเร็จในการครอบคลุมตรรกะระดับกลาง จำนวนมาก กล่าวคือ ส่วนขยายของตรรกะประพจน์แบบสัญชาตญาณเนื่องจากไฮเปอร์ซีเควนต์ในบริบทนี้อิงตามซีเควนต์แบบตัวสืบทอดเดี่ยว จึงมีรูปแบบดังต่อไปนี้:

${\displaystyle \Gamma _{1}\Rightarrow A_{1}\mid \dots \mid \Gamma _{n}\Rightarrow A_{n}}$

การตีความสูตรมาตรฐานสำหรับไฮเปอร์ซีเควนต์ดังกล่าวคือ

${\displaystyle (\bigwedge \Gamma _{1}\to A_{1})\lor \dots \lor (\bigwedge \Gamma _{n}\to A_{n})}$

แคลคูลัสไฮเปอร์ซีเควนต์ส่วนใหญ่สำหรับตรรกะระดับกลางประกอบด้วยกฎประพจน์เวอร์ชันตัวสืบทอดเดี่ยวที่ระบุไว้ข้างต้นและกฎโครงสร้างที่เลือกไว้ ลักษณะเฉพาะของตรรกะระดับกลางเฉพาะนั้นส่วนใหญ่จะถูกบันทึกโดยใช้กฎโครงสร้าง เพิ่มเติมจำนวน หนึ่ง เช่น แคลคูลัสมาตรฐานสำหรับตรรกะระดับกลางLCซึ่งบางครั้งเรียกว่าตรรกะ Gödel–Dummett ยังมีกฎการสื่อสารที่เรียกว่าอีกด้วย: ^{[ 1 ]}

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

มีการแนะนำแคลคูลัสไฮเปอร์ซีเควนต์สำหรับตรรกะระดับกลางอื่นๆ อีกมากมาย^{[ 1 ] [ 10 ] [ 11 ] [ 12 ]}และมีผลลัพธ์ทั่วไปเกี่ยวกับการกำจัดคัตในแคลคูลัสดังกล่าว^{[ 13 ]}

สำหรับตรรกะระดับกลาง ไฮเปอร์ซีเควนต์ถูกใช้เพื่อสร้างแคลคูลัสเชิงวิเคราะห์สำหรับตรรกะโครงสร้างย่อยและตรรกะคลุมเครือ จำนวนมาก ^{[ 1 ] [ 13 ] [ 14 ]}

โครงสร้างไฮเปอร์ซีเควนต์ดูเหมือนจะปรากฏขึ้นครั้งแรกใน^{[ 2 ]}ภายใต้ชื่อคอร์เทจเพื่อให้ได้แคลคูลัสสำหรับตรรกะโมดอลS5ดูเหมือนว่าจะได้รับการพัฒนาอย่างอิสระใน^{[ 3 ]}เพื่อใช้ในการจัดการกับตรรกะโมดอลเช่นกัน และใน^{[ 1 ]} ที่มีอิทธิพล ซึ่งมีการพิจารณาแคลคูลัสสำหรับตรรกะโมดอล ตรรกะระดับกลาง และตรรกะโครงสร้างย่อย และมีการแนะนำคำว่าไฮเปอร์ซีเควนต์