\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*{Lindström's theorem} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations} [[!include foundations - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{the_first_theorem_of_lindstrm}{The first theorem of Lindstr\"o{}m}\dotfill \pageref*{the_first_theorem_of_lindstrm} \linebreak \noindent\hyperlink{the_second_theorem_of_lindstrm}{The second theorem of Lindstr\"o{}m}\dotfill \pageref*{the_second_theorem_of_lindstrm} \linebreak \noindent\hyperlink{discussion}{Discussion}\dotfill \pageref*{discussion} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} \emph{Lindstr\"o{}m's theorem}, or more precisely, Lindstr\"o{}m's theorems, are important results in [[abstract model theory]] due to the Swedish logician [[Per Lindström]] that give syntax-free characterizations of (classical untyped) [[first-order logic]] (`syntax-free' in the sense of not referring to the specific [[syntax|syntactic]] make up of the formulas). \hypertarget{the_first_theorem_of_lindstrm}{}\subsubsection*{{The first theorem of Lindstr\"o{}m}}\label{the_first_theorem_of_lindstrm} This ([[semantics|semantic]]) version of Lindstr\"o{}m's characterization is the best known and is usually meant when one speaks of ` \emph{the} theorem of Lindstr\"o{}m' . It states that the validity of the downward [[Löwenheim-Skolem theorem]] (a sentence that holds in some [[model]] already holds in an at most countable model) and the [[compactness theorem]] (a set of sentences has a model if every finite subset has a model) characterizes up to expressive power standard [[first-order logic]] among all [[formal logic|logics]] satisfying certain regularity conditions\footnote{These conditions formalize some classical background assumptions on logical systems like the restriction of semantics to standard set-theoretic structures and the existence of [[negation]] in the sense that for every sentence $\varphi$ there is $\psi$ such that $\mathfrak{A}\models\varphi$ iff not $\mathfrak{A}\models\psi$.} : A gain in expressive power comes at the price of the loss of the validity of at least one of these theorems e.g. in [[second-order logic]] both theorems fail to hold. \emph{Barwise} (1977, p.45, cf. below) has called the first Lindstr\"o{}m theorem \begin{quote}% one of the first, and still most striking, results in abstract model theory \end{quote} and \hyperlink{VaananenWesterstahl2010}{V\"a{}\"a{}n\"a{}nenWesterst\aa{}hl, p. 102} write that the \begin{quote}% 11-page paper (ed.: the authors refer to (\#Lindstrom1969) ) is without a doubt Pelle Lindstr\"o{}m's most important single contribution to mathematical logic. In it, he uses a surprisingly general notion of a logic \ldots{} \end{quote} and go on to write \hyperlink{VaananenWesterstahl2010}{V\"a{}\"a{}n\"a{}nenWesterst\aa{}hl, p. 104} \begin{quote}% Lindstr\"o{}m's Theorem tells us that any proper extension of [[first-order logic]] has to detect something non-trivial about the set-theoretic [[universe]]. On the other hand, Lindstr\"o{}m's theorem reveals a deep robustness of first-order logic: it does not matter which way you define your syntax - as long as your semantics obeys certain basic principles \ldots{} you will get the same logic. \end{quote} \hypertarget{the_second_theorem_of_lindstrm}{}\subsubsection*{{The second theorem of Lindstr\"o{}m}}\label{the_second_theorem_of_lindstrm} The \emph{second} Lindstr\"o{}m theorem is of a more proof-theoretic nature and involves the concept of an \emph{effective logical system} which draws on [[computability theory]]. It achieves a characterization of standard first-order logic in the class of all effective regular logical systems by the two properties of having an enumerable set of tautologies and validity of the L\"o{}wenheim-Skolem theorem. \hypertarget{discussion}{}\subsection*{{Discussion}}\label{discussion} These results are sometimes viewed as an explanation of the privileged role that standard first-order logic plays in mathematical logic. In the end, what lesson one draws from them (once the classical background assumptions accepted), largely hinges on how one assesses the role of the \emph{[[Löwenheim-Skolem theorem]]} in mathematical logic, which enjoys a rather controversial status and has encountered skepticism already by \emph{Thoralf Skolem}, the man himself. This scepticism is clearly present in the following comment by \emph{Hao Wang} (1974, quoted after Flum(1985), pp.77-78): \begin{quote}% ..what is established (by Lindstr\"o{}m's theorem) is not that first-order logic is the only possible logic but rather that is the only possible logic when we in a sense deny the reality to the concept of uncountability \ldots{} \end{quote} Further alternative characterizations and extensions to other logics are known and constitute the field of [[abstract model theory]]. \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[predicate logic]] \item [[higher order logic]] \item [[Löwenheim-Skolem theorem]] \item [[compactness theorem]] \item [[abstract model theory]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item [[Per Lindström]]: \emph{On Extensions of Elementary Logic}, Theoria 35 pp.1-11 (1969) \item Barwise (ed.): \emph{Handbook of Mathematical Logic} , Elsevier Amsterdam 1977. \end{itemize} A textbook account of the results appears in: \begin{itemize}% \item Ebbinghaus, Flum, Thomas : \emph{Einf\"u{}hrung in die mathematische Logik}, Wissenschaftliche Buchgesellschaft Darmstadt 1986. \end{itemize} A more recent overview of Lindstr\"o{}m's results can be found here: \begin{itemize}% \item [[Jouko Väänänen]], \emph{Lindstr\"o{}m's Theorem} . Ms. (\href{http://www.math.helsinki.fi/logic/opetus/lt/lindstrom_theorem1.pdf}{pdf}) \item [[Jouko Väänänen]], Dag Westerst\aa{}hl: In Memoriam: Per Lindstr\"o{}m. Theoria \textbf{76} (2010), 100-107 \end{itemize} Further material (including a discussion of the broader implications of Lindstr\"o{}m's results for logic) can be found in \begin{itemize}% \item J\"o{}rg Flum, \emph{Characterizing Logics} , (\href{http://projecteuclid.org/download/pdf_1/euclid.pl/1235417268}{pdf}), chap. III of \item Barwise, Feferman (eds.), \emph{Model-theoretic Logics} , Springer Heidelberg 1985 (\href{http://projecteuclid.org/euclid.pl/1235417263#toc}{toc}) \end{itemize} [[!redirects Lindström theorem]] [[!redirects Lindström's theorems]] [[!redirects Lindström-theorem]] [[!redirects Lindström-theorems]] [[!redirects Lindstrom's theorem]] [[!redirects Lindström's Theorem]] [[!redirects Lindstrom's Theorem]] \end{document}