Lihat sumber Matematika Q0

Q0 adalah formulasi lambda kalkulus bertipe sederhana oleh [[Peter B. Andrews|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.<ref>Geoff Sutcliffe. [https://doi.org/10.3233/aic-2010-0469 The CADE-22 automated theorem proving system competition – CASC-22]. ''AI Communications''. 2010. Vol. 23 (1). hlm. 47–59. doi:10.3233/aic-2010-0469.</ref>

== Aksioma Q0 ==
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.

== Tentang Aksioma ==
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.

== Perluasan Inti Logika ==
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.

== Inferensi dalam Q0 ==
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:

# Kejadian Aα dalam C bukan kejadian variabel yang langsung didahului oleh λ, dan
# 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:

# ∃x Px
# Px ⊃ Qx

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

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

== Bacaan lanjutan ==
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 <bdi>1-4020-0763-9</bdi>.<ref>[http://www.springer.com/mathematics/book/978-1-4020-0763-7 An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof]. ''www.springer.com''.</ref>

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.<ref>[https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf Wayback Machine]. ''pdfs.semanticscholar.org''.</ref>
= Referensi =

== Referensi ==
<references />

== Sumber dan atribusi ==

Konten artikel ini diadaptasi dari [https://id.wikipedia.org/w/index.php?title=Matematika+Q0&oldid=29320575 Wikipedia bahasa Indonesia], revisi 29320575 (2026-06-06T08:46:09Z), yang tersedia berdasarkan lisensi Creative Commons Atribusi-BerbagiSerupa (CC BY-SA). Mohon gunakan konten ini secara bijak serta sesuai dengan ketentuan lisensi yang berlaku.

<!-- WIKI_UNISSULA_PRESENTATION_V4 -->