Downward absolute formula (source code)

= Downward absolute formula

A formula is downward absolute when its truth in a larger transitive class implies its truth in a smaller one. Universal formulas with bounded matrices are downward absolute.