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.


1 Answer 1


You can see :

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].


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .