>>14291701A slightly better analogy would predicate logic with quantifiers, since assignment of types is analogous to quantification.
Propositional logic is very stripped down and basic. It essentially just a 2-valued boolean algebra. First-order and higher-order predicate logic are much more semantically complex, because the symbols of quantified predicate logic don't just take truth functions and {0, 1} as there semantic values, but you can have much more complex objects, like sets and numbers.
Propositional logic basically consists of boolean combinations of variables taking values in {0, 1}, for example expressions like
(p v q v r) ^ ~p,
which is true iff q=1 or r=1.
Quantified predicate logic, on the other hand, allows you to construct propositions that have internal structure, and make specific claims about objects in you universe of discourse, e.g.
(Ax) (Ey) x+1=y,
(every object has a successor)
or
(Ax) (Ey) x<y
(every object is smaller than some other object).
