การกำจัดตัวบ่งปริมาณเป็นแนวคิดของการทำให้ง่ายขึ้นที่ใช้ในตรรกศาสตร์ทางคณิตศาสตร์ทฤษฎีแบบจำลองและวิทยาศาสตร์คอมพิวเตอร์เชิงทฤษฎีโดยทั่วไปแล้ว ประโยคที่มีตัวบ่งปริมาณ " เช่นว่า..." สามารถมองได้ว่าเป็นคำถาม "เมื่อใดจึงมีเช่นว่า ...?" และประโยคที่ไม่มีตัวบ่งปริมาณสามารถมองได้ว่าเป็นคำตอบของคำถามนั้น^{[ 1 ]}${\displaystyle \exists x}$${\displaystyle x}$

วิธีหนึ่งในการจำแนกสูตรคือตามปริมาณของตัวบ่งปริมาณสูตรที่มีการสลับตัวบ่งปริมาณ น้อยกว่า จะถือว่าเรียบง่ายกว่า โดยสูตรที่ไม่มีตัวบ่งปริมาณจะเรียบง่ายที่สุดทฤษฎี หนึ่ง จะมีการกำจัดตัวบ่งปริมาณได้ก็ต่อเมื่อสำหรับทุกสูตรจะมีอีกสูตรหนึ่งที่ไม่มีตัวบ่งปริมาณซึ่งเทียบเท่ากับสูตรนั้น ( โมดูลัสของทฤษฎีนี้) ${\displaystyle \alpha }$${\displaystyle \alpha _{QF}}$

ตัวอย่างจากคณิตศาสตร์กล่าวว่าพหุนามกำลัง สองตัวแปรเดียว จะมีรากจริงก็ต่อเมื่อดิสคริมิแนนต์ไม่เป็นลบ: ^{[ 1 ]}

$${\displaystyle \exists x\in \mathbb {R} .(a\neq 0\wedge ax^{2}+bx+c=0)\ \ \Longleftrightarrow \ \ a\neq 0\wedge b^{2}-4ac\geq 0}$$

ในที่นี้ ประโยคทางด้านซ้ายมีคำบ่งปริมาณในขณะที่ประโยคที่เทียบเท่ากันทางด้านขวาไม่มี ${\displaystyle \exists x\in \mathbb {R} }$

ตัวอย่างของทฤษฎีที่แสดงให้เห็นว่าสามารถตัดสินได้โดยใช้การกำจัดตัวบ่งปริมาณ ได้แก่พีชคณิตของเพรสเบอร์เกอร์ [ ^{2 ] [ 3 ] [ 4 ] [ 5 ] [ 6 ] [ 7 ] พีชคณิต}ของสโกเล็ม^{[ 8 ]} ฟิลด์ ปิดเชิงพีชคณิตฟิลด์ปิดจริง^{[ 9 ] [ 10 ]}พีชคณิตบูลีนไร้อะตอมพีชคณิต เทอมลำดับเชิงเส้นหนาแน่น^{[ 9 ]}กลุ่มอาเบเลียน [ ^{11 ] กราฟ}ราโดรวมถึงการผสมผสานหลายอย่าง เช่น พีชคณิตบูลีนกับพีชคณิตของเพรสเบอร์เกอร์ และพีชคณิตเทอมกับ คิว

การกำจัดตัวบ่งปริมาณสำหรับทฤษฎีของจำนวนจริงในฐานะกลุ่มบวกเรียงลำดับคือการกำจัด Fourier–Motzkinสำหรับทฤษฎีของฟิลด์ของจำนวนจริงคือทฤษฎีบทTarski–Seidenberg ^{[ 9 ]}

การกำจัดตัวบ่งปริมาณยังสามารถใช้เพื่อแสดงให้เห็นว่าการ "รวม" ทฤษฎี ที่ตัดสินได้นำไปสู่ทฤษฎีที่ตัดสินได้ใหม่ (ดูทฤษฎีบทเฟเฟอร์แมน-วอท )

หากทฤษฎีใดมีการกำจัดตัวบ่งปริมาณแล้ว ก็สามารถตั้งคำถามเฉพาะเจาะจงได้ว่า มีวิธีการใดที่จะตรวจสอบค่าของแต่ละกรณีได้หรือไม่ หากมีวิธีการดังกล่าว เราจะเรียกว่าอัลกอริทึมการ กำจัดตัวบ่งปริมาณ หากมีอัลกอริทึมดังกล่าวความสามารถในการตัดสินของทฤษฎีนั้นก็จะลดลงเหลือเพียงการตัดสินความจริงของประโยค ที่ไม่มีตัวบ่งปริมาณ เท่านั้น ${\displaystyle \alpha _{QF}}$${\displaystyle \alpha }$

แนวคิดเชิงแบบจำลองทางทฤษฎีต่างๆ เกี่ยวข้องกับการกำจัดตัวบ่งปริมาณ และมีเงื่อนไขที่เทียบเท่ากันหลายประการ

ทฤษฎี ลำดับแรกทุกทฤษฎีที่มีการกำจัดตัวบ่งปริมาณจะสมบูรณ์ตามแบบจำลองในทางกลับกัน ทฤษฎีที่สมบูรณ์ตามแบบจำลองซึ่งทฤษฎีของผลลัพธ์สากลมีคุณสมบัติการรวมเข้าด้วยกันจะมีการกำจัดตัวบ่งปริมาณ^{[ 12 ]}

แบบจำลองของทฤษฎีผลลัพธ์สากลของทฤษฎีคือโครงสร้างย่อยของแบบจำลองของ[ ^{12 ] ทฤษฎี}ลำดับเชิงเส้นไม่มีการกำจัดตัวบ่งปริมาณ อย่างไรก็ตาม ทฤษฎีผลลัพธ์สากลมีคุณสมบัติการรวมเข้าด้วยกัน ${\displaystyle T}$${\displaystyle T}$

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

$${\displaystyle \exists x.\bigwedge _{i=1}^{n}L_{i}}$$

โดยที่แต่ละค่าเป็นตัวอักษร จะเทียบเท่ากับสูตรที่ไม่มีตัวบ่งปริมาณ อันที่จริง สมมติว่าเรารู้ว่าจะกำจัดตัวบ่งปริมาณออกจากการเชื่อมโยงของตัวอักษรได้อย่างไร ถ้าเป็นสูตรที่ไม่มีตัวบ่งปริมาณ เราสามารถเขียนมันในรูปแบบปกติแบบแยกส่วนได้${\displaystyle L_{i}}$${\displaystyle F}$

$${\displaystyle \bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij},}$$

และใช้ข้อเท็จจริงที่ว่า

$${\displaystyle \exists x.\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}}$$

เทียบเท่ากับ

$${\displaystyle \bigvee _{j=1}^{m}\exists x.\bigwedge _{i=1}^{n}L_{ij}.}$$

สุดท้ายนี้ เพื่อกำจัดตัวบ่งปริมาณสากล

$${\displaystyle \forall xF}$$

ในกรณีที่ไม่มีตัวบ่งปริมาณ เราจะแปลง เป็นรูปแบบปกติแบบแยกส่วน และใช้ข้อเท็จจริงที่ว่า เทียบเท่ากับ${\displaystyle F}$${\displaystyle \lnot F}$${\displaystyle \forall xF}$${\displaystyle \lnot \exists x.\lnot F.}$

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

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

ตัวอย่าง: ทฤษฎีบท Nullstellensatzสำหรับฟิลด์ปิดเชิงพีชคณิตและสำหรับฟิลด์ปิดเชิงอนุพันธ์

• การแยกส่วนพีชคณิตทรงกระบอก
• ทฤษฎีการกำจัด
• การกำจัดคำสันธาน