Quantified Propositional Logic and Translations

In traditional propositional logic(PL), the atomic part of formulas are proposition symbols. In first-order logic(FL) the atomic part of formulas are terms, predicates are relations among terms, and quantifiers ∀,∃ are introduced to express the binding of variables ranging over a domain of discourse. We propose a new kind of logics the quantified propositional logic(QL), QL's atomic formulas are in the forms of c, X(p), F(X), where c, p are a propositional symbol, X is a first-order predicate variable and F is a second-order predicate. The quantifiers ∀,∃ are applied on first-order predicate variables. An axiomatic system is given so that the system is sound and complete with the quantified propositional logic. The translations about the quantified propositional logic are given.