Math 2.0

Mathematical logic and foundations Definition

Proof complexity

Builds on Proof theoryPropositional logicTautologyFunction

Definition

Let Σ\Sigma be a finite alphabet, and let TAUT⊆Σ∗\mathrm{TAUT} \subseteq \Sigma^* be the set of tautologies of propositional logic, coded as strings. A propositional proof system, in the sense of Cook and Reckhow, is a function P ⁣:Σ∗→Σ∗P \colon \Sigma^* \to \Sigma^* such that:

  1. PP is computable in time polynomial in the length of its input;
  2. the image of PP is exactly TAUT\mathrm{TAUT}.

A string ww with P(w)=φP(w) = \varphi is a PP-proof of φ\varphi. The system PP is polynomially bounded if there is a polynomial pp such that every φ∈TAUT\varphi \in \mathrm{TAUT} has a PP-proof of length at most p(∣φ∣)p(\abs{\varphi}). Proof complexity is the study of the lengths of proofs in such systems, and of the relations between systems.

Remarks

Example: the truth table system is a proof system. Let PP send a string made of a formula φ\varphi and its full truth table, with all rows true, to φ\varphi. Let PP send every other string to the fixed tautology p∨¬pp \vee \neg p. The check takes time polynomial in the length of the input, and the image of PP is TAUT\mathrm{TAUT}. This system is not polynomially bounded, because the table of a formula with nn variables has 2n2^n rows. Non-example: the map that sends each string to itself is not a proof system, because its image is all of Σ∗\Sigma^*, not TAUT\mathrm{TAUT}. Cook and Reckhow proved that a polynomially bounded proof system exists if and only if NP=coNP\mathrm{NP} = \mathrm{coNP}. Haken proved in 1985 that resolution is not polynomially bounded, using the pigeonhole principle. For stronger systems such as Frege systems, no superpolynomial lower bound is known.

Reading path

To understand this page from the ground up, read these 25 pages in order. The foundations come first.

Show the path as a graph
Element, definition, no evidence levelElementdefinitionProposition, concept, no evidence levelPropositionconceptSet, definition, no evidence levelSetdefinitionConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionPredicate, definition, no evidence levelPredicatedefinitionOrdered pair, definition, no evidence levelOrdered pairdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionTruth table, concept, no evidence levelTruth tableconceptModus ponens, concept, no evidence levelModus ponensconceptExistential quantifier, definition, no evidence levelExistential quantifierdefinitionUniversal quantifier, definition, no evidence levelUniversal quantifierdefinitionCartesian product, definition, no evidence levelCartesian productdefinitionPropositional logic, concept, no evidence levelPropositional logicconceptSubset, definition, no evidence levelSubsetdefinitionMathematical proof, concept, no evidence levelMathematical proofconceptUniqueness quantifier, definition, no evidence levelUniqueness quantifierdefinitionBinary relation, definition, no evidence levelBinary relationdefinitionTautology, definition, no evidence levelTautologydefinitionPredicate logic, concept, no evidence levelPredicate logicconceptFunction, definition, no evidence levelFunctiondefinitionProof theory, concept, no evidence levelProof theoryconceptProof complexity, definition, no evidence levelProof complexitydefinition
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Element definition
  2. Proposition concept
  3. Set definition
  4. Conjunction definition
  5. Disjunction definition
  6. Implication definition
  7. Negation definition
  8. Predicate definition
  9. Ordered pair definition
  10. Biconditional definition
  11. Truth table concept
  12. Modus ponens concept
  13. Existential quantifier definition
  14. Universal quantifier definition
  15. Cartesian product definition
  16. Propositional logic concept
  17. Subset definition
  18. Mathematical proof concept
  19. Uniqueness quantifier definition
  20. Binary relation definition
  21. Tautology definition
  22. Predicate logic concept
  23. Function definition
  24. Proof theory concept
  25. Proof complexity definition

Further reading

  1. Web https://en.wikipedia.org/wiki/Proof_complexity
About this page
Tag13JZKN6WKC
URIm2://13JZKN6WKC
Kinddefinition
WritingW0 stub
MSC03F20, 68Q17
DefinesProof complexity
UsesProof theory, Propositional logic, Tautology, Function
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • an inventory row: the row of the inventory that the node accounts for (0 of 1)
  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.