パラメータ

全称束縛変数をパラメータと呼ぶらしい。Coqだと、公理をパラメータと呼んでいたりしたな。公理も作業仮説であり仮のものと考えると、文字通り仮引数だからだろう。理論を手続きと考えての仮引数。この発想だと、定理は出力＝戻り値か。

理論を「証明の集まり＝名前付き仮引数から名前付き多値戻り値を出力する手続き」と考えることもできる。モジュールとはそういうものだ。

ウェンツェルが証明をミニセオリーの組合せのように考えるのもそういうことだろう。