Completeness proofs for propositional logic with polynomial-time connectives (Q1123883)

Atomic formulas are of the form P(t), where P are monadic predicate variables (which the authors call propositional variables) and t is a term. Composite formulas are constructed by \(\sim\), \&, \(\vee\) and bounded quantfiers \(\forall x\leq t\), \(\exists x\leq t\), as well as \(\forall x\in T\), \(\exists x\in T\) at the end of the paper. When a bounding term is closed, i.e. does not contain individual variables, the corresponding quantifier can be expanded into \& or \(\vee\), which provides completeness and decidability theorem for closed formulas and obvious rules for \(\forall\), \(\exists\). In the presence of free individuum variables, decidability depends of admitted function symbols. The word ``polynomial'' in the title refers to these functions, not to a decision procedure for derivability.