Some discussion related to axiom-of-choice in the main chat room:

The website for Howard-Rubin book with the database was mentioned a few times, for example here:

To get the idea what the book looks like, here are two pages from Howard and Rubin:

@LeakyNun Is something like that similar to the list of equivalent of AC you were hoping for?

@MartinSleziak yes

This book is hard to get - I believe it is out of print - but you can get some idea looking at Google Books.

lol I probably won't understand the statements

And also the website I've mentioned worked at least partially the last time I tried - and there are plans to create a new one: What is current status of Consequences of the Axiom of Choice website?

I have some work-related stuff to do, so I will not have time to look into details of your discussion about AC and vector spaces. (Although I am not sure whether I would be able to help even if I had time.)

@LeakyNun Well, there should be since Goodstein's theorem is not provable in PA.

@MartinSleziak but is there?

Why is 0=0 included in every diagram of the Consequences?

Did you consider trying to ask about PA in Logic chatroom? user21820 spends quite a lot time there and he knows much about logic.

Thanks

I should probably go, so that I do what I have planned for today. This website is quite addictive :-(

For the benefit of people who stumble here upon the above question related to models of PA, it might be useful to mention that the discussion continued in the Logic chatroom.

@MartinSleziak thanks

Can $|A|=|A\times\{0,1\}|$ for a well-orderable $A$ be proved in $\sf ZF$?

Hm, well the $\sf ZFC$ proof should work actually, nevermind

how do you prove it in ZFC?

Well order $A$ in type $\lambda$, well order $A\times\{0,1\}$ in type $\lambda+\lambda$ and then use the fact that ordinal arithmetic doesn't raise the cardinality

but "ordinal arithmetic doesn't raise the cardinality" is from ZFC

It should be a theorem of $\sf ZF$

I tend to agree with you

because I've seen someone proving $|A \times A| = |A|$ using the well-order of $A$

Sure, $|\alpha\times\alpha|=|\alpha|$ is a theorem of $\sf ZF$ for $\alpha\ge\omega$ an ordinal

then it's easy :P

$1 \le 2 \le |A|$

$|A| \le |A+A| \le |A \times A| = |A|$

@AlessandroCodenotti oops, $|A \times A| = |A|$ requires induction

why is that a problem?

@AlessandroCodenotti you can induct without choice?

yes, transfinite induction on ordinals and the primitive recursion theorem on $\sf ON$ work in $\sf ZF$ without problems

so I can't do it without induction ;_;