Upward absolute formula (source code)

= Upward absolute formula

A formula is upward absolute when its truth in a smaller transitive class implies its truth in a larger one. Existential formulas with bounded matrices are upward absolute because their witnesses remain available.