[mizar] Re: How to call it?

[Jesse Alama <jesse.alama@gmail.com>]

Josef Urban <josef.urban@gmail.com> writes:

> 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).

Quite right.  I'd noticed you'd used such a translation for the MPTP
export of Mizar proofs.  We've got a nice menagerie of mappings here.
There's also the so-called critical formulas of epsilon calculus,
which are in a sense the converse of Henkin formulas:

  A --> A[x := epsilon x A]

See

  http://plato.stanford.edu/entries/epsilon-calculus/

(I learned the term "critical formula" when studying epsilon calculus,
but Avigad and Zach call these formulas "transfinite axioms".)

Best,

Jesse

--
Jesse Alama
http://centria.di.fct.unl.pt/~alama/