Bukti pengurangan subjek Barendregt untuk

Saya menemukan masalah dalam bukti pengurangan subjek Barendregt (Thm 4.2.5 dari kalkulasi Lambda dengan tipe ).

Langkah terakhir dari bukti (halaman 60), mengatakan:

"Dan karenanya oleh Lemma 4.1.19 (1), $\quad\Gamma,x:\rho\vdash P:\sigma'$ . "

Namun, menurut Lemma 4.1.19 (1) itu harus $\Gamma[\vec{\alpha}:=\vec{\tau}],x:\rho\vdash P:\sigma'$ , karena substitusi dibuat untuk seluruh konteks, tidak hanya untuk $x:\rho'$ .

Saya kira solusi standarnya adalah entah bagaimana membuktikannya $\vec{\alpha}\notin FV(\Gamma)$ , tetapi saya tidak yakin bagaimana caranya.

Saya punya bukti yang menyederhanakannya dengan melemaskan lemma generasi abstraksi, tetapi saya baru-baru ini menemukan bahwa ada kesalahan dan bukti saya salah, jadi saya tidak yakin bagaimana menyelesaikan masalah ini lagi.

Bisakah seseorang, tolong, beri tahu saya apa yang saya lewatkan di sini?

Saya masih berpikir ada ketidaktepatan dalam bagaimana dia menggunakan lemma. Namun ada solusinya (saya harus berterima kasih kepada Barbara Petit yang datang dengan solusinya).

Sebenarnya, solusinya datang dari definisi (def. 4.2.1), yang secara moral ini:$\geq$

$\sigma>\rho\quad$ jika$\quad\dfrac{\Gamma\vdash P:\sigma}{\Gamma\vdash P:\rho}$

Namun, alih-alih mendefinisikannya dengan cara itu, ia mendefinisikan relasinya hanya dari jenisnya saja. Keuntungan mendefinisikannya dalam urutan, adalah bahwa kita dapat menyimpulkan bahwa jika , maka , yang persis seperti yang ia butuhkan dalam pembuktian (dan dari mana ketidaktepatan datang).$\sigma>\forall\alpha.\sigma$$\alpha\notin FV(\Gamma)$