%%% This file is part of PlanetMath snapshot of 2009-01-12
%%% Primary Title: second order logic
%%% Primary Category Code: 03B15
%%% Filename: SecondOrderLogic.tex
%%% Version: 5
%%% Owner: Henry
%%% Author(s): Henry
%%% PlanetMath is released under the GNU Free Documentation License.
%%% You should have received a file called fdl.txt along with this file.        
%%% If not, please write to gnu@gnu.org.
\documentclass[12pt]{article}
\pagestyle{empty}
\setlength{\paperwidth}{8.5in}
\setlength{\paperheight}{11in}

\setlength{\topmargin}{0.00in}
\setlength{\headsep}{0.00in}
\setlength{\headheight}{0.00in}
\setlength{\evensidemargin}{0.00in}
\setlength{\oddsidemargin}{0.00in}
\setlength{\textwidth}{6.5in}
\setlength{\textheight}{9.00in}
\setlength{\voffset}{0.00in}
\setlength{\hoffset}{0.00in}
\setlength{\marginparwidth}{0.00in}
\setlength{\marginparsep}{0.00in}
\setlength{\parindent}{0.00in}
\setlength{\parskip}{0.15in}

\usepackage{html}

% 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}

\begin{document}

 \emph{Second order logic} refers to \htmladdnormallink{logics}{http://planetmath.org/encyclopedia/Semantics.html} with two (or three) \htmladdnormallink{types}{http://planetmath.org/encyclopedia/Semantics.html} where one type consists of the \htmladdnormallink{objects}{http://planetmath.org/encyclopedia/Identity2.html} of interest and the second is either sets of those objects or \htmladdnormallink{functions}{http://planetmath.org/encyclopedia/Surjective2.html} on those objects (or both, in the three type case). For instance, \htmladdnormallink{second order arithmetic}{http://planetmath.org/encyclopedia/SecondOrderArithmetic.html} has two types: the \htmladdnormallink{numbers}{http://planetmath.org/encyclopedia/Number.html} and the sets of numbers.

Formally, second order logic usually has:

\begin{itemize}
\item the standard \htmladdnormallink{quantifiers}{http://planetmath.org/encyclopedia/VacuousQuantification.html} (four of them, since each type needs its own \htmladdnormallink{universal}{http://planetmath.org/encyclopedia/UniversalFormula.html} and \htmladdnormallink{existential quantifiers}{http://planetmath.org/encyclopedia/VacuousQuantification.html})

\item the standard \htmladdnormallink{connectives}{http://planetmath.org/encyclopedia/NOR.html}

\item the \htmladdnormallink{relation}{http://planetmath.org/encyclopedia/Surjective2.html} $=$ with its \htmladdnormallink{normal}{http://planetmath.org/encyclopedia/ChuSpace.html} \htmladdnormallink{semantics}{http://planetmath.org/encyclopedia/Semantics.html}

\item if the second type \htmladdnormallink{represents}{http://planetmath.org/encyclopedia/RepresentableFunctor.html} sets, a relation $\in$ where the first \htmladdnormallink{argument}{http://planetmath.org/encyclopedia/Argument2.html} is of the first type and the second argument is the second type

\item if the second type represents functions, a \htmladdnormallink{binary}{http://planetmath.org/encyclopedia/Arity.html} function which takes one argument of each type and results in an object of the first type, representing function \htmladdnormallink{application}{http://planetmath.org/encyclopedia/Applications.html}
\end{itemize}

Specific second order logics may deviate from this definition slightly. In particular, there are some \htmladdnormallink{first order logics}{http://planetmath.org/encyclopedia/FirstOrderLogic.html} with additional quantifiers whose strength is \htmladdnormallink{comparable}{http://planetmath.org/encyclopedia/ComparisonOfFilters.html} to that of second order logic. Some mathematicians have argued that these should be considered second order logics, despite not precisely \htmladdnormallink{matching}{http://planetmath.org/encyclopedia/MaximalMatching.html} 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.

\end{document}