diff --git a/content/model-theory/lindstrom/abstract-logics.tex b/content/model-theory/lindstrom/abstract-logics.tex index cd609810..e58c39e4 100644 --- a/content/model-theory/lindstrom/abstract-logics.tex +++ b/content/model-theory/lindstrom/abstract-logics.tex @@ -81,8 +81,8 @@ and $!E \in L(\Lang{L})$ there is a $!F \in L(\Lang{L})$ such that \[ - \Mod[L'](L){!F} = \Setabs{\Struct{M}}{\Expan{M}{a}} \in - \Mod[L](L){!E} \text{ for some } a \in \Domain{M} \}, + \Mod[L'](L){!F} = \Setabs{\Struct{M}}{\Expan{M}{a} \in + \Mod[L](L){!E} \text{ for some } a \in \Domain{M}}, \] where $\Lang{L'} = \Lang{L} \setminus \{c\}$ and $\Expan{M}{a}$ is the expansion of $\Struct{M}$ to $\Lang{L}$ assigning $a$ @@ -93,7 +93,7 @@ called the \emph{relativization} of $!E$ to $\Atom{R}{x, c_1, \dots c_n}$, such that for each !!{structure}~$\Struct{M}$: \[ - \Expan{M}{X, b_1, \ldots, b_n} \models_L !F) \text{ if and + \Expan{M}{X, b_1, \ldots, b_n} \models_L !F \text{ if and only if } \Struct{N} \models_L !E, \] where $\Struct{N}$ is the substructure of $\Struct{M}$ with !!{domain} diff --git a/content/second-order-logic/metatheory/introduction.tex b/content/second-order-logic/metatheory/introduction.tex index 2d6b84cf..f601e985 100644 --- a/content/second-order-logic/metatheory/introduction.tex +++ b/content/second-order-logic/metatheory/introduction.tex @@ -14,7 +14,7 @@ decidable, but at least it is axiomatizable. That is, there are proof systems for first-order logic which are sound and complete, i.e., they give rise to !!a{derivability} relation~$\Proves$ with the property -that for any set of !!{sentence}s~$\Gamma$ and !!{sentence}~$!Q$, +that for any set of !!{sentence}s~$\Gamma$ and !!{sentence}~$!A$, $\Gamma \Entails !A$ iff $\Gamma \Proves !A$. This means in particular that the validities of first-order logic are !!{computably enumerable}. There is a computable function~$f\colon \Nat \to diff --git a/content/second-order-logic/metatheory/second-order-arithmetic.tex b/content/second-order-logic/metatheory/second-order-arithmetic.tex index 34566515..63fdba24 100644 --- a/content/second-order-logic/metatheory/second-order-arithmetic.tex +++ b/content/second-order-logic/metatheory/second-order-arithmetic.tex @@ -33,7 +33,7 @@ consists of the first eight axioms above plus the (second-order) \emph{induction axiom}: \[ -\lforall[X][(X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif \lforall[x][X(x)]]. +\lforall[X][((X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif \lforall[x][X(x)])]. \] It says that if a subset~$X$ of the !!{domain} contains~$\Assign{\Obj{0}}{M}$ and with any~$x \in \Domain{M}$ also @@ -60,8 +60,8 @@ Now for inclusion in the other direction. Consider a variable assignment $s$ with $s(X) = N$. By assumption, \begin{align*} -\Sat{M}{\lforall[X][(X(\Obj 0) \land \lforall[x][(X(x) - \lif X(x'))]) \lif \lforall[x][X(x)]]}, & \text{ thus}\\ +\Sat{M}{\lforall[X][((X(\Obj 0) \land \lforall[x][(X(x) + \lif X(x'))]) \lif \lforall[x][X(x)])]}, & \text{ thus}\\ \Sat{M}{(X(\Obj 0) \land \lforall[x][(X(x) \lif X(x'))]) \lif \lforall[x][X(x)]}[s]. & \end{align*} diff --git a/content/second-order-logic/syntax-and-semantics/expressive-power.tex b/content/second-order-logic/syntax-and-semantics/expressive-power.tex index 4b980ef6..ce235577 100644 --- a/content/second-order-logic/syntax-and-semantics/expressive-power.tex +++ b/content/second-order-logic/syntax-and-semantics/expressive-power.tex @@ -13,7 +13,7 @@ Quantification over second-order variables is responsible for an immense increase in the expressive power of the language over that of first-order logic. Second-order existential quantification lets us -say that functions or relations with certain properties exists. In +say that functions or relations with certain properties exist. In first-order logic, the only way to do that is to specify a non-logical symbol (i.e., !!a{function} or !!{predicate}) for this purpose. Second-order universal quantification lets us say that all diff --git a/content/second-order-logic/syntax-and-semantics/inf-count.tex b/content/second-order-logic/syntax-and-semantics/inf-count.tex index 1d05e10a..abdf012b 100644 --- a/content/second-order-logic/syntax-and-semantics/inf-count.tex +++ b/content/second-order-logic/syntax-and-semantics/inf-count.tex @@ -50,8 +50,8 @@ $\Sat{M}{\lforall[x][\lforall[y][(\eq[u(x)][u(y)] \lif \eq[x][y])]] \land \lexists[y][\lforall[x][\eq/[y][u(x)]]]}[s]$ for some~$s$. If it does, $s(u)$ is !!a{injective} function, and some $y - \in \Domain{M}$ is not in the domain of~$s(u)$. Conversely, if there - is !!a{injective} $f\colon \Domain{M} \to \Domain{M}$ with $\dom{f} + \in \Domain{M}$ is not in the range of~$s(u)$. Conversely, if there + is !!a{injective} $f\colon \Domain{M} \to \Domain{M}$ with $\ran{f} \neq \Domain{M}$, then $s(u) = f$ is such a variable assignment. \end{proof} diff --git a/content/second-order-logic/syntax-and-semantics/satisfaction.tex b/content/second-order-logic/syntax-and-semantics/satisfaction.tex index 064bd801..80d2ae26 100644 --- a/content/second-order-logic/syntax-and-semantics/satisfaction.tex +++ b/content/second-order-logic/syntax-and-semantics/satisfaction.tex @@ -157,7 +157,7 @@ \liff \lnot \Atom{Y}{z})])}[\Subst{s}{N}{Y}]$. And that is the case for any $N \neq \emptyset$ (so that $\Sat{M}{\lexists[y][\Atom{Y}{y}]}[\Subst{s}{N}{Y}]$) and, as in the - previous example, $M = \Domain{M} \setminus s(X)$. In other words, + previous example, $N = \Domain{M} \setminus s(X)$. In other words, $\Sat{M}{\lexists[Y][(\lexists[y][\Atom{Y}{y}] \land \lforall[z][(\Atom{X}{z} \liff \lnot \Atom{Y}{z})])]}[s]$ iff $\Domain{M} \setminus s(X)$ is non-empty, i.e., $s(X) \neq diff --git a/content/second-order-logic/syntax-and-semantics/terms-formulas.tex b/content/second-order-logic/syntax-and-semantics/terms-formulas.tex index 6186a06c..5c81bdba 100644 --- a/content/second-order-logic/syntax-and-semantics/terms-formulas.tex +++ b/content/second-order-logic/syntax-and-semantics/terms-formulas.tex @@ -66,7 +66,7 @@ \begin{defn}[Second-order \usetoken{s}{formula}] The set of \emph{second-order !!{formula}s}~$\FrmSOL[L]$ of the language~$\Lang L$ is defined by adding to -\olref[fol][syn][frm]{defn:terms} the clauses +\olref[fol][syn][frm]{defn:formulas} the clauses \begin{enumerate} \item If $X$ is an $n$-place predicate variable and $t_1$, \dots, $t_n$ are second-order terms of~$\Lang L$, then