We can make first-order sentences to express concepts as " vertices a and b are connected by a path of length 2 ", as well as "...by a path of length 3", "length ≤ 4 ", etc.
But trying to write " vertices a and b are connected [by a path of any length] " isn't obvious ... in fact, it can be proven that no first-order sentence can express this property! Nor can it express the closely-related property "the graph is connected" (without reference to two named vertices a and b).
Hmm, what about second-order logic? It has a bigger name; whatever it means, perhaps it can express more properties?
What exactly is second-order logic? In first-order logic, quantifiers range over elements of the domain: " there exist numbers x and y, ... ". In second-order logic, you can additionally quantify over sets of elements of the domain: " there is a set of numbers, such that ... ".
Example 5.1
For instance, " for all vertices x and y, there exists a set of vertices (call the set "Red"), the red vertices include a path from x to y ". More precisely, " every Red vertex has exactly two Red neighbors, or it is x or y (which each have exactly 1 red neighbor) ". Is this sentence true exactly when the graph is connected? Why does this description of "red vertices" not quite correspond to " just the vertices on a path from x to y "?
An interesting phenomenon: There are some relations between how difficult it is to write down a property, and how difficult to compute it! How might you try to formalize the statement "there is a winning strategy for chess"?
A shortcoming of first-order logic is that it is impossible to express the concept "path". (This can be proven, though we won't do so here.)
Thus, some other logics used to formalize certain systems include:
- As mentioned, second-order logic is like first-order logic, but it also allows quantification over entire relations. Thus, you can make formulas that state things like " For all relations R, if R is symmetric and transitive, then ... ". While less common, we could continue with third-order, fourth-order, etc.
- Temporal logic is based on quantifcation over time. This is useful to describe how a program's state changes over time. In particular, it is used for describing concurrent program specifcations and communication protocols, sequences of communications steps used in security or networking. See, for example, TeachLogic's Model-Checking module3 .
- Linear logic is a "resource-aware" logic. Every premise must be used, but it may be used only once. This models, for example, how keyboard input is usually handled: reading an input also removes it from the input stream, so that it can't be read again.
- 4734 reads
