Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This provides better structural properties for the analysis of this relation and leads to a simple decision algorithm. We generalize this transitivity-free approach to a general class of extensions of BCD allowing to impose some pre-order as well as some fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with η-equality (Scott, Park, etc.). Proving the equivalence between the transitivity-free systems and their BCD-style presentation is addressed by means of cut-elimination techniques from proof theory. Due to the presence of fixpoints, we are led to introduce non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.

We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof system based on inference rules, a combinatorial proof is a syntax-free presentation of a proof that is independent from any set of inference rules. We show that the two proof representations are related via a deep inference decomposition theorem that establishes a new kind of normal form for syntactic proofs. This yields (a) a simple proof of soundness and completeness for first-order combinatorial proofs, and (b) a full completeness theorem: every combinatorial proof is the image of a syntactic proof.