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.