Closed forcing adds no short ordinal sequences
ID: closed-forcing-adds-no-short-ordinal-sequences
If a ground-model order is -closed, it adds no ordinal-valued functions with domain . Recursively decide each name value inside the ground model, using closure at intermediate limit stages and once more at the end. Below each starting condition, conditions deciding the entire function are dense. A generic filter meets them by the dense-below generic meeting lemma. The recursion must be internal to the ground model, since its closure property only covers its own sequences.
New to topics? Read the docs here!