[FOM] First, second order theories, second order characterizations

[Cris Perdue]

After the inquiries about HOL-Omega I sent a message directly to Peter
Vincent Homeier, and am forwarding his reply in case it may be of interest
to some of the readers of this list.

He refers to an attached paper in his email, but I do not include the
attachment as the FOM mailing list software does not support attachments.

Regards,
Cris


On Thu, Sep 12, 2013 at 6:40 PM, Peter Vincent Homeier <
palantir at trustworthytools.com> wrote:

With regards to the proof-theoretic strength of HOL-Omega, it was
> intentionally designed to have its semantics as simple as possible, while
> still providing the nice user features that it does. In particular, it has
> a set theory semantics, as described in the draft paper (not yet published)
> I am attaching. So one may consider that any proof in HOL-Omega could in
> principle be translated into a proof in set theory, and it cannot prove
> anything intrinsically outside of set theory. By set theory I mean the
> normal Zermelo-Fraenkel axioms with the axiom of choice.
>
> Some logics are larger and more ambitious. For example, I have heard that
> there is a set theory for Coq, but it requires an uncountable number of
> inaccessible cardinals. This means it requires assumptions beyond those of
> normal ZFC. Of course, there's nothing wrong with having more assumptions,
> as long as people know what the foundations of their system are.
>
> By the way, although I have not tried the experiment, I believe that
> HOL-Omega could be naturally extended to include dependent types, and thus
> provide all three dimensions of the Barendregt Cube. Provided the
> restrictions about ranks were still enforced, my sense is that it would
> still have a semantics that would be contained within ZFC.
>
> In the attached paper, the set theory semantics is sketched, which makes
> use of cardinals up to a beth fixed point cardinal. While not the very
> highest of the cardinals listed in Cantor's Attic, it's reasonably close to
> the top of those provable in ZFC.
>
> http://cantorsattic.info/Middle_attic
>
> Now, the fact that I used such a cardinal does not necessarily imply that
> that is its proof-theoretic strength. I would love to hear from you and the
> community, who are more expert in this than I, where they think the
> proof-theoretic strength of HOL-Omega lies.
>
> Sincerely,
> Peter
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130914/10f63367/attachment.html>