The Open Logic Text — accessible offline edition

Syntax of First-Order Logic — Source and provenance

Syntax of First-Order Logic

Source and provenance

All 10 authority files and all 1,380 lines are shown exactly and copied byte-for-byte. Reader corrections and all twenty-one bounded reader normalizations are disclosures only; the accepted projected text and authority source below are not altered. Open the exact accepted projected chapter transcript (SHA-256 b91e037b6b987f24a9ad518796ca475b936c645d3773c88af483d0d933524eac).

content/first-order-logic/syntax-and-semantics/syntax.tex

30 lines; SHA-256 75c0e56b3d2f9557e39b9006855f371e6c8f04e8ef9817affd70a793613930ab. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax
  4. \documentclass[../../../include/open-logic-chapter]{subfiles}
  6. \begin{document}
  8. \olchapter{fol}{syn}{Syntax of First-Order Logic}
  10. \olimport{intro-syntax}
  12. \olimport{first-order-languages}
  14. \olimport{terms-formulas}
  16. \olimport{unique-readability}
  18. \olimport{main-operator}
  20. \olimport{subformulas}
  22. \olimport{formation-sequences}
  24. \olimport{free-vars-sentences}
  26. \olimport{substitution}
  28. \OLEndChapterHook
  30. \end{document}

content/first-order-logic/syntax-and-semantics/intro-syntax.tex

33 lines; SHA-256 ba7dcce5f1e3340374ff693a1c22c5bf4ccb0c2709cd8c6d50474d4982f7cdfc. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax
  3. % Section: intro-syntax
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{syn}{itx}
  11. \olsection{Introduction}
  13. In order to develop the theory and metatheory of first-order logic, we
  14. must first define the syntax and semantics of its expressions. The
  15. expressions of first-order logic are terms and !!{formula}s. Terms
  16. are formed from !!{variable}s, !!{constant}s, and !!{function}s.
  17. !!^{formula}s, in turn, are formed from !!{predicate}s together with
  18. terms (these form the smallest, ``atomic'' !!{formula}s), and then
  19. from atomic !!{formula}s we can form more complex ones using logical
  20. connectives and quantifiers. There are many different ways to set
  21. down the formation rules; we give just one possible one. Other systems
  22. will chose different symbols, will select different sets of
  23. connectives as primitive, will use parentheses differently (or even not
  24. at all, as in the case of so-called Polish notation). What all
  25. approaches have in common, though, is that the formation rules define
  26. the set of terms and !!{formula}s \emph{inductively}. If done
  27. properly, every expression can result essentially in only one way
  28. according to the formation rules. The inductive definition resulting
  29. in expressions that are \emph{uniquely readable} means we can give
  30. meanings to these expressions using the same method---inductive
  31. definition.
  33. \end{document}

content/first-order-logic/syntax-and-semantics/first-order-languages.tex

159 lines; SHA-256 582ea4b3b243fe2ee4eb627630172f77f014d4f7d7c93cd13fdb2bb70844c447. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: first-order-languages
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{syn}{fol}
  11. \olsection{First-Order Languages}
  14. Expressions of first-order logic are built up from a basic vocabulary
  15. containing \emph{!!{variable}s}, \emph{!!{constant}s},
  16. \emph{!!{predicate}s} and sometimes \emph{!!{function}s}. From them,
  17. together with logical connectives, quantifiers, and punctuation
  18. symbols such as parentheses and commas, \emph{terms} and
  19. \emph{!!{formula}s} are formed.
  21. \begin{explain}
  22. Informally, !!{predicate}s are names for properties and relations,
  23. !!{constant}s are names for individual objects, and !!{function}s are
  24. names for mappings. These, except for the !!{identity}~$\eq$, are the
  25. \emph{non-logical symbols} and together make up a language. Any
  26. first-order language~$\Lang L$ is determined by its non-logical
  27. symbols. In the most general case, $\Lang L$ contains infinitely many
  28. symbols of each kind.
  29. \end{explain}
  31. In the general case, we make use of the following symbols in
  32. first-order logic:
  34. \begin{enumerate}
  35. \item Logical symbols
  36. \begin{enumerate}
  37. \item Logical connectives:
  38. \startycommalist
  39. \iftag{prvNot}{\ycomma $\lnot$ (negation)}{}%
  40. \iftag{prvAnd}{\ycomma $\land$ (conjunction)}{}%
  41. \iftag{prvOr}{\ycomma $\lor$ (disjunction)}{}%
  42. \iftag{prvIf}{\ycomma $\lif$ (!!{conditional})}{}%
  43. \iftag{prvIff}{\ycomma $\liff$ (!!{biconditional})}{}%
  44. \iftag{prvAll}{\ycomma $\lforall$ (universal quantifier)}{}%
  45. \iftag{prvEx}{\ycomma $\lexists$ (existential quantifier)}{}.
  46. \tagitem{prvFalse}{The propositional constant for !!{falsity}~$\lfalse$.}{}
  47. \tagitem{prvTrue}{The propositional constant for !!{truth}~$\ltrue$.}{}
  48. \item The two-place !!{identity}~$\eq$.
  49. \item A !!{denumerable}s set of !!{variable}s: $\Obj v_0$, $\Obj v_1$, $\Obj
  50. v_2$, \dots
  51. \end{enumerate}
  52. \item Non-logical symbols, making up the \emph{standard
  53. language} of first-order logic
  54. \begin{enumerate}
  55. \item A !!{denumerable}s set of $n$-place !!{predicate}s for each $n>0$: $\Obj
  56. A^n_0$, $\Obj A^n_1$, $\Obj A^n_2$, \dots
  57. \item A !!{denumerable}s set of !!{constant}s: $\Obj c_0$, $\Obj c_1$, $\Obj
  58. c_2$, \dots.
  59. \item A !!{denumerable}s set of $n$-place !!{function}s for each $n>0$:
  60. $\Obj f^n_0$, $\Obj f^n_1$, $\Obj f^n_2$, \dots
  61. \end{enumerate}
  62. \item Punctuation marks: (, ), and the comma.
  63. \end{enumerate}
  65. Most of our definitions and results will be formulated for the full
  66. standard language of first-order logic. However, depending on the
  67. application, we may also restrict the language to only a few
  68. !!{predicate}s, !!{constant}s, and !!{function}s.
  70. \begin{ex}
  71. The language~$\Lang L_A$ of arithmetic contains a single two-place
  72. !!{predicate}~$<$, a single !!{constant}~$\Obj 0$, one one-place
  73. !!{function}~$\prime$, and two two-place !!{function}s~$+$ and~$\times$.
  74. \end{ex}
  76. \begin{ex}
  77. The language of set theory~$\Lang L_Z$ contains only the single
  78. two-place !!{predicate}~$\in$.
  79. \end{ex}
  81. \begin{ex}
  82. The language of orders~$\Lang L_\le$ contains only the two-place
  83. !!{predicate}~$\le$.
  84. \end{ex}
  86. Again, these are conventions: officially, these are just aliases,
  87. e.g., $<$, $\in$, and $\le$ are aliases for $\Obj A^2_0$, $\Obj 0$ for
  88. $\Obj c_0$, $\prime$ for $\Obj f^1_0$, $+$ for $\Obj f^2_0$, $\times$ for
  89. $\Obj f^2_1$.
  91. \iftag{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}{%
  92. In addition to the primitive connectives and
  93. \iftag{notprvEx,notprvAll}{quantifier}{quantifiers} introduced
  94. above, we also use the following \emph{defined} symbols:
  95. \startycommalist
  96. \iftag{defNot}{\ycomma $\lnot$ (negation)}{}%
  97. \iftag{defAnd}{\ycomma $\land$ (conjunction)}{}%
  98. \iftag{defOr}{\ycomma $\lor$ (disjunction)}{}%
  99. \iftag{defIf}{\ycomma $\lif$ (!!{conditional})}{}%
  100. \iftag{defIff}{\ycomma $\liff$ (!!{biconditional})}{}%
  101. \iftag{defAll}{\ycomma $\lforall$ (universal quantifier)}{}%
  102. \iftag{defEx}{\ycomma $\lexists$ (existential quantifier)}{}%
  103. \iftag{defFalse}{\ycomma !!{falsity}~$\lfalse$}{}%
  104. \iftag{defTrue}{\ycomma !!{truth}~$\ltrue$}}{}.
  106. \begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}
  107. \begin{explain}
  108. A defined symbol is not officially part of the language, but is
  109. introduced as an informal abbreviation: it allows us to abbreviate
  110. formulas which would, if we only used primitive symbols, get quite
  111. long. This is obviously an advantage. The bigger advantage, however,
  112. is that proofs become shorter. If a symbol is primitive, it has to be
  113. treated separately in proofs. The more primitive symbols, therefore,
  114. the longer our proofs.
  115. \end{explain}
  116. \end{tagblock}
  118. % Alternate symbols
  120. \begin{intro}
  121. You may be familiar with different terminology and symbols than the
  122. ones we use above. Logic texts (and teachers) commonly use
  123. $\sim$, $\neg$, or~!\ for ``negation'', $\wedge$, $\cdot$, or $\&$
  124. for ``conjunction''. Commonly used symbols for the ``conditional'' or
  125. ``implication'' are $\rightarrow$, $\Rightarrow$, and $\supset$.
  126. \iftag{prvIff,defIff}{Symbols for ``biconditional,'' ``bi-implication,''
  127. or ``(material) equivalence'' are $\leftrightarrow$,
  128. $\Leftrightarrow$, and $\equiv$.}{}
  129. \iftag{prvFalse,defFalse}{The $\lfalse$ symbol is variously called
  130. ``falsity,'' ``falsum,'', ``absurdity,'' or ``bottom.''}{}
  131. \iftag{prvTrue,defTrue}{The $\ltrue$ symbol is variously called
  132. ``truth,'' ``verum,'' or ``top.''}{}
  134. It is conventional to use lower case letters (e.g., $a$, $b$, $c$) from
  135. the beginning of the Latin alphabet for !!{constant}s (sometimes called
  136. names), and lower case letters from the end (e.g., $x$, $y$, $z$) for
  137. !!{variable}s. Quantifiers combine with !!{variable}s, e.g., $x$;
  138. notational variations include $\forall x$, $(\forall x)$, $(x)$, $\Pi x$,
  139. $\bigwedge_x$ for the universal quantifier and $\exists x$, $(\exists
  140. x)$, $(Ex)$, $\Sigma x$, $\bigvee_x$ for the existential quantifier.
  141. \end{intro}
  143. \begin{explain}
  144. We might treat all the propositional operators and both quantifiers as
  145. primitive symbols of the language. We might instead choose a smaller
  146. stock of primitive symbols and treat the other !!{operator}s as
  147. defined. ``Truth functionally complete'' sets of Boolean operators
  148. include $\{ \lnot, \lor \}$, $\{ \lnot, \land \}$, and $\{ \lnot,
  149. \lif\}$---these can be combined with either quantifier for an
  150. expressively complete first-order language.
  152. You may be familiar with two other !!{operator}s: the Sheffer
  153. stroke~$|$ (named after Henry Sheffer), and Peirce's
  154. arrow~$\downarrow$, also known as Quine's dagger. When given their
  155. usual readings of ``nand'' and ``nor'' (respectively), these operators
  156. are truth functionally complete by themselves.
  157. \end{explain}
  159. \end{document}

content/first-order-logic/syntax-and-semantics/terms-formulas.tex

237 lines; SHA-256 0b607ce2324ca66b23b164684f4f35b127107b903bbbd567eb25e94c2ce70210. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: terms-formulas
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{syn}{frm}
  11. \olsection{Terms and \printtoken{P}{formula}}
  13. Once a first-order language~$\Lang L$ is given, we can define
  14. expressions built up from the basic vocabulary of~$\Lang L$. These
  15. include in particular \emph{terms} and \emph{!!{formula}s}.
  17. \begin{defn}[Terms]
  18. \ollabel{defn:terms}
  19. The set of \emph{terms}~$\Trm[L]$ of~$\Lang L$ is
  20. defined inductively by:
  21. \begin{enumerate}
  22. \item Every !!{variable} is a term.
  23. \item Every !!{constant} of~$\Lang L$ is a term.
  24. \item If $f$ is an $n$-place !!{function} and $t_1$, \dots, $t_n$
  25. are terms, then $\Atom{f}{t_1, \ldots, t_n}$ is a term.
  26. \tagitem{limitClause}{
  27. Nothing else is a term.}{}
  28. \end{enumerate}
  29. A term containing no !!{variable}s is a \emph{closed term}.
  30. \end{defn}
  32. \begin{explain}
  33. The !!{constant}s appear in our specification of the language and the
  34. terms as a separate category of symbols, but they could instead have
  35. been included as zero-place !!{function}s. We could then do without
  36. the second clause in the definition of terms. We just have to
  37. understand $\Atom{f}{t_1, \ldots, t_n}$ as just $f$ by itself if $n =
  38. 0$.
  39. \end{explain}
  41. \begin{defn}[Formulas]
  42. \ollabel{defn:formulas}
  43. The set of \emph{!!{formula}s}~$\Frm[L]$ of the language~$\Lang L$
  44. is defined inductively as follows:
  45. \begin{enumerate}
  46. \tagitem{prvFalse}{$\lfalse$ is an atomic !!{formula}.}{}
  48. \tagitem{prvTrue}{$\ltrue$ is an atomic !!{formula}.}{}
  50. \item If $R$ is an $n$-place !!{predicate} of~$\Lang L$ and $t_1$, \dots,
  51. $t_n$ are terms of~$\Lang L$, then $\Atom{R}{t_1,\ldots, t_n}$ is an
  52. atomic !!{formula}.
  54. \item If $t_1$ and $t_2$ are terms of~$\Lang L$, then $\Atom{\eq}{t_1, t_2}$
  55. is an atomic !!{formula}.
  57. \tagitem{prvNot}{If $!A$ is !!a{formula}, then $\lnot !A$ is
  58. !!a{formula}.}{}
  60. \tagitem{prvAnd}{If $!A$ and $!B$ are !!{formula}s, then $(!A \land
  61. !B)$ is !!a{formula}.}{}
  63. \tagitem{prvOr}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lor !B)$
  64. is !!a{formula}.}{}
  66. \tagitem{prvIf}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lif !B)$
  67. is !!a{formula}.}{}
  69. \tagitem{prvIff}{If $!A$ and $!B$ are !!{formula}s, then $(!A \liff !B)$
  70. is !!a{formula}.}{}
  72. \tagitem{prvAll}{If $!A$ is !!a{formula} and $x$ is !!a{variable},
  73. then $\lforall[x][!A]$ is !!a{formula}.}{}
  75. \tagitem{prvEx}{If $!A$ is !!a{formula} and $x$ is !!a{variable},
  76. then $\lexists[x][!A]$ is !!a{formula}.}{}
  78. \tagitem{limitClause}{Nothing else is !!a{formula}.}{}
  79. \end{enumerate}
  80. \end{defn}
  82. \begin{explain}
  83. The definitions of the set of terms and that of !!{formula}s are
  84. \emph{inductive definitions}. Essentially, we construct the set of
  85. !!{formula}s in infinitely many stages. In the initial stage, we
  86. pronounce all atomic formulas to be formulas; this corresponds to the
  87. first few cases of the definition, i.e., the cases for
  88. \iftag{prvTrue}{$\ltrue$, }{}%
  89. \iftag{prvFalse}{$\lfalse$, }{}%
  90. $\Atom{R}{t_1,\dots,t_n}$ and $\Atom{\eq}{t_1,t_2}$. ``Atomic
  91. !!{formula}'' thus means any !!{formula} of this form.
  93. The other cases of the definition give rules for constructing new
  94. !!{formula}s out of !!{formula}s already constructed. At the second
  95. stage, we can use them to construct !!{formula}s out of atomic
  96. !!{formula}s. At the third stage, we construct new formulas from the
  97. atomic formulas and those obtained in the second stage, and so on. A
  98. !!{formula} is anything that is eventually constructed at such a
  99. stage, and nothing else.
  100. \end{explain}
  102. By convention, we write $\eq$ between its arguments and leave out the
  103. parentheses: $\eq[t_1][t_2]$ is an abbreviation for
  104. $\Atom{\eq}{t_1,t_2}$. Moreover, $\lnot \Atom{\eq}{t_1,t_2}$ is
  105. abbreviated as $\eq/[t_1][t_2]$. When writing a formula $(!B \ast !C)$
  106. constructed from $!B$, $!C$ using a two-place connective~$\ast$, we
  107. will often leave out the outermost pair of parentheses and write
  108. simply~$!B \ast !C$.
  110. \begin{intro}
  111. Some logic texts require that the !!{variable}~$x$ must occur in~$!A$
  112. in order for
  113. \iftag{prvEx}{$\lexists[x][!A]$ }{}%
  114. \iftag{notprvEx,notprvAll}{}{and }%
  115. \iftag{prvAll}{$\lforall[x][!A]$ }{}%
  116. to count as
  117. \iftag{notprvEx,notprvAll}{!!a{formula}}{!!{formula}s}.
  118. Nothing bad happens if you don't require this, and it makes things
  119. easier.
  120. \end{intro}
  122. \begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}
  123. \begin{defn}
  124. Formulas constructed using the defined operators are to be understood
  125. as follows:
  127. \begin{tagenumerate}{defTrue,defFalse,defNot,defOr,defAnd,defIf,defIff,defEx,defAll}
  129. \tagitem{defTrue}{$\ltrue$ abbreviates
  130. \iftag{prvFalse}{$\lnot\lfalse$}{$(!A \lor \lnot !A)$ for some
  131. fixed atomic !!{formula}~$!A$}.}{}
  133. \tagitem{defFalse}{$\lfalse$ abbreviates
  134. \iftag{prvTrue}{$\lnot\ltrue$}{$(!A \land \lnot !A)$ for some
  135. fixed atomic !!{formula}~$!A$}.}{}
  137. \tagitem{defNot}{$\lnot !A$ abbreviates $!A \lif \lfalse$.}{}
  139. \tagitem{defOr}{$!A \lor !B$ abbreviates
  140. \iftag{prvAnd}{$\lnot(\lnot !A \land \lnot !B)$}{$\lnot !A \lif
  141. !B$}.}{}
  143. \tagitem{defAnd}{$!A \land !B$ abbreviates
  144. \iftag{prvOr}{$\lnot(\lnot !A \lor \lnot !B)$}{$\lnot (!A \lif
  145. \lnot !B)$}.}{}
  147. \tagitem{defIf}{$!A \lif !B$ abbreviates
  148. \iftag{prvOr}{$\lnot !A \lor !B)$}{$\lnot (!A \land \lnot !B)$}.}{}
  150. \tagitem{defIff}{$!A \liff !B$ abbreviates $(!A \lif !B) \land (!B
  151. \lif !A)$.}{}
  153. \tagitem{defAll}{$\lforall[x][!A]$ abbreviates $\lnot\lexists[x][\lnot !A]$.}{}
  155. \tagitem{defEx}{$\lexists[x][!A]$ abbreviates $\lnot\lforall[x][\lnot !A]$.}{}
  156. \end{tagenumerate}
  157. \end{defn}
  158. \end{tagblock}
  160. If we work in a language for a specific application, we will often
  161. write two-place !!{predicate}s and !!{function}s between the
  162. respective terms, e.g., $t_1 < t_2$ and $(t_1 + t_2)$ in the language
  163. of arithmetic and $t_1 \in t_2$ in the language of set theory. The
  164. successor function in the language of arithmetic is even written
  165. conventionally \emph{after} its argument:~$t'$. Officially, however,
  166. these are just conventional abbreviations for $\Atom{\Obj A^2_0}{t_1, t_2}$,
  167. $\Obj f^2_0(t_1, t_2)$, $\Atom{\Obj A^2_0}{t_1, t_2}$ and $f^1_0(t)$,
  168. respectively.
  170. \begin{defn}[Syntactic identity]
  171. The symbol $\ident$ expresses syntactic identity between strings of
  172. symbols, i.e., $!A \ident !B$ iff $!A$ and $!B$ are strings of symbols
  173. of the same length and which contain the same symbol in each place.
  174. \end{defn}
  176. The $\ident$ symbol may be flanked by strings obtained by
  177. concatenation, e.g., $!A \ident (!B \lor !C)$ means: the string of
  178. symbols~$!A$ is the same string as the one obtained by concatenating
  179. an opening parenthesis, the string $!B$, the $\lor$ symbol, the
  180. string~$!C$, and a closing parenthesis, in this order. If this is the
  181. case, then we know that the first symbol of~$!A$ is an opening
  182. parenthesis, $!A$ contains $!B$ as a substring (starting at the second
  183. symbol), that substring is followed by~$\lor$, etc.
  185. As terms and !!{formula}s are built up from basic elements via inductive
  186. definitions, we can use the following induction principles to prove
  187. things about them.
  189. \begin{lem}[\emph{Principle of induction on terms}]
  190. \ollabel{lem:trmind}
  191. Let $\Lang L$ be a first-order language.
  192. If some property~$P$ is such that
  193. %
  194. \begin{enumerate}
  195. \item it holds for every !!{variable}~$v$,
  196. %
  197. \item it holds for every !!{constant}~$a$ of~$\Lang L$, and
  198. %
  199. \item it holds for $f(t_1,\dotsc,t_n)$ whenever it holds for
  200. $t_1$,~\dots, $t_n$ and $f$~is an $n$-place
  201. !!{function} of~$\Lang L$
  202. \end{enumerate}
  203. (assuming $t_1$,~\dots, $t_n$ are terms of~$\Lang{L}$),
  204. then $P$ holds for every term in~$\Trm[L]$.
  205. \end{lem}
  207. \begin{prob}
  208. Prove \olref[fol][syn][frm]{lem:trmind}.
  209. \end{prob}
  211. \begin{lem}[\emph{Principle of induction on !!{formula}s}]
  212. \ollabel{thm:frmind}
  213. Let $\Lang L$ be a first-order language.
  214. If some property~$P$ holds for all the atomic !!{formula}s
  215. and is such that
  216. %
  217. \begin{enumerate}
  218. \tagitem{prvNot}{it holds for $\lnot !A$ whenever it
  219. holds for~$!A$;}{}
  220. \tagitem{prvAnd}{it holds for $(!A \land !B)$
  221. whenever it holds for $!A$ and~$!B$;}{}
  222. \tagitem{prvOr}{it holds for $(!A \lor !B)$
  223. whenever it holds for $!A$ and~$!B$;}{}
  224. \tagitem{prvIf}{it holds for $(!A \lif !B)$
  225. whenever it holds for $!A$ and~$!B$;}{}
  226. \tagitem{prvIff}{it holds for $(!A \liff !B)$
  227. whenever it holds for $!A$ and~$!B$;}{}
  228. \tagitem{prvEx}{it holds for $\lexists[x][!A]$
  229. whenever it holds for~$!A$;}{}
  230. \tagitem{prvAll}{it holds for $\lforall[x][!A]$
  231. whenever it holds for~$!A$;}{}
  232. \end{enumerate}
  233. (assuming $!A$ and $!B$ are !!{formula}s of~$\Lang{L}$),
  234. then $P$ holds for all formulas in~$\Frm[L]$.
  235. \end{lem}
  237. \end{document}

content/first-order-logic/syntax-and-semantics/unique-readability.tex

203 lines; SHA-256 f2ad2961312808ef6c8dedc884c9f8e00a2be9ef993cfb7be748a9d253d84e66. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: unique-readability
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{syn}{unq}
  11. \olsection{Unique Readability}
  13. \begin{explain}
  14. The way we defined !!{formula}s guarantees that every !!{formula} has
  15. a \emph{unique reading}, i.e., there is essentially only one way of
  16. constructing it according to our formation rules for !!{formula}s and
  17. only one way of ``interpreting'' it. If this were not so, we would
  18. have ambiguous !!{formula}s, i.e., !!{formula}s that have more than
  19. one reading or intepretation---and that is clearly something we want
  20. to avoid. But more importantly, without this property, most of the
  21. definitions and proofs we are going to give will not go through.
  23. Perhaps the best way to make this clear is to see what would happen if
  24. we had given bad rules for forming !!{formula}s that would not
  25. guarantee unique readability. For instance, we could have forgotten
  26. the parentheses in the formation rules for connectives, e.g., we might
  27. have allowed this:
  28. \begin{quote}
  29. If $!A$ and $!B$ are !!{formula}s, then so is $!A \lif !B$.
  30. \end{quote}
  31. Starting from an atomic formula $!D$, this would allow us to form $!D
  32. \lif !D$. From this, together with $!D$, we would get $!D \lif !D
  33. \lif !D$. But there are two ways to do this:
  34. \begin{enumerate}
  35. \item We take $!D$ to be $!A$ and $!D \lif !D$ to be $!B$.
  36. \item We take $!A$ to be $!D \lif !D$ and $!B$ is~$!D$.
  37. \end{enumerate}
  38. Correspondingly, there are two ways to
  39. ``read'' the !!{formula}~$!D \lif !D \lif !D$. It is of the form $!B
  40. \lif !C$ where $!B$ is $!D$ and $!C$ is $!D \lif !D$, but \emph{it is
  41. also} of the form $!B \lif !C$ with $!B$ being $!D \lif !D$ and $!C$
  42. being~$!D$.
  44. If this happens, our definitions will not always work. For instance,
  45. when we define the !!{main operator} of a formula, we say: in a
  46. formula of the form $!B \lif !C$, the !!{main operator} is the
  47. indicated occurrence of~$\lif$. But if we can match the formula $!D
  48. \lif !D \lif !D$ with $!B \lif !C$ in the two different ways mentioned
  49. above, then in one case we get the first occurrence of $\lif$ as the
  50. !!{main operator}, and in the second case the second occurrence. But
  51. we intend the !!{main operator} to be a \emph{function} of the
  52. !!{formula}, i.e., every !!{formula} must have exactly one !!{main
  53. operator} occurrence.
  54. \end{explain}
  56. \begin{lem}
  57. The number of left and right parentheses in !!a{formula}~$!A$ are
  58. equal.
  59. \end{lem}
  61. \begin{proof}
  62. We prove this by induction on the way $!A$ is constructed. This
  63. requires two things: (a) We have to prove first that all atomic
  64. formulas have the property in question (the induction basis). (b) Then
  65. we have to prove that when we construct new formulas out of given
  66. formulas, the new formulas have the property provided the old ones do.
  68. Let $l(!A)$ be the number of left parentheses, and $r(!A)$ the number
  69. of right parentheses in~$!A$, and $l(t)$ and $r(t)$ similarly the
  70. number of left and right parentheses in a term~$t$.
  72. \begin{prob}
  73. Prove that for any term~$t$, $l(t) = r(t)$.
  74. \end{prob}
  76. \begin{enumerate}
  77. \tagitem{prvFalse}{\indcase{!A}{\lfalse}{$\indfrm$ has $0$ left and $0$
  78. right parentheses.}}{}
  80. \tagitem{prvTrue}{\indcase{!A}{\ltrue}{$\indfrm$ has $0$ left and $0$
  81. right parentheses.}}{}
  83. \item \indcase{!A}{\Atom{R}{t_1,\dots,t_n}}{$l(\indfrm) = 1 + l(t_1) +
  84. \dots + l(t_n) = 1 + r(t_1) + \dots + r(t_n) = r(\indfrm)$. Here we
  85. make use of the fact, left as an exercise, that $l(t) = r(t)$ for
  86. any term~$t$.}
  88. \item \indcase{!A}{\eq[t_1][t_2]}{$l(\indfrm) = l(t_1) + l(t_2) =
  89. r(t_1) + r(t_2) = r(\indfrm)$.}
  91. \tagitem{prvNot}{\indcase{!A}{\lnot !B}{By induction hypothesis,
  92. $l(!B) = r(!B)$. Thus $l(\indfrm) = l(!B) = r(!B) =
  93. r(\indfrm)$.}}{}
  95. \item \indcase{!A}{(!B \ast !C)}{By induction hypothesis, $l(!B) =
  96. r(!B)$ and $l(!C) = r(!C)$. Thus $l(\indfrm) = 1 + l(!B) + l(!C) =
  97. 1 + r(!B) + r(!C) = r(\indfrm)$.}
  99. \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{By induction
  100. hypothesis, $l(!B) = r(!B)$. Thus, $l(\indfrm) = l(!B) = r(!B) =
  101. r(\indfrm)$.}}{}
  103. % Print case for \lexists if prvEx and not prvAll
  104. \tagitem{prvAll,notprvEx}{}{\indcase{!A}{\lexists[x][!B]}{By induction
  105. hypothesis, $l(!B) = r(!B)$. Thus, $l(\indfrm) = l(!B) = r(!B) =
  106. r(\indfrm)$.}}
  108. % Just say similarly if prvEx and prvAll
  109. \tagitem{notprvAll,notprvEx}{}{\indcase{!A}{\lexists[x][!B]}{Similarly.}}
  110. \end{enumerate}
  111. \end{proof}
  113. \begin{defn}[Proper prefix]
  114. A string of symbols $!B$ is a \emph{proper prefix} of a string of symbols~$!A$ if
  115. concatenating $!B$ and a non-empty string of symbols yields~$!A$.
  116. \end{defn}
  118. \begin{lem}\ollabel{lem:no-prefix}
  119. If $!A$ is !!a{formula}, and $!B$ is a proper prefix of $!A$, then
  120. $!B$ is not !!a{formula}.
  121. \end{lem}
  123. \begin{proof}
  124. Exercise.
  125. \end{proof}
  127. \begin{prob}
  128. Prove \olref[fol][syn][unq]{lem:no-prefix}.
  129. \end{prob}
  131. \begin{prop}
  132. \ollabel{prop:unique-atomic}
  133. If $!A$ is an atomic !!{formula}, then it satisfies one, and only one
  134. of the following conditions.
  135. \begin{enumerate}
  136. \tagitem{prvFalse}{$!A \ident \lfalse$.}{}
  137. \tagitem{prvTrue}{$!A \ident \ltrue$.}{}
  138. \item $!A \ident \Atom{R}{t_1,\dots,t_n}$ where $R$ is an $n$-place
  139. !!{predicate}, $t_1$, \dots, $t_n$ are terms, and each of $R$,
  140. $t_1$, \dots, $t_n$ is uniquely determined.
  141. \item $!A \ident \eq[t_1][t_2]$ where $t_1$ and $t_2$ are uniquely
  142. determined terms.
  143. \end{enumerate}
  144. \end{prop}
  146. \begin{proof}
  147. Exercise.
  148. \end{proof}
  150. \begin{prob}
  151. Prove \olref[fol][syn][unq]{prop:unique-atomic} (Hint: Formulate and
  152. prove a version of \olref[fol][syn][unq]{lem:no-prefix} for terms.)
  153. \end{prob}
  155. \begin{prop}[Unique Readability]
  156. Every !!{formula} satisfies one, and only one of the following conditions.
  157. \begin{enumerate}
  158. \item $!A$ is atomic.
  160. \tagitem{prvNot}{$!A$ is of the form $\lnot !B$.}{}
  162. \tagitem{prvAnd}{$!A$ is of the form $(!B \land !C)$.}{}
  164. \tagitem{prvOr}{$!A$ is of the form $(!B \lor !C)$.}{}
  166. \tagitem{prvIf}{$!A$ is of the form $(!B \lif !C)$.}{}
  168. \tagitem{prvIff}{$!A$ is of the form $(!B \liff !C)$.}{}
  170. \tagitem{prvAll}{$!A$ is of the form $\lforall[x][!B]$.}{}
  172. \tagitem{prvEx}{$!A$ is of the form $\lexists[x][!B]$.}{}
  173. \end{enumerate}
  174. Moreover, in each case $!B$, or $!B$ and $!C$, are uniquely
  175. determined. This means that, e.g., there are no different pairs $!B$,
  176. $!C$ and $!B'$, $!C'$ so that $!A$ is both of the form
  177. \iftag{prvIf}{$(!B \lif !C)$ and $(!B' \lif !C')$.}{
  178. \iftag{prvOr}{$(!B \lor !C)$ and $(!B' \lor !C')$.}{
  179. \iftag{prvAnd}{$(!B \land !C)$ and $(!B' \land !C')$.}{}}}
  180. \end{prop}
  182. \begin{proof}
  183. The formation rules require that if !!a{formula} is not atomic, it
  184. must start with an opening parenthesis~(, \iftag{prvNot}{$\lnot$,}{}
  185. or a quantifier. On the other hand, every !!{formula} that starts with
  186. one of the following symbols must be atomic: !!a{predicate}, !!a{function}, !!a{constant}\iftag{prvFalse}{, $\lfalse$}{}\iftag{prvTrue}{, $\ltrue$}{}.
  188. So we really only have to show that if $!A$ is of the form $(!B \ast
  189. !C)$ and also of the form $(!B' \mathbin{\ast'} !C')$, then $!B \ident
  190. !B'$, $!C \ident !C'$, and $\ast = {\ast'}$.
  192. So suppose both $!A \ident (!B \ast !C)$ and $!A \ident (!B'
  193. \mathbin{\ast'} !C')$. Then either $!B \ident !B'$ or not. If it is,
  194. clearly $\ast = {\ast'}$ and $!C \ident !C'$, since they then are
  195. substrings of $!A$ that begin in the same place and are of the same
  196. length. The other case is $!B \not\ident !B'$. Since $!B$ and
  197. $!B'$ are both substrings of $!A$ that begin at the same place, one
  198. must be a proper prefix of the other. But this is impossible by
  199. \olref{lem:no-prefix}.
  200. \end{proof}
  203. \end{document}

content/first-order-logic/syntax-and-semantics/main-operator.tex

101 lines; SHA-256 1bc4cc76cc670fdb1069ca53312d13dfcf2ea8444adbb3d9ef4b8d31a5da41fc. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: main-operator
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{syn}{mai}
  11. \olsection{\printtoken{S}{main operator} of a Formula}
  13. \begin{explain}
  14. It is often useful to talk about the last operator used in
  15. constructing !!a{formula}~$!A$. This operator is called the \emph{main
  16. operator} of~$!A$. Intuitively, it is the ``outermost'' operator
  17. of $!A$. For example, the main operator of $\lnot !A$ is $\lnot$,
  18. the main operator of $(!A \lor !B)$ is $\lor$, etc.
  19. \end{explain}
  22. \begin{defn}[!!^{main operator}]
  23. \ollabel{def:main-op}
  24. The \emph{!!{main operator}} of !!a{formula}~$!A$ is
  25. defined as follows:
  26. \begin{enumerate}
  27. \item \indcase*{!A}{!A}{$\indfrm$ has no !!{main operator}.}
  29. \tagitem{prvNot}{\indcase{!A}{\lnot !B}{the !!{main operator} of $\indfrm$
  30. is~$\lnot$.}}{}
  32. \tagitem{prvAnd}{\indcase{!A}{(!B \land !C)}{the !!{main operator} of
  33. $\indfrm$ is~$\land$.}}{}
  35. \tagitem{prvOr}{\indcase{!A}{(!B \lor !C)}{the !!{main operator} of
  36. $\indfrm$ is~$\lor$.}}{}
  38. \tagitem{prvIf}{\indcase{!A}{(!B \lif !C)}{the !!{main operator} of
  39. $\indfrm$ is~$\lif$.}}{}
  41. \tagitem{prvIff}{\indcase{!A}{(!B \liff !C)}{the !!{main operator} of
  42. $\indfrm$ is~$\liff$.}}{}
  44. \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{the !!{main operator}
  45. of $\indfrm$ is~$\lforall$.}}{}
  47. \tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{the !!{main operator} of
  48. $\indfrm$ is~$\lexists$.}}{}
  49. \end{enumerate}
  50. \end{defn}
  52. In each case, we intend the specific indicated \emph{occurrence} of
  53. the !!{main operator} in the formula. For instance, since the formula
  54. $((!D \lif !E) \lif (!E \lif !D))$ is of the form $(!B \lif !C)$ where
  55. $!B$ is $(!D \lif !E)$ and $!C$ is $(!E \lif !D)$, the second
  56. occurrence of $\lif$ is the !!{main operator}.
  58. \begin{explain}
  59. This is a \emph{recursive} definition of a function which maps all
  60. non-atomic !!{formula}s to their !!{main operator} occurrence. Because
  61. of the way !!{formula}s are defined inductively, every
  62. !!{formula}~$!A$ satisfies one of the cases in \olref{def:main-op}.
  63. This guarantees that for each non-atomic !!{formula}~$!A$ !!a{main
  64. operator} exists. Because each !!{formula} satisfies only one of these
  65. conditions, and because the smaller !!{formula}s from which $!A$ is
  66. constructed are uniquely determined in each case, the !!{main
  67. operator} occurrence of~$!A$ is unique, and so we have defined a
  68. function.
  69. \end{explain}
  71. We call !!{formula}s by the names in \olref{tab:main-op} depending on
  72. which symbol their !!{main operator}
  73. is.\iftag{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}
  74. { Recall, however, that defined operators do not officially appear in
  75. !!{formula}s. They are just abbreviations, so officially they cannot
  76. be the main operator of a formula. In proofs about all !!{formula}s
  77. they therefore do not have to be treated separately.}
  79. \begin{table}[!h]
  80. \centering
  81. \begin{tabular}{c | c | c}
  82. !!^{main operator} & Type of !!{formula} & Example\\
  83. \hline
  84. none & atomic (!!{formula}) &
  85. \iftag{prvFalse}{$\lfalse$,}{}
  86. \iftag{prvTrue}{$\ltrue$,}{}
  87. $\Atom{R}{t_1, \dots, t_n}$,
  88. $\eq[t_1][t_2]$\\
  89. $\lnot$ & negation & $\lnot !A$ \\
  90. $\land$ & conjunction & $(!A \land !B$) \\
  91. $\lor$ & disjunction & $(!A \lor !B$) \\
  92. $\lif$ & !!{conditional} & $(!A \lif !B$) \\
  93. $\liff$ & !!{biconditional} & $(!A \liff !B)$ \\
  94. $\lforall[][]$ & universal (!!{formula})& $\lforall[x][!A]$ \\
  95. $\lexists[][]$ & existential (!!{formula})& $\lexists[x][!A]$
  96. \end{tabular}
  97. \caption{Main operator and names of !!{formula}s}
  98. \ollabel{tab:main-op}
  99. \end{table}
  101. \end{document}

content/first-order-logic/syntax-and-semantics/subformulas.tex

111 lines; SHA-256 4c43825e4c236e55d25092ff1f5b68ed38a3f1e9ae8ed12fc2e14f3a03fc6c77. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: subformulas
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{syn}{sbf}
  11. \olsection{\printtoken{P}{subformula}}
  13. \begin{explain}
  14. It is often useful to talk about the !!{formula}s that ``make up'' a
  15. given !!{formula}. We call these its \emph{!!{subformula}s}. Any
  16. !!{formula} counts as !!a{subformula} of itself; a subformula of $!A$
  17. other than $!A$ itself is a \emph{proper !!{subformula}}.
  18. \end{explain}
  20. \begin{defn}[Immediate !!^{subformula}]
  21. If $!A$ is !!a{formula}, the \emph{immediate !!{subformula}s}
  22. of $!A$ are defined inductively as follows:
  23. \begin{enumerate}
  24. \item Atomic !!{formula}s have no immediate !!{subformula}s.
  26. \tagitem{prvNot}{\indcase{!A}{\lnot !B}{The only immediate
  27. !!{subformula} of $\indfrm$ is~$!B$.}}{}
  29. \item \indcase{!A}{(!B \ast !C)}{The immediate !!{subformula}s of
  30. $\indfrm$ are $!B$ and $!C$ ($\ast$ is any one of the two-place
  31. connectives).}
  33. \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{The only immediate
  34. !!{subformula} of $\indfrm$ is~$!B$.}}{}
  36. \tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{The only immediate
  37. !!{subformula} of $\indfrm$ is~$!B$.}}{}
  38. \end{enumerate}
  39. \end{defn}
  41. \begin{defn}[Proper !!^{subformula}]
  42. If $!A$ is !!a{formula}, the \emph{proper !!{subformula}s}
  43. of $!A$ are defined recursively as follows:
  44. \begin{enumerate}
  45. \item Atomic !!{formula}s have no proper !!{subformula}s.
  47. \tagitem{prvNot}{\indcase{!A}{\lnot !B}{The proper !!{subformula}s of
  48. $\indfrm$ are~$!B$ together with all proper !!{subformula}s
  49. of~$!B$.}}{}
  51. \item \indcase{!A}{(!B \ast !C)}{The proper !!{subformula}s of
  52. $\indfrm$ are $!B$, $!C$, together with all proper !!{subformula}s
  53. of $!B$ and those of~$!C$.}
  55. \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{The proper
  56. !!{subformula}s of $\indfrm$ are~$!B$ together with all proper
  57. !!{subformula}s of~$!B$.}}{}
  59. \tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{The proper
  60. !!{subformula}s of $\indfrm$ are~$!B$ together with all proper
  61. !!{subformula}s of~$!B$.}}{}
  62. \end{enumerate}
  63. \end{defn}
  65. \begin{defn}[!!^{subformula}]
  66. The !!{subformula}s of $!A$ are $!A$ itself together with all its
  67. proper !!{subformula}s.
  68. \end{defn}
  70. \begin{explain}
  71. Note the subtle difference in how we have defined immediate
  72. !!{subformula}s and proper !!{subformula}s. In the first case, we
  73. have directly defined the immediate !!{subformula}s of a formula~$!A$
  74. for each possible form of~$!A$. It is an explicit definition by
  75. cases, and the cases mirror the inductive definition of the set of
  76. !!{formula}s. In the second case, we have also mirrored the way the
  77. set of all !!{formula}s is defined, but in each case we have also
  78. included the proper !!{subformula}s of the smaller !!{formula}s $!B$,
  79. $!C$ in addition to these !!{formula}s themselves. This makes the
  80. definition \emph{recursive}. In general, a definition of a function
  81. on an inductively defined set (in our case, !!{formula}s) is recursive
  82. if the cases in the definition of the function make use of
  83. the function itself. To be well defined, we must make sure, however,
  84. that we only ever use the values of the function for arguments that
  85. come ``before'' the one we are defining---in our case, when defining
  86. ``proper !!{subformula}'' for $(!B \ast !C)$ we only use the proper
  87. !!{subformula}s of the ``earlier'' !!{formula}s $!B$ and $!C$.
  88. \end{explain}
  90. \begin{prop}
  91. \ollabel{prop:subfrm-trans}
  92. Suppose $!B$ is a subformula of $!A$ and $!C$ is a subformula of $!B$.
  93. Then $!C$ is a subformula of $!A$. In other words, the subformula
  94. relation is transitive.
  95. \end{prop}
  97. \begin{prob}
  98. Prove \olref[fol][syn][sbf]{prop:subfrm-trans}.
  99. \end{prob}
  101. \begin{prop}
  102. \ollabel{prop:count-subfrms}
  103. Suppose $!A$ is a formula with $n$ connectives and quantifiers.
  104. Then $!A$ has at most $2n+1$ subformulas.
  105. \end{prop}
  107. \begin{prob}
  108. Prove \olref[fol][syn][sbf]{prop:count-subfrms}.
  109. \end{prob}
  111. \end{document}

content/first-order-logic/syntax-and-semantics/formation-sequences.tex

278 lines; SHA-256 dc1735bb077f5086c6fd6e2f968591415a9cba90b65bc0a3d412742cc62bc6ff. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: formation-sequences
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{syn}{fseq}
  11. \olsection{Formation Sequences}
  13. Defining !!{formula}s via an inductive definition, and the
  14. complementary technique of proving properties of !!{formula}s via
  15. induction, is an elegant and efficient approach. However, it can
  16. also be useful to consider a more bottom-up, step-by-step approach
  17. to the construction of !!{formula}s, which we do here using the
  18. notion of a \emph{formation sequence}.
  19. %
  20. To show how terms and !!{formula}s can be introduced in this way
  21. without needing to refer to their inductive definitions, we first
  22. introduce the notion of an arbitrary string of symbols drawn from
  23. some language~$\Lang L$.
  25. \begin{defn}[Strings]
  26. \ollabel{defn:string}
  27. Suppose $\Lang L$ is a first-order language. An \emph{$\Lang
  28. L$-string} is a finite sequence of symbols of~$\Lang L$. Where the
  29. language~$\Lang L$ is clearly fixed by the context, we will often
  30. refer to a $\Lang L$-string simply as a \emph{string}.
  31. \end{defn}
  33. \begin{ex}
  34. For any first-order language $\Lang L$, all
  35. $\Lang L$-!!{formula}s are $\Lang L$-strings, but not
  36. conversely. For example, \[)(\Obj v_0\lif\lexists\] is an
  37. $\Lang L$-string but not an $\Lang L$-!!{formula}.
  38. \end{ex}
  40. \begin{defn}[Formation sequences for terms]
  41. \ollabel{defn:fseq-trm}
  42. A finite sequence of $\Lang L$-strings $\tuple{t_0,\dotsc,t_n}$ is a
  43. \emph{formation sequence} for a term $t$ if $t \ident t_n$ and for all
  44. $i \leq n$, either $t_i$ is !!a{variable} or !!a{constant}, or $\Lang
  45. L$ contains a $k$-ary !!{function}~$f$ and there exist
  46. $m_0,\dotsc,m_k < i$ such that $t_i \ident f(t_{m_0},\dotsc,t_{m_k})$.
  47. When it is necessary to distinguish, we will refer to formation
  48. sequences for terms as \emph{term formation sequences}.
  49. \end{defn}
  51. \begin{ex}
  52. The sequence
  53. \[
  54. \tuple{\Obj c_0, \Obj v_0, \Atom{\Obj f^2_0}{\Obj c_0, \Obj v_0}, \Atom{\Obj f^1_0}{\Atom{\Obj f^2_0}{\Obj c_0, \Obj v_0}}}
  55. \]
  56. is a formation sequence for the term $\Atom{\Obj f^1_0}{\Atom{\Obj
  57. f^2_0}{\Obj c_0, \Obj v_0}}$, as is
  58. \[
  59. \tuple{\Obj v_0, \Obj c_0, \Atom{\Obj f^2_0}{\Obj c_0, \Obj v_0}, \Atom{\Obj f^1_0}{\Atom{\Obj f^2_0}{\Obj c_0, \Obj v_0}}}.
  60. \]
  61. \end{ex}
  63. \begin{defn}[Formation sequences for formulas]
  64. \ollabel{defn:fseq-frm}
  65. A finite sequence of $\Lang L$-strings $\tuple{!A_0,\dotsc,!A_n}$
  66. is a \emph{formation sequence} for~$!A$ if $!A \ident !A_n$ and
  67. for all $i \leq n$, either $!A_i$ is an atomic !!{formula} or there
  68. exist $j,k < i$ and !!a{variable}~$x$ such that one of the following
  69. holds:
  70. \begin{enumerate}
  71. \tagitem{prvNot}{$!A_i \ident \lnot !A_j$.}{}%
  72. \tagitem{prvAnd}{$!A_i \ident (!A_j \land !A_k)$.}{}%
  73. \tagitem{prvOr}{$!A_i \ident (!A_j \lor !A_k)$.}{}%
  74. \tagitem{prvIf}{$!A_i \ident (!A_j \lif !A_k)$.}{}%
  75. \tagitem{prvIff}{$!A_i \ident (!A_j \liff !A_k)$.}{}%
  76. \tagitem{prvAll}{$!A_i \ident \lforall[x][!A_j]$.}{}%
  77. \tagitem{prvEx}{$!A_i \ident \lexists[x][!A_j]$.}{}%
  78. \end{enumerate}
  79. When it is necessary to distinguish, we will refer to formation
  80. sequences for formulas as \emph{formula formation sequences}.
  81. \end{defn}
  83. \begin{ex}
  84. \[
  85. \tuple{
  86. \Atom{\Obj A^1_0}{\Obj v_0},
  87. \Atom{\Obj A^1_1}{\Obj c_1},
  88. (\Atom{\Obj A^1_1}{\Obj c_1} \land \Atom{\Obj A^1_0}{\Obj v_0}),
  89. \lexists[\Obj v_0][(\Atom{\Obj A^1_1}{\Obj c_1} \land \Atom{\Obj A^1_0}{\Obj v_0})]
  90. }
  91. \]
  92. is a formation sequence of $\lexists[\Obj v_0][(\Atom{\Obj A^1_1}{\Obj
  93. c_1} \land \Atom{\Obj A^1_0}{\Obj v_0})]$, as is
  94. \begin{multline*}
  95. \tuple{
  96. \Atom{\Obj A^1_0}{\Obj v_0},
  97. \Atom{\Obj A^1_1}{\Obj c_1},
  98. (\Atom{\Obj A^1_1}{\Obj c_1} \land \Atom{\Obj A^1_0}{\Obj v_0}),
  99. \Atom{\Obj A^1_1}{\Obj c_1},\\
  100. \lforall[\Obj v_1][\Atom{\Obj A^1_0}{\Obj v_0}],
  101. \lexists[\Obj v_0][(\Atom{\Obj A^1_1}{\Obj c_1} \land \Atom{\Obj A^1_0}{\Obj v_0})]
  102. }.
  103. \end{multline*}
  104. %
  105. As can be seen from the second example, formation sequences
  106. may contain ``junk'': !!{formula}s which are redundant or do not
  107. contribute to the construction.
  108. \end{ex}
  110. \begin{prop}\ollabel{prop:formed}
  111. Every !!{formula}~$!A$ in~$\Frm[L]$ has a formation sequence.
  112. \end{prop}
  114. \begin{proof}
  115. Suppose $!A$ is atomic. Then the sequence $\tuple{!A}$ is a
  116. formation sequence for~$!A$.
  117. %
  118. Now suppose that $!B$ and~$!C$ have formation sequences
  119. $\tuple{!B_0,\dotsc,!B_n}$ and $\tuple{!C_0,\dotsc,!C_m}$
  120. respectively.
  121. %
  122. \begin{enumerate}
  123. \tagitem{prvNot}{If $!A \ident \lnot !B$,
  124. then $\tuple{!B_0,\dotsc,!B_n,\lnot !B_n}$
  125. is a formation sequence for~$!A$.}{}
  126. \tagitem{prvAnd}{If $!A \ident (!B \land !C)$,
  127. then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \land !C_m)}$
  128. is a formation sequence for~$!A$.}{}
  129. \tagitem{prvOr}{If $!A \ident (!B \lor !C)$,
  130. then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \lor !C_m)}$
  131. is a formation sequence for~$!A$.}{}
  132. \tagitem{prvIf}{If $!A \ident (!B \lif !C)$,
  133. then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \lif !C_m)}$
  134. is a formation sequence for~$!A$.}{}
  135. \tagitem{prvIff}{If $!A \ident (!B \liff !C)$,
  136. then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \liff !C_m)}$
  137. is a formation sequence for~$!A$.}{}
  138. \tagitem{prvAll}{If $!A \ident \lforall[x][!B]$,
  139. then $\tuple{!B_0,\dotsc,!B_n,\lforall[x][!B_n]}$
  140. is a formation sequence for~$!A$.}{}
  141. \tagitem{prvEx}{If $!A \ident \lexists[x][!B]$,
  142. then $\tuple{!B_0,\dotsc,!B_n,\lexists[x][!B_n]}$
  143. is a formation sequence for~$!A$.}{}
  144. \end{enumerate}
  145. By the principle of induction on !!{formula}s,
  146. every !!{formula} has a formation sequence.
  147. \end{proof}
  149. We can also prove the converse. This is important because it shows
  150. that our two ways of defining formulas are equivalent: they give
  151. the same results. It also means that we can prove theorems about
  152. formulas by using ordinary induction on the length of formation
  153. sequences.
  155. \begin{lem}
  156. \ollabel{lem:fseq-init}
  157. Suppose that $\tuple{!A_0,\dotsc,!A_n}$ is a formation sequence
  158. for~$!A_n$, and that $k \leq n$. Then $\tuple{!A_0,\dotsc,!A_k}$
  159. is a formation sequence for~$!A_k$.
  160. \end{lem}
  162. \begin{proof}
  163. Exercise.
  164. \end{proof}
  166. \begin{prob}
  167. Prove \olref[fol][syn][fseq]{lem:fseq-init}.
  168. \end{prob}
  170. \begin{thm}
  171. \ollabel{thm:fseq-frm-equiv}
  172. $\Frm[L]$ is the set of all $\Lang L$-strings~$!A$ such that
  173. there exists a formula formation sequence for~$!A$.
  174. \end{thm}
  176. \begin{proof}
  177. Let $F$ be the set of all strings of symbols in the language~$\Lang L$
  178. that have a formation sequence. We have seen in
  179. \olref[fol][syn][fseq]{prop:formed} that $\Frm[L] \subseteq F$, so now
  180. we prove the converse.
  182. Suppose $!A$ has a formation sequence $\tuple{!A_0,\dotsc,!A_n}$.
  183. We prove that $!A \in \Frm[L]$ by strong induction on~$n$.
  184. Our induction hypothesis is that every string of symbols with a
  185. formation sequence of length $m < n$ is in $\Frm[L]$.
  186. By the definition of a formation sequence, either $!A \ident !A_n$ is
  187. atomic or there must exist $j,k < n$ such that one of the
  188. following is the case:
  189. \begin{enumerate}
  190. \tagitem{prvNot}{$!A \ident \lnot !A_j$.}{}%
  191. \tagitem{prvAnd}{$!A \ident (!A_j \land !A_k)$.}{}%
  192. \tagitem{prvOr}{$!A \ident (!A_j \lor !A_k)$.}{}%
  193. \tagitem{prvIf}{$!A \ident (!A_j \lif !A_k)$.}{}%
  194. \tagitem{prvIff}{$!A \ident (!A_j \liff !A_k)$.}{}%
  195. \tagitem{prvAll}{$!A \ident \lforall[x][!A_j]$.}{}%
  196. \tagitem{prvEx}{$!A \ident \lexists[x][!A_j]$.}{}%
  197. \end{enumerate}
  198. Now we reason by cases. If $!A$ is atomic then
  199. $!A_n \in \Frm[L_0]$. Suppose instead that
  200. $!A \equiv (!A_j \land !A_k)$. By
  201. \olref[fol][syn][fseq]{lem:fseq-init},
  202. $\tuple{!A_0,\dotsc,!A_j}$ and $\tuple{!A_0,\dotsc,!A_k}$ are
  203. formation sequences for $!A_j$ and~$!A_k$, respectively. Since
  204. these are proper initial subsequences of the formation sequence
  205. for~$!A$, they both have length less than~$n$. Therefore by
  206. the induction hypothesis, $!A_j$ and~$!A_k$ are in~$\Frm[L_0]$,
  207. and by the definition of !!a{formula}, so is
  208. $(!A_j \land !A_k)$. The other cases follow by parallel
  209. reasoning.
  210. \end{proof}
  212. Formation sequences for terms have similar properties to those
  213. for !!{formula}s.
  215. \begin{prop}
  216. \ollabel{prop:fseq-trm-equiv}
  217. $\Trm[L]$ is the set of all $\Lang L$-strings $t$
  218. such that there exists a term formation sequence for~$t$.
  219. \end{prop}
  221. \begin{proof}
  222. Exercise.
  223. \end{proof}
  225. \begin{prob}
  226. Prove \olref[fol][syn][fseq]{prop:fseq-trm-equiv}.
  227. Hint: use a similar strategy to that used in the proof of
  228. \olref[fol][syn][fseq]{thm:fseq-frm-equiv}.
  229. \end{prob}
  231. There are two types of ``junk'' that can appear in formation
  232. sequences: repeated elements, and elements that are irrelevant
  233. to the construction of the formation or term. We can eliminate
  234. both by looking at minimal formation sequences.
  236. \begin{defn}[Minimal formation sequences]
  237. \ollabel{defn:minimal-fseq}
  238. A formation sequence $\tuple{!A_0, \ldots, !A_n}$ for a
  239. formula~$!A$ is a \emph{minimal formation sequence} for~$!A$
  240. if for every other formation sequence~$s$ for~$!A$,
  241. the length of~$s$ is greater than or equal to~$n+1$.
  243. Similarly, a formation sequence $\tuple{t_0, \ldots, t_n}$
  244. for a term~$t$ is a \emph{minimal formation sequence}
  245. for~$t$ if for every other formation sequence~$s$ for~$t$,
  246. the length of~$s$ is greater than or equal to~$n+1$.
  247. \end{defn}
  249. Note that a formula or term can have more than one minimal
  250. formation sequence, but they will contain exactly the same
  251. strings.
  253. \begin{prop}
  254. \ollabel{prop:subformula-equivs}
  255. The following are equivalent:
  256. \begin{enumerate}
  257. \item $!B$ is a sub-!!{formula} of~$!A$.
  258. \item $!B$ occurs in every formation sequence of~$!A$.
  259. \item $!B$ occurs in a minimal formation sequence of~$!A$.
  260. \end{enumerate}
  261. \end{prop}
  263. \begin{proof}
  264. Exercise.
  265. \end{proof}
  267. \begin{prob}
  268. Prove \olref[fol][syn][fseq]{prop:subformula-equivs}.
  269. \end{prob}
  271. \begin{history}
  272. Formation sequences were introduced by Raymond Smullyan in his
  273. textbook \emph{First-Order Logic} \citep{Smullyan1968}.
  274. Additional properties of formation sequences were established by
  275. \citet{Zuckerman1973}.
  276. \end{history}
  278. \end{document}

content/first-order-logic/syntax-and-semantics/free-vars-sentences.tex

102 lines; SHA-256 ea6bea6e587867742143e68dd69a2674fc1544ffaae27236ba1f517fe516bf1f. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: free-vars-sentences
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{syn}{fvs}
  11. \olsection{Free \printtoken{P}{variable} and \printtoken{P}{sentence}}
  13. \begin{defn}[Free occurrences of !!a{variable}]
  14. \ollabel{defn:free-occ}
  15. The \emph{free} occurrences of !!a{variable} in !!a{formula} are defined
  16. inductively as follows:
  17. \begin{enumerate}
  18. \item \indcase*{!A}{$!A$ is atomic}{all !!{variable} occurrences in
  19. $\indfrm$ are free.}
  21. \tagitem{prvNot}{\indcase{!A}{\lnot !B}{the free !!{variable}
  22. occurrences of $\indfrm$ are exactly those of $!B$.}}{}
  24. \item \indcase{!A}{(!B \ast !C)}{the free
  25. !!{variable} occurrences of $\indfrm$ are those in $!B$
  26. together with those in~$!C$.}
  28. \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{the free !!{variable}
  29. occurrences in $\indfrm$ are all of those in~$!B$ except for
  30. occurrences of~$x$.}}{}
  32. \tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{the free !!{variable}
  33. occurrences in $\indfrm$ are all of those in~$!B$ except for
  34. occurrences of~$x$.}}{}
  35. \end{enumerate}
  36. \end{defn}
  38. \begin{defn}[Bound Variables]
  39. An occurrence of !!a{variable} in a formula~$!A$ is \emph{bound} if
  40. it is not free.
  41. \end{defn}
  43. \begin{prob}
  44. Give an inductive definition of the bound variable occurrences along
  45. the lines of \olref[fol][syn][fvs]{defn:free-occ}.
  46. \end{prob}
  48. \begin{defn}[Scope]
  49. \iftag{prvAll}{If $\lforall[x][!B]$ is an occurrence of a subformula
  50. in a formula~$!A$, then the corresponding occurrence of~$!B$ in~$!A$
  51. is called the \emph{scope} of the corresponding occurrence
  52. of~$\lforall[x]$. \iftag{prvEx}{Similarly for $\lexists[x]$.}{}}{If
  53. $\lexists[x][!B]$ is an occurrence of a subformula in a
  54. formula~$!A$, then the corresponding occurrence of~$!B$ in~$!A$ is
  55. called the \emph{scope} of the corresponding occurrence
  56. of~$\lexists[x]$.}
  58. If $!B$ is the scope of a quantifier occurrence
  59. \iftag{prvAll}{$\lforall[x]$\iftag{prvEx}{ or
  60. $\lexists[x]$}{}}{$\lexists[x]$} in~$!A$, then the free occurrences of
  61. $x$ in~$!B$ are bound in \iftag{prvAll}{$\lforall[x][!B]$\iftag{prvEx}{ and
  62. $\lexists[x][!B]$}{}}{$\lexists[x][!B]$}. We say that these
  63. occurrences are \emph{bound by} the
  64. mentioned quantifier occurrence.
  65. \end{defn}
  67. \begin{ex}
  68. Consider the following formula:
  69. \[
  70. \lexists[\Obj v_0][\underbrace{\Atom{\Obj A^2_0}{\Obj v_0,\Obj v_1}}_{!B}]
  71. \]
  72. $!B$ represents the scope of $\lexists[\Obj v_0]$.
  73. The quantifier binds the occurrence of $\Obj v_0$ in $!B$, but
  74. does not bind the occurrence of $\Obj v_1$. So $\Obj v_1$ is
  75. a free variable in this case.
  78. We can now see how this might work in a more complicated
  79. !!{formula}~$!A$:
  80. \[
  81. \lforall[\Obj v_0][\underbrace{(\Atom{\Obj A^1_0}{\Obj v_0} \lif
  82. \Atom{\Obj A^2_0}{\Obj v_0, \Obj v_1})}_{!B}] \lif \lexists[\Obj
  83. v_1][\underbrace{(\Atom{\Obj A^2_1}{\Obj v_0, \Obj v_1} \lor \lforall[\Obj v_0][\overbrace{\lnot \Atom{\Obj A^1_1}{\Obj v_0}}^{!D}])}_{!C}]
  84. \]
  85. $!B$ is the scope of the first $\lforall[\Obj v_0]$, $!C$ is the scope
  86. of $\lexists[\Obj v_1]$, and $!D$ is the scope of the second
  87. $\lforall[\Obj v_0]$. The first $\lforall[\Obj v_0]$ binds the
  88. occurrences of $\Obj v_0$ in~$!B$, $\lexists[\Obj v_1]$ binds the occurrence
  89. of $\Obj v_1$ in $!C$, and the second $\lforall[\Obj v_0]$ binds the
  90. occurrence of $\Obj v_0$ in~$!D$. The first occurrence of $\Obj v_1$
  91. and the fourth occurrence of $\Obj v_0$ are free in~$!A$. The last
  92. occurrence of $\Obj v_0$ is free in $!D$, but bound in $!C$ and~$!A$.
  93. \end{ex}
  95. \begin{defn}[Sentence]
  96. !!^a{formula}~$!A$ is \article{sentence} \emph{!!{sentence}} iff it
  97. contains no free occurrences of !!{variable}s.
  98. \end{defn}
  100. % add examples!
  102. \end{document}

content/first-order-logic/syntax-and-semantics/substitution.tex

126 lines; SHA-256 19393c28f5f036da9c43ce10bfb5f1b2f330dca8cb2ad950d98eab5b1b7e83b2. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: substitution
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{syn}{sub}
  11. \olsection{Substitution}
  13. \begin{defn}[Substitution in a term]
  14. We define $\Subst{s}{t}{x}$, the result of \emph{substituting} $t$
  15. for every occurrence of~$x$ in $s$, recursively:
  16. \begin{enumerate}
  17. \item \indcase{s}{c}{$\Subst{\indfrm}{t}{x}$ is just $s$.}
  19. \item \indcase{s}{y}{$\Subst{\indfrm}{t}{x}$ is also just~$s$,
  20. provided $y$ is a variable and $y \not\ident x$.}
  22. \item \indcase{s}{x}{$\Subst{\indfrm}{t}{x}$ is~$t$.}
  24. \item\indcase{s}{\Atom{f}{t_1, \dots, t_n}}{$\Subst{\indfrmp}{t}{x}$ is
  25. $\Atom{f}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}$.}
  26. \end{enumerate}
  27. \end{defn}
  29. \begin{defn}
  30. A term~$t$ is \emph{!!{free for}} $x$ in $!A$ if none of the free
  31. occurrences of~$x$ in $!A$ occur in the scope of a quantifier that
  32. binds a variable in~$t$.
  33. \end{defn}
  35. \begin{ex} ~
  36. \begin{enumerate}
  37. \item $\Obj v_8$ is free for $\Obj v_1$ in $\lexists[\Obj
  38. v_3]\Atom{\Obj A^2_4}{\Obj v_3,\Obj v_1}$
  40. \item $\Obj f^2_1(\Obj v_1, \Obj v_2)$ is \emph{not} free for $\Obj
  41. v_0$ in $\lforall[\Obj v_2]\Atom{\Obj A^2_4}{\Obj v_0,\Obj v_2}$
  42. \end{enumerate}
  43. \end{ex}
  45. \begin{defn}[Substitution in !!a{formula}]
  46. If $!A$ is !!a{formula}, $x$~is !!a{variable}, and $t$~is a term
  47. !!{free for}~$x$ in~$!A$, then $\Subst{!A}{t}{x}$ is the result of
  48. substituting $t$ for all free occurrences of~$x$ in~$!A$.
  49. \begin{enumerate}
  50. \tagitem{prvFalse}{\indcase{!A}{\lfalse}{$\Subst{\indfrm}{t}{x}$ is
  51. $\lfalse$.}}{}
  53. \tagitem{prvTrue}{\indcase{!A}{\ltrue}{$\Subst{\indfrm}{t}{x}$ is
  54. $\ltrue$.}}{}
  56. \item \indcase{!A}{\Atom{P}{t_1,\dots,
  57. t_n}}{$\Subst{\indfrm}{t}{x}$ is $\Atom{P}{\Subst{t_1}{t}{x},
  58. \dots, \Subst{t_n}{t}{x}}$.}
  60. \item \indcase{!A}{\eq[t_1][t_2]}{$\Subst{\indfrmp}{t}{x}$ is
  61. $\Subst{t_1}{t}{x} = \Subst{t_2}{t}{x}$.}
  63. \tagitem{prvNot}{\indcase{!A}{\lnot !B}{$\Subst{\indfrmp}{t}{x}$ is
  64. $\lnot \Subst{!B}{t}{x}$.}}{}
  66. \tagitem{prvAnd}{\indcase{!A}{(!B \land
  67. !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \land
  68. \Subst{!C}{t}{x})$.}}{}
  70. \tagitem{prvOr}{\indcase{!A}{(!B \lor
  71. !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \lor
  72. \Subst{!C}{t}{x})$.}}{}
  74. \tagitem{prvIf}{\indcase{!A}{(!B \lif
  75. !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \lif
  76. \Subst{!C}{t}{x})$.}}{}
  78. \tagitem{prvIff}{\indcase{!A}{(!B \liff
  79. !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \liff
  80. \Subst{!C}{t}{x})$.}}{}
  82. \tagitem{prvAll}{
  83. \indcase{!A}{\lforall[y][!B]}{$\Subst{\indfrmp}{t}{x}$
  84. is $\lforall[y][\Subst{!B}{t}{x}]$, provided $y$ is a variable
  85. other than $x$; otherwise $\Subst{\indfrmp}{t}{x}$
  86. is just $\indfrm$.}}{}
  88. \tagitem{prvEx}{
  89. \indcase{!A}{\lexists[y][!B]}{$\Subst{\indfrmp}{t}{x}$
  90. is $\lexists[y][\Subst{!B}{t}{x}]$, provided $y$ is a variable
  91. other than $x$; otherwise $\Subst{\indfrmp}{t}{x}$
  92. is just $\indfrm$.}}{}
  93. \end{enumerate}
  94. \end{defn}
  96. \begin{explain}
  97. Note that substitution may be vacuous: If $x$ does not occur in $!A$
  98. at all, then $\Subst{!A}{t}{x}$ is just~$!A$.
  100. The restriction that $t$ must be !!{free for}~$x$ in~$!A$ is necessary to
  101. exclude cases like the following. If $!A \ident \lexists[y][x < y]$
  102. and $t \ident y$, then $\Subst{!A}{t}{x}$ would be $\lexists[y][y <
  103. y]$. In this case the free variable $y$ is ``captured'' by the
  104. quantifier $\lexists[y]$ upon substitution, and that is undesirable.
  105. For instance, we would like it to be the case that whenever
  106. $\lforall[x][!B]$ holds, so does $\Subst{!B}{t}{x}$. But consider
  107. $\lforall[x][\lexists[y][x < y]]$ (here $!B$ is $\lexists[y][x <
  108. y]$). It is a sentence that is true about, e.g., the natural numbers:
  109. for every number~$x$ there is a number~$y$ greater than it. If we
  110. allowed $y$ as a possible substitution for~$x$, we would end up with
  111. $\Subst{!B}{y}{x} \ident \lexists[y][y < y]$, which is false. We
  112. prevent this by requiring that none of the free variables in~$t$ would
  113. end up being bound by a quantifier in~$!A$.
  114. \end{explain}
  116. We often use the following convention to avoid cumbersome notation: If
  117. $!A$ is !!a{formula} which may contain the !!{variable}~$x$ free, we
  118. also write~$!A(x)$ to indicate this. When it is clear which $!A$
  119. and~$x$ we have in mind, and $t$ is a term (assumed to be free for $x$
  120. in $!A(x)$), then we write $!A(t)$ as short for $\Subst{!A}{t}{x}$. So
  121. for instance, we might say, ``we call $!A(t)$ an instance
  122. of~$\lforall[x][!A(x)]$.'' By this we mean that if $!A$~is any
  123. !!{formula}, $x$~!!a{variable}, and $t$~a term that's free for~$x$
  124. in~$!A$, then $\Subst{!A}{t}{x}$ is an instance of~$\lforall[x][!A]$.
  126. \end{document}