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), TST₄. The result says that if A=〈A₀,A₁,A₂,A₃〉 is a standard transitive and rich model of TST₄, 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.