Bir biçimsel dizgede belli bir önermenin, ilksavlar kümesinden türetilebildiğini göstermeye yarayan türetim. || Anl. tanıt, tanıtlama.