Atomless forcing order (source code)

= Atomless forcing order

= Non-atomic forcing order
{synonym}

An order is atomless if it has no <forcing atom>, equivalently every condition has a pair of <incompatible forcing conditions> below it. For a fixed order belonging to a <transitive model>, this property is absolute because its quantifiers range over the unchanged <set> of conditions. Infinite-domain <Fn forcing> with at least two possible values is atomless: prescribe different values at one fresh coordinate.