quantified propositional logic and predicate logic

Question

I am curious if there is a system that allows for both quantification over first-order objects and quantification over propositions, and also has inference rules that allows one to infer from a first-order formula to a formula in quantified propositional logic. More specifically, I am struggling to see how the following step could be valid in any formal system:

∃x (Px ∧ Φ(Px)) ⊢ ∃p(p ∧ Φ(p))

any help would be greatly appreciated.

Answer 1

You can see :

• Alonzo Church, Introduction to Mathematical Logic, Princeton UP (1956): Ch.V Functional Calculi of Second Order, page 295-on.

The calculus has porpositional variables that can be quantified and we have the axioms

⊢ (p)A → A[B/p],

where A[B/p] is the result of substituting formula B in place of propositional variable p, as well as the rule of inference :

if ⊢ A, then ⊢ A[B/p].