Consider a tree $(T, <\_T)$ of height $\omega\_1$, with countable levels. One can view $T$ as a forcing poset by calling a condition $s\in T$ stronger than $t\in T$ if $t <\_T s$.


My question is: when is $T$ proper, as a forcing poset?


If this is too vague, consider the following. The ccc trees are exactly the Suslin trees. However the other common property used to prove properness is countable closure, and no $\omega\_1$-tree can be countably closed (a countably closed tree of infinite height has a level of size continuum). Hence we may ask;


Is there a proper $\omega\_1$-tree which is not Suslin?


**EDIT**


Given Joel's (excellent) answer, I feel I should mention that I'm mainly interested in examples of trees which are branchless, and normal.



Which $\omega_1$-trees are proper?
Concerning your final question, it is consistent that there is a proper normal $\omega\_1$-tree that is not Suslin. If $T$ is a Suslin tree, then we may build a new tree $T^+$, consisting of the all-zero branch, together with nodes branching off (at the first one), followed by a copy of $T$. This is proper as a notion of forcing, since it is *locally* c.c.c., which means that it is dense to move to a condition (off the all-zero branch), below which the forcing is c.c.c. So every generic extension via $T^+$ is actually a c.c.c. extension by $T$. The forcing $T^+$ is essentially $\omega\_1$ many side-by-side copies of $T$, but organized into an $\omega\_1$-tree. But $T^+$ is not Suslin, since it isn't even Aronzsajn. 


If one doesn't insist on normality in the tree, then one can prove outright that there is a proper $\omega\_1$ tree that is not Suslin as follows: consider the tree $S$ consisting of countable ordinal length binary sequences that never have a $0$ after a $1$. Thus, either they are identically $0$, or they are $0$ for some length, followed by some number of $1$s. This tree consists of the all-zero branch, with all-one branches branching off from it, like a comb with $\omega\_1$ many prongs, each of length $\omega\_1$. It is technically an $\omega\_1$-tree, though not normal, and it is proper since it is trivial as a notion of forcing, but it is not Suslin, since it has many uncountable branches and uncountable antichains. 


**Update.** In answer to your revised question, let me say that Martin's axiom rules out not only the existence of Suslin trees, but also rules out the existence of trees of your type.


**Theorem.** If $\text{MA}\_{\omega\_1}$ holds, then then there are no Aronszajn proper $\omega\_1$-trees. 


Proof. Suppose that $\text{MA}\_{\omega\_1}$ holds and suppose that $T$ is an Aronszajn $\omega\_1$-tree. Consider the forcing $\mathbb{P}$ to [specialize $T$](http://boolesrings.org/scoskey/special-uncountable-trees/). This forcing is c.c.c., consisting of finite partial specializing functions. Now, it follows by our MA assumption that there is a specializing function defined on the entire tree. Thus, the tree $T$ is actually special already. (I guess I am just arguing that under this MA assumption, every Aronszajn tree is special.) Now, the point is that no special Aronszajn tree can be proper, since forcing with the tree will collapse $\omega\_1$. QED


Thus, it is consistent with ZFC that there are no trees of the type you seek. In contrast, let me observe one way that positive instances can occur.


**Theorem.** If there is a Suslin tree, then there is an Aronszajn proper normal tree that is not Suslin, just as you seek.


Proof: Let $T$ be a Suslin tree, and let $S$ be an Aronszajn tree. Let $A$ be a maximal uncountable antichain in $S$. Let us make a new tree $U$ by performing surgery on $S$, replacing the part of the tree beyond any node in $A$ with a copy of $T$. That is, if the trees grow downward, then above the antichain $A$, the tree $U$ looks like $S$, but below $A$, the tree $U$ consists of copies of $T$ rooted at each node of $A$. Thus, $U$ is not Suslin, since it still has $A$ as an antichain. It is normal, since any node in $U$ below an element of $A$ can be extended to an element of $A$ and then to any level in $T$ beyond that; and any node not below an element of $A$ is in a copy of $T$ above an element of $A$, and hence can be further extended. It is proper, since forcing with $U$ amounts to forcing with $T$, as $U$ is locally like $T$, since any condition can be refined to a condition below which the forcing looks just like something in $T$. In particular, the forcing again is locally c.c.c., and hence proper. Finally, $U$ is Aronszajn, since any branch in $U$ would either get into the $T$ part, and hence be a branch in $T$, which is impossible, or else stays below $A$, in which case it would be a branch in $S$, which is also impossible. So $U$ is Aronszajn proper normal tree that is not Suslin, making for a positive instance of the kind of tree you seek. QED


