second order logic
Second order logic refers to logics with two (or three) types where one type consists of the objects of interest and the second is either sets of those objects or functions on those objects (or both, in the three type case). For instance, second order arithmetic has two types: the numbers and the sets of numbers.
Formally, second order logic usually has:

•
the standard quantifiers^{} (four of them, since each type needs its own universal^{} and existential quantifiers)

•
the standard connectives^{}
 •

•
if the second type represents sets, a relation $\in $ where the first argument is of the first type and the second argument is the second type

•
if the second type represents functions, a binary function which takes one argument of each type and results in an object of the first type, representing function application
Specific second order logics may deviate from this definition slightly. In particular, there are some first order logics with additional quantifiers whose strength is comparable to that of second order logic. Some mathematicians have argued that these should be considered second order logics, despite not precisely matching the definition above.
Some people, chiefly Quine, have raised philisophical objections to second order logic, centering on the question of whether models require fixing some set of sets or functions as the “actual” sets or functions for the purposes of that model.
Title  second order logic 
Canonical name  SecondOrderLogic 
Date of creation  20130322 13:00:17 
Last modified on  20130322 13:00:17 
Owner  Henry (455) 
Last modified by  Henry (455) 
Numerical id  8 
Author  Henry (455) 
Entry type  Definition 
Classification  msc 03B15 
Synonym  secondorder logic 
Synonym  second order 
Synonym  secondorder 
Related topic  IFLogic 
Defines  second order language 
Defines  secondorder language 
Defines  second order theory 
Defines  secondorder theory 