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?
 A: 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?
There are a lot of ways of showing that this can't be possible. One way is to note that you can easily mechanically check whether or not a CPL formula is provable by simply checking the truth table. On the other hand, we can encode the behavior of a Turing machine as a formula of FOL which is provable if and only if the described Turing machine halts. Therefore, if it was possible for us to know mechanically show whether any given formula of FOL is provable or not (which it would be if we could translate it to a CPL formula), then we'd be able to solve the Halting Problem.
