1:
2: % Notationsvereinbarungen
3: %
4: % Formeln: phi, psi, chi,...
5: % formale Variablen: x, y, z, ...
6: % reelle Zahlen: a, b, c, ...
7: % Goedel sets: V, W, ...
8: % labelled Goedel sets: J, K, L, ...
9: % Barriers: B, C, D, ...
10: % quasi Orderings: Q
11: % elements of them: p, q, ...
12: % Goedellogik Bezeichnung vereinheitlichen
13: %
14: %
15: %\documentclass{llncs}
16:
17: \documentclass[a4paper]{article}
18: \date{Nov 5, 2004}
19: \usepackage[T1]{fontenc}
20: \usepackage[latin1]{inputenc}
21: \usepackage{amsmath,amssymb,amsthm,paralist}
22: % ***
23: % ***
24: \usepackage{mathrsfs}
25: \usepackage{textcomp,xspace}
26:
27: \input{defs}
28:
29: % ***
30: % ***
31: % ***
32: % ***
33: % ***
34: % ***
35: % ***
36:
37: \title{Continuous Fra{\"\i}ss{\'e} Conjecture}
38: \author{Arnold Beckmann \and Martin Goldstern \and Norbert Preining\\[2ex]
39: Institute of Discrete Mathematics and Geometry\\
40: Vienna University of Technology, Austria\\
41: \protect{\texttt{martin.goldstern@tuwien.ac.at}}\\
42: \protect{\texttt{\{beckmann,preining\}@logic.at}}}
43: \pagestyle{plain}
44:
45:
46:
47: \begin{document}
48:
49: \maketitle
50:
51:
52: \begin{abstract}
53: We will investigate the relation of countable closed linear orderings
54: with respect to continuous monotone embeddability and will show
55: that there are exactly $\aleph_1$ many equivalence classes with
56: respect to this embeddability relation. This is an extension of
57: Laver's result \cite{Laver:1971}, who considered (plain) embeddability,
58: which yields coarser equivalence classes. Using this result we show that
59: there are only $\aleph_0$ many different Gödel logics.
60: \end{abstract}
61:
62: \section{Introduction}
63:
64: The starting point of the present work was the question `How many Gödel
65: logics are there?'
66: This question led us to the study of embeddability relations of
67: (countable) linear orderings.
68: The most important result in this field is Laver's classical result
69: on the Fra{\"\i}ss{\'e} Conjecture \cite{Laver:1971} which counts
70: the number of scattered linear orderings with respect
71: to bi-embeddability.
72:
73: We will generalize Laver's method to deal not only with monotone but
74: with continuous monotone embeddings, and come back to Gödel logics in
75: Section~\ref{sec:goedel}, where we use this result to compute the
76: number of Gödel logics.
77: Gödel logics form a class of many-valued logics, which are one of
78: the three fundamental $t$-norm based logics.
79:
80: % ***
81: % ***
82: % ***
83:
84: % ***
85: % ***
86:
87: % ***
88: % ***
89: % ***
90:
91: Our main result is that the set of countable closed linear orderings
92: is better-quasi-ordered by strictly monotone continuous embeddability, even
93: when we consider labeled countable closed linear orderings.
94: As a corollary we derive that there are only countably many Gödel logics.
95:
96: % ***
97: % ***
98: % ***
99: % ***
100: % ***
101: % ***
102:
103: % ***
104: % ***
105: % ***
106:
107: The main concepts in all these discussions are `well-quasi orderings'
108: and `better-quasi-ordering', which have been introduced by
109: Nash-Williams in a series of five papers in the 1960s
110: \cite{Nash:1963,Nash:1964,Nash:1965a,Nash:1965b,Nash:1968}
111:
112: While considering embeddability relation of orderings, examples of
113: infinite descending sequences, as well as infinite antichains can be
114: given \cite{Dushnik,Sierpinski}. In \cite{Fraisse}, Fra{\"\i}ss{\'e}
115: made conjectures to the effect that the embeddability relation is more
116: well behaved in the case of countable order types (later extended to
117: scattered order types), stating that `every descending sequence of
118: countable order types is finite, and every antichain of countable
119: order types is finite.' This conjecture was finally proved by Laver
120: \cite{Laver:1971}.
121:
122:
123: \subsection{Basic concepts}
124:
125: In our exposition we will mainly follow Rosenstein's textbook on linear
126: orderings \cite{Rosenstein:1982}, especially Chapter~10. To keep this
127: article self-contained we will give all the necessary definition and
128: cite some results, but ask the reader to consult the mentioned book
129: for motivation, background and history of these concepts and results, as well
130: as for the proofs.
131: % ***
132:
133: \begin{definition} (\cite{Rosenstein:1982}, 10.12-10.15)
134: A \emph{quasi-ordering} is a reflexive and transitive binary
135: relation $\le_Q$ on a set $Q$.
136: With $<_Q$ we denote the strict part of $\le_Q$, i.e.\ $p\mathrel{<_Q}q$
137: iff $p\mathrel{\le_Q} q$ and $q\mathrel{\nleq}_Q p$.
138: We will often drop the index ${}_Q$ if there is not danger of confusion.
139:
140: % ***
141:
142: We write $p \equiv_Q q$ iff both $p\mathrel{\le_Q} q$ and % ***
143: $q\mathrel{\le_Q} p$ hold.
144: This is an equivalence relation;
145: we write $Q/{\equiv}$ for the set of equivalence classes.
146:
147:
148: An infinite sequence $\vec p = \seqof{p_n}{n<\omega}$ is called good
149: if there are indices $n<k$ with $p_n\le p_k$; $\vec p $ is called
150: bad if it is not good.
151: $\vec p$ is called an
152: \emph{infinite descending chain} if
153: $p_0\mathrel{>_Q}p_1\mathrel{>_Q}p_2\mathrel{>_Q}\dots$.
154: It is called an \emph{anti-chain} of $Q$ if neither
155: $p_i\mathrel{\le_Q} p_j$ nor $p_j\mathrel{\le_Q} p_i$ for $i\neq j$.
156:
157: % ***
158: % ***
159:
160: % ***
161: % ***
162: % ***
163:
164: A set $Q$ is a \emph{well-quasi-ordering}, denoted \emph{wqo}, if
165: any/all conditions in Lemma~\ref{rosenstein:10.17} hold.
166: % ***
167: % ***
168: % ***
169: \end{definition}
170:
171: \begin{lemma}\label{rosenstein:10.17}
172: {\normalfont (\cite{Rosenstein:1982}, 10.16--10.17)}
173: Let $(Q,\le)$ be partial order. Then the following are equivalent:
174: \begin{enumerate}
175: \item All sequences $ \vec q = \seqof{q_i}{i<\omega}$ are good.
176: \item For all sequences $ \vec q = \seqof{q_n}{n<\omega}$ there
177: is an infinite subsequence $\<q_n\suchthat n\in I\>$ which
178: is either strictly increasing ($n<m$ implies $q_n<q_m$) or constant
179: ($n<m$ implies % ***
180: $q_n\equiv q_m$).
181: \item There are no infinite antichains and no infinite decreasing chains
182: in $Q$.
183: \end{enumerate}
184: \end{lemma}
185:
186: \begin{definition} (\cite{Rosenstein:1982}, 10.19)
187: Given quasi-orderings $Q_1$ and $Q_2$, we define the quasi-ordering
188: $Q_1\times Q_2$ by stipulating that
189: $\langle p_1,p_2\rangle\le\langle q_1,q_2\rangle$ if
190: $p_1\mathrel{\le_{Q_1}}q_1$ and $p_2\mathrel{\le_{Q_2}}q_2$.
191: \end{definition}
192:
193: \begin{lemma} {\normalfont (\cite{Rosenstein:1982}, 10.20)}
194: If $Q_1$ and $Q_2$ are wqo, then so is $Q_1\times Q_2$.
195: \end{lemma}
196:
197: \begin{definition}\label{def:seq-order} (\cite{Rosenstein:1982}, 10.21, 10.24)
198: Given a quasi-ordering $Q$, we define the quasi-ordering
199: $Q^{<\omega}$, whose domain is the set of all finite sequences of
200: elements of $Q$, by stipulating that
201: $\<p_0,p_1,\dots,p_{n-1}\>\le\<q_0,q_1,\dots,q_{m-1}\>$ if there
202: is a strictly increasing $h:n\to m$ such that
203: $a_i\mathrel{\le_Q}b_{h(i)}$ for all $i<n$.
204:
205: We define the quasi-ordering $Q^{\omega}$ of $\omega$-sequences of
206: elements of $Q$ by saying that
207: $\seqof{p_n}{n<\omega}\le\seqof{q_n}{n<\omega}$ if there is a
208: strictly increasing $h: \omega\to\omega$ such that
209: $a_n\mathrel{\le_Q}b_{h(n)}$ for all $n<\omega$.
210: \end{definition}
211:
212: \begin{theorem} {\normalfont (\cite{Rosenstein:1982}, 10.23)}
213: If $Q$ is a wqo, then so is $Q^{<\omega}$.
214: \end{theorem}
215:
216: \begin{definition}\label{def:barrier} (\cite{Rosenstein:1982}, 10.31--10.33)
217: If $c$ is a finite subset of $\bbN$, $d$ is any subset of $\bbN$, then we
218: say that $d$ extends $c$ iff: $c = \{i\in d: i \le \max c\}$, i.e.,
219: if $c$ is an initial segment (not necessarily proper) of $d$.
220:
221: An infinite set $B$ of finite subsets of $\bbN$ is a \emph{block} if
222: every infinite subset~$X$ of $\bigcup B:= \bigcup\setof{b}{b\in B}$
223: has an initial segment in~$B$;
224: that is, % ***
225: % ***
226: $X$ extends some element in $B$.
227: A block~$B$
228: % ***
229: is called a \emph{barrier} if no two
230: elements of~$B$ are comparable w.r.t.\ inclusion.
231:
232: A precedence relation $\vor$ on a barrier $B$ is defined as follows:
233: if $b_1$ and $b_2$ are elements of $B$, then we say that $b_1$
234: \emph{precedes}
235: $b_2$, written $b_1\vor b_2$, if there are $i_1<i_2<\dots<i_m$ such
236: that $b_1=\{i_1,i_2,\dots,i_k\}$ and $b_2=\{i_2,\dots,i_m\}$ for some
237: $k$, $1\le k<m$.
238: (In particular, $\{i\} \vor \{j\}$ holds for all $i\not=j$.)
239:
240: A function $f:B\to Q$ on a barrier $B$ is \emph{bad} if, whenever
241: $b_1,b_2\in B$ and $b_1\vor b_2$, $f(b_1)\nleq_Q f(b_2)$.
242: Otherwise we say that $f$ is good.
243: \end{definition}
244:
245: \begin{definition} (\cite{Rosenstein:1982}, 10.30)
246: We say that $Q$ is a \emph{better-quasi-ordering}, denoted
247: \emph{bqo}, if every $f:B\to Q$ is good, for every barrier $B$ of
248: finite subsets of $\bbN$.
249: % ***
250: % ***
251: % ***
252: \end{definition}
253:
254: \begin{remark} Every bqo is a wqo.
255: \end{remark}
256: \begin{proof}
257: Use the % ***
258: barrier $B = \{\{n\}: n\in \bbN\}$.
259: \end{proof}
260: \begin{theorem}\label{bqoomega} {\normalfont (\cite{Rosenstein:1982}, 10.38)}
261: If $Q$ is a bqo, then $Q^{<\omega}$ and $Q^\omega$ are bqo's.
262: \end{theorem}
263:
264: \begin{theorem}\label{rosenstein:10.40}
265: {\normalfont (\cite{Rosenstein:1982}, 10.40)}
266: Let $B$ be a barrier and suppose that $B=B_1\cup B_2$ is a partition
267: of~$B$. Then there is a sub-barrier $C\subseteq B$ such that
268: $C\subseteq B_1$ or $C\subseteq B_2$.
269: \end{theorem}
270:
271: This ends the definitions and results we will need from
272: \cite{Rosenstein:1982}.
273:
274: \begin{definition}
275: A \emph{countable closed linear ordering}, denoted \emph{\cclo{}}, is
276: a countable closed subset of $\bbR$.
277:
278: A \emph{strictly monotone continuous embedding} $h$
279: (denoted \emph{\smc embedding}) from a \cclo $Q_1$ to a \cclo $Q_2$
280: is an embedding $h: Q_1\to Q_2$ which is continuous on $Q_1$, i.e.\
281: whenever $(p_n)_{n\in\bbN}$ is a sequence in $Q_1$ converging to an
282: element $p$ in $Q_1$, then $(h(p_n))_{n\in\bbN}$ is a sequence in $Q_2$
283: converging to an element $h(p)$ in $Q_2$,
284: and strictly monotone on $Q_1$, i.e.\ whenever $p,q\in Q_1$ with
285: $p\mathrel{<_{Q_1}}q$ then $h(p)\mathrel{<_{Q_2}}h(q)$.
286: (Here, ``convergence'' is always understood as convergence in
287: the usual topology of $\bbR$.)
288: \end{definition}
289:
290: \begin{definition}[labeled \cclo]
291: In addition to \cclo, we will also have to consider the following
292: notion: Fix a quasi-order $Q$ (usually a bqo, often a
293: finite set or an ordinal). A \emph{\qcclo} is a function $A$ whose domain
294: $\dom{A}$ is a \cclo\ and whose range is contained in $Q$.
295:
296: We write $A \contemb B$ ($A$ is $Q$-\smc embeddable into $B$, or shortly
297: $A$ is embeddable into $B$) iff there is a \smc embedding
298: $h$ from $\dom{A}$ to $\dom{B}$ with the property
299: $A(a) \le_Q B(h(a))$ for all $a\in\dom{A}$.
300: \end{definition}
301:
302: % ***
303: % ***
304: % ***
305: % ***
306:
307: If $Q$ is a singleton, then $A\contemb B$ reduces just to a
308: \smc embedding from $\dom{A}$ to $\dom{B}$.
309: If $Q = \{p,q\}$ is an antichain, or satisfies $p<q$,
310: and $A(0)=A(1)=q=B(0)=B(1)$, $B(b)=p$ for all $b\not=0,1$, then
311: $A\contemb B$ means that there is a \smc embedding
312: from $\dom{A}$ to $\dom{B}$ which moreover preserves $0$ and $1$.
313: Such embeddings will play an important r\^ole when we investigate Gödel sets
314: and the number of Gödel logics.
315:
316:
317:
318: % ***
319: \section{$Q$-labeled countable closed linear orderings}
320:
321:
322:
323: Let us fix some bqo $(Q,\le)$ for defining \qcclos.
324:
325: \begin{notation}
326: We will use the following notation throughout the paper:
327: \[ \cLpsum \]
328: or
329: \[ \cLpsym \]
330: When we write this term the following conditions are imposed:
331: \begin{itemize}
332: \item $p$ is an element of $Q$.
333: \item All the $L_i$ and $"iL$ are \qcclos.
334: \item Either all $L_i$ are empty, or none of them are empty.
335: Similarly, either all $"iL$ are empty, or none of them are.
336: We do not allow all $L_i$ {\em and} all $"iL$ to be empty.
337: \item $\dom L_i<\dom L_{i+1} < \dom "{i+1}L<\dom "iL$ for all $i$,
338: where we write $A < B $ for ``$A=\emptyset \vee B=\emptyset \vee \sup A < \inf B$''.
339: % ***
340: % ***
341: In particular, between the domains of any two of them (in the non-empty case)
342: we can find an open interval.
343: \item $\lim_{n\to\infty} a_n = \lim_{n\to\infty} "na$,
344: whenever $a_n\in \dom L_n$ and $"na\in\dom "nL$.
345: \end{itemize}
346: % ***
347: % ***
348: % ***
349: % ***
350: % ***
351:
352: The {\em meaning} of such a term is the $Q$-cclo $L$ whose domain is the
353: set $\bigcup_i L_i \cup \{x\} \cup \bigcup_i "iL$ (where
354: $x= \lim_{n\to\infty} a_n $ and/or $x = \lim_{n\to\infty} "na$ for any/all
355: sequences satisfying $a_n\in \dom L_n$ and $"na\in\dom "nL$), and
356: the function
357: $L$ extends all functions $L_i$ and $"iL$, and $L(x) = p$.
358:
359:
360: A ``finite sum'' $$L = L_1 + \cdots + L_n$$ is defined naturally: we allow
361: this expression only when all $L_i$ are nonempty and satisfy $\max\dom L_i<
362: \min \dom L_{i+1}$. In this case we let
363: $\dom( L) = \bigcup_i\dom( L_i)$ and $L = \bigcup_i L_i$.
364: \end{notation}
365:
366: We will consider two slightly different operations ($S$, $S'$ below)
367: to build complicated \qcclos from simpler ones.
368: These two operations naturally correspond to two notions $\rk$, $\rk'$ of rank;
369: a third rank that we occasionally use is the classical Cantor-Bendixson rank
370: $\cbrk$ of a \cclo.
371:
372:
373: \begin{definition}
374: Let $\OO$ be a class of \qcclos. We let $S(\OO)$
375: (`sums from $\OO\/$\/') be the set of all \qcclos which are
376: finite sums of \qcclos from $\OO$, plus the set of all \qcclos
377: of the form
378: \[ \cLpsum \]
379: where $p\in Q$ and all $L_n$ and all $"nL$ are in $\OO$.
380:
381: We let $S'(\OO)$ (`unbounded sums from $\OO$') be the set
382: of all \qcclos of the form
383: \[ \cLpsum \]
384: where $p\in Q$ and all $L_n$ and all $"nL$ are in $\OO$, and
385: \[ \forall n \, \exists k>n \ L_n\contemb L_k
386: \mbox{ \ and \ }
387: \forall n \, \exists k>n \ "nL\contemb "kL. \]
388: \end{definition}
389:
390: As a consequence of the above definition we obtain for unbounded sums,
391: that for all~$n$ there are infinitely many $k>n$ such that $L_n\contemb L_k$
392: and $"nL\contemb "kL$.
393:
394:
395: % ***
396: % ***
397: % ***
398: % ***
399: % ***
400:
401: % ***
402: % ***
403: % ***
404:
405: % ***
406: % ***
407: % ***
408: % ***
409:
410: % ***
411: % ***
412: % ***
413: % ***
414:
415: \begin{definition}\label{def:abcd} \
416: \begin{enumerate}
417: \itm a
418: Let $\sC$ be the set of all
419: % ***
420: % ***
421: \qcclos.
422:
423: \itm b
424: Let $\sC_0= \sC_0' $ be the set of all \qcclos with singleton or empty
425: domain.
426: For any $\alpha \le \omega_1$ let
427: \[ \sC_{\alpha+1} = S(\sC_\alpha) \cup \sC_\alpha \qquad
428: \sC'_{\alpha+1} = S'(\sC'_\alpha) \cup \sC'_\alpha \]
429: and for limit ordinals $\delta>0 $ let
430: $\sC_\delta = \bigcup_{\alpha<\delta} \sC_\alpha$,
431: $\sC'_\delta = \bigcup_{\alpha<\delta} \sC'_\alpha$.
432:
433:
434: \itm c
435: For any % ***
436: $L\in\bigcup_\al\sC_\al$
437: we define the \emph{rank} of~$L$ ($\rk(L)$) as
438: the first ordinal~$\al$ at which $L$ occurs in $\sC_{\al+1}$.
439: Similar, we define $\rk'(L)$ for $L\in\bigcup_\al\sC'_\al$ as
440: the first ordinal~$\al$ at which $L$ occurs in $\sC'_{\al+1}$.
441: % ***
442:
443: \itm d
444: The set of all \qcclos whose domains are suborderings of $\dom L$
445: is denoted with $\sC(L)$.
446: \end{enumerate}
447: \end{definition}
448:
449: It is clear that $\sC'_{\omega_1} \subseteq \sC_{\omega_1} \subseteq \sC$.
450: We will show that $\sC = \sC_{\omega_1}$, and that every order in $\sC$ can
451: be written as a finite sum of orders from $\sC'_{\omega_1}$.
452:
453: \begin{lemma}
454: % ***
455: $ \sC = \sC_{\omega_1}$.
456: That is, for every \qcclo\ $L$ there is a countable
457: ordinal $\alpha$ such that $L\in \sC_{\alpha}$.
458: % ***
459: \end{lemma}
460:
461: \begin{proof}
462: We use the Cantor-Bendixson decomposition, more precisely we
463: use induction on the Cantor-Bendixson rank of $V=\dom L$.
464:
465: For every scattered closed set $V$
466: there is an ordinal $\cbrk(V)$ (the Cantor-Bendixson rank
467: of $V$) and a decomposition
468: \[ V = \bigcup _{\alpha\le \cbrk(V)} \CB_\alpha(V),\]
469: where $\CB_0(V) $ is the set of isolated points of $V$, and
470: more generally each set $\CB_\alpha(V)$ is the set of isolated points
471: of $V\setminus \bigcup_{\beta < \alpha} \CB_\beta(V)$, and
472: $\CB_{\cbrk(V)}(V)$ is finite and nonempty.
473:
474: Assume for the moment that $\CB_{\cbrk(V)}(V)$
475: is a singleton $\{x^*\}$.
476: If $\cbrk(V) = 0$, then % ***
477: $L\in \sC_0$.
478: If $\cbrk(V) > 0$, fix an increasing sequence $\<x_n\>$ and
479: a decreasing sequence $\<"nx\>$, both with limit $x^*$,
480: and $x_n, "nx\notin V$. Now it is easy to see that for
481: all $\beta<\cbrk(V)$
482: \[ \CB_\beta( V \cap [x_n, x_{n+1}] ) =
483: \CB_\beta( V) \cap [x_n, x_{n+1}],\]
484: so $\cbrk(V\cap [x_n,x_{n+1}]) < \cbrk(V)$, similarly for
485: $V\cap ["nx,"{n+1}x]$. Now we can
486: use the induction hypothesis.
487:
488: If $\CB_{\cbrk(V)}(V)$ is not a singleton then we can write $V = V_1 +
489: \cdots + V_n$ for some finite $n$, with each $\CB_{\cbrk(V)}(V_k)$ a singleton,
490: then proceed as above.
491: % ***
492: % ***
493: % ***
494: \end{proof}
495:
496: % ***
497: % ***
498: % ***
499: % ***
500: % ***
501: % ***
502: % ***
503: % ***
504: % ***
505: % ***
506: % ***
507: % ***
508: % ***
509: % ***
510:
511: % ***
512: % ***
513: % ***
514:
515: \begin{definition}
516: The set $\sC':= \sC'_{\omega_1}$ is the smallest family of \qcclos
517: which contains all the singletons and is closed under unbounded sums $S'$.
518: % ***
519: % ***
520: \end{definition}
521:
522: % ***
523:
524: \begin{theorem}\label{thm:finite-ha}
525: Let $L$ be a \qcclo and assume that $(\sC(L), \contemb)$ is a wqo. (See
526: Definition~\ref{def:abcd}(d).)
527: Then $L$ is a finite sum of % ***
528: elements in $\sC'$.
529: \end{theorem}
530:
531: \begin{proof}
532: Induction on $\rk(L)$: Assume that
533: \[ L = \cLpsum \]
534: where all the $L_i$ and $"iL$ are in $\sC'$.
535: Suppose that, for all but a finite number of $L_i$, each
536: $L_i$ is embeddable in infinitely many $L_j$, and for all but a
537: finite number of $"iL$, each $"iL$ is embeddable in infinitely
538: many $"jL$. Then $L$ can be written as
539: \[ L_0 + \dots L_{k-1} + (L_{k+0} + L_{k+1}
540: +\dots+p+\dots+"{l+1}L+"{l+0}L) + "{l-1}L+ \dots +"0L \] where
541: each summand is in $\sC'$.
542:
543: Otherwise there are either infinitely many $L_i$ or $"iL$ each
544: embeddable in only finitely many $L_j$ or $"jL$, resp. We then
545: find a either a subsequence $\<L_{h(n)}\suchthat n<\omega\>$ or
546: $\<"{h(n)}L\suchthat n<\omega\>$ no entry of which can be embedded
547: in any subsequent entry. This bad sequence of suborderings of $L$
548: contradicts the hypothesis of the theorem.
549: \end{proof}
550:
551: \begin{theorem}\label{thm:bqo-wqo}
552: If $(\H,\contemb)$ is a bqo, then $(\sC,\contemb)$ is a wqo.
553: \end{theorem}
554:
555: \begin{proof}
556: We will show for all countable $L$ by induction on the
557: rank~$\rk(L)$ (that is the rank w.r.t.\ the classes in $\sC$ as defined
558: in Definition \ref{def:abcd} (c)),
559: that the collection $\sC(L)$ of \qcclos whose domains are suborderings
560: of $\dom L$ is a wqo w.r.t \smc embeddability.
561:
562: First we show that, if $K$ is in $\sC(L)$, then $K$ can be
563: written as $K=\csymp J$, where all the $J_i$ and $"iJ$ are
564: in $\sC'$. To prove this, observe that $L$ can be written
565: as $\cLpsym$ where the ranks of the $L_i$ and $"iL$ are strictly less
566: than the rank of $L$. Using the induction hypothesis, we see that
567: $(\sC(L_i),\contemb)$ and $(\sC("iL),\contemb)$ are wqo. If $\dom K$ is a
568: sub ordering of $\dom L$, it can be written as $K=\csym Kq$
569: % ***
570: % ***
571: % ***
572: with $K_i\in\sC(L_i)$ and $"iK\in\sC("iL)$.
573: Thus, by Theorem~\ref{thm:finite-ha}, each $K_i$ and $"iK$
574: can be written as finite sum of elements $J_j$ and
575: $"jJ$ in $\sC'$, and $K$ as $\csum Jq$.
576:
577: % ***
578: % ***
579:
580: Now consider a sequence $\<K^l\suchthat l<\omega\>$, where each $K^l$
581: is a \qcclo and subordering of $L$. We will repeatedly thin out
582: this sequence, eventually arriving at a sequence which is good, which
583: will show that our original sequence was good.
584: After having thinned
585: out the sequence $\<K^l\suchthat l<\omega\>$ to a sequence
586: $\<K^{l_i}\suchthat i<\omega\>$, we will (for notational simplicity)
587: relabel our index set so that we will also call the new sequence
588: $\<K^l\suchthat l<\omega\>$.
589:
590: Each $K^l$ can be written as
591: \[ K^l = \csum {J^l}{p^l} \]
592: where each of the summands is in $\sC'$.
593: Using Lemma~\ref{rosenstein:10.17} % ***
594: we thin out our sequence to a new sequence
595: (again called $\<K^l\suchthat l<\omega\>$) such that
596: $p^j \mathrel{\le_Q} p^k$ for all $j<k$.
597:
598: By Theorem~\ref{bqoomega} we know that $\H^\omega$ is a bqo, in
599: particular a wqo.
600: % ***
601: % ***
602: % ***
603: Consider the $\omega$-tuples
604: ${\cC}^l = \< J_0^{l}, J_1^{l}, \dots \>\in \H^\omega$.
605: Using Lemma~\ref{rosenstein:10.17} % ***
606: we can thin out our sequence to obtain a sequence satisfying
607: ${\cC}^{j} \contemb {\cC}^{k}$ for any $j<k$.
608:
609: We now apply the fact that $\H^\omega$ is wqo to the sequence
610: ${}^n\cC = \< "0J^n, "1J^n, \dots \>\in \H^ \omega$ to see
611: that without loss of generality we may also assume
612: ${}^j{\cC} \contemb {}^k{\cC} $ for all $j<k$.
613:
614: Now pick any $n<m$, and consider the sums
615: \[ K^n = \csum {J^n}{p^n} \]
616: and
617: \[ K^m = \csum {J^m}{p^m} . \]
618: Write $x^n$ and $x^m$ for the central points of $K^n$ and $K^m$, respectively
619: (i.e., $x^n = \sup_n \bigcup_i \dom J^n_i = \inf_n \bigcup_i \dom "i{J^n}$, etc.)
620:
621: We know $p^n\mathrel{\le_Q} p^m$, $\cC^n \contemb \cC^m$,
622: $"n\cC \contemb "m\cC$.
623:
624:
625: Thus, there are strictly increasing functions $g$ and $h$ from
626: $\bbN$ to $\bbN$,
627: such that for all $i$,
628: $J_i^n \contemb J_{g(i)}^m$ and $"i{J^n} \contemb "{h(i)}{J^m}$. Let $\alpha_i$ and $"i\alpha$ be functions that witness this, i.e.,
629: let $\alpha_i$ be a function mapping $\dom J_i^n$ to $\dom J_{g(i)}^m$
630: with $J_i^n(x) \le J_{g(i)}^m(\alpha_i(x))$ for all $x\in \dom J_i^n$,
631: and similarly $"iJ^n(x) \le "{g(i)}J^m("i\alpha(x))$ for all $x\in \dom "iJ^n$,
632:
633: Now define $\alpha:\dom K^n \to \dom K^m$ naturally: $\alpha$ extends all
634: functions $\alpha_i$ and $"i\alpha$, and $\alpha(x^n) = x^m$. Clearly
635: $\alpha$ witnesses $K^n\contemb K^m$.
636:
637: \medskip
638:
639: Finally, if $\setof{K_i}{i<\omega}$ is an arbitrary sequence,
640: where each $K_i$ is in $\sC$, then each $K_i\in\cC(K)$ where
641: $K= \csum {K}{p}$ for arbitrary $p$ and empty $"iK$. According to
642: the above remarks, the sequence $\setof{K_i}{i<\omega}$ must be
643: good, so that $\cC$ is a wqo.
644: \end{proof}
645:
646: % ***
647: % ***
648: % ***
649:
650:
651:
652: % ***
653: % ***
654: % ***
655: % ***
656: % ***
657: % ***
658: % ***
659:
660:
661: \begin{theorem}\label{thm:ha-bqo}
662: $(\H,\contemb)$ is a bqo.
663: \end{theorem}
664:
665: We prove the Theorem by a series of lemmas.
666: The first lemma holds for general quasi-orderings which are equipped
667: with a rank function, it forms the main technical part of the proof
668: of Theorem~\ref{thm:ha-bqo}.
669:
670: % ***
671: % ***
672: % ***
673: % ***
674: % ***
675: % ***
676: % ***
677: % ***
678: % ***
679: % ***
680: % ***
681: % ***
682: % ***
683: % ***
684: % ***
685: % ***
686:
687: Let $(Q,\le)$ be a quasi-ordering,
688: and let $\rho$ be a rank function from $Q$ into the ordinals
689: (i.e., a function satisfying $\rho(x)\le \rho(y)$ whenever
690: $x\le y$).
691: Let $\cF$ denote the set of all functions $g:B\to Q$
692: where $B$ is a barrier of finite subsets of $\bbN$. (See
693: Definition~\ref{def:barrier}.)
694:
695:
696: We say that $C$ \emph{is an extended sub-barrier of} $B$
697: if $\bigcup C\subseteq\bigcup B$ and
698: if every element of $C$ is an extension (not necessarily proper)
699: of an element of $B$.
700: $C$ is called a \emph{proper} extended sub-barrier of $B$
701: if $C$ {is an extended sub-barrier of} $B$ and
702: at least one element of $C$ properly extends some element of $B$.
703: For two functions $g:B\to Q$ and $h:C\to Q$ in $\cF$
704: we say that $h$ \emph{is shorter than} $g$ if
705: $C$ is a proper extended sub-barrier of $B$ and
706: if $g$ and $h$ coincide on $B\cap C$, and
707: if, whenever $c\in C$ properly extends $b\in B$,
708: $h(c)\le g(b)$ and $h(c)$ has lower rank than $g(b)$.
709: The following Lemma can be extracted from the proof of Theorem 10.47
710: in Rosenstein \cite{Rosenstein:1982}.
711: Recall from Definition~\ref{def:barrier} that a function $f: B\to Q$
712: is called \emph{bad}
713: if, whenever $b_1,b_2\in B$ and $b_1\vor b_2$,
714: $f(b_1)\nleq f(b_2)$.
715:
716: \begin{lemma}\label{lem:minimal-bad}
717: If $\cF$ contains some bad function, than it contains
718: some minimal bad function,
719: i.e.\ one which is minimal w.r.t.\ `shorter'.
720: \end{lemma}
721:
722: \begin{proof}
723: Assume for the sake of contradiction that
724: $\cF$ contains some bad function,
725: but for any bad $g\in\cF$ there is some bad $h\in\cF$
726: which is shorter than $g$.
727:
728: Let $g:B\to Q$ be bad.
729: With $k(g)$ we denote the minimal $k$ such that there is a shorter
730: $h:C\to Q$ and a $b\in B$ which is properly extended by some element in $C$
731: with $\max b\le k$.
732: Fix some witnesses $C$, $h$ and $b$ for $k(g)$.
733: We define $D$ as the set of all $d\in B$ which do not have extensions
734: in $C$ and which fulfill $d\subset[0,k(g)]\cup\bigcup C$.
735: Obviously $C\cap D=\emptyset$.
736:
737: % ***
738: % ***
739:
740: First observe that for $d\in D$ we have $d\not\subset\bigcup C$:
741: Assume for the sake of contradiction that $d\subset\bigcup C$.
742: Let $X$ be the infinite set $d\cup\big(\bigcup C\cap[\max d,\infty)\big)$,
743: then $X\subseteq\bigcup C$, hence there is some $c\in C$ which is
744: extended by $X$.
745: Since $X$ is also an extension of $d$, $c$ extends $d$ or vice versa.
746: As $c$ extends some element in $B$ and $d\in B$,
747: we have that $c$ cannot be properly extended by $d$ because $B$ is a barrier.
748: But by definition of $D$ we also have that $c$ does not extend $d$.
749: Contradiction.
750:
751: % ***
752:
753: Now, $B^*:=C\cup D$ is a barrier and $g^*:B^*\to Q$ defined by
754: $g^*(c)=h(c)$ for $c\in C$ and $g^*(d)=g(d)$ for $d\in D$
755: is bad and shorter than $g$.
756:
757: We verify these claims:
758: First note that $\bigcup B^* \subseteq \bigcup C\cup [0,k(g)]$.
759: For $B^*$ to be a block let $X\subseteq\bigcup B^*$ be infinite.
760: There is some $d\in B$ which is extended by $X$ (as $B$ is a
761: block, and $\bigcup B^* \subseteq \bigcup B$).
762: If $d$ is not already in $B^*$ then,
763: by definition of $D$, $d$ has some extension
764: in $C$ which must be proper as $d\notin C$.
765: Thus $d\subset\bigcup C$ and $\max d\ge k(g)$,
766: hence $X\subseteq\bigcup C$ % ***
767: as $\bigcup B^*\subseteq\bigcup C\cup [0,k(g)]$.
768: But then there is some $c\in C$ which is extended by $X$.
769: Altogether this shows that $B^*$ is a block.
770:
771: Assume that $B^*$ is not a barrier, then there must be $c\in C$ and
772: $d\in D$ which are comparable.
773: As $c$ is the extension of some element in $B$ and $d\in B$,
774: we have $c\nsubseteq d$ because $B$ is a barrier.
775: But $d\in D$ implies $d\not\subset\bigcup C$, hence $d\nsubseteq c$.
776: Contradiction.
777: Hence $B^*$ must be a barrier.
778:
779: Obviously, $g^*$ is shorter than $g$, as $h$ already has been shorter
780: than $g$.
781: To verify that $g^*$ is bad we assume for the sake of contradiction
782: that $c_1\vor c_2$ and $g^*(c_1)\le g^*(c_2)$.
783: As $h$ is bad, $c_1$ and $c_2$ cannot be in $C$ at the same time.
784: Similar with $g$, they cannot be in $D$ at the same time.
785: If $c_1\in C$ and $c_2\in D$,
786: then $c_2\not\subset\bigcup C$
787: which together with $c_1\vor c_2$, $c_1\in C$ and the definition of $D$
788: shows $\max c_1<k(g)$, hence $c_1\in B$.
789: Hence $g(c_1)=h(c_1)=g^*(c_1)\le g^*(c_2)=g(c_2)$
790: contradicting that $g$ is bad.
791: Therefore, $c_1\in D$ and $c_2\in C$.
792: There is some $b_2\in B$ such that $b_2$ is extended by $c_2$.
793: If $c_1\nvor b_2$ then $b_2\subsetneq c_1$
794: which contradicts that $B$ is a barrier.
795: Hence we have $c_1\vor b_2$.
796: But then $g(c_1)=g^*(c_1)\le g^*(c_2)=h(c_2)\le g(b_2)$
797: contradicts that $g$ is bad.
798: Altogether this shows that $g^*$ is bad.
799:
800: We now define a sequence of bad elements $f_n\in\cF$ in the following way.
801: Let $f_0:B_0\to Q$ be some bad element in $\cF$, and define recursively
802: $B_{n+1}:=B_n^*$ and $f_{n+1}:=f_n^*$.
803: Let $k_n:=k(f_n)$.
804: Then $k_{n+1}\ge k_n$ because `shorter' is transitive and $k_n$ is chosen
805: minimal.
806: Furthermore, $k_n=k_m$ for only finitely many $m$ since
807: $\setof{b\in B_n}{\max b=k_n}$ is finite.
808: Hence $\<k_n \suchthat n<\om\>$ is a non-decreasing unbounded sequence of
809: natural numbers.
810: Also observe that if $b\in B_n$ and $\max b<k_n$ and $n<m$ then $b\in B_m$,
811: and if $b\in B_m\cap B_n$ then $f_m(b)=f_n(b)$.
812:
813: Let $B:=\bigcup\setof{\bigcap\setof{B_n}{n\ge m}}{m<\om}$.
814: We show that $B$ is a barrier.
815: Let $M:=\bigcap\setof{\bigcup B_n}{n<\om}$.
816: $M$ is infinite because $k_n\in M$ for all $n$.
817: Let $X\subseteq M$ be infinite.
818: Then for all $n<\om$ we have $X\subseteq\bigcup B_n$, hence there is
819: some $b_n\in B_n$ which is extended by $X$.
820: If $b_{n+1}$ is a proper extension of $b_n$ then the rank of $f_{n+1}(b_{n+1})$
821: is strictly smaller than the rank of $f_n(b_n)$, hence, for some $m$,
822: $b_n=b_m$ for all $n\ge m$,
823: i.e.\ $b_m\in\bigcap\setof{B_n}{n\ge m}\subseteq B$.
824: In particular, $M\subseteq\bigcup B$ by taking $X:= M\cap[m,\infty)$
825: for $m\in M$.
826: If $k\in\bigcup B$, then there is some $b\in B$ with $k\in b$.
827: $b\in B$ implies that there is some $m$ with $b\in\bigcap_{n\ge m}B_n$.
828: Thus $k\in\bigcup B_n$ for all $n\ge m$.
829: Also
830: $k\in\bigcup B_m \subseteq \bigcup B_{m-1} \subseteq\dots\subseteq\bigcup B_0$,
831: hence $k\in M$.
832: This shows $\bigcup B\subseteq M$.
833: Thus $M=\bigcup B$ and $B$ is a block.
834: Let $b,c\in B$, then $b,c\in B_n$ for some $n$, hence they are not comparable
835: as $B_n$ is a barrier.
836: Altogether this shows that $B$ is a barrier.
837:
838: For $b\in B$ let $m_b := \min\setof{m}{b\in\bigcap\setof{B_n}{n\ge m}}$.
839: We define $f:B\to Q$ by $f(b):=f_{m_b}(b)$
840: and show that $f$ is minimal w.r.t.\ `shorter' and bad.
841: $f$ is shorter than $f_n$ for all $n$,
842: because `shorter' is transitive,
843: $B$ is an extended sub-barrier of $B_n$,
844: if $b\in B\cap B_n$ then $m_b\le n$ hence $f(b)=f_{m_b}(b)=f_n(b)$,
845: and if $c\in B$ properly extends $b\in B_n$, then
846: $m_c>n$ and $f(c)=f_{m_c}(c)\le f_n(b)$ and
847: $\rho(f(c))=\rho(f_{m_c}(c))<\rho(f_n(b))$.
848: $f$ is bad,
849: because if $b,c\in B$, and w.l.o.g.\ $m_b\le m_c$, then
850: $f(b)=f_{m_c}(b)$ and $f(c)=f_{m_c}(c)$ and $f_{m_c}$ is bad.
851: By our general assumption
852: there is some bad $f':B'\to Q$ which is shorter than $f$.
853: Then there are $b'\in B'$ and $b\in B$ such that $b'$ properly extends $b$.
854: Choose $n$ with $k_n>\max b'$.
855: Now $f'$ is shorter than $f_n$ because $f$ is shorter than $f_n$
856: and `shorter' is transitive.
857: But this contradicts the minimality of $k(f_n)$.
858: Hence our general assumption has been wrong, and the theorem is proved.
859: \end{proof}
860:
861:
862: Recall that the rank $\rk'(L)$ of $L\in\sC'$ is given
863: by the minimal $\al$ such that $L\in\sC'_{\al+1}$.
864: A \emph{$\sC'$-term} for $L\in\sC'$ with $\rk'(L)>0$ is a faithful witness
865: for $L\in\sC'$, i.e.\ a decomposition $L=\cLpsym$ with
866: all the $L_i$ and $\li iL$ in $\sC'$ and
867: $\rk'(L_i)<\rk'(L)$ and $\rk'(\li iL)<\rk'(L)$ for all $i$.
868:
869:
870:
871:
872:
873: \begin{lemma}\label{lem:charc-indec}
874: Let $L$ and $K$ be in $\sC'$, with
875: $L=\cLpsym$ and $K=\csym Kq$ being $\sC'$-terms of them.
876: If $p\le q$ and each $L_i$ is embeddable into some $K_j$ and
877: each $\li iL$ is embeddable into some $\li jK$, then $L\contemb K$.
878: \end{lemma}
879:
880: \begin{proof}
881: Let the assumptions of the lemma be fulfilled.
882: Then there are
883: $k_i,l_i\in\om$ such that $k_i<k_{i+1}$, $l_i<l_{i+1}$ and
884: $L_i\contemb K_{k_i}$ and $"iL\contemb "{l_i}K$
885: because $L,K$ are in $\sC'$.
886: Fix \smc embeddings $\si_i:\dom L_i\to \dom K_{k_i}$ and
887: $"i\si:\dom "iL\to \dom "{l_i}K$
888: witnessing $L_i\contemb K_{k_i}$ resp.\ $"iL\contemb "{l_i}K$,
889: and let $b := \lim_i(\sup \dom L_i)$ and $c := \lim_i(\sup \dom K_i)$.
890: We define a map $\si:\dom L\to \dom K$ by
891: \[
892: \si(a) :=
893: \begin{cases}
894: \si_i(a) & \text{if $a\in \dom L_i$}\\
895: "i\si(a) & \text{if $a\in \dom "iL$}\\
896: c & \text{if $a=b$}
897: \end{cases}
898: \]
899: % ***
900: % ***
901: % ***
902: % ***
903: % ***
904: % ***
905: Then $\si$ is a \smc embedding witnessing $L\contemb K$.
906: % ***
907: % ***
908: % ***
909: % ***
910: % ***
911: % ***
912: % ***
913: % ***
914: % ***
915: % ***
916: % ***
917: % ***
918: % ***
919: % ***
920: % ***
921: % ***
922: % ***
923: % ***
924: % ***
925: % ***
926: \end{proof}
927:
928:
929: \begin{proof}[Proof of Theorem \ref{thm:ha-bqo}]
930: Assume for the sake of contradiction that $(\H,\contemb)$ is not a bqo.
931: By applying Lemma~\ref{lem:minimal-bad} we can find some
932: $f:B\to\sC'$ which is bad and minimal w.r.t.\ `shorter'.
933: For each $b\in B$ we fix some $\sC'$-term $f(b)=\cLpsym$.
934:
935: For any $a,b\in B$ with $a\vor b$ we have that
936: $f(a)=\cLpsym\ \ncontemb\ \csym Kq=f(b)$,
937: hence, by applying Lemma~\ref{lem:charc-indec}, we see that at least one
938: of the following holds:
939: \begin{enumerate}
940: \itm i
941: $p\nleq q$
942: \itm ii for some $i$: $L_i\ncontemb K_j$ for all $j$,
943: \itm iii for some $i$: $"iL\ncontemb "jK$ for all $j$.
944: \end{enumerate}
945: By applying Theorem~\ref{rosenstein:10.40}
946: % ***
947: we can find
948: a sub-barrier $B'$ such that one the cases (i), (ii), (iii)
949: always happens on $B'$.
950: In the first case this would form a bad sequence in $(Q,\le)$ which would
951: contradict that $(Q,\le)$ is a wqo.
952: Thus, w.l.o.g.\ we may assume that for all $a,b\in B'$ with $a\vor b$
953: there is some $i$ such that $L_i\ncontemb K_j$ for all $j$.
954: Let $B'(2):=\setof{b_1\cup b_2}{b_1,b_2\in B'\text{ and }b_1\vor b_2}$,
955: then $B'(2)$ is an extended sub-barrier of $B$.
956: Define $g:B'(2)\to\sC'$ by letting $g(b_1\cup b_2)$ be the first $L_i$
957: in $f(b_1)=\cLpsym$ which is not embeddable into
958: any $K_j$ from $f(b_2)=\csym Kq$.
959: Then obviously $g$ is shorter than $f$.
960: But also $g$ is bad, because if $b_1\cup b_2\vor b_3\cup b_4$ then $b_2=b_3$
961: and hence $g(b_1\cup b_2)\ncontemb g(b_3\cup b_4)$.
962: This contradicts the minimality of~$f$.
963: \end{proof}
964:
965:
966: Theorems \ref{thm:bqo-wqo} and \ref{thm:ha-bqo} together yield the
967: following result:
968:
969: \begin{corollary} \label{cor:sc-wqo}
970: $(\sC,\contemb)$ is a wqo.
971: \qed
972: \end{corollary}
973:
974: For the next corollary, we need the following two well-known properties of
975: wqo's:
976:
977: \begin{lemma}\label{omega1.wqo}
978: Let $(Q, {\le})$ be a wqo
979: with uncountable many $\equiv$-equivalence classes.
980: % ***
981: % ***
982: % ***
983: Then there exists a 1-1 monotone map $f:\omega_1\to Q$.
984: \end{lemma}
985: \begin{proof}[Proof sketch]
986: W.l.o.g.\ let each equivalence class of $Q/\equiv$ consist of one element.
987: If each uncountable subset $Q'\subseteq Q$ contains some
988: element $q$ such that also $\setof{r\in Q'}{q \nleq r}$ is uncountable,
989: then we can find sequence
990: \[Q = Q_0 \supseteq Q_1\supseteq Q_2 \supseteq\cdots \]
991: of uncountable sets with
992: elements $q_n\in Q_n$, $Q_{n+1}:= \setof{r\in Q_n}{q_n \nleq r}$. But then
993: $q_n\nleq q_k$ for all $n<k$, contradicting the assumption that $Q$ is
994: wqo.
995:
996:
997: So there must be an uncountable subset $Q'\subseteq Q$ such that
998: for any $q\in Q'$, the set $\setof{r\in Q'}{q \nleq r}$ is countable.
999: But then we can easily find a copy of $\omega_1$ in $Q'$.
1000: % ***
1001:
1002:
1003: Alternatively, start with any 1-1 sequence $\<q_i:i\in \omega_1\>$
1004: in $Q$; define
1005: a coloring $f:[\omega_1]^2\to 2$ by $f(i<j) = 0$ iff $q_i < q_j$, and
1006: apply the Erd\hungarian os-Dushnik-Miller theorem $\omega_1\to (\omega_1,\omega)$. (See \cite[Theorem 11.1]{EHMR}.)
1007:
1008:
1009: % ***
1010:
1011: % ***
1012: % ***
1013: % ***
1014: % ***
1015: % ***
1016: % ***
1017: % ***
1018: % ***
1019: % ***
1020: % ***
1021: % ***
1022: % ***
1023: % ***
1024: % ***
1025: % ***
1026: % ***
1027:
1028: % ***
1029: % ***
1030: % ***
1031: % ***
1032: % ***
1033: % ***
1034: % ***
1035: % ***
1036: % ***
1037: % ***
1038: % ***
1039: % ***
1040: % ***
1041: % ***
1042: % ***
1043: % ***
1044: % ***
1045: \end{proof}
1046:
1047:
1048:
1049: \begin{lemma}\label{lemma:Qomega-countable}
1050: Let $Q$ be a countable bqo (or at least assume that $Q$
1051: has only countably many $\equiv$-equivalence classes).
1052:
1053: Then $Q^\omega$ (quasiordered as in Definition~\ref{def:seq-order})
1054: has only countably many equivalence classes.
1055: \end{lemma}
1056:
1057: \begin{proof} Part I:
1058: We first consider the set $Q^*$ of all sequences
1059: $\vecq = \<q_0,q_1,\ldots\>\in Q^\omega$ satisfying
1060: \[ \forall k\,\exists n>k : q_k \le q_n.\]
1061: and show that this set is countable (modulo $\equiv$).
1062:
1063: By Theorem~\ref{bqoomega},
1064: $Q^\omega$ and hence also $Q^*$ is a wqo.
1065: Assume that $Q^*$ has uncountably many
1066: $\equiv$-classes, then by Lemma~\ref{omega1.wqo} we can find a sequence
1067: $\seqof{\vecq^i}{i \in \omega_1}$,
1068: \[ \vecq^i = \<q^i_0,q^i_1,\ldots\>\in Q^* \]
1069: with $i< j \Rightarrow \vecq^i \le \vecq^j$,
1070: $\vecq^j \nleq \vecq^i$.
1071:
1072:
1073: Let $\al < \omega_1$ be so large such that every element of $Q$ which
1074: appears somewhere as $q^j_n$ is $\le$ to some $q^{j'}_{n'}$ with $j'<\al$.
1075:
1076: We claim that $\vecq^{\alpha+1} \le \vecq^\al$, which will
1077: be the desired contradiction.
1078:
1079: By definition of $\alpha$, $\forall n \, \exists i < \al\, \exists n':
1080: q^{\al+1}_n \le q^i_{n'}$. So for every $n$ there is $n''$ with
1081: $q^{\al+1}_n \le q^\al_{n''}$.
1082: Using $\vecq^\al\in Q^*$, we can find a sequence $k_0 < k_1 < \cdots $
1083: with $q^{\al+1}_n \le q^\al_{k_n}$ for all $n$, which means
1084: $\vecq^{\alpha+1} \le \vecq^\al$.
1085: \medskip
1086:
1087: \noindent Part II: For any sequence
1088: $\vecq = \<q_0,q_1,\ldots\>\in Q^\omega$
1089: we can find a natural number $N=N_{\vecq}$ such that
1090: $\forall k\ge N \,\exists n>k : q_k \le q_n$, otherwise we get
1091: (as in the proof of Theorem~\ref{thm:finite-ha}) a contradiction
1092: to our assumption that $Q$ is a wqo.
1093:
1094: Now assume that $Q^\omega / {\equiv}$ is uncountable, then we can
1095: find a natural number $N^*$ and an
1096: uncountable family $\seqof{\vecq^i}{i < \omega_1}$ of pairwise
1097: nonequivalent sequences in $Q^\omega$ such that for all $i$,
1098: $N_{\vecq^i} = N^*$. Moreover, we may assume that
1099: all initial segments $\<q^i_0, \ldots, q^i_{N^*}\>$ are equal to
1100: each other. Consider the tails
1101: $\<q^i_{N^*+1}, q^i_{N^*+2} , \ldots\> \in Q^\omega$. By definition
1102: of $N_{\vecq^i}$, these tails are all in $Q^*$, defined in part I, above.
1103:
1104: Hence we can find $i\not= j$ such that
1105: \[ \<q^i_{N^*+1}, q^i_{N^*+2} , \ldots\> \equiv
1106: \<q^j_{N^*+1}, q^j_{N^*+2} , \ldots\>.\]
1107: But then also $\vecq^i \equiv \vecq^j$.
1108: \end{proof}
1109:
1110:
1111:
1112: \begin{corollary}\label{cor:S-countable}
1113: Assume that our basic wqo $Q$ is countable.
1114: Then, for any set $\OO \subseteq \sC$ with $\OO/{\equiv}$ countable
1115: we also have that $S'(\OO)/{\equiv}$ and even
1116: $S(\OO)/{\equiv}$ are countable.
1117: \end{corollary}
1118:
1119: \begin{proof}
1120:
1121: If $\<L_0,L_1,\ldots\> \contemb \<L'_0,L'_1,\ldots\>$
1122: and
1123: $\<"0L,"1L,\ldots\> \contemb \<"0L',"1L',\ldots\>$ and $p \le p'$, then
1124: also
1125: $$ L_0 + L_1 + \cdots + p + \cdots "1L + "0L
1126: \ \contemb\
1127: L'_0 + L'_1 + \cdots + p + \cdots "1L' + "0L' . $$
1128:
1129: So the corollary follows from Lemma~\ref{lemma:Qomega-countable}.
1130: \end{proof}
1131:
1132:
1133:
1134: \begin{corollary}
1135: Assume that our basic wqo $Q$ is countable.
1136: W.r.t.\ continuous bi-embeddability
1137: there are exactly $\omega_1$ many equivalence classes of \qcclos.
1138: \end{corollary}
1139: \begin{proof}
1140: It is easy to see (using the countable ordinals) that the number
1141: of equivalence classes is at least $\aleph_1$.
1142:
1143: % ***
1144: % ***
1145: % ***
1146: % ***
1147: % ***
1148: % ***
1149:
1150: On the other hand, Corollary~\ref{cor:S-countable} implies that
1151: $|\sC_{\alpha }|\le \aleph_0$ for all $\alpha <\omega_1$, so
1152: $|\sC_{\omega_1}|\le \aleph_1$.
1153: \end{proof}
1154:
1155:
1156: \section{Gödel logics}\label{sec:goedel}
1157:
1158: % ***
1159: % ***
1160:
1161: Gödel logics are one of the oldest and most interesting families of
1162: many-valued logics. Propositional finite-valued Gödel logics were
1163: introduced by Gödel in \cite{goedel33} to show that intuitionistic logic
1164: does not have a characteristic finite matrix. They
1165: provide the first examples of intermediate logics
1166: (intermediate, that is, in strength between classical and
1167: intuitionistic logics). Dummett \cite{dummett} was the first to
1168: study infinite valued Gödel logics, axiomatizing the set of
1169: tautologies over infinite truth-value sets by intuitionistic logic
1170: extended by the linearity axiom $(A \limp B) \lor (B \limp A)$. Hence,
1171: infinite-valued propositional Gödel logic is also called
1172: Gödel-Dummett logic or Dummett's \textsc{LC}. In terms of Kripke semantics,
1173: the characteristic linearity axiom picks out those accessibility
1174: relations which are linear orders.
1175:
1176: Quantified propositional Gödel logics and first-order Gödel logics are
1177: natural extensions of the propositional logics introduced by Gödel and
1178: Dummett. For both propositional quantified and first-order Gödel
1179: logics it turns out to be inevitable to consider more complex truth
1180: value sets than the standard unit interval.
1181:
1182: Gödel logics occur in a number of different areas of logic
1183: and computer science. For instance, Dunn and Meyer \cite{DM} pointed
1184: out their relation to relevance logics; Visser \cite{visser} employed
1185: \textsc{LC} in investigations of the provability logic of Heyting
1186: arithmetic; three-valued Gödel logic has been used to model
1187: strong equivalence between logic programs. Furthermore, these logics
1188: have recently received increasing attention, both in terms of
1189: foundational investigations and in terms of applications, as they have
1190: been recognized as one of the most important formalizations of fuzzy
1191: logic \cite{hajek}.
1192:
1193: Perhaps the most surprising fact is that whereas there is only one
1194: infinite-valued propositional Gödel logic, there are infinitely many
1195: different logics at the first-order level
1196: \cite{BaazLeitZach96TCS,Baaz96GOEDEL,Prei02LPAR}.
1197: In the light of the general result of Scarpellini \cite{scarpellini}
1198: on non-axiomatizability, it is interesting that
1199: some of the infinite-valued Gödel logics belong to the limited class
1200: of recursively enumerable linearly ordered first-order logics
1201: \cite{horn,TT}.
1202:
1203:
1204:
1205: % ***
1206: % ***
1207: % ***
1208: % ***
1209: % ***
1210: % ***
1211: % ***
1212: % ***
1213: % ***
1214: % ***
1215: % ***
1216: % ***
1217: % ***
1218: % ***
1219: % ***
1220: % ***
1221: % ***
1222: % ***
1223: % ***
1224: % ***
1225: % ***
1226: % ***
1227: % ***
1228:
1229: Recently a full characterization of axiomatizability of Gödel logics
1230: was given \cite{Prei03PHD}, where also the compactness of the
1231: entailment relation is discussed. But one of the most basic questions
1232: has been left open until now: {\em How many Gödel logics are there?}
1233: Lower bounds to this question have been given in
1234: \cite{Baaz96GOEDEL,Prei02LPAR}, and special subclasses of logics
1235: determined by ordinals have been discussed \cite{ono},
1236: but it was a long open question whether there are only countably many
1237: or uncountably many different Gödel logics.
1238:
1239: % ***
1240:
1241: % ***
1242: % ***
1243: % ***
1244: % ***
1245:
1246: % ***
1247: % ***
1248: % ***
1249: % ***
1250:
1251: % ***
1252:
1253: \subsection{Syntax and Semantic}
1254:
1255: In the following we fix a relational language $\LL$
1256: of predicate logic with finitely or countably many predicate symbols.
1257: In addition to the two quantifiers $\forall $ and $\exists$ we
1258: use the connectives $\vee$, $\wedge$, $\to$
1259: and the constant $\bot$ (for `false'); other connectives are
1260: introduced as abbreviations, in particular we let
1261: $\lnot \vhi := (\vhi \to \bot)$.
1262:
1263: Originally, Gödel logics have been defined only based on the fixed
1264: truth value set $[0,1]$. But we can fix a (nearly) arbitrary subset
1265: of $[0,1]$ and consider the Gödel logic induced by this truth value
1266: set.
1267:
1268: \begin{definition}[Gödel set]
1269: A Gödel set is any closed set of real numbers, $V \subseteq [0,1]$
1270: which contains $0$ and $1$.
1271: \end{definition}
1272:
1273: The (propositional) operations on Gödel sets which are used in
1274: defining the semantics of Gödel logics have the property that they are
1275: projecting, i.e.\ that the operation uses one of the arguments (or $1$)
1276: as result:
1277: \begin{definition} For $a,b\in [0,1]$ let $a\wedge b := \min(a,b)$,
1278: $a\vee b:=\max(a,b)$,
1279: \[ a \to b := \left\{
1280: \begin{array}{ll}
1281: 1 & \mbox{if $a\le b$ }\\
1282: b & \mbox{otherwise}\\
1283: \end{array}\right.
1284: \]
1285: The last operation is called `Gödel's implication'.
1286: Note that
1287: % ***
1288: $$(a\to b)\ =\ \sup \{\, x: \, (x\wedge a)\, \le\, b\, \};$$
1289: in order theory this is
1290: expressed as `the maps $x\mapsto (a\wedge x)$ and $y\mapsto (a\to y)$
1291: are residuated'.
1292:
1293: We define $\lnot a:= (a \to 0)$, so $\lnot 0 = 1$, and $\lnot a = 0$ for all
1294: $a>0$.
1295: \end{definition}
1296:
1297:
1298: % ***
1299: % ***
1300: % ***
1301: % ***
1302: % ***
1303: % ***
1304: % ***
1305: % ***
1306: % ***
1307: % ***
1308: % ***
1309: % ***
1310:
1311:
1312: The semantics of Gödel logics, with respect to a fixed Gödel set as
1313: truth value set and a fixed relational language~$\LL$ of predicate logic,
1314: is defined using the extended language $\LL^M$, where $M$ is a universe of
1315: objects.
1316: $\LL^M$ is $\LL$ extended with symbols for
1317: every element of $M$ as constants, so called $M$-symbols.
1318: These symbols are denoted with the same letters.
1319:
1320: \begin{definition}[Semantics of Gödel logic]\label{def:gsemantik}
1321: Fix a Gödel set $V$ (and a relational language $\LL$).
1322: A valuation $v$ into $V$ consists of
1323: \begin{enumerate}
1324: \item a nonempty set $M = M^v$, the
1325: `universe' of $v$,
1326: \item for each $k$-ary predicate symbol $P$,
1327: a function $P^v : M^k \to V$.
1328: \end{enumerate}
1329:
1330: Given a valuation $v$, we can naturally define a value $v(A)$ for
1331: any closed formula $A$ of $\LL^M$
1332: For atomic formulas $\vhi = P(m_1,\ldots, m_n)$,
1333: we define $v(\vhi) = P^v( m_1, \ldots, m_n)$, and for
1334: composite formulas $\vhi$ we define $v(\vhi)$ naturally by:
1335: % ***
1336: \begin{align}
1337: \val(\bot) &= 0\\
1338: \val(\vhi\land \psi) &= \min(\val(\vhi),\val(\psi))\\
1339: \val(\vhi\lor \psi) &= \max(\val(\vhi),\val(\psi))\\
1340: \val(\vhi\limp \psi) &= \val(\vhi) \to \val(\psi)\\
1341: \val(\qa x\vhi(x)) &= \inf \{\val(\vhi(m)) \suchthat m\in M\}\\
1342: \val(\qe x\vhi(x)) &= \sup \{\val(\vhi(m)) \suchthat m\in M\}
1343: \end{align}
1344: (Here we use the fact that % ***
1345: our Gödel sets $V$ are \emph{closed} subsets
1346: of $[0,1]$, in order to be able to interpret $\forall $ and $\exists$
1347: as $\inf$ and $\sup$ in V.)
1348:
1349: For any closed formula $\vhi$ and any Gödel set $V$ we let
1350: $$ \|\vhi\|_V := \inf \{ v(\vhi): \mbox{$v$ a valuation into $V$}\}$$
1351: \end{definition}
1352:
1353: \begin{remark}
1354: Note that the recursive computation of $v(\vhi)$ depends
1355: only on the values $M^v$, $P^v$ and not directly on the
1356: set $V$. Thus, if $V_1\subseteq V_2$ are both Gödel sets, and $v$
1357: is a valuation into $V_1$, then $v$ can be seen also as a valuation
1358: into $V_2$, and the values $v(\vhi)$, computed recursively using
1359: (1)--(6),
1360: do not depend on whether we view $v$ as a $V_1$-valuation or a
1361: $V_2$-valuation.
1362:
1363: If $V_1 \subseteq V_2$, there are more valuations into $V_2$ than
1364: into $V_1$.
1365: Hence $\|\vhi\|_{V_1} \ge \|\vhi\|_{V_2} $ for all closed $\vhi$.
1366: % ***
1367:
1368: Similarly, for any map $h: V_1 \to V_2$, any
1369: valuation $v_1$ into $V_1$ induces a valuation $v_2$
1370: into $V_2$ as follows:
1371: \[
1372: M^ {v_1} = M^ {v_2},\quad P^{v_1}(\vec m) = h(P^{v_2}(\vec m)).
1373: \]
1374: If $h: V_1 \to V_2$ is a \smc embedding
1375: from $V_1$ into $V_2$ which moreover preserves $0$ and $1$,
1376: and if $v_2$ is the valuation induced by $v_1$ and $h$, then
1377: it is easy to verify by induction on the complexity of the
1378: closed formula $\vhi$ that $v_2(\vhi)=h(v_1(\vhi))$, and hence
1379: \[ h(\|\vhi\|_{V_1}) \ge \|\vhi\|_{V_2} \]
1380: for all closed formulas $\vhi$.
1381: \end{remark}
1382:
1383: \begin{definition}[Gödel logics based on $V$]
1384: \label{def:goedellogics}
1385: For a Gödel set $V$ we define the {\em first order Gödel logic $\gdl V$}
1386: as the set of
1387: all closed formulas of $\LL$ such that $\|\vhi\|_V = 1$.
1388: \end{definition}
1389:
1390: From the above remark it is obvious that if $h$ is as above
1391: or $V_1\subseteq V_2$, the Gödel logic $\gdl{V_2}$ is a subset of $\gdl{V_1}$.
1392:
1393: \begin{definition}[Submodel, elementary submodel]
1394: Let $v_1$, $v_2$ be valuations. We write $v_1 \subseteq v_2$
1395: ($v_2$ extends $v_1$) iff
1396: $M^{v_1} \subseteq M^{v_2}$, and for all $k$, all $k$-ary
1397: predicate symbols $P$ in $\LL$, we have
1398: \[ P^{ v_1 } = P^{ v_2 } \upharpoonright (M^{v_1})^k \]
1399: or in other words, if $v_1$ and $v_2$ agree on closed atomic
1400: formulas.
1401:
1402: We write $v_1 \prec v_2$ if $v_1 \subseteq v_2$ and $v_1(\vhi) = v_2(\vhi)$
1403: for all $\LL^{M^{v_1}}$-formulas $\vhi$.
1404: \end{definition}
1405:
1406: \begin{fact}[downward Löwenheim-Skolem]\label{fact:loewenheim}
1407: For any valuation $v$ (with $M^v$ infinite) there is a valuation
1408: $v' \prec v$ with a countable universe~$M^{v'} $.
1409: \end{fact}
1410:
1411: % ***
1412: % ***
1413: % ***
1414: % ***
1415:
1416: % ***
1417: % ***
1418: % ***
1419: % ***
1420: % ***
1421: % ***
1422: % ***
1423: % ***
1424:
1425: % ***
1426: % ***
1427: % ***
1428: % ***
1429: % ***
1430:
1431:
1432: \begin{definition}
1433: The only sub-formula of an atomic formula $P$ in $\LL^M$ is $P$ itself. The
1434: sub-formulas of $\vhi\star \psi$ for $\star\in\{\limp,\land,\lor\}$ are
1435: the subformulas of $\vhi$ and of $\psi$, together with $\vhi\star \psi$
1436: itself. The sub-formulas of $\qa x\vhi(x)$ and $\qe x\vhi(x)$ with
1437: respect to a universe $M$ are all subformulas of all
1438: $\vhi(m)$ for $m\in M$, together with $\qa x\vhi(x)$ (or,
1439: $\qe x\vhi(x)$, respectively) itself.
1440:
1441: The set of valuations of sub-formulas of $\vhi$ under a given
1442: valuation~$\val$ is denoted with
1443: \[ \subval(\val,\vhi) = \{ \val(\psi) \suchthat \psi
1444: \text{ sub-formula of $\vhi$ w.r.t.\ $M^v$}\}\]
1445: \end{definition}
1446:
1447: \begin{lemma}\label{lemma:valuation-cut-off}
1448: Let $\val$ be a valuation with $\val(\vhi)<b<1$
1449: and $b$ does not occur in $\subval(\val,\vhi)$.
1450: Let $\val'$ be the valuation with the same universe as $\val$,
1451: defined by
1452: \[ \val'(\psi) = \begin{cases} \val(\psi) &\text{ if $\val(\psi)<b$}\\
1453: 1 &\text{ otherwise}
1454: \end{cases}\]
1455: for atomic subformulas $\psi$ of $\vhi$ w.r.t.~$M^\val$,
1456: and arbitrary for all other atomic formulas.
1457: Then $\val'$ is a valuation and $\val'(\vhi) = \val(\vhi)$.
1458: \end{lemma}
1459:
1460: \begin{proof}
1461: Let $h_b(a)=a$ if $a<b$ and $=1$ otherwise.
1462: By induction on the complexity of the formula $\psi$
1463: we can easily show that $\val'(\psi)=h_b(\val(\psi))$ for all
1464: subformulas $\psi$ of $\vhi$ w.r.t.\ $M^\val$.
1465: % ***
1466: \end{proof}
1467:
1468: % ***
1469: % ***
1470: % ***
1471: % ***
1472: % ***
1473: % ***
1474: % ***
1475: % ***
1476: % ***
1477: % ***
1478: % ***
1479:
1480: % ***
1481: % ***
1482: % ***
1483: % ***
1484: % ***
1485: % ***
1486: % ***
1487:
1488: \begin{lemma}\label{lemma:countable-into-cantor}
1489: Assume that $M\subset \bbR$ is a countable set and $P$ a perfect
1490: set. Then there is a \smc embedding from $M$ into $P$.
1491: % ***
1492: % ***
1493: % ***
1494: \end{lemma}
1495:
1496: In \cite{Prei03PHD} there is a proof of this lemma which was used to
1497: extend the proof of recursive axiomatizability of `standard' Gödel
1498: logics (those with $V=[0,1]$) to Gödel logics with a truth value set
1499: containing a perfect set in the general case. Here we give a
1500: simple proof.
1501:
1502: % ***
1503:
1504: \begin{proof}
1505: Since there are uncountable many disjoint sets of the form
1506: $\bbQ - x :=\{q-x: q\in \bbQ\}$,
1507: there is some $x$ such that $M\cap (\bbQ -x) = \emptyset$, so
1508: also $(M+x)\cap \bbQ=\emptyset$.
1509: So we may assume
1510: % ***
1511: that $M\cap \bbQ=\emptyset$.
1512: We may also assume $M\subseteq [0,1]$.
1513:
1514: Since $P$ is perfect, we can find an \smc embedding $c$
1515: from the Cantor set $C\subseteq [0,1]$ into $P$.
1516:
1517: Let $i$ be the natural bijection from $2^\omega$ (the set of infinite
1518: $\{0,1\}$-sequences, ordered lexicographically) onto $C$. $i$
1519: is an order preserving homeomorphism.
1520:
1521: For every $m\in M$ let $w(m)\in 2^\omega$ be the binary
1522: representation of $m$. Since $M$ does not contain any
1523: dyadic rational numbers, this representation is unique; moreover,
1524: the map $w$ is smc. Now $c\circ i \circ w$ is an smc embedding from $M$
1525: into $P$.
1526: $$ M \pfeil{w} 2^\omega \pfeil{i} C \pfeil{c} P $$
1527:
1528: % ***
1529: % ***
1530: % ***
1531: % ***
1532: % ***
1533: % ***
1534:
1535: % ***
1536: % ***
1537: % ***
1538: % ***
1539: % ***
1540: % ***
1541: % ***
1542: % ***
1543: % ***
1544: % ***
1545: % ***
1546: % ***
1547: % ***
1548: % ***
1549: % ***
1550: % ***
1551: % ***
1552: % ***
1553: % ***
1554: % ***
1555: % ***
1556: % ***
1557: % ***
1558: % ***
1559: % ***
1560:
1561: % ***
1562:
1563: % ***
1564: % ***
1565: % ***
1566: % ***
1567: % ***
1568: % ***
1569:
1570: % ***
1571: % ***
1572: % ***
1573: % ***
1574: % ***
1575: % ***
1576:
1577: % ***
1578: % ***
1579: % ***
1580: % ***
1581: % ***
1582: % ***
1583:
1584: % ***
1585: % ***
1586: % ***
1587: % ***
1588:
1589: % ***
1590: % ***
1591: % ***
1592: % ***
1593: % ***
1594: % ***
1595: % ***
1596: % ***
1597: % ***
1598: % ***
1599: \end{proof}
1600:
1601: \begin{lemma}\label{lemma:gs-id}
1602: Let $V$ be a truth value set with non-empty perfect kernel $P$, and
1603: let $W= V \cup [\inf P,1]$, then the logics induced by $V$ and $W$
1604: are the same, i.e.\ $\gdl{V} = \gdl{W}$.
1605: \end{lemma}
1606:
1607: \begin{proof}
1608: % ***
1609: % ***
1610: % ***
1611: % ***
1612: % ***
1613: % ***
1614: As $V\subseteq W$ we have $\gdl{W}\subseteq \gdl V$.
1615: (Cf.\ Remark before Definition~\ref{def:goedellogics}.)
1616:
1617: Now assume that $\val_{W}(\vhi)<1$. Due to Fact~\ref{fact:loewenheim},
1618: there is a $\val'_W$ such that $M^{v'}$ is countable
1619: and $\val_W'(\vhi) = \val_W(\vhi)$. The set $M := \subval(v'_W,\vhi)$ has
1620: cardinality at most $\aleph_0$, thus there exists a
1621: $b\in W$ such that $b\notin M$, $\val'_{W}(\vhi)<b<1$.
1622: According to Lemma~\ref{lemma:countable-into-cantor} there is a
1623: \smc embedding $h$ from $[\inf P, b]\cap (M\cup\{b\})$ into $P$.
1624: Define $\val_V(\psi)$ for all atomic subformulas of $\vhi$ as follows:
1625: \[
1626: \val_V(\psi) =
1627: \begin{cases}
1628: \val'_W(\psi) & \text{ if $0<\val_W'(\psi)<\inf P$}\\
1629: h(\val'_{W}(\psi))& \text{ if $\inf P \le \val_W'(\psi)\le b$}\\
1630: 1 & \text{ otherwise}
1631: \end{cases}
1632: \]
1633: and $1$ for all other atomic formulas. According to
1634: Lemma~\ref{lemma:valuation-cut-off} we obtain that
1635: \[ \val_V(\vhi) =
1636: \begin{cases}
1637: \val'_W(\psi) < b < 1 & \text{ if $0<\val_W'(\psi)<\inf P$}\\
1638: h(\val_W'(\vhi)) < h(b) \le 1 &
1639: \text{ if $\inf P \le \val_W'(\psi)\le b$}
1640: \end{cases}
1641: \]
1642: thus $\val_V(\vhi) < 1$ and $\gdl V\subseteq \gdl{W}$.
1643: \end{proof}
1644:
1645: % ***
1646: % ***
1647: % ***
1648: % ***
1649: % ***
1650: % ***
1651: % ***
1652: % ***
1653: % ***
1654: % ***
1655: % ***
1656: % ***
1657: % ***
1658: % ***
1659: % ***
1660: % ***
1661: % ***
1662: % ***
1663: % ***
1664: % ***
1665: % ***
1666: % ***
1667: % ***
1668: % ***
1669: % ***
1670: % ***
1671: % ***
1672: % ***
1673: % ***
1674: % ***
1675: % ***
1676: % ***
1677: % ***
1678: % ***
1679: % ***
1680: % ***
1681: % ***
1682: % ***
1683: % ***
1684: % ***
1685: % ***
1686:
1687: \begin{lemma}\label{lemma:goedelsmc}
1688: Let $V_1$ and $V_2$ be Gödel sets and $Q=\{0,1\}$ with $0<_Q1$.
1689: Let $A_1$ and $A_2$ be $Q$-labeled cclos defined by $\dom(A_i)=V_i$,
1690: $A_i(0)=A_i(1)=1$ and
1691: $A_i(x)=0$ otherwise. If $A_1$ is ($Q$-smc-)embeddable into $A_2$,
1692: then the Gödel logic determined by $V_1$ is a superset of the Gödel
1693: logic determined by $V_2$.
1694: \end{lemma}
1695:
1696: \begin{proof}
1697: In this case of a very simple labeling the property that $A_1$ is
1698: embeddable into $A_2$ reduces to the existence of a smc-embedding of
1699: $V_1$ into $V_2$ preserving $0$ and $1$. According to the Remark
1700: following Definition~\ref{def:gsemantik} this induces the reverse
1701: inclusion of the respective Gödel logics.
1702: \end{proof}
1703:
1704: \begin{corollary}\label{cor:countable}
1705: The set of Gödel logics
1706: \begin{enumerate}
1707: \item[(a)] is countable
1708: \item[(b)] is a (lightface) $\Sigma^1_2$ set
1709: \item[(c)] is a subset of Gödel's constructible universe $L$.
1710: \end{enumerate}
1711: \end{corollary}
1712: \begin{proof}
1713: % ***
1714: % ***
1715: % ***
1716: % ***
1717: % ***
1718: % ***
1719: % ***
1720: % ***
1721: % ***
1722: % ***
1723: % ***
1724: % ***
1725: % ***
1726: % ***
1727: % ***
1728: % ***
1729: % ***
1730: (a) First note that the set of countable Gödel logics (i.e.\ those
1731: with countable truth value set), ordered by $\supseteq$,
1732: is a wqo.
1733: To see this, assume that $\seqof{\gdl n}{n\in\omega}$ is a sequence of
1734: countable Gödel logics.
1735: Take the sequence of countable Gödel sets $\seqof{V_n}{n\in\omega}$
1736: generating these logics and define the
1737: respective $Q$-labeled cclo (also denoted with $V_n$) with
1738: $Q=\{0,1\}$, $0<_Q1$ and $V_n(0) = V_n(1) = 1$, and $V_n(x) = 0$ otherwise.
1739: According to Corollary~\ref{cor:sc-wqo} this sequence of $Q$-labeled cclos
1740: must be good, hence there are numbers $n<m$ such that $V_n$ is
1741: \smc embeddable into $V_m$.
1742: Then Lemma~\ref{lemma:goedelsmc} implies that
1743: $\gdl n$ must be a superset of $\gdl m$.
1744: This shows that the original sequence of Gödel logics
1745: $\seqof{\gdl n}{n\in\omega}$ must be good, too.
1746:
1747: As each countable Gödel logic is a subset of a fixed countable set (the set
1748: of all formulas), the family of countable Gödel logics cannot contain a
1749: copy of $\omega_1$. So by Lemma~\ref{omega1.wqo}, the family of
1750: countable Gödel logics must be countable.
1751:
1752: According to Lemma~\ref{lemma:gs-id} any uncountable Gödel logic, i.e.\
1753: Gödel logic determined by an uncountable Gödel set,
1754: such that $0$ is not included in the prefect kernel $P$ of the Gödel set
1755: is completely determined by the countable part
1756: $V\cap[0,\inf P]$.
1757: So the total number of Gödel logics is at most two times the
1758: number of countable Gödel logics plus $1$ for the logic based on the
1759: full interval, i.e. countable.
1760:
1761: % ***
1762: % ***
1763: % ***
1764: % ***
1765: % ***
1766: % ***
1767: % ***
1768:
1769:
1770: (b) First, note that the set
1771: $$ \{ (v, \vhi, v(\vhi)): M^v = \bbN \}$$
1772: is a Borel set, since we can show by induction on the quantifier
1773: complexity of $\vhi$ that the sets $\{(v, q) : M^v=\bbN, v(\varphi)\ge q\}$
1774: are Borel sets (even of finite rank).
1775:
1776: Next, as set $G$ of formulas is a Gödel logic iff
1777: \begin{quotation}
1778: There {\em exists} a closed set $V \subseteq [0,1]$ (say, coded
1779: as the complement of a sequence of finite intervals) such that:
1780: \begin{itemize}
1781: \item For every $\vhi\in G$, {\em for every $v$} with $M^v=\bbN$, $v(\vhi)=1$,
1782: and
1783: \item For every $\vhi\notin G$, there exists $v$ with $M^v=\bbN$, $v(\vhi)<1$.
1784: \end{itemize}
1785: \end{quotation}
1786:
1787: (We can restrict our attention to valuations $v$ with $v^M=\bbN$ because of
1788: Fact~\ref{fact:loewenheim}.)
1789:
1790: Counting quantifiers we see that this is a $\Sigma^1_2$ property.
1791:
1792:
1793: (c) follows from (a) and (b) by the
1794: Mansfield-Solovay theorem (see \cite{Mansfield:1970},
1795: \cite[8G.1 and 8G.2]{Moschovakis:1980}).
1796: \end{proof}
1797:
1798:
1799: \section*{Questions and future work}
1800:
1801: Define % ***
1802: $\omG $ as the smallest ordinal
1803: $\alpha$ such that: For every well-ordered Gödel set $V$ there is a
1804: well-ordered Gödel set $V'$ of order type $< \alpha$ with $\gdl V=\gdl{V'}$.
1805:
1806: % ***
1807: % ***
1808: % ***
1809: % ***
1810:
1811:
1812: Define $ \omGCB $ as the smallest ordinal
1813: $\alpha$ such that: For every Gödel set $V$ there is a
1814: Gödel set $V'$ whose Cantor-Bendixson rank is $< \alpha$ with $\gdl V=\gdl{V'}$.
1815:
1816: By Corollary~\ref{cor:countable}, both these ordinals are countable.
1817: Furthermore, $\omG \le \omGCB$.
1818: % ***
1819: % ***
1820: % ***
1821: % ***
1822: % ***
1823: % ***
1824: % ***
1825: % ***
1826: % ***
1827: % ***
1828: % ***
1829: % ***
1830: % ***
1831: % ***
1832: % ***
1833: % ***
1834: % ***
1835: % ***
1836: % ***
1837: % ***
1838: % ***
1839: % ***
1840: % ***
1841: % ***
1842: It would be interesting to describe the ordinals $\omG$ and $\omGCB$
1843: by giving lower and upper estimates in terms of well-known
1844: closure ordinals, e.g.\ for inductive definitions and related
1845: reflection principles of set theory.
1846: Are they equal?
1847: Note that
1848: $\omega_1^{CK}\le \omG$.
1849:
1850:
1851:
1852:
1853:
1854:
1855: % \bibliographystyle{alpha}
1856: \let\H\hungarian
1857:
1858: \begin{thebibliography}{EHMR84}
1859:
1860: \bibitem[Baa96]{Baaz96GOEDEL}
1861: M.~Baaz.
1862: \newblock Infinite-valued {Gödel} logics with $0$-$1$-projections and
1863: relativizations.
1864: \newblock In P.~H\'ajek, editor, {\em Proc. {Gödel}'96, Logic Foundations of
1865: Mathematics, Computer Science and Physics -- {Kurt} {Gödel}'s Legacy},
1866: Lecture Notes in Logic 6, pages 23--33. Springer, 1996.
1867:
1868: \bibitem[BLZ96]{BaazLeitZach96TCS}
1869: M.~Baaz, A.~Leitsch, and R.~Zach.
1870: \newblock Completeness of a first-order temporal logic with time-gaps.
1871: \newblock {\em Theoret. Comput. Sci.}, 160(1--2):241--270, June 1996.
1872:
1873: \bibitem[DM40]{Dushnik}
1874: Ben Dushnik and E.~W. Miller.
1875: \newblock Concerning similarity transformations of linearly ordered sets.
1876: \newblock {\em Bull. Amer. Math. Soc.}, 46:322--326, 1940.
1877:
1878: \bibitem[DM71]{DM}
1879: J.~M. Dunn and R.~K. Meyer.
1880: \newblock Algebraic completeness results for {D}ummett's {LC} and its
1881: extensions.
1882: \newblock {\em Z. Math. Logik Grundlagen Math}, 17:225--230, 1971.
1883:
1884: \bibitem[Dum59]{dummett}
1885: M.~Dummett.
1886: \newblock A propositional logic with denumerable matrix.
1887: \newblock {\em J. of Symbolic Logic}, 24:96--107, 1959.
1888:
1889: \bibitem[EHMR84]{EHMR}
1890: Paul Erd{\H{o}}s, Andr{\'a}s Hajnal, Attila M{\'a}t{\'e}, and Richard Rado.
1891: \newblock {\em Combinatorial set theory: partition relations for cardinals},
1892: volume 106 of {\em Studies in Logic and the Foundations of Mathematics}.
1893: \newblock North-Holland Publishing Co., Amsterdam, 1984.
1894:
1895: \bibitem[Fra48]{Fraisse}
1896: Roland Fra{\"{\i}}ss{\'e}.
1897: \newblock Sur la comparaison des types d'ordres.
1898: \newblock {\em C. R. Acad. Sci. Paris}, 226:1330--1331, 1948.
1899:
1900: \bibitem[{G}öd33]{goedel33}
1901: K.~{G}ödel.
1902: \newblock {Z}um {I}ntuitionistischen {A}ussagenkalkül.
1903: \newblock {\em Ergebnisse eines mathematischen Kolloquiums}, 4:34--38, 1933.
1904:
1905: \bibitem[H{\'a}j98]{hajek}
1906: P.~H{\'a}jek.
1907: \newblock {\em Metamathematics of Fuzzy Logic}.
1908: \newblock Kluwer, 1998.
1909:
1910: \bibitem[Hor69]{horn}
1911: A.~Horn.
1912: \newblock Logic with truth values in a linearly ordered {H}eyting algebra.
1913: \newblock {\em Journal of Symbolic Logic}, 34(3):395--409, 1969.
1914:
1915: \bibitem[Lav71]{Laver:1971}
1916: Richard Laver.
1917: \newblock On {F}ra\"\i ss\'e's order type conjecture.
1918: \newblock {\em Ann. of Math. (2)}, 93:89--111, 1971.
1919:
1920: \bibitem[Man70]{Mansfield:1970}
1921: Richard Mansfield.
1922: \newblock Perfect subsets of definable sets of real numbers.
1923: \newblock {\em Pacific J. Math.}, 35:451--457, 1970.
1924:
1925: \bibitem[Mos80]{Moschovakis:1980}
1926: Yiannis~N. Moschovakis.
1927: \newblock {\em Descriptive set theory}, volume 100 of {\em Studies in Logic and
1928: the Foundations of Mathematics}.
1929: \newblock North-Holland Publishing Co., Amsterdam, 1980.
1930:
1931: \bibitem[MTO90]{ono}
1932: P.~Minari, M.~Takano, and H.~Ono.
1933: \newblock Intermediate predicate logics determined by ordinals.
1934: \newblock {\em Journal of Symbolic Logic}, 55(3):1099--1124, 1990.
1935:
1936: \bibitem[NW63]{Nash:1963}
1937: C.~St. J.~A. Nash-Williams.
1938: \newblock On well-quasi-ordering finite trees.
1939: \newblock {\em Proc. Cambridge Philos. Soc.}, 59:833--835, 1963.
1940:
1941: \bibitem[NW64]{Nash:1964}
1942: C.~St. J.~A. Nash-Williams.
1943: \newblock On well-quasi-ordering lower sets of finite trees.
1944: \newblock {\em Proc. Cambridge Philos. Soc.}, 60:369--384, 1964.
1945:
1946: \bibitem[NW65a]{Nash:1965b}
1947: C.~St. J.~A. Nash-Williams.
1948: \newblock On well-quasi-ordering infinite trees.
1949: \newblock {\em Proc. Cambridge Philos. Soc.}, 61:697--720, 1965.
1950:
1951: \bibitem[NW65b]{Nash:1965a}
1952: C.~St. J.~A. Nash-Williams.
1953: \newblock On well-quasi-ordering transfinite sequences.
1954: \newblock {\em Proc. Cambridge Philos. Soc.}, 61:33--39, 1965.
1955:
1956: \bibitem[NW68]{Nash:1968}
1957: C.~St. J.~A. Nash-Williams.
1958: \newblock On better-quasi-ordering transfinite sequences.
1959: \newblock {\em Proc. Cambridge Philos. Soc.}, 64:273--290, 1968.
1960:
1961: \bibitem[Pre02]{Prei02LPAR}
1962: N.~Preining.
1963: \newblock {G}ödel logics and {C}antor-{B}endixon analysis.
1964: \newblock In M.~Baaz and A.~Voronkov, editors, {\em Proceedings of
1965: \textsc{lpar}'2002}, \textsc{lnai}~2514, pages 327--336, October 2002.
1966:
1967: \bibitem[Pre03]{Prei03PHD}
1968: N.~Preining.
1969: \newblock {\em Complete Recursive Axiomatizability of {G}ödel Logics}.
1970: \newblock PhD thesis, Vienna University of Technology, Austria, 2003.
1971:
1972: \bibitem[Ros82]{Rosenstein:1982}
1973: Joseph~G. Rosenstein.
1974: \newblock {\em Linear orderings}, volume~98 of {\em Pure and Applied
1975: Mathematics}.
1976: \newblock Academic Press Inc. [Harcourt Brace Jovanovich Publishers], New York,
1977: 1982.
1978:
1979: \bibitem[Sca62]{scarpellini}
1980: B.~Scarpellini.
1981: \newblock Die {N}ichtaxiomatisierbarkeit des unendlichwertigen
1982: {P}rädikatenkalkülus von {{\L}}ukasiewicz.
1983: \newblock {\em J.~Symbolic Logic}, 27:159--170, 1962.
1984:
1985: \bibitem[Sie50]{Sierpinski}
1986: Wac{\l}aw Sierpi{\'n}ski.
1987: \newblock Sur les types d'ordre des ensembles lin\'eaires.
1988: \newblock {\em Fund. Math.}, 37:253--264, 1950.
1989:
1990: \bibitem[TT84]{TT}
1991: G.~Takeuti and T.~Titani.
1992: \newblock Intuitionistic fuzzy logic and intuitionistic fuzzy set theory.
1993: \newblock {\em J. of Symbolic Logic}, 49:851--866, 1984.
1994:
1995: \bibitem[Vis82]{visser}
1996: A.~Visser.
1997: \newblock On the completeness principle: a study of provability in {H}eyting's
1998: {A}rithmetic.
1999: \newblock {\em Annals of Math. Logic}, 22:263--295, 1982.
2000:
2001: \end{thebibliography}
2002: % \bibliography{bgp}
2003:
2004: \end{document}
2005:
2006: