TAUT: propositional tautology

The problem TAUT – is a formula in disjunctive normal form a tautology? – the archetypical coNP-complete problem. Its instances are the structures of the SAT vocabulary FirstOrder.Language.sat, read disjunctively: a CNF formula and a DNF formula are the same data, a set of clauses (here: terms) with the positive and negative occurrences of the variables in each. The reading is in DescriptiveComplexity.Tautology: every truth assignment satisfies all the literals of some term.

Both halves of the coNP-completeness come from SAT by the same interpretation DescriptiveComplexity.swapSignInterp, which keeps the universe and the terms and exchanges positive with negative occurrences. It witnesses De Morgan's law: a DNF is a tautology exactly when the CNF obtained by negating every literal is unsatisfiable (DescriptiveComplexity.tautology_iff_not_satisfiable). Hence

• DescriptiveComplexity.taut_mem_coNP: TAUTᶜ FO-reduces to SAT, so it is in NP, so TAUT is in coNP;
• DescriptiveComplexity.taut_hard_of_piSODefinable: a Π₁-definable problem has a Σ₁-definable complement, which reduces to SAT by the Cook–Levin discharge DescriptiveComplexity.sat_hard_of_sigmaSODefinable; complementing that reduction (DescriptiveComplexity.OrderedFOReduction.compl) and composing with SATᶜ ≤ᶠᵒ TAUT discharges coNP-hardness.

No new second-order argument is needed: TAUT is coNP-complete (DescriptiveComplexity.TAUT_coNP_complete) purely by the complement machinery of DescriptiveComplexity.Complexity and the duality DescriptiveComplexity.piSODefinable_iff_compl.

The disjunctive reading

def DescriptiveComplexity.Tautology (A : Type) [FirstOrder.Language.sat.Structure A] : Prop

A Language.sat-structure, read as a formula in disjunctive normal form, is a tautology when every assignment of truth values to its elements makes some term true – that is, satisfies every literal of that term. (Elements that are not variables of the formula may be assigned arbitrarily; they are harmless since no term mentions them.)

Equations

• One or more equations did not get rendered due to their size.

De Morgan: tautology is unsatisfiability of the sign swap

theorem DescriptiveComplexity.tautology_iff_not_satisfiable {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] (e : A ≃ B) (hcl : ∀ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![e c]) (hpos : ∀ (c x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![e c, e x]) (hneg : ∀ (c x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![e c, e x]) : Tautology A ↔ ¬Satisfiable B

De Morgan's law, structurally: a DNF formula is a tautology iff the CNF formula obtained by negating every literal is unsatisfiable. The equivalence e presents B as the sign swap of A: same terms, positive and negative occurrences exchanged.

Isomorphism-invariance and the bundled problem

theorem DescriptiveComplexity.tautology_iso {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] (e : FirstOrder.Language.sat.Equiv A B) : Tautology A ↔ Tautology B

Being a tautology is isomorphism-invariant.

def DescriptiveComplexity.TAUT : DecisionProblem FirstOrder.Language.sat

TAUT, as a problem on Language.sat-structures read disjunctively: is every truth assignment a model of some term?

Equations

• DescriptiveComplexity.TAUT = { Holds := fun (A : Type) (inst : FirstOrder.Language.sat.Structure A) => DescriptiveComplexity.Tautology A, iso_invariant := ⋯ }

The sign-swapping interpretation

def DescriptiveComplexity.swapSignInterp : FOInterpretation FirstOrder.Language.sat FirstOrder.Language.sat Unit 1

The sign-swapping interpretation: same universe, same terms, positive and negative occurrences exchanged. One-dimensional, single-tagged and quantifier-free.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.swapSignInterp_isQuantifierFree : swapSignInterp.IsQuantifierFree

The sign swap is quantifier-free.

@[simp]

theorem DescriptiveComplexity.swapSign_isClause {A : Type} [FirstOrder.Language.sat.Structure A] (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![((), w)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![w 0]

@[simp]

theorem DescriptiveComplexity.swapSign_posIn {A : Type} [FirstOrder.Language.sat.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![((), w₁), ((), w₂)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![w₁ 0, w₂ 0]

@[simp]

theorem DescriptiveComplexity.swapSign_negIn {A : Type} [FirstOrder.Language.sat.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![((), w₁), ((), w₂)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![w₁ 0, w₂ 0]

Correctness of the swap, in both directions

theorem DescriptiveComplexity.tautology_iff_not_satisfiable_map (A : Type) [FirstOrder.Language.sat.Structure A] : Tautology A ↔ ¬Satisfiable (swapSignInterp.Map A)

A DNF formula is a tautology iff its sign swap, read as a CNF formula, is unsatisfiable.

theorem DescriptiveComplexity.tautology_map_iff_not_satisfiable (A : Type) [FirstOrder.Language.sat.Structure A] : Tautology (swapSignInterp.Map A) ↔ ¬Satisfiable A

Dually: the sign swap of a CNF formula, read as a DNF formula, is a tautology iff the CNF formula is unsatisfiable.

The reductions

def DescriptiveComplexity.taut_fo_reduction_sat_compl : FOReduction TAUT SATᶜ

TAUT FO-reduces to the complement of SAT, by swapping the sign of every literal.

Equations

• DescriptiveComplexity.taut_fo_reduction_sat_compl = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.swapSignInterp, correct := ⋯ }

def DescriptiveComplexity.sat_compl_fo_reduction_taut : FOReduction SATᶜ TAUT

The complement of SAT FO-reduces to TAUT, by the same swap.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.taut_compl_fo_reduction_sat : FOReduction TAUTᶜ SAT

The complement of TAUT FO-reduces to SAT: a DNF formula fails to be a tautology exactly when its sign swap is satisfiable.

Equations

• One or more equations did not get rendered due to their size.

coNP-completeness

theorem DescriptiveComplexity.taut_mem_coNP : coNP.Mem TAUT

TAUT is in coNP: its complement FO-reduces to SAT, hence is in NP.

theorem DescriptiveComplexity.taut_hard_of_piSODefinable {L : FirstOrder.Language} (Q : DecisionProblem L) : PiSODefinable 1 Q → Nonempty (OrderedFOReduction Q TAUT)

coNP-hardness of TAUT, by complementing the Cook–Levin discharge: a Π₁-definable problem has a Σ₁-definable complement, which reduces to SAT; complementing that reduction lands in SATᶜ, which the sign swap turns into TAUT.

theorem DescriptiveComplexity.TAUT_coNP_complete : coNP.Complete TAUT

TAUT is coNP-complete. Membership is DescriptiveComplexity.taut_mem_coNP and hardness DescriptiveComplexity.taut_hard_of_piSODefinable; both are the Cook–Levin theorem read through the complement, with no second-order argument of their own.

theorem DescriptiveComplexity.taut_coNP_hard : coNP.Hard TAUT

TAUT is coNP-hard.