-
Notifications
You must be signed in to change notification settings - Fork 1
/
Model_theory.tex
4939 lines (4009 loc) · 192 KB
/
Model_theory.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
% Typeset with LaTeX format
\documentclass[titlepage, oneside]{amsbook}
\usepackage{amsmath,amssymb}
\makeindex
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem*{proposition}{Proposition}
\newtheorem{corollary}{Corollary}
\newtheorem*{claim}{Claim}
\newtheorem*{subclaim}{subclaim}
\theoremstyle{definition}
\newtheorem*{notation}{Notation}
\newtheorem{exercise}{Exercise}
\newtheorem{examples}{Example}
\newtheorem{definition}{Definition}
\theoremstyle{remark}
\newtheorem*{note}{Remark}
\newtheorem*{abuse}{Abuse of Notation}
\newtheorem*{rem}{Remark}
\newtheorem*{pro}{PROBLEMS}
\newcommand{\amt}{\ensuremath{\mathfrak A \models \mathcal T }}
\newcommand{\bmt}{\ensuremath{\mathfrak B \models \mathcal T }}
\newcommand{\cmt}{\ensuremath{\mathfrak C \models \mathcal T }}
\newcommand{\dmt}{\ensuremath{\mathfrak D \models \mathcal T }}
\newcommand{\ax}{\ensuremath{\mathfrak{A}_X}}
\newcommand{\Th}{\ensuremath{\mbox{Th}}}
\newcommand{\sv}[1][v_0]{\ensuremath{\Sigma ( #1) }}
\newcommand{\tria}[1]{\ensuremath{\triangle_{\mathfrak{#1}}}}
\newcommand{\theory}{\ensuremath{\mathcal{T}}}
\newcommand{\tee}{\ensuremath{\mathcal{T}}}
\newcommand{\tst}{\ensuremath{\mathcal{T}^{\ast}}}
\newcommand{\tstar}{\ensuremath{\mathcal{T}^{\ast}}}
\newcommand{\Rstar}{\ensuremath{{}^{\ast} \mathfrak R}}
\newcommand{\rstar}{\ensuremath{{}^{\ast} \mathbb R}}
\newcommand{\lan}{\ensuremath{\mathcal{L}}}
\newcommand{\seq}{\ensuremath{\subseteq}}
\newcommand{\ma}{\ensuremath{\mathfrak{A}}}
\newcommand{\mb}{\ensuremath{\mathfrak{B}}}
\newcommand{\mc}{\ensuremath{\mathfrak{C}}}
\newcommand{\md}{\ensuremath{\mathfrak{D}}}
\newcommand{\me}{\ensuremath{\mathfrak{E}}}
\newcommand{\mf}{\ensuremath{\mathfrak{F}}}
\newcommand{\mg}{\ensuremath{\mathfrak{G}}}
\newcommand{\mh}{\ensuremath{\mathfrak{H}}}
\newcommand{\mj}{\ensuremath{\mathfrak{J}}}
\newcommand{\mq}{\ensuremath{\mathfrak{Q}}}
\newcommand{\mr}{\ensuremath{\mathfrak{R}}}
\newcommand{\mm}{\ensuremath{\mathfrak{M}}}
\newcommand{\masb}{\ensuremath{\mathfrak{A} \subseteq \mathfrak{B}}}
\newcommand{\mapb}{\ensuremath{\mathfrak{A} \prec \mathfrak{B}}}
\newcommand{\asb}{\ensuremath{\bf A \subseteq \bf B}}
\newcommand{\reduct}{\ensuremath{\mathfrak{A}' | \mathcal{L}'}}
\newcommand{\real}{\ensuremath{\mathfrak{R}}}
\newcommand{\rational}{\ensuremath{\mathfrak{Q}}}
\newcommand{\reals}{\ensuremath{\mathfrak{R}_{\mathbb{R}}}}
\newcommand{\ba}{\ensuremath{\mathbf{A}}}
\newcommand{\bb}{\ensuremath{\mathbf{B}}}
\newcommand{\bc}{\ensuremath{\mathbf{C}}}
\newcommand{\bd}{\ensuremath{\mathbf{D}}}
\newcommand{\be}{\ensuremath{\mathbf{E}}}
\newcommand{\bg}{\ensuremath{\mathbf{G}}}
\newcommand{\rat}{\ensuremath{\mathbb{Q}}}
\newcommand{\rea}{\ensuremath{\mathbb{R}}}
\newcommand{\nat}{\ensuremath{\mathbb{N}}}
\newcommand{\allforu}[2]{\ensuremath{\forall #1_{0} \dots \forall
#1_{#2}}}
\newcommand{\existsu}[2]{\ensuremath{\exists #1_{0} \dots \exists
#1_{#2}}}
\newcommand{\fru}[2][0]{\ensuremath{\forall u_{#1} \dots \forall
u_{#2}}}
\newcommand{\frv}[2][0]{\ensuremath{\forall v_{#1} \dots \forall
v_{#2}}}
\newcommand{\frw}[2][0]{\ensuremath{\forall w_{#1} \dots \forall
w_{#2}}}
\newcommand{\frx}[2][0]{\ensuremath{\forall x_{#1} \dots \forall
x_{#2}}}
\newcommand{\exu}[2][0]{\ensuremath{\exists u_{#1} \dots \exists
u_{#2}}}
\newcommand{\exv}[2][0]{\ensuremath{\exists v_{#1} \dots \exists
v_{#2}}}
\newcommand{\exw}[2][0]{\ensuremath{\exists w_{#1} \dots \exists
w_{#2}}}
\newcommand{\exx}[2][0]{\ensuremath{\exists x_{#1} \dots \exists
x_{#2}}}
\newcommand{\cnot}[2][0]{\ensuremath{ c_{#1} , \dots , c_{#2}}}
\newcommand{\anot}[2][0]{\ensuremath{ a_{#1} , \dots , a_{#2}}}
\newcommand{\dnot}[2][0]{\ensuremath{ d_{#1} , \dots , d_{#2}}}
\newcommand{\bnot}[2][0]{\ensuremath{ b_{#1} , \dots , b_{#2}}}
\newcommand{\rnot}[2][0]{\ensuremath{ r_{#1} , \dots , r_{#2}}}
\newcommand{\tnot}[2][0]{\ensuremath{ t_{#1} , \dots , t_{#2}}}
\newcommand{\tnt}[2][0]{\ensuremath{ t_{#1} \dots t_{#2}}}
\newcommand{\unot}[2][0]{\ensuremath{ u_{#1} , \dots , u_{#2}}}
\newcommand{\vnot}[2][0]{\ensuremath{ v_{#1} , \dots , v_{#2}}}
\newcommand{\wnot}[2][0]{\ensuremath{ w_{#1} , \dots , w_{#2}}}
\newcommand{\xnot}[2][0]{\ensuremath{ x_{#1} , \dots , x_{#2}}}
\newcommand{\ynot}[2][0]{\ensuremath{ y_{#1} , \dots , y_{#2}}}
\newcommand{\hphi}{\ensuremath{\Hat{\varphi}}}
\newcommand{\ta}{\ensuremath{\theta}}
\newcommand{\vp}{\ensuremath{\varphi}}
\newcommand{\lra}{\ensuremath{\leftrightarrow}}
\newcommand{\amodphi}{\ensuremath{\mathfrak A \models \varphi}}
\newcommand{\amodpsi}{\ensuremath{\mathfrak A \models \psi}}
\newcommand{\bmodphi}{\ensuremath{\mathfrak B \models \varphi}}
\newcommand{\bmodpsi}{\ensuremath{\mathfrak B \models \psi}}
\newcommand{\cmodphi}{\ensuremath{\mathfrak C \models \varphi}}
\newcommand{\cmodpsi}{\ensuremath{\mathfrak C \models \psi}}
\renewcommand{\abstractname}{Introduction}
\begin{document}
\thispagestyle{empty}
\vglue 1truein
\centerline{\bf \Huge Fundamentals of Model Theory}
\vglue .5truein
\centerline{\LARGE William Weiss and Cherie D'Mello}
\vglue .2truein
\centerline{Department of Mathematics}
\centerline{University of Toronto}
\vglue 4.25truein
\centerline{\footnotesize\copyright 2015 W.Weiss and C. D'Mello}
\vfill
\eject
\vglue .25truein
\thispagestyle{empty}
\newpage
\begin{center}
\bf Introduction
\end{center}
\vglue .25truein
\setcounter{page}{1}
Model Theory is the part of mathematics which shows how to apply logic
to the study of structures in pure mathematics. On the one hand it is
the ultimate abstraction; on the other, it has immediate applications
to every-day mathematics. The fundamental tenet of Model Theory is
that mathematical truth, like all truth, is relative. A statement may
be true or false, depending on how and where it is interpreted. This
isn't necessarily due to mathematics itself, but is a consequence of
the language that we use to express mathematical ideas.
What at first seems like a deficiency in our language, can
actually be shaped into a powerful tool for understanding mathematics.
This book provides an introduction to Model Theory which can be used
as a text for a reading course or a summer project at the senior
undergraduate or graduate level. It is also a primer which will give
someone a self contained overview of the subject, before diving into
one of the more encyclopedic standard graduate texts.
Any reader who is familiar with the cardinality of a set and the
algebraic closure of a field can proceed without worry. Many readers
will have some acquaintance with elementary logic, but this is not
absolutely required, since all necessary concepts from logic are
reviewed in Chapter~0. Chapter~1 gives the motivating
examples; it is short and we recommend that you peruse it first, before studying
the more technical aspects of Chapter~0. Chapters~2~and~3 are
selections of some of the most
important techniques in Model Theory. The remaining chapters
investigate
the relationship between Model Theory and the algebra of the real and
complex numbers. Thirty exercises develop familiarity with the
definitions and consolidate understanding of the main proof techniques.
Throughout the book we present applications which cannot easily be
found elsewhere in such detail. Some are chosen for their value in
other areas of mathematics: Ramsey's Theorem, the Tarski-Seidenberg
Theorem. Some are chosen for their immediate appeal to every
mathematician: existence of infinitesimals for calculus, graph
colouring on the plane. And some, like Hilbert's Seventeenth Problem,
are chosen because of how amazing it is that logic can play an
important role in the solution of a problem from high school algebra.
In each case, the derivation is shorter than any
which tries to avoid logic. More importantly, the methods of Model
Theory display clearly the structure of the main ideas of the proofs,
showing how theorems of logic combine with theorems from other areas of
mathematics to produce stunning results.
The theorems here are all are more than thirty years old and due in
great part to the cofounders of the subject, Abraham Robinson and
Alfred Tarski. However, we have not attempted to give a history. When
we attach a name to a theorem, it is simply because that is what
mathematical logicians popularly call it.
The bibliography contains a number of texts that were helpful in the
preparation of this manuscript. They could serve as avenues of further
study and in addition, they contain many other references and
historical notes. The more recent titles were added to show the reader
where the subject is moving today. All are worth a look.
This book began life as notes for William Weiss's graduate course at
the University of Toronto. The notes were revised and expanded by
Cherie D'Mello and William Weiss, based upon suggestions from several
graduate students. The electronic version of this book may be
downloaded and further modified by anyone for the purpose of learning,
provided this paragraph is included in its entirety and so long as no
part of this book is sold for profit.
\tableofcontents%
\setcounter{chapter}{-1}
\chapter{Models, Truth and Satisfaction}
We will use the following symbols:
\begin{itemize}
\item logical symbols:
\begin{itemize}
\item the connectives $\wedge$ ,$\vee$ , $\neg$ , $\to$ ,
$\leftrightarrow$ called ``and'', ``or'', ``not'', ``implies'' and
``iff'' respectively
\item the quantifiers $\forall$ , $\exists$ called ``for all'' and
``there exists''
\item an infinite
collection of variables
\index{variable}%
indexed by the natural numbers $\mathbb{N}$ $v_{0}$ ,$v_{1}$
, $v_{2}$ , \dots
\item the two parentheses $)$, $($
\item the symbol $=$ which is the usual ``equal sign''
\end{itemize}
\item constant symbols : often denoted by the letter $c$ with
subscripts
\item function symbols : often denoted by the letter $F$ with
subscripts;
each function symbol is an m-placed func\-tion sym\-bol for some
natural
number $m \geq 1$
\item relation symbols : often denoted by the letter $R$ with
subscripts; each relational symbol is an n-placed relation symbol for some natural
number $n \geq 1$.
\end{itemize}
\addcontentsline{toc}{section}{Formulas, Sentences, Theories and
Axioms}
We now define terms and formulas.
\begin{definition}\label{D:term}
\index{term}%
A \emph{term} is defined as follows:
\begin{itemize}
\item [(1)] a variable is a term
\item[(2)] a constant symbol is a term
\item[(3)] if $F$ is an m-placed function symbol and
$t_{1},\dots,t_{m}$ are terms, then \\
$F(t_{1} \dots t_{m})$ is a term.
\item[(4)] a string of symbols is a term if and only if it can be shown
to be a term by a finite number of applications of (1), (2) and (3).
\end{itemize}
\end{definition}
\begin{note} This is a recursive definition.
\end{note}
\begin{definition}
\index{formula}%
A \emph{formula} is defined as follows :
\begin{itemize}
\item[(1)] if $t_1$ and $t_2$ are terms, then $(t_1 = t_2 )$ is a
formula.
\item[(2)] if $R$ is an n-placed relation symbol and
$t_1 , \dots , t_n$ are terms, then \\
$(R( t_1 \dots t_n))$ is a formula.
\item[(3)] if $\varphi$ is a formula, then $( \neg \varphi )$ is a
formula
\item[(4)] if $\varphi$ and $\psi$ are formulas then so are $( \varphi
\wedge \psi )$, $ ( \varphi \vee \psi )$, $( \varphi \to \psi )$ and
$ ( \varphi \leftrightarrow \psi )$
\item[(5)] if $v_{i}$ is a variable and $\varphi$ is a formula, then
$( \exists v_{i}) \varphi$ and $( \forall v_{i}) \varphi$ are formulas
\item[(6)] a string of symbols is a formula if and only if it can be
shown
to be a formula by a finite number of applications of (1), (2), (3),
(4) and (5).
\end{itemize}
\end{definition}
\begin{rem} This is another recursive definition. $\neg \varphi$ is
called the negation of $\varphi$; $\varphi \wedge \psi$ is called the
conjunction of $\varphi$ and $\psi$; and $\varphi \vee \psi$ is called the
disjunction of $\varphi $ and $\psi$.
\end{rem}
\begin{definition}\label{D:subform}
\index{subformula}%
A \emph{subformula} of a formula $ \varphi$ is defined as follows:
\begin{itemize}
\item[(1)] $\varphi$ is a subformula of $ \varphi$
\item[(2)] if $ (\neg \psi )$ is a subformula of $ \varphi$ then so is
$\psi$
\item[(3)] if any one of $ (\theta \wedge \psi)$, $(\theta \vee \psi)$,
$(\theta \to \psi)$ or $(\theta \leftrightarrow \psi )$ is a subformula of $
\varphi$,
then so are both $\theta$ and $ \psi $
\item[(4)] if either $( \exists v_{i} ) \psi$ or $( \forall v_{i} ) \psi$
is a subformula of $\varphi$ for some natural number $i$, then $\psi$ is
also a subformula of $\varphi$
\item[(5)] A string of symbols is a subformula of $\varphi$, if and only
if it can be shown to be such by a finite number of applications of (1), (2),
(3) and (4).
\end{itemize}
\end{definition}
\begin{definition}\label{D:bound}
\index{free variable}%
\index{bound variable}%
A variable $v_{i}$ is said to occur \emph{bound} in a formula $\varphi$
iff for some subformula $\psi$ of $\varphi$ either $(\exists v_{i}) \psi$
or $(\forall v_{i}) \psi $ is a subformula of $\varphi$.
In this case each occurrence of $v_{i}$ in $(\exists v_{i}) \psi$ or
$(\forall v_{i}) \psi$ is said to be a
\emph{bound occurrence} of $v_{i}$.
Other occurrences of $v_{i}$ which do not occur bound in $\varphi$ are
said to be
\emph{free}.
\end{definition}
\begin{examples}\label{X:term}
\[ F(v_3) \mbox{ is a term, where $F$ is a unary function symbol.} \]
\[ ((\exists v_3 ) ( v_0 = v_3 ) \wedge (\forall v_0 ) (v_0 = v_0 )) \]
is a formula. In this formula the variable $v_3$ only occurs bound but the variable $v_0$ occurs both bound and free.
\end{examples}
\begin{exercise}\label{E:recon}
Using the previous definitions as a guide, define the substitution of a
term $t$ for a variable $v_{i}$ in a formula $\varphi$.
In particular, demonstrate how to substitute the term for the variable $v_0$
in the formula of the example above.
\end{exercise}
\begin{definition}
\index{language}%
A \emph{language} $\mathcal{L}$ is a set consisting of
all
the logical symbols with perhaps some constant, function
and/or relational symbols included. It is understood that
the formulas of
$\mathcal{L}$ are made up from this set in the manner prescribed above.
Note that all the formulas of $\mathcal{L}$ are uniquely described
by listing only the
constant, function and relation symbols of $\lan$.
\end{definition}
We use $t(v_{0}, \dots , v_{k} ) $ to denote a term $t$ all of whose
variables occur among $v_{0}, \dots , v_{k}$.
We use $\varphi (v_{0}, \dots , v_{k}) $ to denote a formula $\varphi$
all of whose free variables occur among $v_{0}, \dots , v_{k}$.
\begin{examples}\label{X:form}
These would be formulas of any language :
\begin{itemize}
\item For any variable $v_i$: $(v_i = v_i )$
\item for any term $t(v_{0}, \dots , v_{k})$ and other terms $t_1$ and
$t_2$: \[ ((t_1 = t_2 ) \to (t(v_{0},
\dots , v_{i-1} , t_1 , v_{i+1} , \dots ,
v_{k} ) = t (v_{0}, \dots , v_{i-1}, t_2 , v_{i+1}, \dots , v_{k})))\]
\item for any formula $\varphi(v_{0}, \dots ,v_{k})$ and terms
$t_1$ and $t_2$:
\[ ((t_1 = t_2 ) \to (\varphi ( v_{0}, \dots , v_{i-1} , t_1 , v_{i+1} ,
\dots , v_{k} ) \leftrightarrow \varphi (v_{0}, \dots , v_{i-1}, t_2
, v_{i+1},
\dots ,
v_{k}))) \]
\end{itemize}
Note the simple way we denote the substitution of $t_1$ for $v_i$.
\end{examples}
\begin{definition}
\index{model}%
A \emph{model} (or structure) $\mathfrak{A}$ for a
language $\mathcal{L}$ is an ordered pair $\langle \mathbf{A}
,\mathcal{I} \rangle$
where $\mathbf{A}$ is a nonempty set and $\mathcal{I}$ is an \emph{interpretation
function} with domain the set of all constant, function and relation
symbols of $\mathcal{L}$ such that:
\begin{enumerate}
\item if $c$ is a constant symbol, then $\mathcal{I} (c) \in
\mathbf{A}$; $\mathcal{I}(c)$ is called a
constant
\item if $F$ is an m-placed function symbol, then
$\mathcal{I}(F)$ is an m-placed function on $\mathbf{A}$
\item if $R$ is an n-placed relation symbol, then $\mathcal{I}(R)$ is an
n-placed relation on $\mathbf{A}$.
\end{enumerate}
$\ba$ is called the \emph{universe} of the model $\mathfrak{A}$. We
generally denote models with Gothic letters and their universes with
the
corresponding Latin letters in boldface. One set
may be involved as a universe with many diff\-erent interpretation
functions of the
language $\mathcal{L}$. The model is \emph{both} the universe
\emph{and} the interpretation function.
\end{definition}
\begin{rem} The importance of Model Theory lies in the observation that
mathematical objects can be cast as models for a language. For instance,
the real numbers with the usual ordering $\pmb{<}$ and the usual
arithmetic operations, addition $\pmb{+}$ and multiplication $\pmb{\cdot}$
along with the special numbers $\bf{0}$ and $\bf{1}$ can be described
as a
model. Let $\lan$ contain one two-placed (i.e. binary) relation symbol
$R_0$, two two-placed function symbols $F_1$ and $F_2$ and two constant
symbols $c_0$ and $c_1$. We build a model by letting the universe $\ba$
be the set of real numbers. The interpretation function $\mathcal I$ will
map $R_0$ to $\pmb{<}$, i.e. $R_0$ will be interpreted as $\pmb{<}$.
Similarly, $\mathcal I (F_1)$ will be $\pmb{+}$, $\mathcal I (F_2)$ will
be $\pmb{\cdot}$, $\mathcal I (c_0)$ will be $\bf{0}$ and $\mathcal
I(c_1)$ will be $\bf 1$. So $\langle \ba , \mathcal I \rangle$ is an
example of a model for the language described by
$\{ R_0 , F_1 , F_2 , c_0 ,c_1 \}$.
\end{rem}
We now wish to show how to use formulas to express mathematical statements
about elements of a model. We first need to see how to interpret a term
in a model.
\begin{definition}
\index{$t[x_{0}, \dots ,x_{q}]$}%
The value $t[x_{0}, \dots ,x_{q}]$ of a term
$t(v_{0}, \dots , v_{q})$ at $x_{0}, \dots , x_{q}$ in the
universe $\ba$ of the model
$\mathfrak{A}$ is defined as follows:
\begin{enumerate}
\item if $t$ is $v_{i}$ then $t[x_{0}, \cdots , x_{q}]$ is $x_{i}$,
\item if t is the constant symbol c, then $t[x_{0}, \dots , x_{q}] $ is
$\mathcal{I}(c)$,
the interpretation of $c$ in $\mathbf{A}$,
\item if $t$ is $F(t_{1} \dots t_{m})$ where $F$ is an m-placed
function symbol and $t_{1}, \dots ,t_{m}$ are terms, then $t[x_{0}, \dots
, x_{q}]$ is $G(t_{1}[x_{0}, \dots ,x_{q}], \dots , t_{m}[x_{0}, \dots
,x_{q}])$
where $G $ is the m-placed function $ \mathcal{I}(F)$, the
interpretation
of $F$ in $\mathbf{A}$.
\end{enumerate}
\end{definition}
\begin{definition}
\index{model!satisfies}%
Suppose $\mathfrak{A}$ is a model for a language
$\mathcal{L}$. The sequence \\
$x_{0}, \dots ,x_{q}$ of elements of $\ba$ \emph{satisfies} the
formula $\varphi (v_{0} , \dots ,v_{q})$ all of whose free and bound
variables are among $v_{0}, \dots , v_{q}$, in the model $\mathfrak{A}$,
written $\mathfrak{A} \models \varphi [x_{0} , \dots ,x_{q}] $ provided
we have:
\begin{enumerate}
\item if $\varphi(v_{0}, \dots ,v_{q})$ is the formula
$(t_{1} = t_{2})$, then
\[
\mathfrak{A} \models (t_{1} = t_{2})[x_{0}, \dots , x_{q}] \mbox{
means that } t_{1}[x_{0}, \dots ,x_{q}] \mbox{ equals } t_{2}[x_{0},
\dots ,x_{q}] \mbox{,}
\]
\item if $\varphi (v_{0}, \dots ,v_{q})$ is the formula
$(R(t_{1} \dots t_{n}))$ where $R$ is an n-placed relation symbol, then
\[ \mathfrak{A} \models (R(t_{1} \dots t_{n}))[x_{0} , \dots , x_{q}]
\mbox{ means }
S(t_{1}[x_{0}, \dots ,x_{q}], \dots , t_{n}[x_{0}, \dots ,x_{q}]) \]
where $S$ is the n-placed relation $\mathcal{I}(R)$, the
interpretation of $R$ in $\mathbf{A}$,
\item if $\varphi$ is $( \neg \theta ) $, then
\[
\mathfrak{A} \models \varphi [x_{0}, \dots ,x_{q}]
\mbox{ means not } \mathfrak{A} \models \theta[x_{0}, \dots ,x_{q}]
\mbox{,}
\]
\item if $\varphi$ is $( \theta \wedge \psi)$, then
\[
\mathfrak{A} \models \varphi [x_{0}, \dots ,x_{q} ] \mbox{ means both }
\mathfrak{A} \models \theta [x_{0} , \dots , x_{q}] \mbox{ and }
\mathfrak{A} \models \psi [x_{0}, \dots x_{q}] \mbox{,} \]
\item if $\varphi$ is $(\theta \vee \psi)$ then
\[
\mathfrak{A} \models \varphi [x_{0} ,\dots ,x_{q}] \mbox{ means either }
\mathfrak{A} \models \theta [x_{0}, \dots , x_{q}] \mbox{ or }
\mathfrak{A} \models \psi [x_{0}, \dots , x_{q}] \mbox{,} \]
%6
\item if $\varphi $ is $( \theta \to \psi) $ then
\[
\mathfrak{A} \models \varphi [x_{0} ,\dots ,x_{q}] \mbox{ means that }
\mathfrak{A} \models \theta [x_{0}, \dots , x_{q}] \mbox{ implies }
\mathfrak{A} \models \psi [x_{0}, \dots , x_{q}] \mbox{,} \]
\item if $\varphi $ is $( \theta \leftrightarrow \psi) $ then
\[
\mathfrak{A} \models \varphi [x_{0} ,\dots ,x_{q}] \mbox{ means that }
\mathfrak{A} \models \theta [x_{0}, \dots , x_{q}] \mbox{ iff }
\mathfrak{A} \models \psi [x_{0}, \dots , x_{q}] \mbox{,} \]
%8
\item if $\varphi$ is $\forall v_{i} \theta$, then
\[ \mathfrak{A} \models \varphi [x_{0} , \dots , x_{q}] \mbox{ means for
every } x \in \mathbf{A}, \mathfrak{A} \models \theta [x_{0}, \dots ,
x_{i-1}, x, x_{i+1} , \dots , x_{q}] \mbox{,} \]
%9
\item if $\varphi$ is $\exists v_{i} \theta$, then
\[ \mathfrak{A} \models \varphi [x_{0} , \dots , x_{q}] \mbox{ means for
some } x \in \mathbf{A}, \mathfrak{A} \models \theta [x_{0}, \dots ,
x_{i-1}, x, x_{i+1} , \dots , x_{q}]. \]
\end{enumerate}
\end{definition}
\begin{exercise} Each of the formulas of Example \ref{X:form} is
satisfied in any model $\ma$ for any language $\lan$ by any (long
enough) sequence $ x_0 , x_1 , \dots , x_q $
of $\ba$. This is where you test your solution to
Exercise~\ref{E:recon}, especially with respect to the term and formula from Example \ref{X:term}.
\end{exercise}
We now prove two lemmas which show that the preceding concepts are
well-defined. In the first one, we see that the value of a term only
depends upon the values of the variables which actually occur in the
term. In this lemma the equal sign $=$ is used, not as a logical
symbol in the formal sense, but in its usual sense to denote equality
of mathematical objects --- in this case, the values of terms, which
are elements of the universe of a model.
\begin{lemma}\label{L:zippy}
Let $\mathfrak{A}$ be a model for $\mathcal{L}$ and let
$t(v_{0}, \dots ,v_{p})$ be a term of $\mathcal{L}$. Let $x_{0} , \dots ,
x_{q}$ and $y_{0} , \dots, y_{r}$ be sequences from $\mathbf{A}$
such that $p \leq q$ and $p \leq r$, and let $x_{i}= y_{i}$ whenever
$v_{i}$ actually occurs in $t(\vnot{p})$. Then \[ t[x_{0}, \dots ,x_{q}] =
t[y_{0},
\dots , y_{r}] \].
\end{lemma}
\begin{proof} We use induction on the complexity of the term $t$.
\begin{enumerate}
\item If $t$ is $v_i$ then $x_i=y_i$ and so we have
\[t[\xnot{q}]=x_i=y_i=t[\ynot{r}] \mbox{ since } p\leq q \mbox{ and } p
\leq r. \]
\item If $t$ is the constant symbol $c$, then
\[t[\xnot{q}] = \mathcal I (c) = t[\ynot{r}] \]
where $\mathcal I (c) $ is the interpretation of $c$ in $\ba$.
\item If $t$ is $F(t_{1} \dots t_{m})$ where $F$ is an m-placed
function symbol, $t_{1}, \dots ,t_{m}$ are terms and $\mathcal I (F)
= G$, then \\
$t[x_{0}, \dots
, x_{q}]=G(t_{1}[x_{0}, \dots ,x_{q}], \dots , t_{m}[x_{0}, \dots
,x_{q}])$ and \\
$t[y_{0}, \dots
, y_{r}]=G(t_{1}[y_{0}, \dots ,y_{r}], \dots , t_{m}[y_{0}, \dots
,y_{r}])$. \\
By the induction hypothesis we have that $t_i [\xnot{q}] = t_i [
\ynot{r}] $ for $ 1
\leq i
\leq m$ since $t_1, \dots , t_m$ have all their variables among $\{
\vnot{p} \} $. So we have $t[ \xnot{q} ] = t [ \ynot{r} ] $.
\end{enumerate}
\end{proof}
In the next lemma the equal sign $=$ is used in both senses --- as a
formal logical symbol in the formal language $\lan$ and also to denote
the usual equality of mathematical objects. This is common practice
where the context allows the reader to distinguish the two usages of
the same symbol. The lemma confirms that satisfaction of a formula
depends only upon the values of its free variables.
\begin{lemma}\label{L:sat} Let $\ma$ be a model for $\lan$ and $\varphi$
a formula of
$\lan$, all of whose free and bound variables occur among $\vnot{p}$.
Let $\xnot{q}$ and $\ynot{r}$ ($q,r \geq p $) be two sequences such
that
$x_i$ and $y_i$ are equal for all $i$ such that $v_i$ occurs
free in $\varphi$. Then \[ \amodphi [ \xnot{q}] \mbox{ iff } \ma \models
\varphi [ \ynot{r} ] \]
\end{lemma}
\begin{proof} Let $\ma$ and $\lan$ be as above. We prove the lemma by
induction on the complexity of $\varphi$.
\begin{enumerate}
\item If $\varphi(v_{0}, \dots ,v_{p})$ is the formula $(t_{1} = t_{2})$, then we use Lemma \ref{L:zippy} to get:
\[ \begin{aligned}
\mathfrak{A} \models (t_{1} = t_{2})[x_{0}, \dots , x_{q}] &
\mbox{ iff } t_{1}[x_{0}, \dots ,x_{q}] = t_{2}[x_{0}, \dots ,x_{q}]\\
%
& \mbox{ iff }
t_{1}[y_{0}, \dots ,y_{r}] = t_{2}[y_{0}, \dots ,y_{r}]\\
%
& \mbox{ iff } \mathfrak{A} \models (t_{1} = t_{2})[y_{0}, \dots
, y_{r}].
\end{aligned} \]
\item If $\varphi (v_{0}, \dots ,v_{p})$ is the formula
$(R(t_{1} \dots t_{n})) $ where $R$ is an n-placed relation symbol
with interpretation $S$, then
again by Lemma \ref{L:zippy}, we get:
\[ \begin{aligned}
\mathfrak{A} \models (R(t_{1} \dots t_{n}))[x_{0} , \dots , x_{q}]
& \mbox{ iff } S(t_{1}[x_{0}, \dots ,x_{q}], \dots , t_{n}[x_{0}, \dots
,x_{q}]) \\
& \mbox{ iff } S(t_{1}[y_{0}, \dots ,y_{r}], \dots , t_{n}[y_{0}, \dots
,y_{r}]) \\
& \mbox{ iff } \ma \models R ( t_1 \dots t_n ) [ \ynot{r} ].
\end{aligned} \]
\item If $\varphi$ is $( \neg \theta ) $, the inductive hypothesis
gives that the lemma is true for $\theta$. So,
\[ \begin{aligned}
\mathfrak{A} \models \varphi [x_{0}, \dots ,x_{q}]
& \mbox{ iff not } \mathfrak{A} \models \theta[x_{0}, \dots ,x_{q}] \\
& \mbox{ iff not } \mathfrak{A} \models \theta[y_{0}, \dots ,y_{r}] \\
& \mbox{ iff } \mathfrak{A} \models \varphi [y_{0}, \dots ,y_{r}].
\end{aligned} \]
\item If $\varphi$ is $( \theta \wedge \psi)$, then using the inductive
hypothesis on $\theta$ and $\psi$ we get
\[ \begin{aligned}
\mathfrak{A} \models \varphi [x_{0}, \dots ,x_{q} ]
&\mbox{ iff both }
\mathfrak{A} \models \theta [x_{0} , \dots , x_{q}] \mbox{ and }
\mathfrak{A} \models \psi [x_{0}, \dots x_{q}] \\
&\mbox{ iff both }
\mathfrak{A} \models \theta [y_{0} , \dots , y_{r}] \mbox{ and }
\mathfrak{A} \models \psi [y_{0}, \dots y_{r}] \\
& \mbox{ iff } \mathfrak{A} \models \varphi [y_{0}, \dots ,y_{r} ].
\end{aligned} \]
\item If $\varphi$ is $(\theta \vee \psi)$ then
\[ \begin{aligned}
\mathfrak{A} \models \varphi [x_{0} ,\dots ,x_{q}] & \mbox{ iff either }
\mathfrak{A} \models \theta [x_{0}, \dots , x_{q}] \mbox{ or }
\mathfrak{A} \models \psi [x_{0}, \dots , x_{q}] \\
& \mbox{ iff either }
\mathfrak{A} \models \theta [y_{0}, \dots , y_{r}] \mbox{ or }
\mathfrak{A} \models \psi [y_{0}, \dots , y_{r}] \\
& \mbox{ iff } \mathfrak{A} \models \varphi [y_{0} ,\dots ,y_{r}].
\end{aligned} \]
%6
\item If $\varphi $ is $( \theta \to \psi) $ then
\[ \begin{aligned}
\mathfrak{A} \models \varphi [x_{0} ,\dots ,x_{q}] & \mbox{ iff }
\mathfrak{A} \models \theta [x_{0}, \dots , x_{q}] \mbox{ implies }
\mathfrak{A} \models \psi [x_{0}, \dots , x_{q}] \\
& \mbox{ iff }
\mathfrak{A} \models \theta [y_{0}, \dots , y_{r}] \mbox{ implies }
\mathfrak{A} \models \psi [y_{0}, \dots , y_{r}] \\
& \mbox{ iff } \mathfrak{A} \models \varphi [y_{0} ,\dots ,y_{r}] .
\end{aligned} \]
\item If $\varphi $ is $( \theta \leftrightarrow \psi) $ then
\[ \begin{aligned}
\mathfrak{A} \models \varphi [x_{0} ,\dots ,x_{q}] & \mbox{ iff we have }
\mathfrak{A} \models \theta [x_{0}, \dots , x_{q}] \mbox{ iff }
\mathfrak{A} \models \psi [x_{0}, \dots , x_{q}] \\
& \mbox{ iff we have }
\mathfrak{A} \models \theta [y_{0}, \dots , y_{r}] \mbox{ iff }
\mathfrak{A} \models \psi [y_{0}, \dots , y_{r}] \\
& \mbox{ iff } \mathfrak{A} \models \varphi [y_{0} ,\dots ,y_{r}].
\end{aligned} \]
%8
\item If $\varphi$ is $(\forall v_{i}) \theta$, then
\[\begin{aligned} \mathfrak{A} \models \varphi [x_{0} , \dots , x_{q}]
&\mbox{ iff for
every } z \in \mathbf{A}, \mathfrak{A} \models \theta [x_{0}, \dots ,
x_{i-1}, z, x_{i+1} , \dots , x_{q}]\\
&\mbox{ iff for every } z \in \ba, \ma \models \theta [\ynot{i-1}, z ,
y_{i+1}, \dots , y_r] \\
&\mbox{ iff } \ma \models \varphi [\ynot{r}] .\\
\end{aligned} \]
The inductive hypothesis uses the sequences $ x_0, \dots ,
x_{i-1}, z, x_{i+1}, \dots , x_{q}$ and $ y_0 , \dots , y_{i-1} , z,
y_{i+1} , \dots , y_r $ with the formula $\theta$.
%9
\item If $\varphi$ is $(\exists v_{i}) \theta$, then
\[ \begin{aligned}\mathfrak{A} \models \varphi [x_{0} , \dots ,
x_{q}] &\mbox{ iff for some } z \in \mathbf{A}, \mathfrak{A} \models
\theta
[x_{0}, \dots ,x_{i-1}, z, x_{i+1} , \dots , x_{q}] \\
&\mbox{ iff for some } z \in \ba, \ma \models \theta
[\ynot{i-1},z,y_{i+1}, \dots , y_r]\\
&\mbox{ iff } \ma \models \varphi [\ynot{r}]. \\
\end{aligned} \]
The inductive hypothesis uses the sequences $ x_0, \dots ,
x_{i-1}, z, x_{i+1} , \dots , x_{q}$ and $ y_0 , \dots , y_{i-1} , z,
y_{i+1} , \dots , y_r $ with the formula $\theta$.
\end{enumerate}
\end{proof}
\begin{definition}
\index{sentence}%
A \emph{sentence} is a formula with no free
variables.
\end{definition}
If $\varphi$ is a sentence, we can write
$\mathfrak{A} \models \varphi$
without any mention of a sequence from $\mathbf{A}$ since by the
previous lemma, it doesn't matter which sequence from $\ba$ we use. In
this case we say: \begin{itemize}
\item $\mathfrak{A}$ \emph{satisfies} $\varphi$
\item or $\mathfrak{A}$ is a \emph{model} of $\varphi$
\item or $\varphi$ \emph{holds} in $\mathfrak{A}$
\item or $\varphi$ is \emph{true} in $\mathfrak{A}$
\end{itemize}
If $\varphi$ is a sentence of $\lan$, we write
$\models \varphi$ to mean that $\ma \models \varphi$ for every model
$\ma$ for $\lan$. Intuitively then, $\models \varphi$ means that
$\varphi$ is true under any relevant interpretation (model for $\lan$).
Alternatively, no relevant example (model for $\lan$) is a
counterexample to $\varphi$ --- so $\varphi $ is true.
\begin{lemma}\label{L:altform} Let $\varphi(v_{0}, \dots ,v_{q})$ be a
formula
of the
language $\mathcal{L}$. There is another formula $\varphi' (v_{0},
\dots ,v_{q})$ of $\mathcal{L}$ such that
\begin{enumerate}
\item $\varphi'$ has exactly the same free and bound occurrences of
variables as $\varphi$.
\item $\varphi'$ can possibly contain $\neg$,
$\wedge$ and
$\exists$ but no other connective or quantifier.
\item $\models ( \forall v_{0}) \dots (\forall
v_{q}) (\varphi
\leftrightarrow \varphi' )$
\end{enumerate}
\end{lemma}
\begin{exercise} Prove the above lemma by induction on the complexity
of $\varphi$. As a reward, note that this lemma can be used to shorten future proofs by induction on complexity of formulas.
\end{exercise}
\addcontentsline{toc}{section}{Prenex Normal Form}
\begin{definition}
\index{prenex normal form}%
A formula $\varphi $ is said to be in
\emph{prenex
normal form} whenever
\begin{itemize}
\item[(1)] there are no quantifiers occurring in $\varphi $, or
\item[(2)] $\varphi $ is $(\exists v_{i}) \psi$ where $\psi$ is in prenex normal
form and $v_{i}$ does not occur bound in $\psi$, or
\item[(3)] $\varphi $ is $(\forall v_{i}) \psi$ where $\psi$ is in prenex normal
form and $v_{i}$ does not occur bound in $\psi$.
\end{itemize}
\end{definition}
\begin{rem}
If $\varphi $ is in prenex normal form, then no variable occurring in $\varphi $ occurs both free and bound and no bound variable occurring in $\varphi $ is bound by more than one quantifier.
In the written order, all of the quantifiers precede all of the connectives.
\end{rem}
\begin{lemma}\label{L:prenex} Let $\varphi (v_{0} , \dots , v_{p}) $
be any formula
of a language $\mathcal{L} $. There is a
formula $\varphi^* $ of $\mathcal{L} $ which has the following
properties:
\begin{enumerate}
\item $\varphi^* $ is in prenex normal form
\item $\varphi $ and $\varphi^* $ have the same free occurrences of
variables, and
\item $\models (\forall v_{0}) \dots (\forall v_{p})(\varphi
\leftrightarrow \varphi^* )$
\end{enumerate}
\end{lemma}
\begin{exercise} Prove this lemma by induction on the complexity of
$\varphi$.
\end{exercise}
There is a notion of rank on prenex formulas --- the number of
alternations of quantifiers. The usual formulas of elementary
mathematics have
prenex rank $0$, i.e. no alternations of quantifiers. For example: \[
(\forall x) ( \forall y) ( 2 xy \leq x^2 + y^2) . \]
However, the $\epsilon - \delta$ definition of a limit of a function
has prenex rank 2 and is much more difficult for students to comprehend
at first sight: \[ (\forall \epsilon ) (\exists \delta ) (\forall x ) ( ( 0 <
\epsilon \wedge 0 < | x-a| < \delta) \to | F (x) - L | < \epsilon). \]
A formula of prenex rank 4 would make any mathematician look twice.
\chapter{Notation and Examples}
Although the formal notation for
formulas is precise, it can become cumbersome and difficult to read.
Confident that the
reader would be able, if necessary, to put formulas into their formal
form, we will
relax our formal behaviour. In particular,
we will write formulas any way we want using appropriate symbols
for variables, constant symbols, function and relation symbols. We
will omit
parentheses or add them for clarity. We will use
binary
function and relation symbols between the arguments rather than in
front as is the usual case
for ``plus'', ``times'' and ``less than''.
Whenever a language $\lan$ has only finitely many relation, function and
constant symbols we often write, for example: \[ \lan = \{ < , R_0 , + ,
F_1 , c_0 , c_1 \} \] omitting explicit mention of the logical symbols
(including the infinitely many variables) which are always in $\lan$.
Correspondingly we may denote a model $\ma$ for $\lan$ as: \[ \ma =
\langle \ba , \pmb{<}, \bf{S}_{0} , \pmb{+}, \bf{G}_{1} ,
\bf{a}_{0} ,\bf{a}_{1} \rangle \]
where the interpretations of the symbols in the language $\lan$ are
given by
$\mathcal I (<) = \; \pmb{<}$, $\mathcal I (R_0) = \bf{S_0}$,
$\mathcal
I (+) = \; \pmb{+}$ , $ \mathcal I (F_1) = \bf{G}_{1}$, $ \mathcal{I}
(c_0)
= \bf{a}_{0} $ and $ \mathcal I (c_1) = \bf{a_1} $.
\begin{examples}\label{X:real}
\index{ $\langle \mathbb R ,\pmb{<} , \pmb{+} ,\mathbf{\cdot}
, \mathbf{0}, \mathbf{1} \rangle $}%
\index{ $\langle \mathbb Q ,\pmb{<} , \pmb{+} ,\mathbf{\cdot}
, \mathbf{0}, \mathbf{1} \rangle $}%
\index{ $\langle \mathbb C , \pmb{+} ,\mathbf{\cdot}
, \mathbf{0}, \mathbf{1} \rangle $}%
\index{real numbers}%
\index{rational numbers}%
\index{complex}%
$\mathfrak R = \langle \mathbb R , \pmb{<} , \pmb{+} , \mathbf{\cdot}
,\mathbf{0}, \mathbf{1} \rangle $ and
$\mathfrak Q = \langle \mathbb Q ,\pmb{<} ,\pmb{ +} ,
\mathbf{\cdot},\mathbf{0}, \mathbf{ 1} \rangle $, where $\mathbb R$
is the reals,
$\mathbb Q$ the
rationals ,
are models for the language $\lan = \{ <, + , \cdot , 0,1 \}$. Here
${<}$ is a binary relation symbol, ${ +}$ and ${\cdot}$
are binary function symbols, ${0}$ and
${ 1}$ are constant symbols whereas $\pmb{<}$, $\pmb{+} $,
$\mathbf{\cdot}$, $\mathbf{0}$, $\mathbf{1}$ are the well
known
relations, arithmetic functions and
constants.
Similarly, $\mathfrak C = \langle \mathbb C , \pmb{+} ,\mathbf{\cdot} ,
\mathbf{0} ,
\mathbf{1} \rangle $, where
$\mathbb C$ is the complex numbers, is a model for the language $\lan =
\{ +, \cdot, 0 , 1 \} $. Note the exceptions to the boldface
convention for these popular sets.
\end{examples}
\begin{examples}\label{X:theory} Here $\mathcal{L} = \{ < , + ,
\cdot ,
0 , 1 \}$, where $<$ is a binary relation symbol, $+$ and $\cdot$ are
binary function symbols
and $0$ and $1$ are constant symbols. The following
formulas are sentences.
\begin{enumerate}
%1
\item $(\forall x) \neg (x < x)$
%2
\item $(\forall x)( \forall y ) \neg (x <y \wedge y < x )$
%3
\item $(\forall x)(\forall y)(\forall z ) ( x < y \wedge y < z \to x
< z)$
%4
\item $(\forall x )(\forall y ) (x < y \vee y < x \vee x = y)$
%5
\item $(\forall x)(\forall y ) ( x < y \to (
\exists z) (x < z \wedge z < y))$
%6
\item $(\forall x ) (\exists y) ( x < y)$
%7
\item $(\forall x) (\exists y) (y < x)$
%8
\item $ (\forall x)(\forall y)(\forall z)( x+(y+z) = (x+y)+z
) $
\item $(\forall x) (x+0 =x)$
%10
\item $(\forall x) (\exists y) (x+y = 0 )$
%11
\item $ (\forall x) (\forall y) (x+y = y+x)$
\item $(\forall x)(\forall y)(\forall z) (x \cdot (y \cdot z)
= (x
\cdot y) \cdot z)$
\item $(\forall x) (x \cdot 1 = x )$
%17