(Why) Are the following definitions of Axiom A equivalent?
Soft question: Which one is more common, natural, or usually easier to verify?
What was Baumgartner's original definition?
( B artoszynski) A forcing notion $ P $ satisfies Axiom A iff there is a sequence $ \langle \leq^n : n < \omega \rangle $ of orderings on $ P $ (not necessarily transitive) such that
- $ p \leq^{n + 1} q $ implies $ p \leq^n q $ and $ p \leq q $ for all $ p, q \in P $,
- if $ \langle p_n : n < \omega \rangle $ is a sequence of conditions such that $ p_{n + 1} \leq^n p_n $ for all $ n < \omega $, then there is a $ q \in P $ such that $ q \leq^n p_n $ for all $ n < \omega $,
- if $ A \subseteq P $ is an antichain, then, for each $ p \in P $ and each $ n < \omega $, there is a $ q \leq^n p $ such that $ \{ r \in A : q \text{ is compatible with } r \} $ is countable.
( J ech) A forcing notion $ P $ satisfies Axiom A iff there is a sequence $ \langle \leq^n : n < \omega \rangle $ of partial orderings on $ P $ such that
- $ p \leq^0 q $ implies $ p \leq q $ for all $ p, q \in P $,
- $ p \leq^{n + 1} q $ implies $ p \leq^n q $ for all $ p, q \in P $,
- if $ \langle p_n : n < \omega \rangle $ is a sequence of conditions such that $ p_{n + 1} \leq^n p_n $ for all $ n < \omega $, then there is a $ q \in P $ such that $ q \leq^n p_n $ for all $ n < \omega $,
- for each $ p \in P $, $ n < \omega $, and each ordinal name $ \dot{\alpha} $, there is a $ q \leq^n p $ and a countable $ B $ such that $ q \Vdash \dot{\alpha} \in \check{B} $.
I think J1 and J2 say more than just B1. (Does $ p \leq^0 q $ imply $ p \leq q $ in Bartoszynski's definition? Is this important at all?)
How important is Bartoszynski's addition not necessarily transitive? Does one need the transitivity to prove the equivalence?
But, of course, my question mainly concerns J4 versus B3.
Finally, what is meant by ordinal name? $ \mathbb{1} \Vdash \dot{\alpha} \in \mathbf{ON} $ or $ p \Vdash \dot{\alpha} \in \mathbf{ON} $? ($ \mathbf{ON} $ denotes the class of all ordinal numbers.)
First of all, the difference between B1 and J1,2 is immaterial and I imagine that B1 is simply a typo on the author's part. The fact is that you might as well always take $\leq^0$ to be the original order; furthermore, you can freely throw away finitely many of the orders and start the sequence $\leq^n$ further along without affecting anything. I'm not sure why Bartoszyinski allows nontransitive orders. Perhaps he has some arguments where this is relevant but taking the transitive envelope isn't possible.
Regarding your final question, a name for a foo always means a name which is forced by 1 to be a foo. In particular an ordinal name $\dot{\alpha}$ is a name such that $1\Vdash\dot{\alpha}\in\mathrm{Ord}$. This convention is used all over the place.
As for the issue of B3 vs J4, they are equivalent. The idea behind this is that ordinal names are morally the same thing as maximal antichains. Starting with an ordinal name $\dot{\alpha}$ you can extract a maximal antichain of conditions which force $\dot{\alpha}$ to have a particular value. Conversely, given a maximal antichain $A$ you can take an enumeration $f$ of $A$ and then mix the (check names for the) values of $f$ over $A$ to get an ordinal name.
With this idea it is clear that B3 and J4 are equivalent. Starting from B3 and an ordinal name $\dot{\alpha}$, assign a maximal antichain $A$ to $\dot{\alpha}$ as above and apply B3. Your $B$ is now the values of $\dot{\alpha}$ supported on the countable subset given by B3. Conversely, starting from J4 and an antichain $A$, we can assume $A$ is maximal and assign to it an ordinal name $\dot{\alpha}$ as above. Apply J4 to it to get a countable set of values $B$. Your countable set of conditions now consists of those whose value in the enumeration you took when building $\dot{\alpha}$ lies in $B$.