QBF with k alternations is complete for the k-th level

Lax564036.QbfComplete · concepts/Lax564036/QbfComplete.lean · lax-564036

proven

Loading review…

Natural Language Statement

Theorem

For every $k \ge 1$ , QBF $_k$ is $\Sigma_k^p$ -complete and QBF $^\forall_k$ is $\Pi_k^p$ -complete under first-order reductions, theorems of Stockmeyer and Wrathall. Every problem of the level reduces to the corresponding QBF problem by the reduction of the Cook–Levin theorem carrying the block marks: the second-order quantifier blocks of a definition become the quantifier blocks of the formula. At $k = 1$ these are an NP-complete and a coNP-complete problem.

Concept map

23 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

Show types on hover

1	import Lax904597.Problems
2	import Lax904597.Interpretations
3	import Lax904597.Relativized
4	import Lax904597.SecondOrder
5	import Lax904597.Classes
6	import Lax904597.Sat
7	import Lax904597.Machines
8	import Lax485149.Problems
9	import Lax485149.Complement
10	import Lax535992.ClassPTIME
11	import Lax564036.Hierarchy
12	import Lax564036.Difference
13	import Lax564036.Tautology
14	import Lax564036.ThreeDnfTautology
15	import Lax564036.SatUnsat
16	import Lax564036.QuantifiedBooleanFormulas
17	import Lax564036.AlternatingMachines
18
19	/-!
20	---
21	title: QBF with k alternations is complete for the k-th level
22	type: theorem
23	---
24	For every $k \ge 1$ , QBF $_k$ is $\Sigma_k^p$ -complete and
25	QBF $^\forall_k$ is $\Pi_k^p$ -complete under first-order reductions,
26	theorems of Stockmeyer and Wrathall. Every problem of the level reduces to
27	the corresponding QBF problem by the reduction of the Cook–Levin theorem
28	carrying the block marks: the second-order quantifier blocks of a definition
29	become the quantifier blocks of the formula. At $k = 1$ these are an
30	NP-complete and a coNP-complete problem.
31	-/
32
33	namespace Lax564036.QbfComplete
34
35	open FirstOrder FirstOrder.Language
36	open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.SecondOrder
37	open Lax904597.Classes Lax904597.Sat Lax904597.Machines
38	open Lax485149.Problems Lax485149.Complement Lax535992.ClassPTIME
39	open Lax564036.Hierarchy Lax564036.Difference Lax564036.Tautology Lax564036.ThreeDnfTautology
40	open Lax564036.SatUnsat Lax564036.QuantifiedBooleanFormulas Lax564036.AlternatingMachines
41
42	/-- QBF with `k + 1` blocks, existential first, is `Σₖ₊₁ᵖ`-complete. -/
43	axiom qbf_complete : ∀ (k : ℕ), (SigmaP (k + 1)).Complete (QBF (k + 1))
44
45	/-- QBF with `k + 1` blocks, universal first, is `Πₖ₊₁ᵖ`-complete. -/
46	axiom qbfPi_complete : ∀ (k : ℕ), (PiP (k + 1)).Complete (QBFPi (k + 1))
47
48	/-- QBF with one existential block is NP-complete. -/
49	axiom qbf_one_NP_complete : NP.Complete (QBF 1)
50
51	/-- QBF with one universal block is coNP-complete. -/
52	axiom qbfPi_one_coNP_complete : coNP.Complete (QBFPi 1)
53
54	end Lax564036.QbfComplete
55

Show ProofShow ProofShow ProofShow Proof

Builds on

Used by

none

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

QBF with k alternations is complete for the k-th level

Flags

Flag this concept

Natural Language Statement

Theorem

1 `qbf_complete` proven

2 `qbf_one_NP_complete` proven

3 `qbfPi_complete` proven

4 `qbfPi_one_coNP_complete` proven

Lean source view on GitHub

Discussion

Settings

Your comments

QBF with k alternations is complete for the k-th level

Natural Language Statement

Theorem

1 qbf_complete proven

2 qbf_one_NP_complete proven

3 qbfPi_complete proven

4 qbfPi_one_coNP_complete proven

Lean source view on GitHub

Discussion

1 `qbf_complete` proven

2 `qbf_one_NP_complete` proven

3 `qbfPi_complete` proven

4 `qbfPi_one_coNP_complete` proven