PlanetMath (more info)
 Math for the people, by the people. Sponsor PlanetMath
Encyclopedia | Requests | Forums | Docs | Wiki | Random | RSS  
Login
create new user
name:
pass:
forget your password?
Main Menu
Viewing Version 1 of 'second order logic'
[ view 'second order logic' | back to history ]

Title of object: second order logic
Canonical Name: SecondOrderLogic
Type: Definition

Created on: 2002-08-28 23:16:05.20123-04
Modified on: 2002-08-28 23:16:05.20123-04

Creator: Henry
Modifier: Henry
Author: Henry

Defines: second order language, second-order language, second order theory, second-order theory, SO
Synonyms: second order logic=second-order logic
second order logic=second order
second order logic=second-order

Preamble:

% this is the default PlanetMath preamble. as your knowledge
% of TeX increases, you will probably want to edit this, but
% it should be fine as is for beginners.
% almost certainly you want these
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
% used for TeXing text within eps files
%\usepackage{psfrag}
% need this for including graphics (\includegraphics)
%\usepackage{graphicx}
% for neatly defining theorems and propositions
%\usepackage{amsthm}
% making logically defined graphics
%\usepackage{xypic}
% there are many more packages, add them here as you need them
% define commands here
%\PMlinkescapeword{theory}
Content:

\emph{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 arithmatic has two types: the numbers and the sets of numbers.
Formally, second order logic usually has:
\begin{itemize}
\item the standard quantifiers (four of them, since each type needs its own universal and existential quantifiers)
\item the standard connectives
\item the relation $=$ with its normal semantics
\item 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
\item 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
\end{itemize}
Specific second order logics may deviate from this definition slightly. In particular, some mathematicians have argued that first order logics which additional quantifiers which give it most or all of the strength of second order logic should be considered second order logics.
Some people, chiefly Quine, have raised philisophical objections to second order logic, centering on the fact that each model requires fixing some set of sets or functions as the "actual" sets or functions for the purposes of that model.