Threshold logic proof systems
Samuel R. Buss, Peter Clote · 2006
A cedent is any sequence F1, . . . , Fn of formulas separated by commas. Cedents are sometimes designated by Γ,Δ, . . . (capital Greek letters). A sequent is given by Γ Δ, where Γ,Δ are arbitrary cedents. The size [resp. depth] of a cedent F1, . . . , Fn is ∑ 1≤i≤n size(Fi) [resp. max1≤i≤n(depth(Fi))]. The size [resp. depth] of a sequent Γ Δ is size(Γ)+size(Δ) [resp. max(depth(Γ), depth(Δ))]. The intended interpretation of the sequent Γ Δ is ∧Γ → ∨Δ. An initial sequent is of the form F F where F is any formula of propositional threshold logic. The rules of inference of PTK, the sequent calculus of