A combinatorial result related to the consistency of New Foundations

We prove a combinatorial result for models of the 4-fragment of the Simple Theory of Types (TST), TST4. The result says that if A=〈A0,A1,A2,A3〉 is a standard transitive and rich model of TST4, then A satisfies the 〈0,0,n〉-property, for all n≥2. This property has arisen in the context of the consistency problem of the theory New Foundations (NF). The result is a weak form of the combinatorial condition (existence of ω-extendible coherent triples) that was shown in Tzouvaras (2007) [5], to be equivalent to the consistency of NF. Such weak versions were introduced in Tzouvaras (2009) [6], in order to relax the intractability of the original condition. The result strengthens one of the main theorems of Tzouvaras (2007) [5, Theorem 3.6] which is just equivalent to the 〈0,0,2〉-property.