Re: Re: How to call it?

Josef Urban <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <CAFP4q16pKrfSY1OSZssfSkFMH-cmH8-u80Kp80QbS5_di2N5Hg@mail.gmail.com> 
On Mon, Mar 12, 2012 at 12:39 AM, Jesse Alama <[email protected]> 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
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.