Typical ambiguity is the schema asserting that every closed well-typed sentence is equivalent to its uniform type-raise. It is not an assertion that adjacent types have the same cardinality. To obtain finite satisfiability, color finite increasing rank selections by the truth values of the finitely many sentences concerned. The Ramsey's theorem gives a homogeneous rank set; two overlapping windows then have equal truth vectors, yielding the desired type-raise equivalences. The compactness theorem gives a first-order model of the entire schema.
New to topics? Read the docs here!