The Open Logic Text

en · official · sha256:de3b4556380933730fba4e63fbb3c53e7c1f9998bb38ac3ae25e3eb82f877262

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: first-order-languages \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{fol} \olsection{First-Order Languages} Expressions of first-order logic are built up from a basic vocabulary containing \emph{!!{variable}s}, \emph{!!{constant}s}, \emph{!!{predicate}s} and sometimes \emph{!!{function}s}. From them, together with logical connectives, quantifiers, and punctuation symbols such as parentheses and commas, \emph{terms} and \emph{!!{formula}s} are formed. \begin{explain} Informally, !!{predicate}s are names for properties and relations, !!{constant}s are names for individual objects, and !!{function}s are names for mappings. These, except for the !!{identity}~$\eq$, are the \emph{non-logical symbols} and together make up a language. Any first-order language~$\Lang L$ is determined by its non-logical symbols. In the most general case, $\Lang L$ contains infinitely many symbols of each kind. \end{explain} In the general case, we make use of the following symbols in first-order logic: \begin{enumerate} \item Logical symbols \begin{enumerate} \item Logical connectives: \startycommalist \iftag{prvNot}{\ycomma $\lnot$ (negation)}{}% \iftag{prvAnd}{\ycomma $\land$ (conjunction)}{}% \iftag{prvOr}{\ycomma $\lor$ (disjunction)}{}% \iftag{prvIf}{\ycomma $\lif$ (!!{conditional})}{}% \iftag{prvIff}{\ycomma $\liff$ (!!{biconditional})}{}% \iftag{prvAll}{\ycomma $\lforall$ (universal quantifier)}{}% \iftag{prvEx}{\ycomma $\lexists$ (existential quantifier)}{}. \tagitem{prvFalse}{The propositional constant for !!{falsity}~$\lfalse$.}{} \tagitem{prvTrue}{The propositional constant for !!{truth}~$\ltrue$.}{} \item The two-place !!{identity}~$\eq$. \item A !!{denumerable}s set of !!{variable}s: $\Obj v_0$, $\Obj v_1$, $\Obj v_2$, \dots \end{enumerate} \item Non-logical symbols, making up the \emph{standard language} of first-order logic \begin{enumerate} \item A !!{denumerable}s set of $n$-place !!{predicate}s for each $n>0$: $\Obj A^n_0$, $\Obj A^n_1$, $\Obj A^n_2$, \dots \item A !!{denumerable}s set of !!{constant}s: $\Obj c_0$, $\Obj c_1$, $\Obj c_2$, \dots. \item A !!{denumerable}s set of $n$-place !!{function}s for each $n>0$: $\Obj f^n_0$, $\Obj f^n_1$, $\Obj f^n_2$, \dots \end{enumerate} \item Punctuation marks: (, ), and the comma. \end{enumerate} Most of our definitions and results will be formulated for the full standard language of first-order logic. However, depending on the application, we may also restrict the language to only a few !!{predicate}s, !!{constant}s, and !!{function}s. \begin{ex} The language~$\Lang L_A$ of arithmetic contains a single two-place !!{predicate}~$<$, a single !!{constant}~$\Obj 0$, one one-place !!{function}~$\prime$, and two two-place !!{function}s~$+$ and~$\times$. \end{ex} \begin{ex} The language of set theory~$\Lang L_Z$ contains only the single two-place !!{predicate}~$\in$. \end{ex} \begin{ex} The language of orders~$\Lang L_\le$ contains only the two-place !!{predicate}~$\le$. \end{ex} Again, these are conventions: officially, these are just aliases, e.g., $<$, $\in$, and $\le$ are aliases for $\Obj A^2_0$, $\Obj 0$ for $\Obj c_0$, $\prime$ for $\Obj f^1_0$, $+$ for $\Obj f^2_0$, $\times$ for $\Obj f^2_1$. \iftag{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}{% In addition to the primitive connectives and \iftag{notprvEx,notprvAll}{quantifier}{quantifiers} introduced above, we also use the following \emph{defined} symbols: \startycommalist \iftag{defNot}{\ycomma $\lnot$ (negation)}{}% \iftag{defAnd}{\ycomma $\land$ (conjunction)}{}% \iftag{defOr}{\ycomma $\lor$ (disjunction)}{}% \iftag{defIf}{\ycomma $\lif$ (!!{conditional})}{}% \iftag{defIff}{\ycomma $\liff$ (!!{biconditional})}{}% \iftag{defAll}{\ycomma $\lforall$ (universal quantifier)}{}% \iftag{defEx}{\ycomma $\lexists$ (existential quantifier)}{}% \iftag{defFalse}{\ycomma !!{falsity}~$\lfalse$}{}% \iftag{defTrue}{\ycomma !!{truth}~$\ltrue$}}{}. \begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll} \begin{explain} A defined symbol is not officially part of the language, but is introduced as an informal abbreviation: it allows us to abbreviate formulas which would, if we only used primitive symbols, get quite long. This is obviously an advantage. The bigger advantage, however, is that proofs become shorter. If a symbol is primitive, it has to be treated separately in proofs. The more primitive symbols, therefore, the longer our proofs. \end{explain} \end{tagblock} % Alternate symbols \begin{intro} You may be familiar with different terminology and symbols than the ones we use above. Logic texts (and teachers) commonly use $\sim$, $\neg$, or~!\ for ``negation'', $\wedge$, $\cdot$, or $\&$ for ``conjunction''. Commonly used symbols for the ``conditional'' or ``implication'' are $\rightarrow$, $\Rightarrow$, and $\supset$. \iftag{prvIff,defIff}{Symbols for ``biconditional,'' ``bi-implication,'' or ``(material) equivalence'' are $\leftrightarrow$, $\Leftrightarrow$, and $\equiv$.}{} \iftag{prvFalse,defFalse}{The $\lfalse$ symbol is variously called ``falsity,'' ``falsum,'', ``absurdity,'' or ``bottom.''}{} \iftag{prvTrue,defTrue}{The $\ltrue$ symbol is variously called ``truth,'' ``verum,'' or ``top.''}{} It is conventional to use lower case letters (e.g., $a$, $b$, $c$) from the beginning of the Latin alphabet for !!{constant}s (sometimes called names), and lower case letters from the end (e.g., $x$, $y$, $z$) for !!{variable}s. Quantifiers combine with !!{variable}s, e.g., $x$; notational variations include $\forall x$, $(\forall x)$, $(x)$, $\Pi x$, $\bigwedge_x$ for the universal quantifier and $\exists x$, $(\exists x)$, $(Ex)$, $\Sigma x$, $\bigvee_x$ for the existential quantifier. \end{intro} \begin{explain} We might treat all the propositional operators and both quantifiers as primitive symbols of the language. We might instead choose a smaller stock of primitive symbols and treat the other !!{operator}s as defined. ``Truth functionally complete'' sets of Boolean operators include $\{ \lnot, \lor \}$, $\{ \lnot, \land \}$, and $\{ \lnot, \lif\}$---these can be combined with either quantifier for an expressively complete first-order language. You may be familiar with two other !!{operator}s: the Sheffer stroke~$|$ (named after Henry Sheffer), and Peirce's arrow~$\downarrow$, also known as Quine's dagger. When given their usual readings of ``nand'' and ``nor'' (respectively), these operators are truth functionally complete by themselves. \end{explain} \end{document}

Referencing norms: CONSTANT_SYMBOL, CommonFragment, FUNCTION_SYMBOL, IDENTITY_SYMBOL, L_FOL, LanguageReachesDirect, LanguageReachesTransitive, OBJECT_VARIABLE, PREDICATE_SYMBOL, in_common_fragment, language_extends, language_reaches

en · official · sha256:7028f22b1918b60034df30060366d761c5949820650a468865a26dcf696755d7

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: free-vars-sentences \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{fvs} \olsection{Free \printtoken{P}{variable} and \printtoken{P}{sentence}} \begin{defn}[Free occurrences of !!a{variable}] \ollabel{defn:free-occ} The \emph{free} occurrences of !!a{variable} in !!a{formula} are defined inductively as follows: \begin{enumerate} \item \indcase*{!A}{$!A$ is atomic}{all !!{variable} occurrences in $\indfrm$ are free.} \tagitem{prvNot}{\indcase{!A}{\lnot !B}{the free !!{variable} occurrences of $\indfrm$ are exactly those of $!B$.}}{} \item \indcase{!A}{(!B \ast !C)}{the free !!{variable} occurrences of $\indfrm$ are those in $!B$ together with those in~$!C$.} \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{the free !!{variable} occurrences in $\indfrm$ are all of those in~$!B$ except for occurrences of~$x$.}}{} \tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{the free !!{variable} occurrences in $\indfrm$ are all of those in~$!B$ except for occurrences of~$x$.}}{} \end{enumerate} \end{defn} \begin{defn}[Bound Variables] An occurrence of !!a{variable} in a formula~$!A$ is \emph{bound} if it is not free. \end{defn} \begin{prob} Give an inductive definition of the bound variable occurrences along the lines of \olref[fol][syn][fvs]{defn:free-occ}. \end{prob} \begin{defn}[Scope] \iftag{prvAll}{If $\lforall[x][!B]$ is an occurrence of a subformula in a formula~$!A$, then the corresponding occurrence of~$!B$ in~$!A$ is called the \emph{scope} of the corresponding occurrence of~$\lforall[x]$. \iftag{prvEx}{Similarly for $\lexists[x]$.}{}}{If $\lexists[x][!B]$ is an occurrence of a subformula in a formula~$!A$, then the corresponding occurrence of~$!B$ in~$!A$ is called the \emph{scope} of the corresponding occurrence of~$\lexists[x]$.} If $!B$ is the scope of a quantifier occurrence \iftag{prvAll}{$\lforall[x]$\iftag{prvEx}{ or $\lexists[x]$}{}}{$\lexists[x]$} in~$!A$, then the free occurrences of $x$ in~$!B$ are bound in \iftag{prvAll}{$\lforall[x][!B]$\iftag{prvEx}{ and $\lexists[x][!B]$}{}}{$\lexists[x][!B]$}. We say that these occurrences are \emph{bound by} the mentioned quantifier occurrence. \end{defn} \begin{ex} Consider the following formula: \[ \lexists[\Obj v_0][\underbrace{\Atom{\Obj A^2_0}{\Obj v_0,\Obj v_1}}_{!B}] \] $!B$ represents the scope of $\lexists[\Obj v_0]$. The quantifier binds the occurrence of $\Obj v_0$ in $!B$, but does not bind the occurrence of $\Obj v_1$. So $\Obj v_1$ is a free variable in this case. We can now see how this might work in a more complicated !!{formula}~$!A$: \[ \lforall[\Obj v_0][\underbrace{(\Atom{\Obj A^1_0}{\Obj v_0} \lif \Atom{\Obj A^2_0}{\Obj v_0, \Obj v_1})}_{!B}] \lif \lexists[\Obj 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}] \] $!B$ is the scope of the first $\lforall[\Obj v_0]$, $!C$ is the scope of $\lexists[\Obj v_1]$, and $!D$ is the scope of the second $\lforall[\Obj v_0]$. The first $\lforall[\Obj v_0]$ binds the occurrences of $\Obj v_0$ in~$!B$, $\lexists[\Obj v_1]$ binds the occurrence of $\Obj v_1$ in $!C$, and the second $\lforall[\Obj v_0]$ binds the occurrence of $\Obj v_0$ in~$!D$. The first occurrence of $\Obj v_1$ and the fourth occurrence of $\Obj v_0$ are free in~$!A$. The last occurrence of $\Obj v_0$ is free in $!D$, but bound in $!C$ and~$!A$. \end{ex} \begin{defn}[Sentence] !!^a{formula}~$!A$ is \article{sentence} \emph{!!{sentence}} iff it contains no free occurrences of !!{variable}s. \end{defn} % add examples! \end{document}

Referencing norms: BOUND_OCCURRENCE, FREE_OCCURRENCE, SCOPE, SENTENCE

en · official · sha256:718aa114fb35380a6407fbdd37b630261cb419dc1cc12cc02a02484f548bfd79

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: main-operator \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{mai} \olsection{\printtoken{S}{main operator} of a Formula} \begin{explain} It is often useful to talk about the last operator used in constructing !!a{formula}~$!A$. This operator is called the \emph{main operator} of~$!A$. Intuitively, it is the ``outermost'' operator of $!A$. For example, the main operator of $\lnot !A$ is $\lnot$, the main operator of $(!A \lor !B)$ is $\lor$, etc. \end{explain} \begin{defn}[!!^{main operator}] \ollabel{def:main-op} The \emph{!!{main operator}} of !!a{formula}~$!A$ is defined as follows: \begin{enumerate} \item \indcase*{!A}{!A}{$\indfrm$ has no !!{main operator}.} \tagitem{prvNot}{\indcase{!A}{\lnot !B}{the !!{main operator} of $\indfrm$ is~$\lnot$.}}{} \tagitem{prvAnd}{\indcase{!A}{(!B \land !C)}{the !!{main operator} of $\indfrm$ is~$\land$.}}{} \tagitem{prvOr}{\indcase{!A}{(!B \lor !C)}{the !!{main operator} of $\indfrm$ is~$\lor$.}}{} \tagitem{prvIf}{\indcase{!A}{(!B \lif !C)}{the !!{main operator} of $\indfrm$ is~$\lif$.}}{} \tagitem{prvIff}{\indcase{!A}{(!B \liff !C)}{the !!{main operator} of $\indfrm$ is~$\liff$.}}{} \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{the !!{main operator} of $\indfrm$ is~$\lforall$.}}{} \tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{the !!{main operator} of $\indfrm$ is~$\lexists$.}}{} \end{enumerate} \end{defn} In each case, we intend the specific indicated \emph{occurrence} of the !!{main operator} in the formula. For instance, since the formula $((!D \lif !E) \lif (!E \lif !D))$ is of the form $(!B \lif !C)$ where $!B$ is $(!D \lif !E)$ and $!C$ is $(!E \lif !D)$, the second occurrence of $\lif$ is the !!{main operator}. \begin{explain} This is a \emph{recursive} definition of a function which maps all non-atomic !!{formula}s to their !!{main operator} occurrence. Because of the way !!{formula}s are defined inductively, every !!{formula}~$!A$ satisfies one of the cases in \olref{def:main-op}. This guarantees that for each non-atomic !!{formula}~$!A$ !!a{main operator} exists. Because each !!{formula} satisfies only one of these conditions, and because the smaller !!{formula}s from which $!A$ is constructed are uniquely determined in each case, the !!{main operator} occurrence of~$!A$ is unique, and so we have defined a function. \end{explain} We call !!{formula}s by the names in \olref{tab:main-op} depending on which symbol their !!{main operator} is.\iftag{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll} { Recall, however, that defined operators do not officially appear in !!{formula}s. They are just abbreviations, so officially they cannot be the main operator of a formula. In proofs about all !!{formula}s they therefore do not have to be treated separately.} \begin{table}[!h] \centering \begin{tabular}{c | c | c} !!^{main operator} & Type of !!{formula} & Example\\ \hline none & atomic (!!{formula}) & \iftag{prvFalse}{$\lfalse$,}{} \iftag{prvTrue}{$\ltrue$,}{} $\Atom{R}{t_1, \dots, t_n}$, $\eq[t_1][t_2]$\\ $\lnot$ & negation & $\lnot !A$ \\ $\land$ & conjunction & $(!A \land !B$) \\ $\lor$ & disjunction & $(!A \lor !B$) \\ $\lif$ & !!{conditional} & $(!A \lif !B$) \\ $\liff$ & !!{biconditional} & $(!A \liff !B)$ \\ $\lforall[][]$ & universal (!!{formula})& $\lforall[x][!A]$ \\ $\lexists[][]$ & existential (!!{formula})& $\lexists[x][!A]$ \end{tabular} \caption{Main operator and names of !!{formula}s} \ollabel{tab:main-op} \end{table} \end{document}

Referencing norms: MAIN_OPERATOR

en · official · sha256:bc7340aac83c25a83bb328ed2eff94dd48c05d616bdcb302e6442ba2eacea116

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: subformulas \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{sbf} \olsection{\printtoken{P}{subformula}} \begin{explain} It is often useful to talk about the !!{formula}s that ``make up'' a given !!{formula}. We call these its \emph{!!{subformula}s}. Any !!{formula} counts as !!a{subformula} of itself; a subformula of $!A$ other than $!A$ itself is a \emph{proper !!{subformula}}. \end{explain} \begin{defn}[Immediate !!^{subformula}] If $!A$ is !!a{formula}, the \emph{immediate !!{subformula}s} of $!A$ are defined inductively as follows: \begin{enumerate} \item Atomic !!{formula}s have no immediate !!{subformula}s. \tagitem{prvNot}{\indcase{!A}{\lnot !B}{The only immediate !!{subformula} of $\indfrm$ is~$!B$.}}{} \item \indcase{!A}{(!B \ast !C)}{The immediate !!{subformula}s of $\indfrm$ are $!B$ and $!C$ ($\ast$ is any one of the two-place connectives).} \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{The only immediate !!{subformula} of $\indfrm$ is~$!B$.}}{} \tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{The only immediate !!{subformula} of $\indfrm$ is~$!B$.}}{} \end{enumerate} \end{defn} \begin{defn}[Proper !!^{subformula}] If $!A$ is !!a{formula}, the \emph{proper !!{subformula}s} of $!A$ are defined recursively as follows: \begin{enumerate} \item Atomic !!{formula}s have no proper !!{subformula}s. \tagitem{prvNot}{\indcase{!A}{\lnot !B}{The proper !!{subformula}s of $\indfrm$ are~$!B$ together with all proper !!{subformula}s of~$!B$.}}{} \item \indcase{!A}{(!B \ast !C)}{The proper !!{subformula}s of $\indfrm$ are $!B$, $!C$, together with all proper !!{subformula}s of $!B$ and those of~$!C$.} \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{The proper !!{subformula}s of $\indfrm$ are~$!B$ together with all proper !!{subformula}s of~$!B$.}}{} \tagitem{prvEx}{\indcase{!A}{\lexists[x][!B]}{The proper !!{subformula}s of $\indfrm$ are~$!B$ together with all proper !!{subformula}s of~$!B$.}}{} \end{enumerate} \end{defn} \begin{defn}[!!^{subformula}] The !!{subformula}s of $!A$ are $!A$ itself together with all its proper !!{subformula}s. \end{defn} \begin{explain} Note the subtle difference in how we have defined immediate !!{subformula}s and proper !!{subformula}s. In the first case, we have directly defined the immediate !!{subformula}s of a formula~$!A$ for each possible form of~$!A$. It is an explicit definition by cases, and the cases mirror the inductive definition of the set of !!{formula}s. In the second case, we have also mirrored the way the set of all !!{formula}s is defined, but in each case we have also included the proper !!{subformula}s of the smaller !!{formula}s $!B$, $!C$ in addition to these !!{formula}s themselves. This makes the definition \emph{recursive}. In general, a definition of a function on an inductively defined set (in our case, !!{formula}s) is recursive if the cases in the definition of the function make use of the function itself. To be well defined, we must make sure, however, that we only ever use the values of the function for arguments that come ``before'' the one we are defining---in our case, when defining ``proper !!{subformula}'' for $(!B \ast !C)$ we only use the proper !!{subformula}s of the ``earlier'' !!{formula}s $!B$ and $!C$. \end{explain} \begin{prop} \ollabel{prop:subfrm-trans} Suppose $!B$ is a subformula of $!A$ and $!C$ is a subformula of $!B$. Then $!C$ is a subformula of $!A$. In other words, the subformula relation is transitive. \end{prop} \begin{prob} Prove \olref[fol][syn][sbf]{prop:subfrm-trans}. \end{prob} \begin{prop} \ollabel{prop:count-subfrms} Suppose $!A$ is a formula with $n$ connectives and quantifiers. Then $!A$ has at most $2n+1$ subformulas. \end{prop} \begin{prob} Prove \olref[fol][syn][sbf]{prop:count-subfrms}. \end{prob} \end{document}

Referencing norms: SUBFORMULA

en · official · sha256:b0a210d3016ed1c8da325e3f5e3f478cf148469b593c8235fed47406be8f9653

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: substitution \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{sub} \olsection{Substitution} \begin{defn}[Substitution in a term] We define $\Subst{s}{t}{x}$, the result of \emph{substituting} $t$ for every occurrence of~$x$ in $s$, recursively: \begin{enumerate} \item \indcase{s}{c}{$\Subst{\indfrm}{t}{x}$ is just $s$.} \item \indcase{s}{y}{$\Subst{\indfrm}{t}{x}$ is also just~$s$, provided $y$ is a variable and $y \not\ident x$.} \item \indcase{s}{x}{$\Subst{\indfrm}{t}{x}$ is~$t$.} \item\indcase{s}{\Atom{f}{t_1, \dots, t_n}}{$\Subst{\indfrmp}{t}{x}$ is $\Atom{f}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}$.} \end{enumerate} \end{defn} \begin{defn} A term~$t$ is \emph{!!{free for}} $x$ in $!A$ if none of the free occurrences of~$x$ in $!A$ occur in the scope of a quantifier that binds a variable in~$t$. \end{defn} \begin{ex} ~ \begin{enumerate} \item $\Obj v_8$ is free for $\Obj v_1$ in $\lexists[\Obj v_3]\Atom{\Obj A^2_4}{\Obj v_3,\Obj v_1}$ \item $\Obj f^2_1(\Obj v_1, \Obj v_2)$ is \emph{not} free for $\Obj v_0$ in $\lforall[\Obj v_2]\Atom{\Obj A^2_4}{\Obj v_0,\Obj v_2}$ \end{enumerate} \end{ex} \begin{defn}[Substitution in !!a{formula}] If $!A$ is !!a{formula}, $x$~is !!a{variable}, and $t$~is a term !!{free for}~$x$ in~$!A$, then $\Subst{!A}{t}{x}$ is the result of substituting $t$ for all free occurrences of~$x$ in~$!A$. \begin{enumerate} \tagitem{prvFalse}{\indcase{!A}{\lfalse}{$\Subst{\indfrm}{t}{x}$ is $\lfalse$.}}{} \tagitem{prvTrue}{\indcase{!A}{\ltrue}{$\Subst{\indfrm}{t}{x}$ is $\ltrue$.}}{} \item \indcase{!A}{\Atom{P}{t_1,\dots, t_n}}{$\Subst{\indfrm}{t}{x}$ is $\Atom{P}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}$.} \item \indcase{!A}{\eq[t_1][t_2]}{$\Subst{\indfrmp}{t}{x}$ is $\Subst{t_1}{t}{x} = \Subst{t_2}{t}{x}$.} \tagitem{prvNot}{\indcase{!A}{\lnot !B}{$\Subst{\indfrmp}{t}{x}$ is $\lnot \Subst{!B}{t}{x}$.}}{} \tagitem{prvAnd}{\indcase{!A}{(!B \land !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \land \Subst{!C}{t}{x})$.}}{} \tagitem{prvOr}{\indcase{!A}{(!B \lor !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \lor \Subst{!C}{t}{x})$.}}{} \tagitem{prvIf}{\indcase{!A}{(!B \lif !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \lif \Subst{!C}{t}{x})$.}}{} \tagitem{prvIff}{\indcase{!A}{(!B \liff !C)}{$\Subst{\indfrmp}{t}{x}$ is $(\Subst{!B}{t}{x} \liff \Subst{!C}{t}{x})$.}}{} \tagitem{prvAll}{ \indcase{!A}{\lforall[y][!B]}{$\Subst{\indfrmp}{t}{x}$ is $\lforall[y][\Subst{!B}{t}{x}]$, provided $y$ is a variable other than $x$; otherwise $\Subst{\indfrmp}{t}{x}$ is just $\indfrm$.}}{} \tagitem{prvEx}{ \indcase{!A}{\lexists[y][!B]}{$\Subst{\indfrmp}{t}{x}$ is $\lexists[y][\Subst{!B}{t}{x}]$, provided $y$ is a variable other than $x$; otherwise $\Subst{\indfrmp}{t}{x}$ is just $\indfrm$.}}{} \end{enumerate} \end{defn} \begin{explain} Note that substitution may be vacuous: If $x$ does not occur in $!A$ at all, then $\Subst{!A}{t}{x}$ is just~$!A$. The restriction that $t$ must be !!{free for}~$x$ in~$!A$ is necessary to exclude cases like the following. If $!A \ident \lexists[y][x < y]$ and $t \ident y$, then $\Subst{!A}{t}{x}$ would be $\lexists[y][y < y]$. In this case the free variable $y$ is ``captured'' by the quantifier $\lexists[y]$ upon substitution, and that is undesirable. For instance, we would like it to be the case that whenever $\lforall[x][!B]$ holds, so does $\Subst{!B}{t}{x}$. But consider $\lforall[x][\lexists[y][x < y]]$ (here $!B$ is $\lexists[y][x < y]$). It is a sentence that is true about, e.g., the natural numbers: for every number~$x$ there is a number~$y$ greater than it. If we allowed $y$ as a possible substitution for~$x$, we would end up with $\Subst{!B}{y}{x} \ident \lexists[y][y < y]$, which is false. We prevent this by requiring that none of the free variables in~$t$ would end up being bound by a quantifier in~$!A$. \end{explain} We often use the following convention to avoid cumbersome notation: If $!A$ is !!a{formula} which may contain the !!{variable}~$x$ free, we also write~$!A(x)$ to indicate this. When it is clear which $!A$ and~$x$ we have in mind, and $t$ is a term (assumed to be free for $x$ in $!A(x)$), then we write $!A(t)$ as short for $\Subst{!A}{t}{x}$. So for instance, we might say, ``we call $!A(t)$ an instance of~$\lforall[x][!A(x)]$.'' By this we mean that if $!A$~is any !!{formula}, $x$~!!a{variable}, and $t$~a term that's free for~$x$ in~$!A$, then $\Subst{!A}{t}{x}$ is an instance of~$\lforall[x][!A]$. \end{document}

Referencing norms: COND_FREE_FOR, SUBSTITUTION, VARIABLE_CAPTURE

en · official · sha256:c3c8bf1580ea4ce5d914e05b95ffef2ab338e3838c769ab6e311e60a704d3f11

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: terms-formulas \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{frm} \olsection{Terms and \printtoken{P}{formula}} Once a first-order language~$\Lang L$ is given, we can define expressions built up from the basic vocabulary of~$\Lang L$. These include in particular \emph{terms} and \emph{!!{formula}s}. \begin{defn}[Terms] \ollabel{defn:terms} The set of \emph{terms}~$\Trm[L]$ of~$\Lang L$ is defined inductively by: \begin{enumerate} \item Every !!{variable} is a term. \item Every !!{constant} of~$\Lang L$ is a term. \item If $f$ is an $n$-place !!{function} and $t_1$, \dots, $t_n$ are terms, then $\Atom{f}{t_1, \ldots, t_n}$ is a term. \tagitem{limitClause}{ Nothing else is a term.}{} \end{enumerate} A term containing no !!{variable}s is a \emph{closed term}. \end{defn} \begin{explain} The !!{constant}s appear in our specification of the language and the terms as a separate category of symbols, but they could instead have been included as zero-place !!{function}s. We could then do without the second clause in the definition of terms. We just have to understand $\Atom{f}{t_1, \ldots, t_n}$ as just $f$ by itself if $n = 0$. \end{explain} \begin{defn}[Formulas] \ollabel{defn:formulas} The set of \emph{!!{formula}s}~$\Frm[L]$ of the language~$\Lang L$ is defined inductively as follows: \begin{enumerate} \tagitem{prvFalse}{$\lfalse$ is an atomic !!{formula}.}{} \tagitem{prvTrue}{$\ltrue$ is an atomic !!{formula}.}{} \item If $R$ is an $n$-place !!{predicate} of~$\Lang L$ and $t_1$, \dots, $t_n$ are terms of~$\Lang L$, then $\Atom{R}{t_1,\ldots, t_n}$ is an atomic !!{formula}. \item If $t_1$ and $t_2$ are terms of~$\Lang L$, then $\Atom{\eq}{t_1, t_2}$ is an atomic !!{formula}. \tagitem{prvNot}{If $!A$ is !!a{formula}, then $\lnot !A$ is !!a{formula}.}{} \tagitem{prvAnd}{If $!A$ and $!B$ are !!{formula}s, then $(!A \land !B)$ is !!a{formula}.}{} \tagitem{prvOr}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lor !B)$ is !!a{formula}.}{} \tagitem{prvIf}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lif !B)$ is !!a{formula}.}{} \tagitem{prvIff}{If $!A$ and $!B$ are !!{formula}s, then $(!A \liff !B)$ is !!a{formula}.}{} \tagitem{prvAll}{If $!A$ is !!a{formula} and $x$ is !!a{variable}, then $\lforall[x][!A]$ is !!a{formula}.}{} \tagitem{prvEx}{If $!A$ is !!a{formula} and $x$ is !!a{variable}, then $\lexists[x][!A]$ is !!a{formula}.}{} \tagitem{limitClause}{Nothing else is !!a{formula}.}{} \end{enumerate} \end{defn} \begin{explain} The definitions of the set of terms and that of !!{formula}s are \emph{inductive definitions}. Essentially, we construct the set of !!{formula}s in infinitely many stages. In the initial stage, we pronounce all atomic formulas to be formulas; this corresponds to the first few cases of the definition, i.e., the cases for \iftag{prvTrue}{$\ltrue$, }{}% \iftag{prvFalse}{$\lfalse$, }{}% $\Atom{R}{t_1,\dots,t_n}$ and $\Atom{\eq}{t_1,t_2}$. ``Atomic !!{formula}'' thus means any !!{formula} of this form. The other cases of the definition give rules for constructing new !!{formula}s out of !!{formula}s already constructed. At the second stage, we can use them to construct !!{formula}s out of atomic !!{formula}s. At the third stage, we construct new formulas from the atomic formulas and those obtained in the second stage, and so on. A !!{formula} is anything that is eventually constructed at such a stage, and nothing else. \end{explain} By convention, we write $\eq$ between its arguments and leave out the parentheses: $\eq[t_1][t_2]$ is an abbreviation for $\Atom{\eq}{t_1,t_2}$. Moreover, $\lnot \Atom{\eq}{t_1,t_2}$ is abbreviated as $\eq/[t_1][t_2]$. When writing a formula $(!B \ast !C)$ constructed from $!B$, $!C$ using a two-place connective~$\ast$, we will often leave out the outermost pair of parentheses and write simply~$!B \ast !C$. \begin{intro} Some logic texts require that the !!{variable}~$x$ must occur in~$!A$ in order for \iftag{prvEx}{$\lexists[x][!A]$ }{}% \iftag{notprvEx,notprvAll}{}{and }% \iftag{prvAll}{$\lforall[x][!A]$ }{}% to count as \iftag{notprvEx,notprvAll}{!!a{formula}}{!!{formula}s}. Nothing bad happens if you don't require this, and it makes things easier. \end{intro} \begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll} \begin{defn} Formulas constructed using the defined operators are to be understood as follows: \begin{tagenumerate}{defTrue,defFalse,defNot,defOr,defAnd,defIf,defIff,defEx,defAll} \tagitem{defTrue}{$\ltrue$ abbreviates \iftag{prvFalse}{$\lnot\lfalse$}{$(!A \lor \lnot !A)$ for some fixed atomic !!{formula}~$!A$}.}{} \tagitem{defFalse}{$\lfalse$ abbreviates \iftag{prvTrue}{$\lnot\ltrue$}{$(!A \land \lnot !A)$ for some fixed atomic !!{formula}~$!A$}.}{} \tagitem{defNot}{$\lnot !A$ abbreviates $!A \lif \lfalse$.}{} \tagitem{defOr}{$!A \lor !B$ abbreviates \iftag{prvAnd}{$\lnot(\lnot !A \land \lnot !B)$}{$\lnot !A \lif !B$}.}{} \tagitem{defAnd}{$!A \land !B$ abbreviates \iftag{prvOr}{$\lnot(\lnot !A \lor \lnot !B)$}{$\lnot (!A \lif \lnot !B)$}.}{} \tagitem{defIf}{$!A \lif !B$ abbreviates \iftag{prvOr}{$\lnot !A \lor !B)$}{$\lnot (!A \land \lnot !B)$}.}{} \tagitem{defIff}{$!A \liff !B$ abbreviates $(!A \lif !B) \land (!B \lif !A)$.}{} \tagitem{defAll}{$\lforall[x][!A]$ abbreviates $\lnot\lexists[x][\lnot !A]$.}{} \tagitem{defEx}{$\lexists[x][!A]$ abbreviates $\lnot\lforall[x][\lnot !A]$.}{} \end{tagenumerate} \end{defn} \end{tagblock} If we work in a language for a specific application, we will often write two-place !!{predicate}s and !!{function}s between the respective terms, e.g., $t_1 < t_2$ and $(t_1 + t_2)$ in the language of arithmetic and $t_1 \in t_2$ in the language of set theory. The successor function in the language of arithmetic is even written conventionally \emph{after} its argument:~$t'$. Officially, however, these are just conventional abbreviations for $\Atom{\Obj A^2_0}{t_1, t_2}$, $\Obj f^2_0(t_1, t_2)$, $\Atom{\Obj A^2_0}{t_1, t_2}$ and $f^1_0(t)$, respectively. \begin{defn}[Syntactic identity] The symbol $\ident$ expresses syntactic identity between strings of symbols, i.e., $!A \ident !B$ iff $!A$ and $!B$ are strings of symbols of the same length and which contain the same symbol in each place. \end{defn} The $\ident$ symbol may be flanked by strings obtained by concatenation, e.g., $!A \ident (!B \lor !C)$ means: the string of symbols~$!A$ is the same string as the one obtained by concatenating an opening parenthesis, the string $!B$, the $\lor$ symbol, the string~$!C$, and a closing parenthesis, in this order. If this is the case, then we know that the first symbol of~$!A$ is an opening parenthesis, $!A$ contains $!B$ as a substring (starting at the second symbol), that substring is followed by~$\lor$, etc. As terms and !!{formula}s are built up from basic elements via inductive definitions, we can use the following induction principles to prove things about them. \begin{lem}[\emph{Principle of induction on terms}] \ollabel{lem:trmind} Let $\Lang L$ be a first-order language. If some property~$P$ is such that % \begin{enumerate} \item it holds for every !!{variable}~$v$, % \item it holds for every !!{constant}~$a$ of~$\Lang L$, and % \item it holds for $f(t_1,\dotsc,t_n)$ whenever it holds for $t_1$,~\dots, $t_n$ and $f$~is an $n$-place !!{function} of~$\Lang L$ \end{enumerate} (assuming $t_1$,~\dots, $t_n$ are terms of~$\Lang{L}$), then $P$ holds for every term in~$\Trm[L]$. \end{lem} \begin{prob} Prove \olref[fol][syn][frm]{lem:trmind}. \end{prob} \begin{lem}[\emph{Principle of induction on !!{formula}s}] \ollabel{thm:frmind} Let $\Lang L$ be a first-order language. If some property~$P$ holds for all the atomic !!{formula}s and is such that % \begin{enumerate} \tagitem{prvNot}{it holds for $\lnot !A$ whenever it holds for~$!A$;}{} \tagitem{prvAnd}{it holds for $(!A \land !B)$ whenever it holds for $!A$ and~$!B$;}{} \tagitem{prvOr}{it holds for $(!A \lor !B)$ whenever it holds for $!A$ and~$!B$;}{} \tagitem{prvIf}{it holds for $(!A \lif !B)$ whenever it holds for $!A$ and~$!B$;}{} \tagitem{prvIff}{it holds for $(!A \liff !B)$ whenever it holds for $!A$ and~$!B$;}{} \tagitem{prvEx}{it holds for $\lexists[x][!A]$ whenever it holds for~$!A$;}{} \tagitem{prvAll}{it holds for $\lforall[x][!A]$ whenever it holds for~$!A$;}{} \end{enumerate} (assuming $!A$ and $!B$ are !!{formula}s of~$\Lang{L}$), then $P$ holds for all formulas in~$\Frm[L]$. \end{lem} \end{document}

Referencing norms: CLOSED_TERM, EXISTENTIAL_QUANTIFIER, FOL_ATOM, FOL_FORMULA, QuantifierOfLanguage, TERM, UNIVERSAL_QUANTIFIER, binds_variable, quantifier_of

en · official · sha256:92a31b5968b24d2705616d2beea7e5582953395c152c30493fae51b5f39ec631

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: unique-readability \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{unq} \olsection{Unique Readability} \begin{explain} The way we defined !!{formula}s guarantees that every !!{formula} has a \emph{unique reading}, i.e., there is essentially only one way of constructing it according to our formation rules for !!{formula}s and only one way of ``interpreting'' it. If this were not so, we would have ambiguous !!{formula}s, i.e., !!{formula}s that have more than one reading or intepretation---and that is clearly something we want to avoid. But more importantly, without this property, most of the definitions and proofs we are going to give will not go through. Perhaps the best way to make this clear is to see what would happen if we had given bad rules for forming !!{formula}s that would not guarantee unique readability. For instance, we could have forgotten the parentheses in the formation rules for connectives, e.g., we might have allowed this: \begin{quote} If $!A$ and $!B$ are !!{formula}s, then so is $!A \lif !B$. \end{quote} Starting from an atomic formula $!D$, this would allow us to form $!D \lif !D$. From this, together with $!D$, we would get $!D \lif !D \lif !D$. But there are two ways to do this: \begin{enumerate} \item We take $!D$ to be $!A$ and $!D \lif !D$ to be $!B$. \item We take $!A$ to be $!D \lif !D$ and $!B$ is~$!D$. \end{enumerate} Correspondingly, there are two ways to ``read'' the !!{formula}~$!D \lif !D \lif !D$. It is of the form $!B \lif !C$ where $!B$ is $!D$ and $!C$ is $!D \lif !D$, but \emph{it is also} of the form $!B \lif !C$ with $!B$ being $!D \lif !D$ and $!C$ being~$!D$. If this happens, our definitions will not always work. For instance, when we define the !!{main operator} of a formula, we say: in a formula of the form $!B \lif !C$, the !!{main operator} is the indicated occurrence of~$\lif$. But if we can match the formula $!D \lif !D \lif !D$ with $!B \lif !C$ in the two different ways mentioned above, then in one case we get the first occurrence of $\lif$ as the !!{main operator}, and in the second case the second occurrence. But we intend the !!{main operator} to be a \emph{function} of the !!{formula}, i.e., every !!{formula} must have exactly one !!{main operator} occurrence. \end{explain} \begin{lem} The number of left and right parentheses in !!a{formula}~$!A$ are equal. \end{lem} \begin{proof} We prove this by induction on the way $!A$ is constructed. This requires two things: (a) We have to prove first that all atomic formulas have the property in question (the induction basis). (b) Then we have to prove that when we construct new formulas out of given formulas, the new formulas have the property provided the old ones do. Let $l(!A)$ be the number of left parentheses, and $r(!A)$ the number of right parentheses in~$!A$, and $l(t)$ and $r(t)$ similarly the number of left and right parentheses in a term~$t$. \begin{prob} Prove that for any term~$t$, $l(t) = r(t)$. \end{prob} \begin{enumerate} \tagitem{prvFalse}{\indcase{!A}{\lfalse}{$\indfrm$ has $0$ left and $0$ right parentheses.}}{} \tagitem{prvTrue}{\indcase{!A}{\ltrue}{$\indfrm$ has $0$ left and $0$ right parentheses.}}{} \item \indcase{!A}{\Atom{R}{t_1,\dots,t_n}}{$l(\indfrm) = 1 + l(t_1) + \dots + l(t_n) = 1 + r(t_1) + \dots + r(t_n) = r(\indfrm)$. Here we make use of the fact, left as an exercise, that $l(t) = r(t)$ for any term~$t$.} \item \indcase{!A}{\eq[t_1][t_2]}{$l(\indfrm) = l(t_1) + l(t_2) = r(t_1) + r(t_2) = r(\indfrm)$.} \tagitem{prvNot}{\indcase{!A}{\lnot !B}{By induction hypothesis, $l(!B) = r(!B)$. Thus $l(\indfrm) = l(!B) = r(!B) = r(\indfrm)$.}}{} \item \indcase{!A}{(!B \ast !C)}{By induction hypothesis, $l(!B) = r(!B)$ and $l(!C) = r(!C)$. Thus $l(\indfrm) = 1 + l(!B) + l(!C) = 1 + r(!B) + r(!C) = r(\indfrm)$.} \tagitem{prvAll}{\indcase{!A}{\lforall[x][!B]}{By induction hypothesis, $l(!B) = r(!B)$. Thus, $l(\indfrm) = l(!B) = r(!B) = r(\indfrm)$.}}{} % Print case for \lexists if prvEx and not prvAll \tagitem{prvAll,notprvEx}{}{\indcase{!A}{\lexists[x][!B]}{By induction hypothesis, $l(!B) = r(!B)$. Thus, $l(\indfrm) = l(!B) = r(!B) = r(\indfrm)$.}} % Just say similarly if prvEx and prvAll \tagitem{notprvAll,notprvEx}{}{\indcase{!A}{\lexists[x][!B]}{Similarly.}} \end{enumerate} \end{proof} \begin{defn}[Proper prefix] A string of symbols $!B$ is a \emph{proper prefix} of a string of symbols~$!A$ if concatenating $!B$ and a non-empty string of symbols yields~$!A$. \end{defn} \begin{lem}\ollabel{lem:no-prefix} If $!A$ is !!a{formula}, and $!B$ is a proper prefix of $!A$, then $!B$ is not !!a{formula}. \end{lem} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[fol][syn][unq]{lem:no-prefix}. \end{prob} \begin{prop} \ollabel{prop:unique-atomic} If $!A$ is an atomic !!{formula}, then it satisfies one, and only one of the following conditions. \begin{enumerate} \tagitem{prvFalse}{$!A \ident \lfalse$.}{} \tagitem{prvTrue}{$!A \ident \ltrue$.}{} \item $!A \ident \Atom{R}{t_1,\dots,t_n}$ where $R$ is an $n$-place !!{predicate}, $t_1$, \dots, $t_n$ are terms, and each of $R$, $t_1$, \dots, $t_n$ is uniquely determined. \item $!A \ident \eq[t_1][t_2]$ where $t_1$ and $t_2$ are uniquely determined terms. \end{enumerate} \end{prop} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[fol][syn][unq]{prop:unique-atomic} (Hint: Formulate and prove a version of \olref[fol][syn][unq]{lem:no-prefix} for terms.) \end{prob} \begin{prop}[Unique Readability] Every !!{formula} satisfies one, and only one of the following conditions. \begin{enumerate} \item $!A$ is atomic. \tagitem{prvNot}{$!A$ is of the form $\lnot !B$.}{} \tagitem{prvAnd}{$!A$ is of the form $(!B \land !C)$.}{} \tagitem{prvOr}{$!A$ is of the form $(!B \lor !C)$.}{} \tagitem{prvIf}{$!A$ is of the form $(!B \lif !C)$.}{} \tagitem{prvIff}{$!A$ is of the form $(!B \liff !C)$.}{} \tagitem{prvAll}{$!A$ is of the form $\lforall[x][!B]$.}{} \tagitem{prvEx}{$!A$ is of the form $\lexists[x][!B]$.}{} \end{enumerate} Moreover, in each case $!B$, or $!B$ and $!C$, are uniquely determined. This means that, e.g., there are no different pairs $!B$, $!C$ and $!B'$, $!C'$ so that $!A$ is both of the form \iftag{prvIf}{$(!B \lif !C)$ and $(!B' \lif !C')$.}{ \iftag{prvOr}{$(!B \lor !C)$ and $(!B' \lor !C')$.}{ \iftag{prvAnd}{$(!B \land !C)$ and $(!B' \land !C')$.}{}}} \end{prop} \begin{proof} The formation rules require that if !!a{formula} is not atomic, it must start with an opening parenthesis~(, \iftag{prvNot}{$\lnot$,}{} or a quantifier. On the other hand, every !!{formula} that starts with one of the following symbols must be atomic: !!a{predicate}, !!a{function}, !!a{constant}\iftag{prvFalse}{, $\lfalse$}{}\iftag{prvTrue}{, $\ltrue$}{}. So we really only have to show that if $!A$ is of the form $(!B \ast !C)$ and also of the form $(!B' \mathbin{\ast'} !C')$, then $!B \ident !B'$, $!C \ident !C'$, and $\ast = {\ast'}$. So suppose both $!A \ident (!B \ast !C)$ and $!A \ident (!B' \mathbin{\ast'} !C')$. Then either $!B \ident !B'$ or not. If it is, clearly $\ast = {\ast'}$ and $!C \ident !C'$, since they then are substrings of $!A$ that begin in the same place and are of the same length. The other case is $!B \not\ident !B'$. Since $!B$ and $!B'$ are both substrings of $!A$ that begin at the same place, one must be a proper prefix of the other. But this is impossible by \olref{lem:no-prefix}. \end{proof} \end{document}

Referencing norms: UNIQUE_READABILITY

en · official · sha256:13b3edc44f9a5b3b58a0ec5e9bef295be50012956acdc1911deb503d9db6ce9c

% Part: normal-modal-logic % Chapter: syntax-and-semantics % Section: schemas \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{syn}{sch} \olsection{Schemas and Validity} \begin{defn} A \emph{schema} is a set of !!{formula}s comprising all and only the substitution instances of some modal !!{formula}~$!C$, i.e., \[ \Setabs{!B}{\lexists[!D_1], \dots, \lexists[!D_n] \left(!B = \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \right) }. \] The !!{formula}~$!C$ is called the \emph{characteristic} !!{formula} of the schema, and it is unique up to a renaming of the !!{propositional variable}s. !!^a{formula}~$!A$ is an \emph{instance} of a schema if it is a member of the set. \end{defn} It is convenient to denote a schema by the meta-linguistic expression obtained by substituting `$!A$', `$!B$',~\dots, for the atomic components of~$!C$. So, for instance, the following denote schemas: `$!A$', `$!A \lif \Box!A$', `$!A \lif (!B \lif !A)$'. They correspond to the characteristic !!{formula}s $p$, $p \lif \Box p$, $p \lif (q \lif p)$. The schema `$!A$' denotes the set of \emph{all} !!{formula}s. \begin{defn} A schema is \emph{true} in a model if and only if all of its instances are; and a schema is \emph{valid} if and only if it is true in every model. \end{defn} \begin{prop}\ollabel{prop:Kvalid} The following schema \Ax{K} is valid \begin{equation*} \Box(!A \lif !B) \lif (\Box !A \lif \Box !B). \tag{\Ax{K}} \end{equation*} \end{prop} \begin{proof} We need to show that all instances of the schema are true at every world in every model. So let $\mModel{M} = \tuple{W,R,V}$ and $w \in W$ be arbitrary. To show that a conditional is true at a world we assume the antecedent is true to show that the consequent is true as well. In this case, let $\mSat{M}{\Box(!A \lif !B)}[w]$ and $\mSat{M}{\Box !A}[w]$. We need to show $\mSat{M}{\Box !B}[w]$. So let $w'$ be arbitrary such that $Rww'$. Then by the first assumption $\mSat{M}{!A \lif !B}[w']$ and by the second assumption $\mSat{M}{!A}[w']$. It follows that $\mSat{M}{!B}[w']$. Since $w'$ was arbitrary, $\mSat{M}{\Box !B}[w]$. \end{proof} \begin{prop}\ollabel{prop:Dual-valid} The following schema \Dual{} is valid \begin{equation*} \Diamond !A \liff \lnot\Box\lnot !A. \tag{\Dual} \end{equation*} \end{prop} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[nml][syn][sch]{prop:Dual-valid}. \end{prob} \begin{prop}\ollabel{prop:soundMP} If $!A$ and $!A \lif !B$ are true at a world in a model then so is $!B$. Hence, the valid !!{formula}s are closed under modus ponens. \end{prop} \begin{prop}\ollabel{prop:valid-instances} !!^a{formula}~$!A$ is valid iff all its substitution instances are. In other words, a schema is valid iff its characteristic !!{formula} is. \end{prop} \begin{proof} The ``if'' direction is obvious, since $!A$ is a substitution instance of itself. To prove the ``only if'' direction, we show the following: Suppose $\mModel{M} = \tuple{W, R, V}$ is a modal model, and $!B \ident \SSubst{!A}{\subst{!D_1}{p_1},\dots,\subst{!D_n}{p_n}}$ is a substitution instance of~$!A$. Define $\mModel{M'} = \tuple{W, R, V'}$ by $V'(p_i) = \Setabs{w}{\mSat{M}{!D_i}[w]}$. Then $\mSat{M}{!B}[w]$ iff $\mSat{M'}{!A}[w]$, for any~$w \in W$. (We leave the proof as an exercise.) Now suppose that $!A$ was valid, but some substitution instance $!B$ of~$!A$ was not valid. Then for some $\mModel{M} = \tuple{W, R, V}$ and some $w \in W$, $\mSat/{M}{!B}[w]$. But then $\mSat/{M'}{!A}[w]$ by the claim, and $!A$ is not valid, a contradiction. \end{proof} \begin{prob} Prove the claim in the ``only if'' part of the proof of \olref[nml][syn][sch]{prop:valid-instances}. (Hint: use induction on~$!A$.) \end{prob} Note, however, that it is not true that a schema is true in a model iff its characteristic formula is. Of course, the ``only if'' direction holds: if every instance of $!A$ is true in~$\mModel{M}$, $!A$~itself is true in~$\mModel{M}$. But it may happen that $!A$ is true in~$\mModel{M}$ but some instance of~$!A$ is false at some world in~$\mModel{M}$. For a very simple counterexample consider~$p$ in a model with only one world~$w$ and $V(p) = \{w\}$, so that $p$ is true at~$w$. But $\lfalse$ is an instance of~$p$, and not true at~$w$. \begin{prob} Show that none of the following !!{formula}s are valid: \begin{enumerate} \item[\Ax{D}:] \quad $\Box p \lif \Diamond p$; \item[\Ax{T}:] \quad $\Box p \lif p$; \item[\Ax{B}:] \quad $p \lif \Box\Diamond p$; \item[\Ax{4}:] \quad $\Box p \lif \Box \Box p$; \item[\Ax{5}:] \quad $\Diamond p \lif \Box \Diamond p$. \end{enumerate} \end{prob} \begin{table}[t] \centering \begin{tabular}{| l || l |} \hline {\emph{Valid Schemas}} & {\emph{Invalid Schemas}} \\ \hline\hline $\Box(!A \lif !B) \lif (\Diamond !A \lif \Diamond !B)$ & $\Box (!A \lor !B) \lif (\Box !A \lor \Box !B)$ \\ $\Diamond (!A \lif !B) \lif (\Box !A \lif \Diamond !B)$ & $(\Diamond !A \land \Diamond !B) \lif \Diamond (!A \land !B)$\\ $\Box (!A \land !B) \liff (\Box !A \land \Box !B)$ & $!A \lif \Box !A$ \\ $\Box !A \lif \Box (!B \lif !A)$ & $\Box \Diamond !A \lif !B$ \\ $\lnot \Diamond !A \lif \Box (!A \lif !B)$ & $\Box \Box !A \lif \Box !A$ \\ $\Diamond (!A \lor !B) \liff (\Diamond !A \lor \Diamond !B)$ & $\Box \Diamond !A \lif \Diamond \Box !A$. \\ \hline \end{tabular} \caption{Valid and (or?) invalid schemas.} \ollabel{tab:valid-invalidSchemas} \end{table} \begin{prob}%\ollabel{ex:in/validSchemas} Prove that the schemas in the first column of \olref[nml][syn][sch]{tab:valid-invalidSchemas} are valid and those in the second column are not valid. \end{prob} \begin{prob} Decide whether the following schemas are valid or invalid: \begin{enumerate} \item $(\Diamond !A \lif \Box !B) \lif (\Box !A \lif \Box !B)$; \item $\Diamond(!A \lif !B) \lor \Box(!B \lif !A)$. \end{enumerate} \end{prob} \begin{prob} For each of the following schemas find a model $\mModel{M}$ such that every instance of the !!{formula} is true in $\mModel{M}$: \begin{enumerate} \item $p \lif \Diamond\Diamond p$; \item $\Diamond p \lif \Box p$. \end{enumerate} \end{prob} \end{document}

Referencing norms: CHARACTERISTIC_FORMULA, EX_K_A, EX_K_B, EX_K_INNER, EX_K_ROOT, EX_K_SLOT_A1, EX_K_SLOT_A2, EX_K_SLOT_B, SCHEMATIC_VARIABLE, SCHEMA_EXHIBIT_K, SCHEMA_INSTANCE, SCHEMA_NOTION, ShapeInUse, shape_in_use, shape_reads_as

en · official · sha256:9cbcac585d773b2acf783b001958836c24f338fb4be525d55a22841e965270b7

% Part: propositional-logic % Chapter: syntax-and-semantics % Section: formulas \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{pl}{syn}{fml} \olsection{Propositional \usetoken{P}{formula}} !!^{formula}s of propositional logic are built up from \emph{!!{propositional variable}s}\iftag{prvFalse}{\iftag{prvTrue}{,}{ and} the propositional constant~$\lfalse$}{}\iftag{prvTrue}{\iftag{prvFalse}{ and}{} the propositional constant~$\ltrue$}{} using \emph{logical connectives}. \begin{enumerate} \item !!^a{denumerable} set~$\PVar$ of !!{propositional variable}s $\Obj p_0$, $\Obj p_1$, \dots \tagitem{prvFalse}{The propositional constant for !!{falsity}~$\lfalse$.}{} \tagitem{prvTrue}{The propositional constant for !!{truth}~$\ltrue$.}{} \item The logical connectives: \startycommalist \iftag{prvNot}{\ycomma $\lnot$ (negation)}{}% \iftag{prvAnd}{\ycomma $\land$ (conjunction)}{}% \iftag{prvOr}{\ycomma $\lor$ (disjunction)}{}% \iftag{prvIf}{\ycomma $\lif$ (!!{conditional})}{}% \iftag{prvIff}{\ycomma $\liff$ (!!{biconditional})}{}% \item Punctuation marks: (, ), and the comma. \end{enumerate} We denote this language of propositional logic by $\Lang L_0$. \iftag{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}{% In addition to the primitive connectives introduced above, we also use the following \emph{defined} symbols: \startycommalist \iftag{defNot}{\ycomma $\lnot$ (negation)}{}% \iftag{defAnd}{\ycomma $\land$ (conjunction)}{}% \iftag{defOr}{\ycomma $\lor$ (disjunction)}{}% \iftag{defIf}{\ycomma $\lif$ (!!{conditional})}{}% \iftag{defIff}{\ycomma $\liff$ (!!{biconditional})}{}% \iftag{defFalse}{\ycomma $\lfalse$ (!!{falsity})}{}% \iftag{defTrue}{\ycomma $\ltrue$ (!!{truth})}}{}. \begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll} \begin{explain} A defined symbol is not officially part of the language, but is introduced as an informal abbreviation: it allows us to abbreviate formulas which would, if we only used primitive symbols, get quite long. This is obviously an advantage. The bigger advantage, however, is that proofs become shorter. If a symbol is primitive, it has to be treated separately in proofs. The more primitive symbols, therefore, the longer our proofs. \end{explain} \end{tagblock} % Alternate symbols \begin{intro} You may be familiar with different terminology and symbols than the ones we use above. Logic texts (and teachers) commonly use either $\sim$, $\neg$, and~!\ for ``negation'', $\wedge$, $\cdot$, and $\&$ for ``conjunction''. Commonly used symbols for the ``conditional'' or ``implication'' are $\rightarrow$, $\Rightarrow$, and $\supset$. \iftag{prvIff,defIff}{Symbols for ``biconditional,'' ``bi-implication,'' or ``(material) equivalence'' are $\leftrightarrow$, $\Leftrightarrow$, and $\equiv$.}{} \iftag{prvFalse,defFalse}{The $\lfalse$ symbol is variously called ``falsity,'' ``falsum,'' ``absurdity,'' or ``bottom.''}{} \iftag{prvTrue,defTrue}{The $\ltrue$ symbol is variously called ``truth,'' ``verum,'' or ``top.''}{} \end{intro} \begin{defn}[Formula] \ollabel{defn:formulas} The set~$\Frm[L_0]$ of \emph{!!{formula}s} of propositional logic is defined inductively as follows: \begin{enumerate} \tagitem{prvFalse}{$\lfalse$ is an atomic !!{formula}.}{} \tagitem{prvTrue}{$\ltrue$ is an atomic !!{formula}.}{} \item Every !!{propositional variable}~$\Obj p_i$ is an atomic !!{formula}. \tagitem{prvNot}{If $!A$ is !!a{formula}, then $\lnot !A$ is !!a{formula}.}{} \tagitem{prvAnd}{If $!A$ and $!B$ are !!{formula}s, then $(!A \land !B)$ is !!a{formula}.}{} \tagitem{prvOr}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lor !B)$ is !!a{formula}.}{} \tagitem{prvIf}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lif !B)$ is !!a{formula}.}{} \tagitem{prvIff}{If $!A$ and $!B$ are !!{formula}s, then $(!A \liff !B)$ is !!a{formula}.}{} \tagitem{limitClause}{Nothing else is !!a{formula}.}{} \end{enumerate} \end{defn} \begin{explain} The definition of !!{formula}s is an \emph{inductive definition}. Essentially, we construct the set of !!{formula}s in infinitely many stages. In the initial stage, we pronounce all atomic formulas to be formulas; this corresponds to the first few cases of the definition, i.e., the cases for \iftag{prvTrue}{$\ltrue$, }{}% \iftag{prvFalse}{$\lfalse$, }{}% $\Obj p_i$. ``Atomic !!{formula}'' thus means any !!{formula} of this form. The other cases of the definition give rules for constructing new !!{formula}s out of !!{formula}s already constructed. At the second stage, we can use them to construct !!{formula}s out of atomic !!{formula}s. At the third stage, we construct new formulas from the atomic formulas and those obtained in the second stage, and so on. A !!{formula} is anything that is eventually constructed at such a stage, and nothing else. \end{explain} When writing a formula $(!B \ast !C)$ constructed from $!B$, $!C$ using a two-place connective~$\ast$, we will often leave out the outermost pair of parentheses and write simply~$!B \ast !C$. \begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll} \begin{defn} Formulas constructed using the defined operators are to be understood as follows: \begin{tagenumerate}{defTrue,defFalse,defNot,defOr,defAnd,defIf,defIff,defEx,defAll} \tagitem{defTrue}{$\ltrue$ abbreviates \iftag{prvFalse}{$\lnot\lfalse$}{$(!A \lor \lnot !A)$ for some fixed atomic !!{formula}~$!A$}.}{} \tagitem{defFalse}{$\lfalse$ abbreviates \iftag{prvTrue}{$\lnot\ltrue$}{$(!A \land \lnot !A)$ for some fixed atomic !!{formula}~$!A$}.}{} \tagitem{defNot}{$\lnot !A$ abbreviates $!A \lif \lfalse$.}{} \tagitem{defOr}{$!A \lor !B$ abbreviates \iftag{prvAnd}{$\lnot(\lnot !A \land \lnot !B)$}{$\lnot !A \lif !B$}.}{} \tagitem{defAnd}{$!A \land !B$ abbreviates \iftag{prvOr}{$\lnot(\lnot !A \lor \lnot !B)$}{$\lnot (!A \lif \lnot !B)$}.}{} \tagitem{defIf}{$!A \lif !B$ abbreviates \iftag{prvOr}{$\lnot !A \lor !B)$}{$\lnot (!A \land \lnot !B)$}.}{} \tagitem{defIff}{$!A \liff !B$ abbreviates $(!A \lif !B) \land (!B \lif !A)$.}{} \end{tagenumerate} \end{defn} \end{tagblock} \begin{defn}[Syntactic identity] The symbol $\ident$ expresses syntactic identity between strings of symbols, i.e., $!A \ident !B$ iff $!A$ and $!B$ are strings of symbols of the same length and which contain the same symbol in each place. \end{defn} The $\ident$ symbol may be flanked by strings obtained by concatenation, e.g., $!A \ident (!B \lor !C)$ means: the string of symbols~$!A$ is the same string as the one obtained by concatenating an opening parenthesis, the string $!B$, the $\lor$ symbol, the string~$!C$, and a closing parenthesis, in this order. If this is the case, then we know that the first symbol of $!A$ is an opening parenthesis, $!A$ contains $!B$ as a substring (starting at the second symbol), that substring is followed by $\lor$, etc. \end{document}

Referencing norms: BICONDITIONAL, CONDITIONAL, CONJUNCTION, ConnectiveOfLanguage, DISJUNCTION, FALSUM, NEGATION, PROP_ATOM, PROP_FORMULA, connective_arity, connective_of

en · official · sha256:1bf3dd192a9a34d89339d0d2d19d51f5488fb3881f9c6df3b760d3f9f2a19c74

% Part: propositional-logic % Chapter: propositional-logic % Section: preliminaries \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{pl}{syn}{pre} \olsection{Preliminaries} \begin{thm}[\emph{Principle of induction on !!{formula}s}] \ollabel{thm:induction} If some property~$P$ holds for all the atomic !!{formula}s and is such that \begin{enumerate} \tagitem{prvNot}{it holds for $\lnot !A$ whenever it holds for~$!A$;}{} \tagitem{prvAnd}{it holds for $(!A \land !B)$ whenever it holds for $!A$ and~$!B$;}{} \tagitem{prvOr}{it holds for $(!A \lor !B)$ whenever it holds for $!A$ and~$!B$;}{} \tagitem{prvIf}{it holds for $(!A \lif !B)$ whenever it holds for $!A$ and~$!B$;}{} \tagitem{prvIff}{it holds for $(!A \liff !B)$ whenever it holds for $!A$ and~$!B$;}{} \end{enumerate} then $P$ holds for all !!{formula}s. \end{thm} \begin{proof} Let $S$ be the collection of all !!{formula}s with property~$P$. Clearly $S \subseteq \Frm[L_0]$. $S$~satisfies all the conditions of \olref[fml]{defn:formulas}: it contains all atomic !!{formula}s and is closed under the !!{operator}s. $\Frm[L_0]$ is the smallest such class, so $\Frm[L_0] \subseteq S$. So $\Frm[L_0] = S$, and every formula has property~$P$. \end{proof} \begin{prop}\ollabel{prop:balanced} Any !!{formula} in~$\Frm[L_0]$ is \emph{balanced}, in that it has as many left parentheses as right ones. \end{prop} \begin{prob} Prove \olref[pl][syn][pre]{prop:balanced} \end{prob} \begin{prop} \ollabel{prop:noinit} No proper initial segment of !!a{formula} is !!a{formula}. \end{prop} \begin{prob} Prove \olref[pl][syn][pre]{prop:noinit} \end{prob} \begin{prop}[Unique Readability] Any !!{formula}~$!A$ in $ \Frm[L_0]$ has exactly one parsing as one of the following \begin{enumerate} \tagitem{prvFalse}{$\lfalse$.}{} \tagitem{prvTrue}{$\ltrue$.}{} \item $\Obj p_n$ for some $\Obj p_n \in \PVar$. \tagitem{prvNot}{$\lnot !B$ for some !!{formula}~$!B$.}{} \tagitem{prvAnd}{$(!B \land !C)$ for some !!{formula}s $!B$ and~$!C$.}{} \tagitem{prvOr}{$(!B \lor !C)$ for some !!{formula}s $!B$ and~$!C$.}{} \tagitem{prvIf}{$(!B \lif !C)$ for some !!{formula}s $!B$ and~$!C$.}{} \tagitem{prvIff}{$(!B \liff !C)$ for some !!{formula}s $!B$ and~$!C$.}{} \end{enumerate} Moreover, this parsing is \emph{unique}. \end{prop} \begin{proof} By induction on $!A$. For instance, suppose that $!A$ has two distinct readings as $(!B \lif !C)$ and $(!B' \lif !C')$. Then $!B$ and $!B'$ must be the same (or else one would be a proper initial segment of the other); so if the two readings of $!A$ are distinct it must be because $!C$ and $!C'$ are distinct readings of the same sequence of symbols, which is impossible by the inductive hypothesis. \end{proof} \begin{defn}[Uniform Substitution] If $!A$ and $!B$ are !!{formula}s, and $\Obj p_i$ is a !!{propositional variable}, then $\Subst{!A}{!B}{\Obj p_i}$ denotes the result of replacing each occurrence of $\Obj p_i$ by an occurrence of $!B$ in $!A$; similarly, the simultaneous substitution of $\Obj p_1$, \dots,~$\Obj p_n$ by !!{formula}s $!B_1$, \dots,~$!B_n$ is denoted by $\SSubst{!A}{\subst{!B_1}{\Obj p_1},\dots,\subst{!B_n}{\Obj p_n}}$. \end{defn} \begin{prob} For each of the five !!{formula}s below determine whether the !!{formula} can be expressed as a substitution \( \Subst{!A}{!B}{\Obj p_i} \) where \( !A \) is (i) \( \Obj p_0 \); (ii) \( ( \lnot \Obj p_0 \land \Obj p_1) \); and (iii) \( ( ( \lnot \Obj p_0 \lif \Obj p_1 ) \land \Obj p_2 ) \). In each case specify the relevant substitution. \begin{enumerate} \item \( \Obj p_1 \) \item \( ( \lnot \Obj p_0 \land \Obj p_0 ) \) \item \( ( ( \Obj p_0 \lor \Obj p_1 ) \land \Obj p_2 ) \) \item \( \lnot ( ( \Obj p_0 \lif \Obj p_1 ) \land \Obj p_2 ) \) \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 )) \) \end{enumerate} \end{prob} \begin{prob} Give a mathematically rigorous definition of $\Subst{!A}{!B}{p}$ by induction. \end{prob} \end{document}

Referencing norms: L_PROP, PROP_VARIABLE, belongs_to_language