Artikel ini membutuhkan lebih banyak pranala ke artikel lain untuk meningkatkan kualitasnya. Silakan mengembangkan artikel ini dengan menambahkan pranala yang relevan ke konteks pada teks eksisting. (November 2025) (Pelajari cara dan kapan saatnya untuk menghapus pesan templat ini)

Q0 adalah formulasi lambda kalkulus bertipe sederhana oleh Peter Andrews, yang menyediakan fondasi bagi matematika setara dengan logika orde pertama ditambah teori himpunan. Q0 merupakan bentuk logika orde tinggi dan memiliki hubungan erat dengan logika yang digunakan dalam keluarga pembuktian teorema HOL (HOL theorem prover).

Sistem pembuktian teorema TPS dan ETPS didasarkan pada Q0. Pada Agustus 2009, TPS memenangkan kompetisi pertama di antara sistem pembuktian teorema orde tinggi.^[1]

Sistem ini hanya memiliki lima aksioma, yang dapat dinyatakan sebagai berikut: (1)

gooT∧gooF=∀xo[gooxo]

(2α)

[xα​=yα]⊃[hoα​xα​=hoα​yα]

(3αβ)

fαβ​=gαβ​=∀xβ​[fαβ​xβ​=gαβ​xβ]

(4)

[λxα​Bβ]Aα​=SAα​xα​​Bβ​

(5)

ιi(oi)[Qoiiyi]=yi

(Aksioma 2, 3, dan 4 merupakan skema aksioma—keluarga aksioma serupa. Instansi dari Aksioma 2 dan 3 hanya berbeda berdasarkan tipe variabel dan konstanta, sedangkan instansi Aksioma 4 dapat memiliki ekspresi apa pun yang menggantikan A dan B.)

Subskrip "o" adalah simbol tipe untuk nilai boolean, dan subskrip "i" adalah simbol tipe untuk nilai individu (non-boolean). Urutan simbol ini merepresentasikan tipe fungsi, dan dapat menyertakan tanda kurung untuk membedakan tipe fungsi yang berbeda. Huruf Yunani subskrip seperti α dan β adalah variabel sintaksis untuk simbol tipe. Huruf kapital tebal seperti A, B, dan C adalah variabel sintaksis untuk WFF (well-formed formulas), sedangkan huruf kecil tebal seperti x, y adalah variabel sintaksis untuk variabel. S menunjukkan substitusi sintaksis pada semua kejadian bebas.

Satu-satunya konstanta primitif adalah Q((oα)α), yang menyatakan kesetaraan anggota dari setiap tipe α, dan ℩(i(oi)), yang merupakan operator deskripsi untuk individu, yaitu elemen unik dari himpunan yang hanya berisi satu individu. Simbol λ dan tanda kurung (“[" dan "]”) merupakan bagian dari sintaks bahasa. Semua simbol lain adalah singkatan dari istilah yang mengandung simbol-simbol ini, termasuk kuantor ∀ dan ∃.

Dalam Aksioma 4, x harus bebas untuk A dalam B, yang berarti substitusi tidak menyebabkan variabel bebas dari A menjadi terikat dalam hasil substitusi.

Aksioma 1 menyatakan bahwa T dan F adalah satu-satunya nilai boolean.

Skema aksioma 2α dan 3αβ menyatakan sifat fundamental dari fungsi.

Skema aksioma 4 mendefinisikan sifat notasi λ.

Aksioma 5 menyatakan bahwa operator seleksi merupakan invers dari fungsi kesetaraan pada individu. (Diberikan satu argumen, Q memetakan individu tersebut ke himpunan/predikat yang mengandung individu itu. Dalam Q0, x = y adalah singkatan dari Qxy, yang merupakan singkatan dari (Qx)y.) Operator ini juga dikenal sebagai operator deskripsi pasti.

Dalam Andrews (2002), Aksioma 4 dijabarkan dalam lima subbagian yang merinci proses substitusi. Aksioma yang disajikan di sini dibahas sebagai alternatif dan dibuktikan dari subbagian tersebut.

Andrews memperluas logika ini dengan definisi operator seleksi untuk koleksi semua tipe, sehingga

(5a)

ια(oα)[Qoαα​yi]=yi

merupakan teorema (nomor 5309). Dengan kata lain, semua tipe memiliki operator deskripsi pasti. Perluasan ini bersifat konservatif, sehingga sistem yang diperluas konsisten jika inti logika konsisten.

Ia juga memperkenalkan Aksioma 6 tambahan, yang menyatakan bahwa terdapat tak hingga banyak individu, beserta aksioma alternatif ekuivalen tentang ketakterhinggaan.

Berbeda dengan banyak formulasi teori tipe dan asisten pembukti berbasis teori tipe lainnya, Q0 tidak menyediakan tipe dasar selain o dan i, sehingga bilangan kardinal hingga dibangun sebagai koleksi individu yang mematuhi postulat Peano, bukan sebagai tipe dalam arti teori tipe sederhana.

Q0 memiliki satu aturan inferensi.

Aturan R: Dari C dan Aα = Bα, inferensikan hasil penggantian satu kejadian Aα dalam C dengan kejadian Bα, asalkan kejadian Aα dalam C bukan (kejadian variabel) yang langsung didahului oleh λ.

Aturan inferensi turunan R′ memungkinkan penalaran dari himpunan hipotesis H.

Aturan R′: Jika H ⊦ Aα = Bα, dan H ⊦ C, dan D diperoleh dari C dengan mengganti satu kejadian Aα dengan kejadian Bα, maka H ⊦ D, dengan syarat:

1. Kejadian Aα dalam C bukan kejadian variabel yang langsung didahului oleh λ, dan
2. Tidak ada variabel bebas dalam Aα = Bα yang merupakan anggota H terikat dalam C pada kejadian Aα yang diganti.

Catatan: Pembatasan penggantian Aα dengan Bα dalam C memastikan bahwa setiap variabel bebas dalam hipotesis dan Aα = Bα tetap memiliki nilai yang sama setelah penggantian.

Teorema Deduksi untuk Q0 menunjukkan bahwa bukti dari hipotesis menggunakan Aturan R′ dapat diubah menjadi bukti tanpa hipotesis menggunakan Aturan R.

Berbeda dengan beberapa sistem serupa, inferensi dalam Q0 dapat mengganti sub-ekspresi pada kedalaman apa pun dalam WFF dengan ekspresi yang setara. Misalnya, diberikan aksioma:

1. ∃x Px
2. Px ⊃ Qx

dan fakta bahwa A ⊃ B ≡ (A ≡ A ∧ B), kita dapat melanjutkan tanpa menghapus kuantor:

1. Px ≡ (Px ∧ Qx) (instansiasi untuk A dan B)
2. ∃x (Px ∧ Qx) (aturan R, substitusi ke baris 1 menggunakan baris 3)

Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2nd ed.). Dordrecht, The Netherlands: Kluwer Academic Publishers. ISBN 1-4020-0763-9.^[2]

Church, Alonzo (1940). "A Formulation of the Simple Theory of Types" . Journal of Symbolic Logic. 5 (2): 56–58. doi:10.2307/2266170. JSTOR 2266170. S2CID 15889861.^[3]

1. ^ Sutcliffe, Geoff (2010). "The CADE-22 automated theorem proving system competition – CASC-22". AI Communications. 23 (1): 47–59. doi:10.3233/aic-2010-0469. ISSN 0921-7126.
2. ^ "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof". www.springer.com. Diakses tanggal 2025-11-08.
3. ^ "Wayback Machine" (PDF). pdfs.semanticscholar.org. Diakses tanggal 2025-11-08.