Substitusi

Buka Definisi

Unfolding a definition (definitional equivalence)

Bentuk

P \;\stackrel{\text{def}}{\iff}\; Q

Premis-premisnya di kiri, dibaca “maka”, dan kesimpulannya di kanan.

Butuh 1 premis.

Kenapa boleh

Definisi adalah kesepakatan penamaan, jadi kedua sisinya benar di saat yang persis sama. Membukanya bukan langkah yang perlu dibenarkan lagi — tetapi juga tidak menghasilkan pengetahuan baru; yang berubah hanya bentuknya.

Contoh

“ $n$ genap” berarti “ada bilangan bulat $k$ dengan $n = 2k$ ”. Membukanya mengubah pernyataan tentang paritas menjadi pernyataan tentang perkalian, dan itulah yang membuat langkah berikutnya mungkin.

Jebakan

Yang dibuka harus definisinya, bukan teoremanya. Mengganti “ $n$ genap” dengan “ $n^2$ habis dibagi 4” bukan membuka definisi — itu memakai hasil lain yang perlu dibuktikan lebih dulu.

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 Substitusi

Substitusi Kesamaan