Re: [mizar] Re: How to call it?

[Josef Urban <josef.urban@gmail.com>]

On Mon, Mar 12, 2012 at 12:39 AM, Jesse Alama <jesse.alama@gmail.com> wrote:

> "Henkin constant", in the sense of Henkin's proof of the completeness
> theorem for first-order logic, is not related to fixed variables.

Interesting. I got rid of local constants when translating Mizar
proofs to TPTP by introducing exactly the kind of axioms that Henkin
uses (http://www.springerlink.com/content/b7383x43l55p1183/).

To make things even merrier, there is also herbrandization
(http://en.wikipedia.org/wiki/Herbrandization).

Josef