Propositional proof complexity deals with the lengths of polynomial-time verifiable proofs for Boolean tautologies. An abundance of proof systems is known, including algebraic and semialgebraic systems, which work with polynomial equations and inequalities, respectively. The most basic algebraic proof system is based on Hilbert's Nullstellensatz (Beame et al., 1996). Tropical arithmetic has many applications in various areas of mathematics. The operations are the real addition (as the tropical multiplication) and the minimum (as the tropical addition). Recently, (Bertran and Easton, 2017; Grigoriev and Podolskii, 2018; Joo, Mincheva, 2018) demonstrated a version of Nullstellensatz in the tropical setting.

In this paper we introduce (semi)algebraic proof systems that use min-plus arithmetic. For the dual-variable encoding of Boolean variables (two tropical variables $x$ and $\overline{x}$ per one Boolean variable $x$) and $\{0,1\}$-encoding of the truth values, we prove that a *static* (Nullstellensatz-based) tropical proof system polynomially simulates *daglike* resolution and also has short proofs for the propositional pigeon-hole principle. Its dynamic version strengthened by an additional derivation rule (a tropical analogue of resolution by linear inequality) is equivalent to the system Res(LP) (aka R(LP)), which derives nonnegative linear combinations of linear inequalities; this latter system is known to polynomially simulate Krají?ek's Res(CP) (aka R(CP)) with unary coefficients. Therefore, tropical proof systems give a finer hierarchy of proof systems below Res(LP) for which we still do not have exponential lower bounds. For the truth values encoded by $\{0,\infty\}$, dynamic tropical proofs are equivalent to Res($\infty$), which is a small-depth Frege system called also DNF resolution.

Finally, we provide lower bounds on the tropical degree of derivations of a tropical version of the Knapsack problem and on the size of derivations of a much simplified tropical version of the Binary Value Principle in static tropical proof systems. Also, we establish the non-deducibility of the tropical resolution rule in these systems and discuss the necessity of the use of non-integer coefficients in tropical proofs.

Additional explanations, an example, new/updated pictures. Also a reference to [GP23].

Propositional proof complexity deals with the lengths of polynomial-time verifiable proofs for Boolean tautologies. An abundance of proof systems is known, including algebraic and semialgebraic systems, which work with polynomial equations and inequalities, respectively. The most basic algebraic proof system is based on Hilbert's Nullstellensatz (Beame et al., 1996). Tropical arithmetic has many applications in various areas of mathematics. The operations are the real addition (as the tropical multiplication) and the minimum (as the tropical addition). Recently, (Bertran and Easton, 2017; Grigoriev and Podolskii, 2018; Joo, Mincheva, 2018) demonstrated a version of Nullstellensatz in the tropical setting.

In this paper we introduce (semi)algebraic proof systems that use min-plus arithmetic. For the dual-variable encoding of Boolean variables (two tropical variables $x$ and $\overline{x}$ per one Boolean variable $x$) and $\{0,1\}$-encoding of the truth values, we prove that a *static* (Nullstellensatz-based) tropical proof system polynomially simulates *daglike* resolution and also has short proofs for the propositional pigeon-hole principle. Its dynamic version strengthened by an additional derivation rule (a tropical analogue of resolution by linear inequality) is equivalent to the system Res(LP) (aka R(LP)), which derives nonnegative linear combinations of linear inequalities; this latter system is known to polynomially simulate Krají?ek's Res(CP) (aka R(CP)) with unary coefficients. Therefore, tropical proof systems give a finer hierarchy of proof systems below Res(LP) for which we still do not have exponential lower bounds. For the truth values encoded by $\{0,\infty\}$, dynamic tropical proofs are equivalent to Res($\infty$), which is a small-depth Frege system called also DNF resolution.

Finally, we provide lower bounds on the tropical degree of derivations of a tropical version of the Knapsack problem and on the size of derivations of a much simplified tropical version of the Binary Value Principle in static tropical proof systems. Also, we establish the non-deducibility of the tropical resolution rule in these systems and discuss the necessity of the use of non-integer coefficients in tropical proofs.