\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{finite set} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations} [[!include foundations - contents]] \hypertarget{mathematics}{}\paragraph*{{Mathematics}}\label{mathematics} [[!include mathematicscontents]] \hypertarget{finite_sets}{}\section*{{Finite sets}}\label{finite_sets} \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{Constructivist}{Finiteness constructively and internally}\dotfill \pageref*{Constructivist} \linebreak \noindent\hyperlink{properties_and_relationships}{Properties and relationships}\dotfill \pageref*{properties_and_relationships} \linebreak \noindent\hyperlink{Finitist}{Finiteness without infinity}\dotfill \pageref*{Finitist} \linebreak \noindent\hyperlink{Challenge}{Challenge: Finiteness predicatively without infinity}\dotfill \pageref*{Challenge} \linebreak \noindent\hyperlink{External}{Finite objects in a topos}\dotfill \pageref*{External} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} A \textbf{finite set} is a set $A$ for which there exists a [[bijection]] between $A$ and the set $[n] \coloneqq \{k\in N | k\lt n\}$ for some $n\in N$, where $N$ is the natural numbers. Classically, the finite sets are the [[finitely presentable object|finitely presentable objects]] in [[Set]]. Constructively, the same is true if \emph{finitely presented} is properly interpreted, see there for details. The category [[FinSet]] of finite sets and functions between them is essentially the subject matter of [[combinatorics]]; it's fundamental in the subject of [[structure types]]. \hypertarget{Constructivist}{}\subsection*{{Finiteness constructively and internally}}\label{Constructivist} In [[constructive mathematics]], and internally to a [[topos]], a number of classically equivalent notions of finiteness become distinguishable: \begin{itemize}% \item A set is \textbf{[[finite]]} (for emphasis \textbf{Bishop-finite} or \textbf{$B$-finite}) if (as above) it admits a [[bijection]] with $[n]$ for some [[natural number]] $n$. \item A set is \textbf{[[subfinite]]} (or \textbf{$\tilde{B}$-finite}) if it admits an [[injection]] into some finite set $[n]$; that is, it is a [[subset]] of a finite set. \item A set is \textbf{finitely indexed} (or \textbf{[[Kuratowski-finite]]}, \textbf{$K$-finite}, or even sometimes, confusingly, \emph{subfinite}) if it admits a [[surjection]] from some finite set $[n]$; that is, it is a [[quotient set]] of a finite set. \item A set is \textbf{subfinitely indexed} (or \textbf{[[Kuratowski-subfinite]]} or \textbf{$\tilde{K}$-finite}) if it admits a surjection from a subfinite set, or equivalently admits an injection to a finitely indexed set; that is, it is a [[subquotient set]] of a finite set. \item A set $X$ is \textbf{[[Dedekind-finite]]} if it satisfies one of the following: \begin{itemize}% \item any [[injection]] $X\hookrightarrow X$ must be a [[bijection]]. \item for any function $f\colon \mathbb{N} \to X$ from the [[natural numbers]], there exist $n,m$ with $n \ne m$ such that $f(n) = f(m)$. \end{itemize} In contrast to the previous three notions, Dedekind-finite [[infinite sets]] can coexist with [[excluded middle|PEM]], although [[countable choice]] suffices to banish them. The above two versions of Dedekind-finiteness are equivalent under PEM, but constructively they may differ. \end{itemize} In constructive mathematics, one is usually interested in the finite sets, although the finitely indexed sets are also sometimes useful, as are the Dedekind-finite sets in the second sense. \hypertarget{properties_and_relationships}{}\subsubsection*{{Properties and relationships}}\label{properties_and_relationships} Of course, we have \begin{displaymath} \itexarray{ & & finitely\;indexed\\ & \neArrow & & \seArrow\\ finite & & & & subfinitely\;indexed\\ & \seArrow & & \neArrow\\ & & subfinite } \end{displaymath} Moreover: \begin{itemize}% \item Finite and subfinite sets have [[decidable equality]]. Conversely, any [[complement|complemented]] subset of a finite set is finite. \item Finite sets are closed under finite limits and colimits. \item A finitely indexed set with decidable equality must actually be finite. For it is then the quotient of a decidable equivalence relation, hence a coequalizer of finite sets. In particular, a set which is both finitely indexed and subfinite must be finite, i.e. the above ``commutative square'' of implications is also a ``pullback''. \item Finite sets are always [[projective object|projective]]; that is, the ``finite [[axiom of choice]]'' always holds. \item However, if a finite set with $2$ elements (or any set, finite or not, with at least $2$ distinct elements) is [[choice object|choice]], or if every finitely-indexed set (or even any $2$-indexed set) is projective, then the logic must be classical (see [[excluded middle]] for a proof). \item Finite sets are also Dedekind-finite (in either sense). \item If \emph{[[filtered category]]} means \emph{admitting cocones of every Bishop-finite diagram}, then a set is Bishop-finite iff it is a [[compact object|finitely presented object]] in Set and it is Kuratowski-finite iff it is a [[finitely generated object]] in Set. \end{itemize} \hypertarget{Finitist}{}\subsection*{{Finiteness without infinity}}\label{Finitist} The above definition of ``finite,'' and hence all the above definitions except for Dedekind-finiteness, only make sense given the set of natural numbers, i.e., given an axiom of infinity. However, they can all be rephrased to make sense even without an axiom of infinity (and thus in a topos without a [[natural numbers object]]). Basically, you define (for a given set $S$) the concept of `collection of subsets of $S$ that includes all of the finite subsets' by requiring it to be closed under inductive operations appropriate for the sense of `finite' that you want; then $S$ is finite if and only if it is an element of all such collections. Namely, for any set $S$ we define the following subsets of the [[power set]] $P(S)$. \begin{itemize}% \item $K(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A \mapsto A \cup B$ for $A$ a subset of $S$ and $B$ a [[singleton]] in $S$. Then $S$ is finitely-indexed iff $S \in K(S)$. Note that $K(S)$ is also the free [[semilattice]] generated by $S$. \item $\tilde{K}(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A \mapsto A \cup B$ for $A$ a subset of $S$ and $B$ a [[subsingleton]] in $S$. Then $S$ is subfinitely-indexed iff $S \in \tilde{K}(S)$. \item $B(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A \mapsto A \cup B$ for $A$ a subset of $S$ and $B$ a singleton in $S$ [[disjoint sets|disjoint]] from $A$. Then $S$ is finite iff $S \in B(S)$. \item $\tilde{B}(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A \mapsto A \cup B$ for $A$ a subset of $S$ and $B$ a subsingleton in $S$ disjoint from $A$. Then $S$ is subfinite iff $S \in \tilde{B}(S)$. \end{itemize} \hypertarget{Challenge}{}\subsection*{{Challenge: Finiteness predicatively without infinity}}\label{Challenge} Can you think of a way to define these notions of finite without power objects and without a natural numbers object? More specifically (and generously), can you define them in an arbitrary [[locally cartesian closed category|locally cartesian closed]] [[pretopos]] with [[enough projectives]]? \hypertarget{External}{}\subsection*{{Finite objects in a topos}}\label{External} In a topos, there are both ``external'' and ``internal'' versions of all the above notions of finiteness, depending on whether we interpret their meaning ``globally'' or in the [[internal logic]] of the topos. See [[finite object]]. \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} The [[category]] [[FinSet]] of finite sets is [[equivalence of categories|equivalent]] to that of finite [[Boolean algebras]] by the [[power set]]-[[functor]]. See at \emph{\href{FinSet#OppositeCategory}{FinSet -- Opposite category}} for details and see at \emph{[[Stone duality]]} for more. \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[hereditarily finite set]] \item [[FinSet]] \item [[finite object]] \item the [[cardinality]] of a finite set is a [[finite number]] \item [[cofinite subset]] \item [[countable ordinal]] \item [[finite-dimensional vector space]] \item [[finite homotopy type]], \begin{itemize}% \item [[finite CW-complex]], [[finite spectrum]] \end{itemize} \item [[profinite set]] \item [[finite cover]] \item [[finite graph]] \item [[finite category]] \item [[space of finite subsetc]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item [[Kazimierz Kuratowski|C. Kuratowski]], \emph{Sur la notion d'ensemble fini} , Fund. Math. \textbf{I} (1920) pp.130-131. (\href{http://matwbn.icm.edu.pl/ksiazki/fm/fm1/fm1117.pdf}{pdf}) \end{itemize} See also \begin{itemize}% \item Wikipedia, \emph{\href{https://en.wikipedia.org/wiki/Finite_set}{Finite set}} \end{itemize} [[!redirects finite set]] [[!redirects finite sets]] [[!redirects Bishop-finite set]] [[!redirects Bishop-finite sets]] [[!redirects Bishop-finite]] [[!redirects Bishop finite set]] [[!redirects Bishop finite sets]] [[!redirects Bishop finite]] [[!redirects B-finite set]] [[!redirects B-finite sets]] [[!redirects F-finite set]] [[!redirects F-finite sets]] [[!redirects subfinite set]] [[!redirects subfinite sets]] [[!redirects Bishop-subfinite set]] [[!redirects Bishop-subfinite sets]] [[!redirects Bishop-subfinite]] [[!redirects Bishop subfinite set]] [[!redirects Bishop subfinite sets]] [[!redirects Bishop subfinite]] [[!redirects B-tilde-finite set]] [[!redirects B-tilde-finite sets]] [[!redirects F-tilde-finite set]] [[!redirects F-tilde-finite sets]] [[!redirects finitely indexed set]] [[!redirects finitely indexed sets]] [[!redirects finitely-indexed set]] [[!redirects finitely-indexed sets]] [[!redirects Kuratowski-finite set]] [[!redirects Kuratowski-finite sets]] [[!redirects Kuratowski-finite]] [[!redirects Kuratowski finite set]] [[!redirects Kuratowski finite sets]] [[!redirects K-finite set]] [[!redirects K-finite sets]] [[!redirects subfinitely indexed set]] [[!redirects subfinitely indexed sets]] [[!redirects subfinitely-indexed set]] [[!redirects subfinitely-indexed sets]] [[!redirects Kuratowski-subfinite set]] [[!redirects Kuratowski-subfinite sets]] [[!redirects Kuratowski subfinite set]] [[!redirects Kuratowski subfinite sets]] [[!redirects Kuratowski subfinite]] [[!redirects K-tilde-finite set]] [[!redirects K-tilde-finite sets]] [[!redirects Dedekind-finite set]] [[!redirects Dedekind-finite sets]] [[!redirects Dedekind finite set]] [[!redirects Dedekind finite sets]] [[!redirects D-finite set]] [[!redirects D-finite sets]] \end{document}