= Solution
\b[Entail is <co-NP>-complete under <polynomial-time many-one reductions>.] For valid <propositional formulas>, <semantic entailment> holds exactly when the <logical conjunction> of the premise and the conclusion's <logical negation> is an <unsatisfiable Boolean formula>:
$$
\varphi\models\psi
\quad\Longleftrightarrow\quad
\varphi\land\neg\psi\text{ is unsatisfiable}.
$$
A counterexample to <semantic entailment> is a <Boolean valuation> making $\varphi$ true and $\psi$ false. Guessing one <bit> for each distinct <Boolean variable> and evaluating both <propositional formulas> is a <polynomial-time algorithm>. Thus the <complement> of Entail belongs to <NP>. Malformed descriptions, also in that <complement>, can be accepted after a deterministic syntax check. Hence Entail belongs to <co-NP> as a <formal language> over all <strings>.
For hardness, the <unsatisfiable Boolean formula> problem is <co-NP>-hard: if $A\in\mathrm{co\text{-}NP}$, then $\overline A\in\mathrm{NP}$, and the permitted <NP-hardness> of <SAT> supplies a <polynomial-time many-one reduction> $r$ with
$$
x\in\overline A\quad\Longleftrightarrow\quad r(x)\in\mathrm{SAT}.
$$
We may ensure $r(x)$ is always a valid <propositional formula>, replacing any malformed output by a fixed contradiction. It follows that $x\in A$ exactly when $r(x)$ is unsatisfiable. This justifies using the unsatisfiability problem as a hardness source without an extra assumption.
Map a valid <propositional formula> $\theta$ to
$$
f(\theta)=\langle\theta,\ p\land\neg p\rangle,
$$
where $p$ is a fixed <Boolean variable>. The second <propositional formula> is false under every <Boolean valuation>. Consequently it is entailed by $\theta$ precisely when no <Boolean valuation> satisfies $\theta$. Thus
$$
\theta\text{ unsatisfiable}
\quad\Longleftrightarrow\quad f(\theta)\in\mathrm{Entail}.
$$
The output has only constant additional length and is computable in <polynomial time>. If the source unsatisfiability language rejects malformed <strings>, map them to the fixed no-instance $\langle p,p\land\neg p\rangle$. This completes a total <polynomial-time many-one reduction> and proves the claimed <co-NP>-completeness.
$$
\boxed{\mathrm{Entail}\text{ is co-NP-complete}.}
$$
Back to article page
