Kuantor

Instansiasi Universal

Universal instantiation (∀-elimination)

Bentuk

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

Butuh 1 premis.

Kenapa boleh

Ini langkah yang mengubah pernyataan umum menjadi pernyataan tentang satu nilai tertentu. Biasanya nilai itu ditulis di langkahnya sendiri: “dari (1), dengan x=3x = 3”.

Contoh

Dari ∀x,  x2≥0\forall x,\; x^2 \ge 0 kita boleh mengambil x=3x = 3 dan mendapat 32≥03^2 \ge 0. Boleh juga x=−7x = -7.

Jebakan

Nilai yang dipilih bebas, tetapi harus satu nilai yang konkret. Menggantinya dengan lambang yang masih mewakili apa saja bukan instansiasi, melainkan langkah lain.

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