Countermodel (source code)

= Countermodel

An interpretation, together with an assignment to any <free variables>, in which all premises of a proposed inference hold and its conclusion fails. By soundness of the <inference rules>, a <countermodel> proves that the inference cannot be derived. For example, on $\{0,1\}$ with $P=Q=\{0\}$ and $x=0$, the formula $\forall y(P(y)\to Q(y))$ is true but $P(x)\to\forall y Q(y)$ is false. A pointwise assumption about $x$ cannot justify unrestricted <universal quantification>.