Editing Second-order logic (section)

==Examples==
[[File:Kindl-Treppe Aug2021d.jpg|thumb|[[Graffiti]] in [[Neukölln]] (Berlin) showing the simplest second-order sentence admitting nontrivial models, “{{math|∃''φ'' ''φ''}}”.]]

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:<ref name="mcohen">{{cite web|title=Second Order Logic |last=Marc Cohen |first=S. |url=https://faculty.washington.edu/smcohen/120/SecondOrder.pdf |website=Philosophy 120A - Introduction to Logic |date=2007}}</ref>

<math display="block">\exists x\,\mathrm{Cube}(x)</math>

However, we cannot do the same with the predicate. That is, the following expression:

<math display="block">\exists\mathrm{P}\,\mathrm{P}(b)</math>

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 (mathematics)|set]] of individuals.<ref name="mcohen"/>

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:

<math display="block">\exists\mathrm{P}\,\forall x\,(\mathrm{P}x\leftrightarrow(\mathrm{Cube}(x)\vee\mathrm{Tet}(x))).</math>

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:

<math display="block">\forall\mathrm{P}\,(\forall x\,(\mathrm{P}x\leftrightarrow(\mathrm{Cube}(x)\vee\mathrm{Tet}(x)))\rightarrow\lnot\exists x\,(\mathrm{P}x\wedge\mathrm{Dodec}(x))).</math>

Second-order quantification is especially useful because it gives the ability to express [[reachability]] properties. For example, if Parent(''x'', ''y'') denotes that ''x'' is a parent of ''y'', then first-order logic cannot express the property that ''x'' is an [[ancestor]] of ''y''. In second-order logic we can express this by saying that every set of people containing ''y'' and closed under the Parent relation contains ''x'':

<math display="block">\forall\mathrm{P}\,((\mathrm{P}y\wedge\forall a\,\forall b\,((\mathrm{P}b\wedge\mathrm{Parent}(a,b))\rightarrow\mathrm{P}a))\rightarrow\mathrm{P}x).</math>

It is notable that while we have variables for predicates in second-order-logic, we don't have variables for properties of predicates. We cannot say, for example, that there is a property Shape(''P'') that is true for the predicates ''P'' Cube, Tet, and Dodec. This would require [[Higher-order logic|third-order logic]].<ref>{{Citation |last=Väänänen |first=Jouko |title=Second-order and Higher-order Logic |date=2021 |url=https://plato.stanford.edu/archives/fall2021/entries/logic-higher-order/ |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |edition=Fall 2021 |publisher=Metaphysics Research Lab, Stanford University |access-date=2022-05-03}}</ref>
<!-- Is this reference (for the old wrong example) still useful?

In first-order logic, such a property has to be written out explicitly for each case. For example, we can say that no object is both a cube and a tetrahedron:<ref>Stapleton, G., Howse, J., & [[John M. Lee|Lee, J. M.]], eds., ''Diagrammatic Representation and Inference: 5th International Conference, Diagrams 2008'' ([[Berlin]]/[[Heidelberg]]: [[Springer Science+Business Media|Springer]], 2008), [https://books.google.com/books?id=EuNtCQAAQBAJ&pg=PA258 p. 258].</ref>{{rp|258}} -->