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 = 〈 A 0 , A 1 , A 2 , A 3 〉 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.