Relationship between propositional logic, first-order logic, second-order logic higher-order logic, and type theory I understand there is propositional logic, first-order logic, second-order logic higher-order logic, and type theory, where the latter logics are extensions of the former logics. Can someone explain the differences between these types of logics for someone who knows some basic linear algebra, set theory, calculus, and boolean algebra. Specific examples of the differences are appreciated, because wikipedia is a bit over my head on this one.
 A: I'll speak about their grammatical differences, leaving their proof- and model-theoretic differences for someone more qualified to discuss. Each of these logics has a vocabulary $V$, which is the set of symbols out of which its well-formed formulas (e.g. terms, sentences)  are generated. One usually singles out a subset of $V$ as the set of logical vocabulary $V_L$. It is these $V_L$s that distinguish logics at the ground level, making it very transparent which is an extension of which. Let's see:


*

*$V_L$(PL) = { '$\lnot$' , '$\land$' }

*$V_L$(FOL) = $V_L$(PL) $\cup$ { '=' , ' $\forall_1$ ' } where $\forall_1$ quantifies over individuals

*$V_L$(SOL) = $V_L$(FOL) $\cup$ { ' $\forall_2$' } where $\forall_2$ quantifies over properties (of individuals)

*$V_L$(HOL) = $V_L$(FOL) $\cup$ { ' $\forall_n$' } where $\forall_n$ quantifies over yet higher-order properties

*$V_L$(TT) = $V_L$(_OL) $\cup$ { ' $\lambda$' } where _OL is a _-order logic (usually _ > 0)
Of course, each of these systems could be defined in different ways, choosing different sets of logical vocabulary. This is just one way of going about it. Now, as you already said, each of these logics extends the ones coming before it. With this vocabulary talk we can give precise meaning to that:

Def. Logic A is an extension of logic B iff $V_L$(B) $\subset$ $V_L$(A).

In the event that the converse doesn't hold, A is said to be a proper extension of B.
Lastly, for specific examples of differences, consider these formulas:


*

*PL: '$\phi \lor \lnot \phi$'

*FOL: '$\forall x (x = x)$'

*SOL: '$(a = b) \equiv \forall P (P(a) \leftrightarrow P(b))$'

*TT: $\forall x ([\lambda x. x](x) = x)$
Each of these sentences is also valid for logics following it (the other direction doesn't hold, of course). Notice that higher-order logic is left out, because there is no sentence $\phi$ s.t. HOL $\models \phi$ but SOL $\not\models \phi$, due to the fact that the power-set operation is SOL-expressible (Hintikka 1995).
For corrections/suggestions, please leave a comment or simply edit this post.
A: Here is my attempt to answer this question in a clear and concise way (without going into formal or philosophical discussions), but may be flawed:
Propositional logic (PL): 
Can only be used to talk about truth values/booleans (B) (true, false)
First-order logic (FOL):
Can be used talk about objects/individuals (I) (1, 2, 3, socrates,...)
There are things called Relations/Predicates (P) that are used to express properties about these objects/individuals.
In FOL, these predicates can only be first order: They can only talk about individuals directly. More precisely, they may only be allowed to have a "type" of the form I^n -> B (where I^n is an n-tuple of individuals and n is at least 0; if n is only allowed to be 0, we are left with propositional logic)
In FOL, only individuals can be quantified over, not predicates..
Note: Although definitions of FOL often contain the notion of function symbols, this is a human convenience and can be replaced with predicates without any loss in expressivity (see First order logic - why do we need function symbols? , or the way functions are defined in Prolog). Lets therefore not bother about function symbols for this discussion. 
Second-order logic (SOL):
In SOL,  predicates may also be quantified over,  in additionally to what can be done in FOL.
But the type that predicates are allowed to have remains the same as in FOL, i.e.  I^n -> B.
Higher-order Logic (HOL):
In HOL, the constraint that predicates may only have types of the form  I^n -> B may be dropped.
Predicates can therefore depend on other predicates and have types such as (I -> B) -> B or ((I -> B) -> B) -> B.
If this view is correct: The existing taxonomy is somewhat misleading since there is no "index" i in any of these logics that you can uniformly tweak/increase to go from PL (i=0) to FOL (i=1) to SOL (i=2) to HOL (i=infinity). The jumps from PL to FOL to SOL involve drastic structural additions to the sentences that can be written in each of these logics. It may therefore be easier and more understandable to answer this question with a description of HOL and make successive constraints to successively arrive at SOL, FOL and finally PL.
