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.
Logic – Relationship Between Propositional Logic, First-Order Logic, Second-Order Logic, and Type Theory
first-order-logichigher-order-logiclogicpropositional-calculustype-theory
Related Solutions
There are really two different meanings of "higher-order":
Referring to syntax
Systems that include variables for one or more types of "individuals" and also variabels for "sets" of individuals, "relations" on the set of individuals, or "functions" from individuals to individuals are called "higher order".
One common system for higher-order logic (with one type of individuals) is the following inductive definition of a large collection of "types":
- The set of individuals is a type
- If $\sigma_1, \ldots, \sigma_k$ are types, then there is a type $\sigma_1 \times \cdots \times \sigma_k$ whose elements are sequences $(a_1, \ldots, a_k)$ where $a_i$ is of type $\sigma_1$ for each $i \leq k$. There are also projection functions to extract each component of such a sequence.
- If $\sigma$ and $\delta$ are types, there is a type $\sigma \to \delta$ whose elements are functions with domain $\sigma$ and codomain $\delta$ (i.e. functions that take an input of type $\sigma$ to an output of type $\delta$)
- If $\sigma$ is a type, there is a type $P(\sigma)$ each element of which is a subset of $\sigma$
The logic contains, for each type, a universal quantifier over objects of that type and an existential quantifier over objects of that type. As you can see, this looks just like a kind of type theory. One difference is that higher-order logic is more like classical logic than intuitionistic type theory. In particular there are no dependent types and no "judgments", just formulas and proofs that are analogous to the ones from first-order logic.
Indeed, all the syntax of this "higher-order" logic can be interpreted as just a multi-sorted first-order logic.
Referring to semantics
"Higher-order semantics", also called "full semantics" and "standard semantics", are a particular semantics for higher-order logic in which the "higher order sorts" are taken to include all the elements they possible can. For example, in full semantics, once the set of individuals $i$ is determined for a model, the collection of objects of type $P(i)$ in that model must be contain all subsets of $i$, and the collection of objects of type $i\to i$ must contain all functions from $i$ to $i$, etc. In this way, all the higher types in a model are determined solely by the set of individuals in the model.
In "Henkin semantics" for higher-order logic, the collection of objects of type $P(i)$ in the model might be a proper subset of the powerset of $i$ in that model, and the collection of objects of type $i \to i$ might be just a proper subset of all the function from $i$ to $i$, etc.
These semantics have very different properties. Full semantics, by more or less arbitrarily reducing the number of models, allows for categorical theories for the natural numbers and the real numbers. Henkin semantics have the same completeness and compactness properties as first-order logic.
While they don't own the term, the HOL family of mechanized proof assistants (HOL4, HOL Light, Isabelle/HOL) is highly successful and influential. These are all implementations of (extensions of) simple type theory as described by this paper referenced on the HOL4 site. The most significant extension that applies to all of them is that they use a polymorphic typed lambda calculus and not purely a simply typed lambda calculus.
While "type theory" nowadays usually means systems based on typed lambda calculi or the study thereof, to the extent that it is being contrasted to HOL, it is likely to mean specifically dependently typed lambda calculi. Even more specifically, it often means a descendant of Intuitionistic or Martin-Löf Type Theory (ITT). Again, there are highly successful and influential implementations of these, most notably Coq and the LF-family including Twelf. Dependently typed lambda calculi generalize simply typed lambda calculi (and in practice, often generalize polymorphic lambda calculi as well), so something like HOL is, roughly speaking, a sub-language of ITT. However, these systems are used in dramatically different ways. In HOL, a proposition is literally a Boolean expression and the goal is to show that it is the true Boolean. In ITT, a propositions-as-types perspective is typically taken so that a proposition is modeled as a type and the goal is to produce a value of that type.
People usually don't mean Russell's theory of types unless they are talking about the early history of formal logic. "Higher order logic" could possibly also be used simply as a contrast to first-order logic, i.e. as "not-first-order logic" and in that sense second-order logic would be a "higher order logic", but people rarely talk about third- or fourth-order logic, so they'd be likely to specifically refer to second-order logic where most of the good and bad things that come with moving beyond first-order logic have already occurred.
Best Answer
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:
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.