# Predicate and propositional logic

I know that predicate logic provides a richer syntax, which allows us to model greater scenarios than propositional logic. But is there some sort of "formal proof" that predicate logic expresses some things that propositional logic can't?

I do understand that this question might have some exceptional answer, in the sense that we might be comparing apples and oranges or something like that. In that case, could you point out any flaw in the understanding in logic that I might have had to have been lead to this question?

To start, first-order classical predicate logic (FOL) and classical propositional logic (CPL) have different languages and in particular CPL is a sublanguage of FOL. On the face of it, CPL doesn't say anything about the new forms introduced by FOL. Still, what we usually ask for when comparing logics is whether we can translate one to the other while preserving provability. There are multiple different presentations of FOL which differ superficially, and we don't want those superficial differences to lead us to thinking them inequivalent. As a less trivial example, classical second-order propositional logic (SOPL), not to be confused with second-order predicate logic, allows us to write expressions like $\forall P.P\lor\neg P$. However, we can translate SOPL to CPL by noting since in a classical propositional logics all (closed) formulas are equivalent to either $\top$ or $\bot$, we can rewrite $\forall P.P\lor\neg P$ as $(\top\lor\neg\top)\land(\bot\lor\neg\bot)$ which is a formula of CPL. For FOL and CPL the question becomes: can we translate FOL to CPL in such a way as to preserve provability?