[FOM] Queries on absoluteness

[Joe Shipman]

Is there a well-known example of a sentence of arithmetic A such that
ZF |- (Con(ZF)->(Con(ZF+A) & Con(ZF+~A))) ?

If not a well-known one, is there at least a definite one that can be stated informally in an unambiguous way which would be a feasible amount of work to completely formalize?

If this is still too hard, can you do better than a Pi^1_2 statement?

What is the lowest formal syntactic complexity, in either set theory or nth order arithmetic, for a sentence A whose informal meaning is something something like this:

For every real number x there is another real number y such that R(x,y) 

where R means “y is a code for how x is obtained as an element of L”. 

In more detail: There is a definable well-ordering of L, and if V=L then each real number x corresponds to some countable ordinal in that ordering, and y could be a code for a relation on the natural numbers whose order type is that ordinal and thus determine x uniquely if the relation it gives on N is indeed a well-ordering.

I’m not sure how hard it is to formalize such an R and what the minimum syntactic complexity of the resulting sentence A could be. A would of course not be equivalent to V=L but would follow from it and thus be provably relatively consistent with ZF, while ~A is obviously also provably relatively consistent with ZF (because A is false in any model where CH fails due to the coding only giving aleph-1 many reals). 

— JS