Kuantor

Instansiasi Eksistensial

Existential instantiation (∃-elimination)

Bentuk

∃x P(x)    ⊢    P(c)\exists x\, P(x) \;\;\vdash\;\; P(c)
Premis-premisnya di kiri, dibaca “maka”, dan kesimpulannya di kanan.

Butuh 1 premis.

Kenapa boleh

Kalau kita tahu ada sesuatu yang memenuhi PP, kita boleh menamainya — “sebut saja cc” — supaya bisa bekerja dengan contoh itu. Yang kita tahu tentang cc hanya satu: P(c)P(c) benar.

Contoh

Dari “ada bilangan prima genap” kita boleh menulis: misalkan pp adalah bilangan prima genap. Selanjutnya kita boleh memakai p=2p = 2 sebagai temuan, bukan sebagai asumsi diam-diam.

Jebakan

Nama itu harus baru dan tidak boleh dipakai untuk hal lain. Dan yang diperoleh hanya “P(c)P(c) untuk cc ini”, bukan “P(x)P(x) untuk semua xx” — bagian kedua itu lompatan yang tidak sah.

Dipakai di

Belum ada pembuktian yang memakai aturan ini — daftarnya akan terisi sendiri begitu teorema mulai ditulis, karena setiap langkah mencatat aturan yang dipakainya.

Aturan lain di Kuantor