Proof Complexity Of Systems Of (non-deterministic .
Proof complexity of systems of(non-deterministic) decision trees and branchingprogramsDraft in preparation — Comments appreciated!Sam Buss Anupam Das†Dept. of MathematicsUC San Diegosbuss@ucsd.eduDept. of Computer ScienceUniversity of Copenhagenanupam.das@di.ku.dkAlexander KnopDept. of MathematicsUC San Diegoaknop@ucsd.eduMarch 11, 2020AbstractThis paper studies propositional proof systems in which lines are sequents of decision trees or branching programs — either deterministicor nondeterministic. The systems LDT and LNDT are propositionalproof systems in which lines represent, respectively, deterministic or nondeterministic decision trees. Branching programs are modeled as decision dags. Adding extension to LDT and LNDT gives systems eLDTand eLNDT in which lines represent deterministic and non-deterministicbranching programs, respectively.Deterministic and non-deterministic branching programs correspondto log-space (L) and nondeterministic log-space (NL). Thus the systemseLDT and eLNDT are propositional proof systems that reason with (nonuniform) L and NL properties.The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in the systems LDT, LNDT, eLDT,and eLNDT. These systems are also compared with Frege systems, constantdepth Frege systems and extended Frege systems. Supportedin part by Simons Foundation grant 578919by a a Marie Sklodowska-Curie fellowship, Monotonicity in Logic and Complexity, ERC project 753431.† Supported1
1IntroductionPropositional proof systems are widely studied because of their connectionsto complexity classes and their usefulness for computer-based reasoning. Thefirst connections to computational complexity arose largely from the work ofCook and Reckhow [11, 16, 17], showing a connection to the NP-coNP question.These results, building on the work of Tseitin [37] initiated the study of therelative efficiency of propositional proof systems. The present paper introducespropositional proof systems that are closely connected to log-space (L) andnondeterministic log-space (NL).Our original motivation for this study was to investigate propositional proofsystems corresponding to the first-order bounded arithmetic theories VL andVNL for L and NL, see [15]. This follows a long line of work defining formaltheories of bounded arithmetic that correspond to computational complexityclasses, as well as to provability in propositional proof systems. The first resultsof this type were due (independently) to Cook [11] who gave a translation fromPV to extended Frege (eF) proofs and to Paris and Wilkie [33] who gave atranslation from I 0 to constant-depth Frege (AC0 -Frege) proofs. Since thefirst-order bounded arithmetic theory S12 is conservative over the equationaltheory PV, Cook’s translation also applies to the bounded arithmetic theoryS21 [6]. As shown in the table below, similar propositional translations havesince been given for a range of other theories, including first-order, second-orderand equational theories.FormalTheoriesPropositionalProof SystemsComplexityClassPV, S12eFPPSA, U12Ti2 , Si 120QBFPSPACEGi , G i 1PΣi[29, 31, 6]Frege (F)ALogTime[14, 15, 1]VNCp VLGLVNLGNL [11, 6][18, 6]L[34, 15]NL[35, 15]The first three theories are first-order theories; the last three theories are secondorder. The last three theories could also be viewed as multi-sorted first-ordertheories, but their formalization as second-order theories makes it possible forthem to work elegantly with weak complexity classes. (For an introduction tothese and related results, see the books [6, 15, 27, 28].)A hallmark of the propositional translations in the table above is that thelines in the propositional proofs express (nonuniform) properties in the corresponding complexity class. For instance, a line in a Frege proof is a propositionalformula, and the evaluation problem for propositional formulas is complete foralternating log-time (ALogTime), cf. [7]. Likewise, a line in a eF proof is (implicitly) a Boolean circuit, and the Boolean circuit value problem is well known2
to be complete for P, cf. [32]. In the usual formulation of eF, the lines only“implicitly” express Boolean circuits, since it is necessary to expand the definitions of extension variables to form the circuit; however, Jeřábek [23] made thisconnection explicit in a propositional proof system Circuit-Frege CF, in whichlines are actually Boolean circuits.The present paper’s main goal is to define alternatives for the proof systems GL and GNL corresponding to log-space and nondeterministic logspace, see [34, 35, 12, 13]. The proof system GL restricts cut formulas tobe “ΣCNFp2q” formulas; the subformula property then implies that proofs contain only ΣCNFp2q formulas when proving ΣCNFp2q theorems. GNL similarlyrestricts cut formulas to be “ΣKrom” formulas. (A ΣKrom formula has theform D zϕp z, xq, where ϕ is a conjunction C1 C2 Cn with each Ci adisjunction of any number of x-literals and at most two z-literals.) ΣCNFp2qand ΣKrom have expressive power equivalent to nonuniform L and NL respectively [24, 20], but they are are somewhat ad hoc classes of quantified formulas,and their connections to L and NL are indirect. In this paper, we propose newproof systems, called eLDT and eLNDT, intended to be alternatives for GL and GNL respectively. The lines in eLDT and eLNDT proofs are sequentsof formulas expressing branching programs and nondeterministic branching programs, respectively. The advantage of our systems is that deterministic andnondeterministic branching programs correspond directly to nonuniform L andNL respectively and do not require the use of quantified formulas. This follows an earlier unpublished suggestion of S. Cook [10], who gave a system for Lbased on branching programs via “Prover-Liar” games (see [9]). (See [38] for acomprehensive introduction to branching programs.)To design the proof systems eLDT and eLNDT, we need to choose representations for branching programs. For this, we use a formula-based representation,as this fits well into the customary frameworks for proof systems. The formulasappearing in eLDT and eLNDT proofs will be descriptions of decision trees. Decision trees are not as powerful as branching programs since branching programsmay be dags instead of trees. Accordingly, we also allow extension variables.The use of extension variables allows decision trees to express branching programs; this is similar to the way the extension variables in extended Frege proofsallow formulas to express circuits. An example is given in the figure on page 27.We start in Section 2 describing proof systems LDT and LNDT that workwith just deterministic and nondeterministic decision trees (without extensionvariables). Deterministic decision trees are represented by formulas using asingle “case” or “if-then-else” connective, written in infix notation ApB, whichmeans “if p is false, then A, else B”. The condition p is required to be a literal,but A and B are arbitrary formulas. The system LDT is a sequent calculussystem in which all formulas are decision trees. Nondeterministic decision treesare represented with formulas that may also use disjunctions, allowing formulasof the form A B. The system LNDT is a sequent calculus in which all formulasare nondeterministic decision trees.LDT and LNDT are weak systems; in fact, they are both polynomiallysimulated by depth-2 LK (the sequent calculus LK with all formulas of depth3
two). Figure 1 shows the equivalences between systems as currently established.The equivalences and separations that concern LDT and LNDT are proved inSection 4.Section 5 introduces the proof systems eLDT and eLNDT for branchingprograms and nondeterministic branching programs. These again are sequentcalculus systems. These systems are obtained from LDT and LNDT by addingthe extension rule, thereby effectively changing the expressive power of formulasfrom decision trees to decision diagrams. (Decision diagrams are of course thesame as a branching programs).An important issue is designing these proof systems is how to handle isomorphic or bisimilar branching programs. Two branching programs A and Bare isomorphic if there is an isomorphism (a bijection) between the nodes ofthe branching programs. The most convenient solution perhaps would be toallow the propositional proof systems to freely replace any branching programwith any isomorphic branching program: for this, we could allow “isomorphismaxioms” or “bisimilarity axioms” A Ø B whenever the two programs are isomorphic or bisimilar (respectively). For instance, isomorphism axioms of thistype were used by Jeřábek [23] for the reformulation of extended Frege usingBoolean circuits as lines. The problem with using isomorphism or bisimilarityaxioms is that — as argued in the next paragraph — the isomorphism andbisimilarity problems for branching programs are known to be in NL, but theynot known to be in L. In other words, it is open whether valid isomorphism orbisimilarity axioms are recognizable in log-space. This make the use of theseaxioms undesirable, at least for eLDT, as it is a proof system for log-space.As a sketch of how to recognize bisimilarity with a NL algorithm, let Aand B be branching programs. A “path” in either A or B is specified by somesequence of values v1 , v2 , v3 , . . . of True or False (1 or 0): a path is traversedin the obvious way, starting the source of the branching program, and usingthe value vi to decide how to branch when reaching the i-th vertex. (Note thisallows a variable to be given conflicting truth values at different points in thepath.) Then A and B are bisimilar provided that any given path in A reachesa vertex labelled with a literal p, a disjunction , or a constant 1 or 0 if andonly if the same path in B reaches a vertex with the same label. This is clearlycoNL verifiable; namely, by nondeterministically choosing a path to traversesimultaneously in A and B that witnesses non-bisimularity. Two branchingprograms are isomorphic provided that they are bisimilar, and that in addition,any two paths reach distinct nodes in A if and only if they reach distinct nodesin B. This property clearly can also be checked co-nondeterministically. SinceNL “ coNL ([21, 36]), these properties are also in NL.One way to handle isomorphism and bisimilarity would be to nonethelessuse (say) isomorphism axioms, but require that they be accompanied by an explicit isomorphism. In our setting, this might mean giving an explicit renamingof extension variables that makes the two formulas and the definitions of theirassociated extension variables identical. We instead adopt a more conservative approach, and do not allow isomorphism axioms. Instead, the equivalenceof isomorphic branching programs (and more generally, of bisimilar branching4
eLKÐÑTree-eLKeLNDTeLDTqpThm 6.4Thm 6.1FregeÐÑLKÐÑTree-LK2-LKÐÑLNDTThm 4.9Thm 3.9Tree-2-LKÐÑTree-LNDTÐÑLDT ÐÑ 1-LKThm 4.9Thm 4.7Thm 3.10Tree-LDTqpThm 3.9Thm 3.10Tree-1-LKFigure 1: Relations between proof systems. Ñ means “polynomially simulates”;Ñqp means “quasipolynomially simulates”; 99K means “exponentially separatedfrom”. d-LK is the system of dag-like LK proofs with only depth d formulaeoccurring (atomic formulae have depth 0) By default, all proof systems allowdag-like proofs, unless they are labeled as “Tree”.programs) is proved explicitly, using induction on the size of the branchingprograms.Since formulas in eLDT and eLNDT proofs express nonuniform L and NLproperties, respectively, they are intermediate in expressive power between Booleanformulas (expressing NC1 properties) and Boolean circuits (expressing nonuniform P properties). Thus it is not surprising that, as shown in Figure 1, thesetwo systems are between Frege and extended Frege in strength. In addition,since NL properties and even st-connectivity in graphs can be expressed byquasipolynomial formulas, it is not unexpected that Frege proofs can quasipolynomially simulate eLNDT, and hence eLDT. These facts are proved in Section 6.5
2Decision tree formulas and LDT proofsThis section describes decision tree (DT) formulas, and the associated sequentcalculus proof system LDT. All our proof systems are propositional proof systems with variables x, y, z . . . intended to range over the Boolean values Falseand True. We use 0 and 1 to denote the constants False and True, respectively.A literal is either a propositional variable x or a negated propositional variablex. We use use variables p, q, r, . . . to range over literals.The only connective for forming decision tree formulas (DT formulas) is the3-ary “case” function, written in infix notation as pApBq where A and B areformulas and p is required to be a literal. This informally means “if p is false,then A, else B”. The syntax is formalized by:Definition 2.1. The decision tree formulas, or DT formulas for short, areinductively defined by(1) any literal p is a DT formula, and(2) if A and B are DT formulas and p is a literal, then pApBq is a DT formula.We call p a decision literal.The parentheses in (2) ensure unique readability, but we informally writejust ApB when the meaning is clear.Suppose α is a truth assignment to the variables; the semantics of DT formulas is defined by extending α to be a truth assignment to all DT formulas byinductively defining“ 1 αpxq#αpAqαpApBq “αpBq(1)αpxqif αppq “ 0otherwise.It is important that only literals p may serve as the decision literals in DTformulas. Notably, for C a complex formula, an expression of the form pA C Bq,which evaluates to A if C is true and to B if C is false, would in general be onlya decision diagram, not a decision tree.Although there is no explicit negation of DT formulas, we informally definethe negation A of a DT formula inductively by letting x denote x, and lettingApB denote the formula A p B. Of course A is a DT formula whenever A is,and A correctly expresses the negation of A. Notice also that negative decisionliterals are ‘syntactic sugar’, since Ap̄B is equivalent to BpA. Nonetheless thenotation is useful for making later definitions more intuitive.Our definition of DT formulas is somewhat different from the usual definitionof decision trees. The more common definition would allow 0 and 1 as atomicformulas instead of literals p as in condition (1) of Definition 2.1. We call suchformulas 0{1-DT formulas. DT formulas and 0{1-DT formulas are are equivalentin expressive power as the constants 0 and 1 are equivalent to ppp and ppp. Moregenerally, any formula 0pA, 1pA, Ap0 or Ap1 is equivalent to ppA, ppA, App,6
0qr0q0pq110100001q0p1qr111Figure 2: A DT formula q p pq q rq, and an equivalent 0{1-DT formulap1q0q p p0 q p0r1qq. Edges labelled with 0 are dotted; edges labelled with 1 aresolid. The formulas are true if both p and q are false, or all three of p, q and rare true.or App, respectively. Conversely, a literal p, when used as atom, is equivalentto 0p1.Remark 2.2 (Expressive power of decision trees). It is easy to decide the validity or satisfiability of a DT formula with a log-space algorithm. A DT formulais presented as fully parenthesized, syntactically correct formula, and it is wellknown that formulas can be efficiently parsed in L. To check satisfiability, forexample, one examines each leaf in the formula tree (each atomic subformula p)and verifies whether the path from the root to the leaf, assigning true to theliteral at the leaf, is permitted under any consistent assignment of truth valuesto variables. There is also a log-space algorithm to check the equivalence of twogiven DT formulas.The size of a DT formula A is the number of occurrences of atomic formulasin A. Recall that a (Boolean) CNF formula is a conjunction of disjunctionsof literals; each such disjunction is called a clause. Likewise a (Boolean) DNFformula is a disjunction of conjunctions of literals; each such conjunction iscalled a term. A DT formula A of size n can be expressed as a DNF formulaof size Opn2 q with at most n disjuncts. This is defined formally as TmspAq inSection 3: informally, TmspAq is formed by converting the formula to a 0{1DT formula, and then forming the disjunction, taken over all leaves labelledby a 1, of the terms expressing that that leaf is reached. A dual constructionexpresses a DT formula A as a CNF, denoted ClspAq of size Opn2 q with at mostn conjuncts.It is folklore that the construction can be partially reversed: namely anyBoolean function that is equivalently expressed by a DNF formula ϕ and aCNF formula ψ can be represented by a DT formula of size quasipolynomial inthe sizes of ϕ and ψ. This bound is optimal, as [25] proves a quasipolynomiallower bound.We next define the proof system LDT for reasoning about DT formulas.Lines in an LDT proof are sequents, hence they express disjunctions of DT’s.Thus lines in LDT proofs can express DNF properties: for these, the validity7
problem is non-trivial, in fact, coNP-complete.Definition 2.3. A cedent, denoted Γ, etc., is a multiset of formulas; we oftenuse commas for multiset union, and write Γ, A for the multiset Γ, tAu. A sequentis an expression Γ Ñ where Γ and are cedents. Γ and are called theantecedent and succedent, respectively.The intended meaning of Γ Ñ is that if every formula in Γ is true, thensome formula in is true. Accordingly, Γ Ñ is true under a truth assignment α iff αpAq “ 0 for some A P Γ or αpAq “ 1 for some A P . A sequent isvalid iff it is true for every truth assignment.Definition 2.4. The sequent calculus LDT is a proof system in which linesare sequents of DT formulas. The valid initial sequents (axioms) are, for p anyliteral,Ñ p, p.pÑpp, p ÑThe rules of inference are:Contraction rules:Weakening rules:Cut rule:Decision rules:A, A, Γ Ñ A, Γ Ñ c-l:w-l:ΓÑ A, Γ Ñ cut:c-r:Γ Ñ , A, AΓ Ñ , Aw-r: Γ Ñ Γ Ñ , AΓ Ñ , AA, Γ Ñ ΓÑ dec-l:A, Γ Ñ , pp, B, Γ Ñ ApB, Γ Ñ dec-r:Γ Ñ , A, pp, Γ Ñ , BΓ Ñ , ApBProofs are, by default, dag-like. I.e. a proof of a sequent S in LDT is a sequence pS0 , . . . , Sn q such that S is Sn and each Sk is either an initial sequentor is the conclusion of an inference step whose premises occur amongst pSi qiăk .The subsystem where proofs are restricted to be tree-like (i.e. trees of sequentscomposed by inference steps) is denoted Tree-LDT.The size of a proof is the sum of the sizes of the formulas occurring in theproof.The inference rules that are new to LDT are the two decision rules, dec-land dec-r. Since ApB is equivalent to pA pq pB pq, the lower sequentof a dec-r is true (under some fixed truth assignment) iff both upper sequentsare true under the same assignment. This property of dec-r inferences is called“invertibility”; in particular, it means that the dec-r rule is sound. Similarly,since ApB is also equivalent to pA pq pB pq, the dec-l rule is also soundand invertible.8
Remark 2.5 (Cut-free completeness). The invertibility properties also implythat the cut-free fragment of LDT is complete. To prove this by induction onthe complexity of sequents, start with a valid sequent Γ Ñ ; choose any nonatomic formula ApB in Γ or , and apply the appropriate decision rule dec-l ordec-r that introduces this formula. The upper sequents of this inference are alsovalid. Since they have logical complexity strictly less then the logical complexityof Γ Ñ , and thus, arguing by induction, they have cut-free proofs. The basecase of the induction is when Γ Ñ contains only atomic formulas; in thiscase, it can be inferred from an initial sequent with weakenings. Note that thisshows in fact, that any valid sequent can be proved in LDT using only decisionrules, weakenings, and initial sequents. The system also enjoys a ‘local’ cutelimination procedure, via standard techniques, but that is beyond the scope ofthis work.Proposition 2.6. The following have polynomial size, cut-free, Tree-LDT proofs:(e) p, B Ñ ApB(f) ApB Ñ A, p(g) ApB, p Ñ B(a) A Ñ A(b) Ñ A, A(c) A, A Ñ(d)
Theories Proof Systems Class PV, S1 2 eF P [11, 6] PSA, U1 2 QBF PSPACE [18, 6] Ti 2, S i p1 2 G i, G 1 P i [29, 31, 6] VNC0 Frege (F) ALogTime [14, 15, 1] VL GL L [34, 15] VNL GNL NL [35, 15] The rst three theories are rst-order theories; the last three theories are second-order. The last three theories could also be viewed as multi-sorted rst .
since 1950 E. German, Suhl choke-bore barrel mark PROOF MARKS: GERMAN PROOF MARKS, cont. PROOF MARKS: ITALIAN PROOF MARKS, cont. ITALIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1951 Brescia provisional proof for all guns since 1951 Gardone provisional proof for all guns
PROOF MARKS: BELGIAN PROOF MARKSPROOF MARKS: BELGIAN PROOF MARKS, cont. BELGIAN PROOF MARKS PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1852 Liege provisional black powder proof for breech loading guns and rifled barrels - Liege- double proof marking for unfurnished barrels - Liege- triple proof provisional marking for
2154 PROOF MARKS: GERMAN PROOF MARKS, cont. PROOF MARK CIRCA PROOF HOUSE TYPE OF PROOF AND GUN since 1950 E. German, Suhl repair proof since 1950 E. German, Suhl 1st black powder proof for smooth bored barrels since 1950 E. German, Suhl inspection mark since 1950 E. German, Suhl choke-bore barrel mark PROOF MARKS: GERMAN PROOF MARKS, cont.
PROOF MARKS: GERMAN PROOF MARKSPROOF MARKS: GERMAN PROOF MARKS, cont. GERMAN PROOF MARKS Research continues for the inclusion of Pre-1950 German Proofmarks. PrOOF mark CirCa PrOOF hOuse tYPe OF PrOOF and gun since 1952 Ulm since 1968 Hannover since 1968 Kiel (W. German) since 1968 Munich since 1968 Cologne (W. German) since 1968 Berlin (W. German)
Propositional vs Uniform Proof Complexity Propositional proof complexity studies the lengths of proofs of tautology families in proof systems such as Frege and bdFrege (bounded-depth Frege). Uniform proof complexity studies the power of weak formal theories such as VNC1 and V0. Both proof systems and theories are often associated with .
explain our techniques, for both the algebraic and proof complexity worlds. 1.1 Algebraic proof systems We now describe the algebraic proof systems that are the subject of this paper. If one has a set of polynomials (called axioms) f 1;:::; f m 2F[x 1;:::;x n] over some field F, then (the weak version of) Hilbert's Nullstellensatz shows that .
We present a textual analysis of three of the most common introduction to proof (ITP) texts in an effort to explore proof norms as undergraduates are indoctrinated in mathematical practices. We focus on three areas that are emphasized in proof literature: warranting, proof frameworks, and informal instantiations.
and Proof Chapter 2 Notes Geometry. 2 Unit 3 – Chapter 2 – Reasoning and Proof Monday September 30 2-3 Conditional Statements Tuesday October 1 2-5 Postulates and Proof DHQ 2-3 Block Wed/Thurs. Oct 2/3 2-6 Algebraic Proof DHQ 2-5 UNO Proof Activity
