Primitive positive formula (source code)

= Primitive positive formula
{title2=$\exists\bar y\,\bigwedge_j\theta_j$}

= Tame formula
{synonym}

A primitive positive formula is generated from <atomic formulas> using only <logical conjunction> and <existential quantification>. It can be put in the form $\exists\bar y\,\bigwedge_j\theta_j(\bar x,\bar y)$ with each $\theta_j$ atomic. The exam terminology tame formula refers to this fragment. Its <reduced product> transfer needs only filter intersection and upward closure, together with coordinatewise choices of witnesses.