Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Second-order logic
Summary
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.
First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence says that for every formula P, and every individual x, either Px is true or not(Px) is true (this is the law of excluded middle). Second-order logic also includes quantification over sets, functions, and other variables (see section below). Both first-order and second-order logic use the idea of a domain of discourse (often called simply the "domain" or the "universe"). The domain is a set over which individual elements may be quantified.
First-order logic can quantify over individuals, but not over properties. That is, we can take an atomic sentence like Cube(b) and obtain a quantified sentence by replacing the name with a variable and attaching a quantifier:
∃x Cube(x)
However, we cannot do the same with the predicate. That is, the following expression
∃P P(b)
is not a sentence of first-order logic, but this is a legitimate sentence of second-order logic. Here, P is a predicate variable and is semantically a set of individuals.
As a result, second-order logic has greater expressive power than first-order logic. For example, there is no way in first-order logic to identify the set of all cubes and tetrahedrons. But the existence of this set can be asserted in second-order logic as
∃P ∀x (Px ↔ (Cube(x) ∨ Tet(x))).
We can then assert properties of this set. For instance, the following says that the set of all cubes and tetrahedrons does not contain any dodecahedrons:
∀P (∀x (Px ↔ (Cube(x) ∨ Tet(x))) → ¬ ∃x (Px ∧ Dodec(x))).
Second-order quantification is especially useful because it gives the ability to express reachability properties.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.