การกำจัดตัวบ่งปริมาณ

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

Definition

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

Scope

หัวข้อนี้ครอบคลุมคำจำกัดความของการกำจัดตัวบ่งปริมาณ เกณฑ์ในการสร้างคุณสมบัตินี้ แนวคิดที่เกี่ยวข้องของความสมบูรณ์ของแบบจำลอง (model completeness) และตัวอย่างที่เป็นแบบฉบับของอันดับเชิงเส้นหนาแน่น (dense linear orders), ฟิลด์ปิดเชิงพีชคณิต (algebraically closed fields), ฟิลด์ปิดจริง (real closed fields) และเลขคณิตของเพรสเบอร์เกอร์ (Presburger arithmetic) พร้อมกับผลลัพธ์ด้านการตัดสินใจที่ตัวอย่างเหล่านี้บ่งชี้

Core questions

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

Key theories

การทดสอบการกำจัดตัวบ่งปริมาณ

เพียงพอที่จะกำจัดตัวบ่งปริมาณเชิงการมีอยู่ (existential quantifier) ตัวเดียวออกจากการเชื่อมโยงของสูตรอะตอมมิกและสูตรอะตอมมิกเชิงปฏิเสธ ซึ่งลดคุณสมบัติลงสู่เงื่อนไขเฉพาะที่สามารถจัดการได้ ซึ่งมักตรวจสอบผ่านการฝังโครงสร้างย่อย (embeddings of substructures)

ฟิลด์ปิดเชิงพีชคณิตและฟิลด์ปิดจริง

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

กระบวนการตัดสินใจของ Tarski

การกำจัดตัวบ่งปริมาณสำหรับฟิลด์ปิดจริงให้ขั้นตอนวิธีในการตัดสินความจริงของข้อความอันดับหนึ่ง (first-order statement) ใดๆ เกี่ยวกับจำนวนจริงในภาษาของฟิลด์อันดับ (ordered fields) ดังนั้นพีชคณิตและเรขาคณิตเบื้องต้นจึงสามารถตัดสินใจได้

Clinical relevance

การกำจัดตัวบ่งปริมาณเปลี่ยนคำถามเชิงตรรกะให้เป็นพีชคณิต: โดยให้กระบวนการตัดสินใจที่ใช้ในพีชคณิตเชิงคอมพิวเตอร์และการตรวจสอบ และเนื้อหาเชิงเรขาคณิต เช่น ลักษณะกึ่งพีชคณิตของชุดที่สามารถนิยามได้บนจำนวนจริง เชื่อมโยงทฤษฎีแบบจำลอง (model theory) เข้ากับเรขาคณิตพีชคณิตจริง (real algebraic geometry) และ o-minimality

History

การกำจัดตัวบ่งปริมาณถูกใช้โดย Skolem, Langford และ Presburger ในช่วงทศวรรษ 1920 และ 1930 เพื่อตัดสินทฤษฎีเฉพาะ และ Tarski ได้สร้างคุณสมบัตินี้สำหรับฟิลด์ปิดจริง ซึ่งนำไปสู่กระบวนการตัดสินใจอันโด่งดังของเขาสำหรับพีชคณิตและเรขาคณิตเบื้องต้น Robinson ได้ปรับแนวคิดที่เกี่ยวข้องใหม่ผ่านความสมบูรณ์ของแบบจำลอง ทำให้เทคนิคนี้เป็นหลักสำคัญของทฤษฎีแบบจำลองประยุกต์

Key figures

• Alfred Tarski
• Thoralf Skolem
• Abraham Robinson
• Mojzesz Presburger

Seminal works

• marker2002
• hodges1993
• tarski1951

Frequently asked questions

เหตุใดการกำจัดตัวบ่งปริมาณจึงทำให้ทฤษฎีสามารถตัดสินใจได้?

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

ทุกทฤษฎียอมรับการกำจัดตัวบ่งปริมาณหรือไม่?

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