[FOM] J_2

[Arnon Avron]

On Thu, Mar 21, 2013 at 05:48:22AM -0500, Nik Weaver wrote:
 
> My paper "Analysis in J_2" (arXiv:math/0509245) might be of interest.
> I show how core mathematics, particularly abstract analysis, can be
> developed within Jensen's J_2.  This is a set theoretic structure,
> but a very concrete one, I would say just as concrete as the natural
> numbers.

Nik,

I think your paper on J_2 is important and interesting (and I have even
made some simplifications of it). However, I am afraid that saying
that J_2 is just as concrete as the natural numbers is an exaggeration.
For the natural numbers, as well for as the elements of HF, we have
*canonical* representations. By using these representations
we can compute with these object, and  the basic relations between them
are decidable. Can you say that about J_2? Are the membership
relation and the equality relations on J_2 decidable, and if so -
in what sense?

Arnon