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

ระบบพิสูจน์ทฤษฎีบทTPS และ ETPS ที่เก็บถาวรเมื่อวันที่ 11 เมษายน 2554 ที่Wayback Machine นั้น ใช้ Q ₀ เป็นพื้นฐาน ในเดือนสิงหาคม พ.ศ. 2552 TPS ชนะการแข่งขันครั้งแรกในบรรดาระบบพิสูจน์ทฤษฎีบทลำดับสูง^{[ 1 ]}

ระบบนี้มีสัจพจน์เพียงห้าข้อ ซึ่งสามารถกล่าวได้ดังนี้:

${\displaystyle (1)}$  ${\displaystyle g_{oo}T\land g_{oo}F=\forall x_{o}[g_{oo}x_{o}]}$

${\displaystyle (2^{\alpha })}$  ${\displaystyle [x_{\alpha }=y_{\alpha }]\supset [h_{o\alpha }x_{\alpha }=h_{o\alpha }y_{\alpha }]}$

${\displaystyle (3^{\alpha \beta })}$  ${\displaystyle f_{\alpha \beta }=g_{\alpha \beta }=\forall x_{\beta }[f_{\alpha \beta }x_{\beta }=g_{\alpha \beta }x_{\beta }]}$

${\displaystyle (4)}$  ${\displaystyle [\lambda \mathbf {x_{\alpha }} \mathbf {B} _{\beta }]\mathbf {A} _{\alpha }=\mathbf {S} _{A_{\alpha }}^{\mathbf {x} _{\alpha }}\mathbf {B} _{\beta }}$

${\displaystyle (5)}$  ℩${\displaystyle _{i(oi)}[{\text{Q}}_{oii}y_{i}]=y_{i}\,}$

(สัจพจน์ข้อ 2, 3 และ 4 เป็นแบบแผนสัจพจน์ ซึ่งเป็นกลุ่มของสัจพจน์ที่คล้ายคลึงกัน ตัวอย่างของสัจพจน์ข้อ 2 และข้อ 3 จะแตกต่างกันเฉพาะประเภทของตัวแปรและค่าคงที่เท่านั้น แต่ตัวอย่างของสัจพจน์ข้อ 4 สามารถใช้นิพจน์ใดก็ได้มาแทนที่AและB )

ตัวอักษร " o " ที่อยู่ด้านล่างเป็นสัญลักษณ์แทนค่าบูลีน และตัวอักษร " i " ที่อยู่ด้านล่างเป็นสัญลักษณ์แทนค่าอินเทอร์แอ็กทีฟ (ไม่ใช่บูลีน) ลำดับของสัญลักษณ์เหล่านี้แสดงถึงประเภทของฟังก์ชัน และอาจมีวงเล็บเพื่อแยกแยะประเภทของฟังก์ชันที่แตกต่างกัน ตัวอักษรกรีกที่อยู่ด้านล่าง เช่น α และ β เป็นตัวแปรทางไวยากรณ์สำหรับสัญลักษณ์ประเภท ตัวอักษรพิมพ์ใหญ่ตัวหนา เช่นA , BและC เป็นตัวแปรทางไวยากรณ์สำหรับ WFF และตัวอักษรพิมพ์เล็กตัวหนา เช่น xและyเป็นตัวแปรทางไวยากรณ์สำหรับตัวแปร Sแสดงถึงการแทนที่ทางไวยากรณ์ในทุกตำแหน่งที่ว่างอยู่

ค่าคงที่พื้นฐานเพียงอย่างเดียวคือQ _((oα)α)ซึ่งแสดงถึงความเท่าเทียมกันของสมาชิกแต่ละประเภท α และ℩ _(i(oi))ซึ่งแสดงถึงตัวดำเนินการอธิบายสำหรับแต่ละบุคคล ซึ่งเป็นองค์ประกอบเฉพาะของเซตที่มีบุคคลเพียงหนึ่งเดียว สัญลักษณ์ λ และวงเล็บเหลี่ยม ("[" และ "]") เป็นไวยากรณ์ของภาษา สัญลักษณ์อื่นๆ ทั้งหมดเป็นตัวย่อของคำที่มีสัญลักษณ์เหล่านี้ รวมถึงตัวบ่งปริมาณ ∀ และ ∃

ในสัจพจน์ข้อที่ 4 xต้องเป็นตัวแปรอิสระสำหรับAในBซึ่งหมายความว่าการแทนที่นั้นจะไม่ทำให้ตัวแปรอิสระใดๆ ของAกลายเป็นตัวแปรผูกมัดในผลลัพธ์ของการแทนที่

• สัจพจน์ข้อที่ 1 แสดงให้เห็นว่าTและFเป็นค่าบูลีนเพียงสองค่าเท่านั้น
• แบบแผนสัจพจน์ 2 ^αและ 3 ^αβ แสดงถึงคุณสมบัติพื้นฐานของฟังก์ชัน
• แผนผังสัจพจน์ข้อที่ 4 กำหนดลักษณะของสัญลักษณ์ λ
• สัจพจน์ข้อ ที่5 กล่าวว่า ตัวดำเนินการเลือกคือฟังก์ชันผกผันของฟังก์ชันความเท่าเทียมกันบนตัวบุคคล (เมื่อกำหนดอาร์กิวเมนต์หนึ่งตัวQจะแมปตัวบุคคลนั้นไปยังเซต/述语ที่ประกอบด้วยตัวบุคคลนั้น ในQ₀ _, x = yเป็นตัวย่อของQxyซึ่งเป็นตัวย่อของ(Qx)y ) ตัวดำเนินการนี้ยังเป็นที่รู้จักในชื่อตัวดำเนินการอธิบายที่แน่นอน

ในงานของแอนดรูว์ส ปี 2002สัจพจน์ข้อที่ 4 ได้รับการพัฒนาเป็นห้าส่วนย่อยที่แยกย่อยกระบวนการแทนที่ สัจพจน์ที่นำเสนอในที่นี้ได้รับการกล่าวถึงในฐานะทางเลือกอื่นและได้รับการพิสูจน์จากส่วนย่อยเหล่านั้น

แอนดรูว์ขยายตรรกะนี้ด้วยการกำหนดนิยามของตัวดำเนินการเลือกสำหรับคอลเลกชันทุกประเภท เพื่อให้

${\displaystyle (5a)}$  ℩${\displaystyle _{\alpha (o\alpha )}[{\text{Q}}_{o\alpha \alpha }y_{i}]=y_{i}\,}$

เป็นทฤษฎีบท (หมายเลข 5309) กล่าวอีกนัยหนึ่งคือ ทุกประเภทมีตัวดำเนินการอธิบายที่แน่นอน นี่เป็นการขยายแบบอนุรักษ์นิยมดังนั้นระบบที่ขยายออกไปจึงมีความสอดคล้องหากแกนหลักมีความสอดคล้อง

นอกจากนี้ เขายังเสนอสัจพจน์เพิ่มเติมข้อที่ 6ซึ่งระบุว่ามีบุคคลจำนวนอนันต์ พร้อมกับสัจพจน์ทางเลือกอื่นๆ ที่เทียบเท่ากันของความเป็นอนันต์

แตกต่างจากรูปแบบอื่นๆ ของทฤษฎีประเภทและตัวช่วยพิสูจน์ที่อิงตามทฤษฎีประเภท Q ₀ไม่ได้กำหนดประเภทพื้นฐานอื่นนอกจากoและiดังนั้นจำนวนเชิงคาร์ดินัลจำกัดจึงถูกสร้างขึ้นเป็นกลุ่มของบุคคลที่ปฏิบัติตามหลักการของ Peano ตามปกติ แทนที่จะเป็นประเภทในความหมายของทฤษฎีประเภทแบบง่ายๆ

Q ₀มีกฎการอนุมานเพียงข้อเดียว

กฎ R.จากCและ A _α = B _α เพื่ออนุมานผลลัพธ์ของการแทนที่A _α หนึ่งครั้ง ในCด้วย B _α หนึ่งครั้ง โดยมีเงื่อนไขว่าการปรากฏของA _αในC นั้น (การปรากฏของตัวแปร) ไม่ได้อยู่ก่อนหน้าλทันที

กฎการอนุมานที่ได้มาR′ช่วยให้สามารถให้เหตุผลจากชุดสมมติฐานHได้

กฎ R′.ถ้า H ⊦ A _α = B _αและH ⊦ CและDได้มาจากการ แทนที่A _α หนึ่งครั้ง ด้วยB _α หนึ่งครั้งจาก C แล้ว H ⊦ Dโดยมีเงื่อนไขว่า:

• การปรากฏของA _αในCไม่ใช่การปรากฏของตัวแปรที่อยู่หน้าλ ทันที และ
• ไม่มีตัวแปรอิสระในA _α = B _αและสมาชิกของHถูกผูกไว้ในCที่ตำแหน่งแทนที่ของA _α

หมายเหตุ: ข้อจำกัดในการแทนที่A _αด้วย B _αในCทำให้มั่นใจได้ว่าตัวแปรอิสระใดๆ ในทั้งสมมติฐานและA _α = B _α จะยังคงถูกจำกัดให้มีค่าเดียวกันในทั้งสองกรณีหลังจากทำการแทนที่แล้ว

ทฤษฎีบทการหักล้างสำหรับ Q ₀แสดงให้เห็นว่าการพิสูจน์จากสมมติฐานโดยใช้กฎ R′ สามารถแปลงเป็นการพิสูจน์โดยไม่ต้องใช้สมมติฐานและใช้กฎ R ได้

แตกต่างจากระบบที่คล้ายคลึงกันบางระบบ การอนุมานในQ ₀จะแทนที่นิพจน์ย่อยที่ระดับความลึกใด ๆ ภายใน WFF ด้วยนิพจน์ที่เท่ากัน ตัวอย่างเช่น เมื่อกำหนดสัจพจน์:

1. ∃x Px 2. Px ⊃ Qx

และเนื่องจากA ⊃ B ≡ (A ≡ A ∧ B)เราจึงสามารถดำเนินการต่อได้โดยไม่ต้องลบตัวบ่งปริมาณออก:

3. Px ≡ (Px ∧ Qx)    แทนค่าสำหรับ A และ B 4. ∃x (Px ∧ Qx)    กฎ R แทนค่าลงในบรรทัดที่ 1 โดยใช้บรรทัดที่ 3

• คำอธิบายเชิงลึกเพิ่มเติมเกี่ยวกับ Q ₀ ; ส่วนหนึ่งของบทความเกี่ยวกับทฤษฎีประเภทของเชิร์ชในสารานุกรมปรัชญาแห่งสแตนฟอร์ด
• ภาพรวมเกี่ยวกับตรรกศาสตร์ทางคณิตศาสตร์ (รวมถึงตรรกศาสตร์ที่พัฒนาต่อยอดจาก Q ₀ ต่างๆ ): รากฐานของคณิตศาสตร์ ลำดับวงศ์และภาพรวมdoi:10.4444/ 100.111