The Open Logic Text — accessible offline edition

Syntax and Semantics — Source and provenance

Syntax and Semantics

Source and provenance

All 7 files in the exact Syntax and Semantics source boundary appear line by line and are copied byte-for-byte for download. All 374 formulas link to exact source coordinates.

content/propositional-logic/syntax-and-semantics/formation-sequences.tex

153 lines; SHA-256 4057bf6b85c70ad9ee56dc5365b21a1daa0a99550079bdafb1ab16f36b943356. Open the 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{pl}{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}.
  20. \begin{defn}[Formation sequences for formulas]
  21. \ollabel{defn:fseq-frm}
  22. A finite sequence $\tuple{!A_0,\dotsc,!A_n}$ of strings of
  23. symbols from the language~$\Lang L_0$ is a \emph{formation
  24. sequence} for $!A$ if $!A \ident !A_n$ and for all $i \leq n$,
  25. either $!A_i$ is an atomic formula or there exist $j,k < i$
  26. such that one of the following holds:
  27. \begin{enumerate}
  28. \tagitem{prvNot}{$!A_i \ident \lnot !A_j$.}{}%
  29. \tagitem{prvAnd}{$!A_i \ident (!A_j \land !A_k)$.}{}%
  30. \tagitem{prvOr}{$!A_i \ident (!A_j \lor !A_k)$.}{}%
  31. \tagitem{prvIf}{$!A_i \ident (!A_j \lif !A_k)$.}{}%
  32. \tagitem{prvIff}{$!A_i \ident (!A_j \liff !A_k)$.}{}%
  33. \end{enumerate}
  34. \end{defn}
  36. \begin{ex}
  37. \[
  38. \tuple{
  39. \Obj p_0,
  40. \Obj p_1,
  41. (\Obj p_1 \land \Obj p_0),
  42. \lnot (\Obj p_1 \land \Obj p_0)
  43. }
  44. \]
  45. is a formation sequence of
  46. $\lnot (\Obj p_1 \land \Obj p_0)$, as is
  47. \[
  48. \tuple{
  49. \Obj p_0,
  50. \Obj p_1,
  51. \Obj p_0,
  52. (\Obj p_1 \land \Obj p_0),
  53. (\Obj p_0 \lif \Obj p_1),
  54. \lnot (\Obj p_1 \land \Obj p_0)
  55. }.
  56. \]
  57. %
  58. As can be seen from the second example, formation sequences
  59. may contain `junk': formulas which are redundant or do not
  60. contribute to the construction.
  61. \end{ex}
  63. \begin{prop}
  64. \ollabel{prop:formed}
  65. Every !!{formula}~$!A$ in~$\Frm[L_0]$ has a formation sequence.
  66. \end{prop}
  68. \begin{proof}
  69. Suppose $!A$ is atomic. Then the sequence~$\tuple{!A}$ is a
  70. formation sequence for~$!A$.
  71. %
  72. Now suppose that $!B$ and~$!C$ have formation sequences
  73. $\tuple{!B_0,\dotsc,!B_n}$ and $\tuple{!C_0,\dotsc,!C_m}$
  74. respectively.
  75. %
  76. \begin{enumerate}
  77. \tagitem{prvNot}{If $!A \ident \lnot !B$,
  78. then $\tuple{!B_0,\dotsc,!B_n,\lnot !B_n}$
  79. is a formation sequence for~$!A$.}{}
  80. \tagitem{prvAnd}{If $!A \ident (!B \land !C)$,
  81. then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \land !C_m)}$
  82. is a formation sequence for~$!A$.}{}
  83. \tagitem{prvOr}{If $!A \ident (!B \lor !C)$,
  84. then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \lor !C_m)}$
  85. is a formation sequence for~$!A$.}{}
  86. \tagitem{prvIf}{If $!A \ident (!B \lif !C)$,
  87. then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \lif !C_m)}$
  88. is a formation sequence for~$!A$.}{}
  89. \tagitem{prvIff}{If $!A \ident (!B \liff !C)$,
  90. then $\tuple{!B_0,\dotsc,!B_n,!C_0,\dotsc,!C_m,(!B_n \liff !C_m)}$
  91. is a formation sequence for~$!A$.}{}
  92. \end{enumerate}
  93. By the principle of induction on !!{formula}s,
  94. every !!{formula} has a formation sequence.
  95. \end{proof}
  97. We can also prove the converse. This is important because it shows
  98. that our two ways of defining formulas are equivalent: they give
  99. the same results. It also means that we can prove theorems about
  100. formulas by using ordinary induction on the length of formation
  101. sequences.
  103. \begin{lem}
  104. \ollabel{lem:fseq-init}
  105. Suppose that $\tuple{!A_0,\dotsc,!A_n}$ is a formation sequence
  106. for~$!A_n$, and that $k \leq n$. Then $\tuple{!A_0,\dotsc,!A_k}$
  107. is a formation sequence for~$!A_k$.
  108. \end{lem}
  110. \begin{proof}
  111. Exercise.
  112. \end{proof}
  114. \begin{thm}
  115. \ollabel{thm:fseq-frm-equiv}
  116. $\Frm[L_0]$ is the set of all strings of symbols
  117. in the language~$\Lang L_0$ with a formation sequence.
  118. \end{thm}
  120. \begin{proof}
  121. Let $F$ be the set of all strings of symbols in the
  122. language~$\Lang L_0$ that have a formation sequence.
  123. We have seen in \olref[pl][syn][fseq]{prop:formed} that
  124. $\Frm[L_0] \subseteq F$, so now we prove the converse.
  126. Suppose $!A$ has a formation sequence $\tuple{!A_0,\dotsc,!A_n}$.
  127. We prove that $!A \in \Frm[L_0]$ by strong induction on~$n$.
  128. Our induction hypothesis is that every string of symbols with a
  129. formation sequence of length $m < n$ is in~$\Frm[L_0]$.
  130. By the definition of a formation sequence, either $!A_n$ is
  131. atomic or there must exist $j,k < n$ such that one of the
  132. following is the case:
  133. \begin{enumerate}
  134. \tagitem{prvNot}{$!A_n \ident \lnot !A_j$.}{}%
  135. \tagitem{prvAnd}{$!A_n \ident (!A_j \land !A_k)$.}{}%
  136. \tagitem{prvOr}{$!A_n \ident (!A_j \lor !A_k)$.}{}%
  137. \tagitem{prvIf}{$!A_n \ident (!A_j \lif !A_k)$.}{}%
  138. \tagitem{prvIff}{$!A_n \ident (!A_j \liff !A_k)$.}{}%
  139. \end{enumerate}
  140. Now we reason by cases. If $!A_n$ is atomic then
  141. $!A_n \in \Frm[L_0]$. Suppose instead that $!A \equiv
  142. (!A_j \land !A_k)$. By \olref[pl][syn][fseq]{lem:fseq-init},
  143. $\tuple{!A_0,\dotsc,!A_j}$ and $\tuple{!A_0,\dotsc,!A_k}$ are
  144. formation sequences for $!A_j$ and~$!A_k$ respectively. Since
  145. these are proper initial subsequences of the formation sequence
  146. for~$!A$, they both have length less than~$n$. Therefore by
  147. the induction hypothesis, $!A_j$ and~$!A_k$ are in~$\Frm[L_0]$,
  148. and so by the definition of !!a{formula}, so is
  149. $(!A_j \land !A_k)$. The other cases follow by parallel
  150. reasoning.
  151. \end{proof}
  153. \end{document}

content/propositional-logic/syntax-and-semantics/formulas.tex

182 lines; SHA-256 8777d77e48e3a41a527b1b737c67e00cb7850f4fa0902ce24846000b40724756. Open the preserved source file.

  1. % Part: propositional-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: formulas
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{pl}{syn}{fml}
  11. \olsection{Propositional \usetoken{P}{formula}}
  13. !!^{formula}s of propositional logic are built up from
  14. \emph{!!{propositional
  15. variable}s}\iftag{prvFalse}{\iftag{prvTrue}{,}{ and} the
  16. propositional constant~$\lfalse$}{}\iftag{prvTrue}{\iftag{prvFalse}{
  17. and}{} the propositional constant~$\ltrue$}{} using \emph{logical
  18. connectives}.
  20. \begin{enumerate}
  21. \item !!^a{denumerable} set~$\PVar$ of !!{propositional variable}s $\Obj p_0$,
  22. $\Obj p_1$, \dots
  23. \tagitem{prvFalse}{The propositional constant for !!{falsity}~$\lfalse$.}{}
  24. \tagitem{prvTrue}{The propositional constant for !!{truth}~$\ltrue$.}{}
  25. \item The logical connectives:
  26. \startycommalist
  27. \iftag{prvNot}{\ycomma $\lnot$ (negation)}{}%
  28. \iftag{prvAnd}{\ycomma $\land$ (conjunction)}{}%
  29. \iftag{prvOr}{\ycomma $\lor$ (disjunction)}{}%
  30. \iftag{prvIf}{\ycomma $\lif$ (!!{conditional})}{}%
  31. \iftag{prvIff}{\ycomma $\liff$ (!!{biconditional})}{}%
  32. \item Punctuation marks: (, ), and the comma.
  33. \end{enumerate}
  35. We denote this language of propositional logic by $\Lang L_0$.
  37. \iftag{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}{%
  38. In addition to the primitive connectives introduced
  39. above, we also use the following \emph{defined} symbols:
  40. \startycommalist
  41. \iftag{defNot}{\ycomma $\lnot$ (negation)}{}%
  42. \iftag{defAnd}{\ycomma $\land$ (conjunction)}{}%
  43. \iftag{defOr}{\ycomma $\lor$ (disjunction)}{}%
  44. \iftag{defIf}{\ycomma $\lif$ (!!{conditional})}{}%
  45. \iftag{defIff}{\ycomma $\liff$ (!!{biconditional})}{}%
  46. \iftag{defFalse}{\ycomma $\lfalse$ (!!{falsity})}{}%
  47. \iftag{defTrue}{\ycomma $\ltrue$ (!!{truth})}}{}.
  49. \begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}
  50. \begin{explain}
  51. A defined symbol is not officially part of the language, but is
  52. introduced as an informal abbreviation: it allows us to abbreviate
  53. formulas which would, if we only used primitive symbols, get quite
  54. long. This is obviously an advantage. The bigger advantage, however,
  55. is that proofs become shorter. If a symbol is primitive, it has to be
  56. treated separately in proofs. The more primitive symbols, therefore,
  57. the longer our proofs.
  58. \end{explain}
  59. \end{tagblock}
  61. % Alternate symbols
  63. \begin{intro}
  64. You may be familiar with different terminology and symbols than the
  65. ones we use above. Logic texts (and teachers) commonly use either
  66. $\sim$, $\neg$, and~!\ for ``negation'', $\wedge$, $\cdot$, and $\&$
  67. for ``conjunction''. Commonly used symbols for the ``conditional'' or
  68. ``implication'' are $\rightarrow$, $\Rightarrow$, and $\supset$.
  69. \iftag{prvIff,defIff}{Symbols for ``biconditional,'' ``bi-implication,''
  70. or ``(material) equivalence'' are $\leftrightarrow$,
  71. $\Leftrightarrow$, and $\equiv$.}{}
  72. \iftag{prvFalse,defFalse}{The $\lfalse$ symbol is variously called
  73. ``falsity,'' ``falsum,'' ``absurdity,'' or ``bottom.''}{}
  74. \iftag{prvTrue,defTrue}{The $\ltrue$ symbol is variously called
  75. ``truth,'' ``verum,'' or ``top.''}{}
  76. \end{intro}
  78. \begin{defn}[Formula]
  79. \ollabel{defn:formulas}
  80. The set~$\Frm[L_0]$ of \emph{!!{formula}s} of propositional logic
  81. is defined inductively as follows:
  82. \begin{enumerate}
  83. \tagitem{prvFalse}{$\lfalse$ is an atomic !!{formula}.}{}
  85. \tagitem{prvTrue}{$\ltrue$ is an atomic !!{formula}.}{}
  87. \item Every !!{propositional variable}~$\Obj p_i$ is an atomic
  88. !!{formula}.
  90. \tagitem{prvNot}{If $!A$ is !!a{formula}, then $\lnot !A$ is
  91. !!a{formula}.}{}
  93. \tagitem{prvAnd}{If $!A$ and $!B$ are !!{formula}s, then $(!A \land
  94. !B)$ is !!a{formula}.}{}
  96. \tagitem{prvOr}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lor !B)$
  97. is !!a{formula}.}{}
  99. \tagitem{prvIf}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lif !B)$
  100. is !!a{formula}.}{}
  102. \tagitem{prvIff}{If $!A$ and $!B$ are !!{formula}s, then $(!A \liff !B)$
  103. is !!a{formula}.}{}
  105. \tagitem{limitClause}{Nothing else is !!a{formula}.}{}
  106. \end{enumerate}
  107. \end{defn}
  109. \begin{explain}
  110. The definition of !!{formula}s is an
  111. \emph{inductive definition}. Essentially, we construct the set of
  112. !!{formula}s in infinitely many stages. In the initial stage, we
  113. pronounce all atomic formulas to be formulas; this corresponds to the
  114. first few cases of the definition, i.e., the cases for
  115. \iftag{prvTrue}{$\ltrue$, }{}%
  116. \iftag{prvFalse}{$\lfalse$, }{}%
  117. $\Obj p_i$. ``Atomic !!{formula}''
  118. thus means any !!{formula} of this form.
  120. The other cases of the definition give rules for constructing new
  121. !!{formula}s out of !!{formula}s already constructed. At the second
  122. stage, we can use them to construct !!{formula}s out of atomic
  123. !!{formula}s. At the third stage, we construct new formulas from the
  124. atomic formulas and those obtained in the second stage, and so on. A
  125. !!{formula} is anything that is eventually constructed at such a
  126. stage, and nothing else.
  127. \end{explain}
  129. When writing a formula $(!B \ast !C)$ constructed from $!B$, $!C$
  130. using a two-place connective~$\ast$, we will often leave out the
  131. outermost pair of parentheses and write simply~$!B \ast !C$.
  133. \begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}
  134. \begin{defn}
  135. Formulas constructed using the defined operators are to be understood
  136. as follows:
  138. \begin{tagenumerate}{defTrue,defFalse,defNot,defOr,defAnd,defIf,defIff,defEx,defAll}
  140. \tagitem{defTrue}{$\ltrue$ abbreviates
  141. \iftag{prvFalse}{$\lnot\lfalse$}{$(!A \lor \lnot !A)$ for some
  142. fixed atomic !!{formula}~$!A$}.}{}
  144. \tagitem{defFalse}{$\lfalse$ abbreviates
  145. \iftag{prvTrue}{$\lnot\ltrue$}{$(!A \land \lnot !A)$ for some
  146. fixed atomic !!{formula}~$!A$}.}{}
  148. \tagitem{defNot}{$\lnot !A$ abbreviates $!A \lif \lfalse$.}{}
  150. \tagitem{defOr}{$!A \lor !B$ abbreviates
  151. \iftag{prvAnd}{$\lnot(\lnot !A \land \lnot !B)$}{$\lnot !A \lif
  152. !B$}.}{}
  154. \tagitem{defAnd}{$!A \land !B$ abbreviates
  155. \iftag{prvOr}{$\lnot(\lnot !A \lor \lnot !B)$}{$\lnot (!A \lif
  156. \lnot !B)$}.}{}
  158. \tagitem{defIf}{$!A \lif !B$ abbreviates
  159. \iftag{prvOr}{$\lnot !A \lor !B)$}{$\lnot (!A \land \lnot !B)$}.}{}
  161. \tagitem{defIff}{$!A \liff !B$ abbreviates $(!A \lif !B) \land (!B
  162. \lif !A)$.}{}
  163. \end{tagenumerate}
  164. \end{defn}
  165. \end{tagblock}
  167. \begin{defn}[Syntactic identity]
  168. The symbol $\ident$ expresses syntactic identity between strings of
  169. symbols, i.e., $!A \ident !B$ iff $!A$ and $!B$ are strings of symbols
  170. of the same length and which contain the same symbol in each place.
  171. \end{defn}
  173. The $\ident$ symbol may be flanked by strings obtained by
  174. concatenation, e.g., $!A \ident (!B \lor !C)$ means: the string of
  175. symbols~$!A$ is the same string as the one obtained by concatenating
  176. an opening parenthesis, the string $!B$, the $\lor$ symbol, the
  177. string~$!C$, and a closing parenthesis, in this order. If this is the
  178. case, then we know that the first symbol of $!A$ is an opening
  179. parenthesis, $!A$ contains $!B$ as a substring (starting at the second
  180. symbol), that substring is followed by $\lor$, etc.
  182. \end{document}

content/propositional-logic/syntax-and-semantics/introduction.tex

79 lines; SHA-256 2ad06497283fa1399d56862c75caf1a418bb753fbb0195658af9f0c57183a441. Open the preserved source file.

  1. % Part: propositional-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: introduction
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{pl}{syn}{int}
  11. \olsection{Introduction}
  13. Propositional logic deals with !!{formula}s that are built from
  14. !!{propositional variable}s using the propositional connectives
  15. $\lnot$, $\land$, $\lor$, $\lif$, and $\liff$. Intuitively,
  16. !!a{propositional variable}~$p$ stands for a sentence or proposition
  17. that is true or false. Whenever the ``truth value'' of the
  18. !!{propositional variable} in !!a{formula} is determined, so is the
  19. truth value of any !!{formula}s formed from them using propositional
  20. connectives. We say that propositional logic is \emph{truth
  21. functional}, because its semantics is given by functions of truth
  22. values. In particular, in propositional logic we leave out of
  23. consideration any further determination of truth and falsity, e.g.,
  24. whether something is necessarily true rather than just contingently
  25. true, or whether something is known to be true, or whether something
  26. is true now rather than was true or will be true. We only consider
  27. two truth values true ($\True$) and false ($\False$), and so exclude
  28. from discussion the possibility that a statement may be neither true
  29. nor false, or only half true. We also concentrate only on connectives where
  30. the truth value of !!a{formula} built from them is completely
  31. determined by the truth values of its parts (and not, say, on its
  32. meaning). In particular, whether the truth value of conditionals in
  33. English is truth functional in this sense is contentious. The material
  34. conditional~$\lif$ is; other logics deal with conditionals that are
  35. not truth functional.
  37. In order to develop the theory and metatheory of truth-functional
  38. propositional logic, we must first define the syntax and semantics of
  39. its expressions. We will describe one way of constructing
  40. !!{formula}s from !!{propositional variable}s using the connectives.
  41. Alternative definitions are possible. Other systems will choose
  42. different symbols, will select different sets of connectives as
  43. primitive, and will use parentheses differently (or even not at all,
  44. as in the case of so-called Polish notation). What all approaches
  45. have in common, though, is that the formation rules define the set of
  46. !!{formula}s \emph{inductively}. If done properly, every expression
  47. can result essentially in only one way according to the formation
  48. rules. The inductive definition resulting in expressions that are
  49. \emph{uniquely readable} means we can give meanings to these
  50. expressions using the same method---inductive definition.
  52. Giving the meaning of expressions is the domain of semantics. The
  53. central concept in semantics for propositional logic is that of
  54. satisfaction in !!a{valuation}. !!^a{valuation}~$\pAssign{v}$ assigns
  55. truth values $\True$, $\False$ to the !!{propositional variable}s. Any
  56. !!{valuation} determines a truth value $\pValue{v}(!A)$ for any
  57. !!{formula}~$!A$. !!^a{formula} is satisfied in
  58. !!a{valuation}~$\pAssign{v}$ iff $\pValue{v}(!A) = \True$---we write
  59. this as $\pSat{v}{!A}$. This relation can also be defined by induction on
  60. the structure of~$!A$, using the truth functions for the logical
  61. connectives to define, say, satisfaction of $!A \land !B$ in terms of
  62. satisfaction (or not) of $!A$ and~$!B$.
  64. On the basis of the satisfaction relation $\pSat{v}{!A}$ for sentences
  65. we can then define the basic semantic notions of tautology,
  66. entailment, and satisfiability. !!^a{formula} is a tautology,
  67. $\Entails !A$, if every !!{valuation} satisfies it, i.e.,
  68. $\pValue{v}(!A) = \True$ for any~$\pAssign{v}$. It is entailed by a
  69. set of !!{formula}s, $\Gamma \Entails !A$, if every !!{valuation} that
  70. satisfies all the !!{formula}s in~$\Gamma$ also satisfies~$!A$. And a
  71. set of !!{formula}s is satisfiable if some !!{valuation} satisfies all
  72. !!{formula}s in it at the same time. Because !!{formula}s are
  73. inductively defined, and satisfaction is in turn defined by induction
  74. on the structure of !!{formula}s, we can use induction to prove
  75. properties of our semantics and to relate the semantic notions
  76. defined.
  79. \end{document}

content/propositional-logic/syntax-and-semantics/preliminaries.tex

120 lines; SHA-256 78673f8419aa1f936f1ecc5629c0fa92c74fd4ee3102badf5f389e3d775f48d6. Open the preserved source file.

  1. % Part: propositional-logic
  2. % Chapter: propositional-logic
  3. % Section: preliminaries
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{pl}{syn}{pre}
  11. \olsection{Preliminaries}
  13. \begin{thm}[\emph{Principle of induction on !!{formula}s}]
  14. \ollabel{thm:induction}
  15. If some property~$P$ holds for all the atomic !!{formula}s and is
  16. such that
  17. \begin{enumerate}
  18. \tagitem{prvNot}{it holds for $\lnot !A$ whenever it holds
  19. for~$!A$;}{}
  20. \tagitem{prvAnd}{it holds for $(!A \land !B)$
  21. whenever it holds for $!A$ and~$!B$;}{}
  22. \tagitem{prvOr}{it holds for $(!A \lor !B)$
  23. whenever it holds for $!A$ and~$!B$;}{}
  24. \tagitem{prvIf}{it holds for $(!A \lif !B)$
  25. whenever it holds for $!A$ and~$!B$;}{}
  26. \tagitem{prvIff}{it holds for $(!A \liff !B)$
  27. whenever it holds for $!A$ and~$!B$;}{}
  28. \end{enumerate}
  29. then $P$ holds for all !!{formula}s.
  30. \end{thm}
  32. \begin{proof}
  33. Let $S$ be the collection of all !!{formula}s with
  34. property~$P$. Clearly $S \subseteq \Frm[L_0]$. $S$~satisfies all the
  35. conditions of \olref[fml]{defn:formulas}: it contains all atomic
  36. !!{formula}s and is closed under the !!{operator}s. $\Frm[L_0]$ is
  37. the smallest such class, so $\Frm[L_0] \subseteq S$. So $\Frm[L_0] = S$, and
  38. every formula has property~$P$.
  39. \end{proof}
  41. \begin{prop}\ollabel{prop:balanced}
  42. Any !!{formula} in~$\Frm[L_0]$ is \emph{balanced}, in that it has
  43. as many left parentheses as right ones.
  44. \end{prop}
  46. \begin{prob}
  47. Prove \olref[pl][syn][pre]{prop:balanced}
  48. \end{prob}
  50. \begin{prop} \ollabel{prop:noinit}
  51. No proper initial segment of !!a{formula} is !!a{formula}.
  52. \end{prop}
  54. \begin{prob}
  55. Prove \olref[pl][syn][pre]{prop:noinit}
  56. \end{prob}
  58. \begin{prop}[Unique Readability]
  59. Any !!{formula}~$!A$ in $ \Frm[L_0]$ has exactly one parsing as one of
  60. the following
  61. \begin{enumerate}
  62. \tagitem{prvFalse}{$\lfalse$.}{}
  64. \tagitem{prvTrue}{$\ltrue$.}{}
  66. \item $\Obj p_n$ for some $\Obj p_n \in \PVar$.
  68. \tagitem{prvNot}{$\lnot !B$ for some !!{formula}~$!B$.}{}
  70. \tagitem{prvAnd}{$(!B \land !C)$ for some !!{formula}s $!B$ and~$!C$.}{}
  72. \tagitem{prvOr}{$(!B \lor !C)$ for some !!{formula}s $!B$ and~$!C$.}{}
  74. \tagitem{prvIf}{$(!B \lif !C)$ for some !!{formula}s $!B$ and~$!C$.}{}
  76. \tagitem{prvIff}{$(!B \liff !C)$ for some !!{formula}s $!B$ and~$!C$.}{}
  77. \end{enumerate}
  78. Moreover, this parsing is \emph{unique}.
  79. \end{prop}
  81. \begin{proof}
  82. By induction on $!A$. For instance, suppose that $!A$ has two distinct
  83. readings as $(!B \lif !C)$ and $(!B' \lif !C')$. Then $!B$ and $!B'$
  84. must be the same (or else one would be a proper initial segment of the
  85. other); so if the two readings of $!A$ are distinct it must be because
  86. $!C$ and $!C'$ are distinct readings of the same sequence of symbols,
  87. which is impossible by the inductive hypothesis.
  88. \end{proof}
  91. \begin{defn}[Uniform Substitution]
  92. If $!A$ and $!B$ are !!{formula}s, and $\Obj p_i$ is a !!{propositional
  93. variable}, then $\Subst{!A}{!B}{\Obj p_i}$ denotes the result of
  94. replacing each occurrence of $\Obj p_i$ by an occurrence of $!B$ in $!A$;
  95. similarly, the simultaneous substitution of $\Obj p_1$, \dots,~$\Obj p_n$ by
  96. !!{formula}s $!B_1$, \dots,~$!B_n$ is denoted by
  97. $\SSubst{!A}{\subst{!B_1}{\Obj p_1},\dots,\subst{!B_n}{\Obj p_n}}$.
  98. \end{defn}
  100. \begin{prob} For each of the five !!{formula}s below determine whether the
  101. !!{formula} can be expressed as a substitution \( \Subst{!A}{!B}{\Obj p_i} \)
  102. where \( !A \) is (i) \( \Obj p_0 \); (ii) \( ( \lnot \Obj p_0 \land \Obj
  103. p_1) \); and (iii) \( ( ( \lnot \Obj p_0 \lif \Obj p_1 ) \land \Obj
  104. p_2 ) \). In each case specify the relevant substitution.
  105. \begin{enumerate}
  106. \item \( \Obj p_1 \)
  107. \item \( ( \lnot \Obj p_0 \land \Obj p_0 ) \)
  108. \item \( ( ( \Obj p_0 \lor \Obj p_1 ) \land \Obj p_2 ) \)
  109. \item \( \lnot ( ( \Obj p_0 \lif \Obj p_1 ) \land \Obj p_2 ) \)
  110. \item \( (( \lnot ( \Obj p_0 \lif \Obj p_1 ) \lif ( \Obj p_0 \lor \Obj p_1 )) \land \lnot ( \Obj p_0 \land \Obj p_1 )) \)
  111. \end{enumerate}
  112. \end{prob}
  114. \begin{prob}
  115. Give a mathematically rigorous definition of $\Subst{!A}{!B}{p}$ by
  116. induction.
  117. \end{prob}
  119. \end{document}

content/propositional-logic/syntax-and-semantics/semantic-notions.tex

96 lines; SHA-256 0167b2bab0dc2a75d011556643190a246d29831244a60bde5515b1b2f431406a. Open the preserved source file.

  1. % Part: propositional-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: semantic-notions
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{pl}{syn}{sem}
  11. \olsection{Semantic Notions}
  13. We define the following semantic notions:
  15. \begin{defn}
  16. \begin{enumerate}
  17. \item !!^a{formula}~$!A$ is \emph{satisfiable} if for
  18. some~$\pAssign{v}$, $\pSat{v}{!A}$; it is
  19. \emph{unsatisfiable} if for no $\pAssign{v}$, $\pSat{v}{!A}$;
  20. \item !!^a{formula}~$!A$ is a \emph{tautology} if $\pSat{v}{!A}$ for
  21. all !!{valuation}s~$\pAssign{v}$;
  22. \item !!^a{formula}~$!A$ is \emph{contingent} if it is satisfiable but
  23. not a tautology;
  24. \item If $\Gamma$ is a set of !!{formula}s, $\Gamma \Entails !A$ (``$\Gamma$
  25. entails $!A$'') if and only if $\pSat{v}{!A}$ for every
  26. !!{valuation}~$\pAssign{v}$ for which $\pSat{v}{\Gamma}$.
  27. \item If $\Gamma$ is a set of !!{formula}s, $\Gamma$ is
  28. \emph{satisfiable} if there is !!a{valuation}~$\pAssign{v}$ for which
  29. $\pSat{v}{\Gamma}$, and $\Gamma$ is
  30. \emph{unsatisfiable} otherwise.
  31. \end{enumerate}
  32. \end{defn}
  34. \begin{prob}
  35. For each of the following four !!{formula}s determine whether it
  36. is (a)~satisfiable, (b)~tautology, and (c)~contingent.
  37. \begin{enumerate}
  38. \item \( ( \Obj p_0 \lif ( \lnot \Obj p_1 \lif \lnot \Obj p_0 ) ) \).
  39. \item \( ( ( \Obj p_0 \land \lnot \Obj p_1 ) \lif ( \lnot \Obj p_0 \land \Obj p_2 )) \liff ( ( \Obj p_2 \lif \Obj p_0 ) \lif ( \Obj p_0 \lif \Obj p_1 )) \).
  40. \item \( ( \Obj p_0 \liff \Obj p_1 ) \lif ( \Obj p_2 \liff \lnot \Obj p_1 ) \).
  41. \item \( (( \Obj p_0 \liff ( \lnot \Obj p_1 \land \Obj p_2 )) \lor ( \Obj p_2 \lif ( \Obj p_0 \liff \Obj p_1 ))) \).
  42. \end{enumerate}
  43. \end{prob}
  45. \begin{prop}
  46. \ollabel{prop:semanticalfacts}
  47. \begin{enumerate}
  48. \item $!A$ is a tautology if and only if
  49. $\emptyset \Entails !A$;
  50. \item If $\Gamma \Entails !A$ and $\Gamma \Entails !A \lif !B$ then
  51. $\Gamma \Entails !B$;
  52. \item If $\Gamma$ is satisfiable then every finite subset of $\Gamma$
  53. is also satisfiable;
  54. \item \ollabel{def:monotonicity} Monotonicity: if $\Gamma \subseteq \Delta$
  55. and $\Gamma \Entails !A$ then also $\Delta \Entails !A$;
  56. \item \ollabel{def:Cut} Transitivity: if $\Gamma \Entails !A$ and
  57. $\Delta \cup \{ !A\} \Entails !B$ then $\Gamma \cup \Delta \Entails
  58. !B$.
  59. \end{enumerate}
  60. \end{prop}
  62. \begin{proof}
  63. Exercise.
  64. \end{proof}
  66. \begin{prob}
  67. Prove \olref[pl][syn][sem]{prop:semanticalfacts}
  68. \end{prob}
  70. \begin{prop}\ollabel{prop:entails-unsat}
  71. $\Gamma \Entails !A$ if and only if $\Gamma \cup \{\lnot !A\}$
  72. is unsatisfiable.
  73. \end{prop}
  75. \begin{proof}
  76. Exercise.
  77. \end{proof}
  79. \begin{prob}
  80. Prove \olref[pl][syn][sem]{prop:entails-unsat}
  81. \end{prob}
  83. \begin{thm}[Semantic Deduction Theorem]
  84. \ollabel{thm:sem-deduction} $\Gamma \Entails !A \lif !B$ if and only
  85. if $\Gamma \cup \{!A\} \Entails !B$.
  86. \end{thm}
  88. \begin{proof}
  89. Exercise.
  90. \end{proof}
  92. \begin{prob}
  93. Prove \olref[pl][syn][sem]{thm:sem-deduction}
  94. \end{prob}
  96. \end{document}

content/propositional-logic/syntax-and-semantics/syntax-and-semantics.tex

30 lines; SHA-256 799d1dab63cda19a28c1dbf7097052fb790bbce609aecd5367d2e368decdb18b. Open the preserved source file.

  1. % Part: propositional-logic
  2. % Chapter: syntax-and-semantics
  4. \documentclass[../../../include/open-logic-chapter]{subfiles}
  6. \begin{document}
  8. \olchapter{pl}{syn}{Syntax and Semantics}
  10. \begin{editorial}
  11. This is a very quick summary of definitions only. It should be
  12. expanded to provide a gentle intro to proofs by induction on
  13. formulas, with lots more examples.
  14. \end{editorial}
  16. \olimport{introduction}
  18. \olimport{formulas}
  20. \olimport{preliminaries}
  22. \olimport{formation-sequences}
  24. \olimport{valuations-sat}
  26. \olimport{semantic-notions}
  28. \OLEndChapterHook
  30. \end{document}

content/propositional-logic/syntax-and-semantics/valuations-sat.tex

198 lines; SHA-256 d1454e8c2366f3a204a371523f41feacbdc72402f7a3a7ae6635b60b17c90481. Open the preserved source file.

  1. % Part: propositional-logic
  2. % Chapter: syntax-and-semantics
  3. % Section: valuations-sat
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{pl}{syn}{val}
  11. \olsection{\usetoken{P}{valuation} and Satisfaction}
  13. \begin{defn}[!!^{valuation}s]
  14. Let $\{\True, \False\}$ be the set of the two truth values, ``true''
  15. and ``false.'' A \emph{!!{valuation}} for $\Lang{L_0}$ is a
  16. function~$\pAssign{v}$ assigning either $\True$ or $\False$ to the
  17. !!{propositional variable}s of the language, i.e., $\pAssign{v} \colon
  18. \PVar \to \{\True, \False \}$.
  19. \end{defn}
  21. \begin{defn}
  22. Given !!a{valuation}~$\pAssign{v}$, define the evaluation function
  23. $\pValue{v} \colon \Frm[L_0] \to \{\True, \False \}$ inductively by:
  24. \begin{align*}
  25. \iftag{prvFalse}{\pValue{v}(\lfalse) & = \False; \\}{}
  26. \iftag{prvTrue}{\pValue{v}(\ltrue) & = \True; \\}{}
  27. \pValue{v}(\Obj p_n) & = \pAssign{v}(\Obj p_n); \\
  28. \iftag{prvNot}{\pValue{v}(\lnot !A) & = \begin{cases}
  29. \True & \text{if } \pValue{v}(!A) = \False;\\
  30. \False & \text{otherwise.}
  31. \end{cases} \\ }{}
  32. \iftag{prvAnd}{\pValue{v}(!A \land !B) & = \begin{cases}
  33. \True &
  34. \text{if $\pValue{v}(!A) = \True$ and $\pValue{v}(!B) = \True$;}\\
  35. \False &
  36. \text{if $\pValue{v}(!A) = \False$ or $\pValue{v}(!B) = \False$}.
  37. \end{cases}\\}{}
  38. \iftag{prvOr}{\pValue{v}(!A \lor !B) & = \begin{cases}
  39. \True &
  40. \text{if $\pValue{v}(!A) = \True$ or $\pValue{v}(!B) = \True$;}\\
  41. \False &
  42. \text{if $\pValue{v}(!A) = \False$ and $\pValue{v}(!B) = \False$}.
  43. \end{cases}\\}{}
  44. \iftag{prvIf}{\pValue{v}(!A \lif !B) & = \begin{cases}
  45. \True &
  46. \text{if $\pValue{v}(!A) = \False$ or $\pValue{v}(!B) = \True$;}\\
  47. \False &
  48. \text{if $\pValue{v}(!A) = \True$ and $\pValue{v}(!B) = \False$}.
  49. \end{cases}\\}{}
  50. \iftag{prvIff}{\pValue{v}(!A \liff !B) & = \begin{cases}
  51. \True &
  52. \text{if $\pValue{v}(!A) = \pValue{v}(!B)$;}\\
  53. \False &
  54. \text{if $\pValue{v}(!A) \neq \pValue{v}(!B)$}.
  55. \end{cases}}{}
  56. \end{align*}
  57. \end{defn}
  59. \begin{explain}
  60. The clauses correspond to the following truth tables:
  61. \begin{center}
  62. \iftag{prvNot}{
  63. \begin{tabular}{|c||c|} \hline
  64. $!A$ & $ \lnot !A$ \\
  65. \hline \hline
  66. $\True$ & $\False$ \\
  67. $\False$ & $\True$ \\
  68. \hline
  69. \end{tabular}
  70. }{}
  71. \iftag{prvAnd}{
  72. \begin{tabular}{|cc||c|} \hline
  73. $!A$ & $!B$ & $!A \land !B$ \\
  74. \hline \hline
  75. $\True$ & $\True$ & $\True$ \\
  76. $\True$ & $\False$ & $\False$ \\
  77. $\False$ & $\True$ & $\False$ \\
  78. $\False$ & $\False$ & $\False$ \\
  79. \hline
  80. \end{tabular}
  81. }{}
  82. \iftag{prvOr}{
  83. \begin{tabular}{|cc||c|} \hline
  84. $!A$ & $!B$ & $!A \lor !B$ \\
  85. \hline \hline
  86. $\True$ & $\True$ & $\True$ \\
  87. $\True$ & $\False$ & $\True$ \\
  88. $\False$ & $\True$ & $\True$ \\
  89. $\False$ & $\False$ & $\False$ \\
  90. \hline
  91. \end{tabular}
  92. }{}%
  93. \iftag{notprvNot,notprvAnd,notprvOr,notprvIf}{}{\\[1em]}
  94. \iftag{prvIf}{
  95. \begin{tabular}{|cc||c|} \hline
  96. $!A$ & $!B$ & $!A \lif !B$ \\
  97. \hline \hline
  98. $\True$ & $\True$ & $\True$ \\
  99. $\True$ & $\False$ & $\False$ \\
  100. $\False$ & $\True$ & $\True$ \\
  101. $\False$ & $\False$ & $\True$ \\
  102. \hline
  103. \end{tabular}
  104. }{}
  105. \iftag{prvIff}{
  106. \begin{tabular}{|cc||c|} \hline
  107. $!A$ & $!B$ & $!A \liff !B$ \\
  108. \hline \hline
  109. $\True$ & $\True$ & $\True$ \\
  110. $\True$ & $\False$ & $\False$ \\
  111. $\False$ & $\True$ & $\False$ \\
  112. $\False$ & $\False$ & $\True$ \\
  113. \hline
  114. \end{tabular}
  115. }{}
  116. \end{center}
  117. \end{explain}
  119. \begin{prob}
  120. Consider adding to $\Lang{L_0}$ a ternary connective $\diamondsuit$
  121. with evaluation given by
  122. \begin{gather*}
  123. \pValue{v}(\diamondsuit( !A , !B , !C ) ) = \begin{cases}
  124. \pValue{v}( !B ) &
  125. \text{if $\pValue{v}(!A) = \True$;}\\
  126. \pValue{v}( !C ) &
  127. \text{if $\pValue{v}(!A) = \False $}.
  128. \end{cases}
  129. \end{gather*}
  130. Write down the truth table for this connective.
  131. \end{prob}
  133. \begin{thm}[Local Determination]
  134. \ollabel{thm:LocalDetermination} Suppose that $\pAssign{v_1}$ and
  135. $\pAssign{v_2}$ are !!{valuation}s that agree on the !!{propositional
  136. variable}s occurring in $!A$, i.e., $\pAssign{v_1}(\Obj p_n) =
  137. \pAssign{v_2}(\Obj p_n)$ whenever $\Obj p_n$ occurs in some
  138. !!{formula}~$!A$. Then $\pValue{v_1}$ and $\pValue{v_2}$ also agree
  139. on~$!A$, i.e., $\pValue{v_1}(!A) = \pValue{v_2}(!A)$.
  140. \end{thm}
  142. \begin{proof}
  143. By induction on $!A$.
  144. \end{proof}
  146. \begin{defn}[Satisfaction]
  147. \ollabel{defn:satisfaction} We can inductively define the notion of
  148. \emph{satisfaction of !!a{formula}~$!A$ by
  149. !!a{valuation}~$\pAssign{v}$}, $\pSat{v}{!A}$, as follows.
  150. (We write $\pSat/{v}{!A}$ to mean ``not $\pSat{v}{!A}$.'')
  151. \begin{enumerate}
  152. \tagitem{prvFalse}{%
  153. \indcase{!A}{\lfalse}{$\pSat/{v}{\indfrm}$.}}{}
  155. \tagitem{prvTrue}{%
  156. \indcase{!A}{\ltrue}{$\pSat{v}{\indfrm}$.}}{}
  158. \item \indcase{!A}{\Obj p_i}{$\pSat{v}{\indfrm}$
  159. iff $\pAssign{v}(\Obj p_i) = \True$.}
  161. \tagitem{prvNot}{%
  162. \indcase{!A}{\lnot !B}{$\pSat{v}{\indfrm}$ iff
  163. $\pSat/{v}{!B}$.}}{}
  165. \tagitem{prvAnd}{%
  166. \indcase{!A}{(!B \land !C)}{$\pSat{v}{\indfrm}$ iff $\pSat{v}{!B}$
  167. and $\pSat{v}{!C}$.}}{}
  169. \tagitem{prvOr}{%
  170. \indcase{!A}{(!B \lor !C)}{$\pSat{v}{\indfrm}$ iff
  171. $\pSat{v}{!B}$ or $\pSat{v}{!C}$ (or both).}}{}
  173. \tagitem{prvIf}{%
  174. \indcase{!A}{(!B \lif !C)}{$\pSat{v}{\indfrm}$ iff $\pSat/{v}{!B}$
  175. or $\pSat{v}{!C}$ (or both).}}{}
  177. \tagitem{prvIff}{%
  178. \indcase{!A}{(!B \liff !C)}{$\pSat{v}{\indfrm}$ iff either both
  179. $\pSat{v}{!B}$ and $\pSat{v}{!C}$, or neither $\pSat{v}{!B}$
  180. nor $\pSat{v}{!C}$.}}{}
  181. \end{enumerate}
  182. If $\Gamma$ is a set of !!{formula}s, $\pSat{v}{\Gamma}$ iff
  183. $\pSat{v}{!A}$ for every~$!A \in \Gamma$.
  184. \end{defn}
  186. \begin{prop}\ollabel{prop:sat-value}
  187. $\pSat{v}{!A}$ iff $\pValue{v}(!A) = \True$.
  188. \end{prop}
  190. \begin{proof}
  191. By induction on~$!A$.
  192. \end{proof}
  194. \begin{prob}
  195. Prove \olref[pl][syn][val]{prop:sat-value}
  196. \end{prob}
  198. \end{document}

Propositional Logic: introduction to this part

Verbatim source for the part wrapper; imports and tags are source scaffolding, not omitted book prose.

content/propositional-logic/propositional-logic.tex

% Part: propositional-logic

\documentclass[../../include/open-logic-part]{subfiles}

\begin{document}

\olpart{pl}{Propositional Logic}

\begin{editorial}
  This part contains material on classical propositional logic. The
  first chapter is relatively rudimentary and just lists definitions
  and results, many proofs are not carried out but are left as
  exercises. The material on proof systems and the completeness
  theorem is included from the part on first-order logic, with the
  ``FOL'' tag set to false. This leaves out everything related to
  predicates, terms, and quantifiers, and replaces talk of
  !!{structure}s~$\Struct{M}$ with talk about
  !!{valuation}s~$\pAssign{v}$.

  It is planned to expand this part to include
  more detail, and to add further topics and results, such as
  truth-functional completeness.
\end{editorial}

\olimport[syntax-and-semantics]{syntax-and-semantics}

\tagfalse{FOL}

\olimport[../first-order-logic/proof-systems]{proof-systems}

\iftag{prfSC}{%
  \olimport[../first-order-logic/sequent-calculus]{sequent-calculus}
}{}

\iftag{prfND}{%
  \olimport[../first-order-logic/natural-deduction]{natural-deduction}
}{}

\iftag{prfTab}{%
  \olimport[../first-order-logic/tableaux]{tableaux}
}{}

\iftag{prfAX}{%
  \olimport[../first-order-logic/axiomatic-deduction]{axiomatic-deduction}
}{}

\olimport[../first-order-logic/completeness]{completeness}

\tagtrue{FOL}

\OLEndPartHook

\end{document}