The Open Logic Text

en · official · sha256:f7381ed0c309b5f79d9133bf06a9f766e10b0fd2cbeb773dee7fb6d172803ea0EN

% Part: first-order-logic % Chapter: completeness % Section: completeness-theorem \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{com}{cth}} {\olfileid{pl}{com}{cth}} \olsection{The Completeness Theorem} \begin{explain} Let's combine our results: we arrive at the completeness theorem. \end{explain} \begin{thm}[Completeness Theorem] \ollabel{thm:completeness} Let $\Gamma$ be a set of !!{sentence}s. If $\Gamma$ is consistent, it is satisfiable. \end{thm} \begin{proof} Suppose $\Gamma$ is consistent.\iftag{FOL}{ By \olref[hen]{lem:henkin}, there is a saturated consistent set $\Gamma' \supseteq \Gamma$.}{} By \olref[lin]{lem:lindenbaum}, there is a $\Gamma^* \supseteq \iftag{FOL}{\Gamma'}{\Gamma}$ which is consistent and !!{complete}. \iftag{FOL}{ Since $\Gamma' \subseteq \Gamma^*$, for each !!{formula}~$!A(x)$, $\Gamma^*$ contains !!a{sentence} of the form \iftag{prvEx} {$\lexists[x][!A(x)] \lif !A(c)$} {$\lnot\lforall[x][!A(x)] \lif \lnot !A(c)$} and so $\Gamma^*$ is saturated. If $\Gamma$ does not contain~$\eq$, then by}{By} \olref[mod]{lem:truth}, $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!A}$ iff $!A \in \Gamma^*$. From this it follows in particular that for all $!A \in \Gamma$, $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!A}$, so $\Gamma$ is satisfiable.\iftag{FOL}{ If $\Gamma$ does contain~$\eq$, then by \olref[ide]{lem:truth}, for all !!{sentence}s~$!A$, $\Sat{\equivclass{M}{\approx}}{!A}$ iff $!A \in \Gamma^*$. In particular, $\Sat{\equivclass{M}{\approx}}{!A}$ for all $!A \in \Gamma$, so $\Gamma$ is satisfiable.}{} \end{proof} \begin{cor}[Completeness Theorem, Second Version] \ollabel{cor:completeness} For all $\Gamma$ and !!{sentence}s~$!A$: if $\Gamma \Entails !A$ then $\Gamma \Proves !A$. \end{cor} \begin{proof} Note that the $\Gamma$'s in \olref{cor:completeness} and \olref{thm:completeness} are universally quantified. To make sure we do not confuse ourselves, let us restate \olref{thm:completeness} using a different variable: for any set of !!{sentence}s~$\Delta$, if $\Delta$ is consistent, it is satisfiable. By contraposition, if $\Delta$ is not satisfiable, then $\Delta$ is inconsistent. We will use this to prove the corollary. Suppose that $\Gamma \Entails !A$. Then $\Gamma \cup \{\lnot !A\}$ is unsatisfiable by \olref[syn][sem]{prop:entails-unsat}. Taking $\Gamma \cup \{\lnot !A\}$ as our $\Delta$, the previous version of \olref{thm:completeness} gives us that $\Gamma \cup \{\lnot !A\}$ is inconsistent. By \iftag{FOL}{% \tagrefs{prfAX/{fol:axd:prv:prop:prov-incons}, prfSC/{fol:seq:prv:prop:prov-incons}, prfND/{fol:ntd:prv:prop:prov-incons}, prfTab/{fol:tab:prv:prop:prov-incons}}}{% \tagrefs{prfAX/{pl:axd:prv:prop:prov-incons}, prfSC/{pl:seq:prv:prop:prov-incons}, prfND/{pl:ntd:prv:prop:prov-incons}, prfTab/{pl:tab:prv:prop:prov-incons}}}, $\Gamma \Proves !A$. \end{proof} \tagprob{FOL} \begin{prob} Use \olref[fol][com][cth]{cor:completeness} to prove \olref[fol][com][cth]{thm:completeness}, thus showing that the two formulations of the completeness theorem are equivalent. \end{prob} \tagendprob \tagprob{notFOL} \begin{prob} Use \olref[pl][com][cth]{cor:completeness} to prove \olref[pl][com][cth]{thm:completeness}, thus showing that the two formulations of the completeness theorem are equivalent. \end{prob} \tagendprob \tagprob{FOL} \begin{prob} In order for !!a{derivation} system to be complete, its rules must be strong enough to prove every unsatisfiable set inconsistent. Which of the rules of !!{derivation} were necessary to prove completeness? Are any of these rules not used anywhere in the proof? In order to answer these questions, make a list or diagram that shows which of the rules of !!{derivation} were used in which results that lead up to the proof of \olref[fol][com][cth]{thm:completeness}. Be sure to note any tacit uses of rules in these proofs. \end{prob} \tagendprob \tagprob{notFOL} \begin{prob} In order for !!a{derivation} system to be complete, its rules must be strong enough to prove every unsatisfiable set inconsistent. Which of the rules of !!{derivation} were necessary to prove completeness? Are any of these rules not used anywhere in the proof? In order to answer these questions, make a list or diagram that shows which of the rules of !!{derivation} were used in which results that lead up to the proof of \olref[pl][com][cth]{thm:completeness}. Be sure to note any tacit uses of rules in these proofs. \end{prob} \tagendprob \end{document}

Ссылаются нормы: AdequateNeedsBothHalves, COMPLETENESS, adequate_for, complete_for

en · official · sha256:a5290ef1e66ada9c4918abecca14a283949f19fb92d053f4917a472fef006767EN

% Part: first-order-logic % Chapter: natural-deduction % Section: proof-theoretic-notions \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{ntd}{ptn}} {\olfileid{pl}{ntd}{ptn}} \olsection{Proof-Theoretic Notions} \begin{editorial} This section collects the definitions the provability relation and consistency for natural deduction. \end{editorial} \begin{explain} Just as we've defined a number of important semantic notions (validity, entailment, satisfiability), we now define corresponding \emph{proof-theoretic notions}. These are not defined by appeal to satisfaction of !!{sentence}s in !!{structure}s, but by appeal to the !!{derivability} or !!{nonderivability} of certain !!{sentence}s from others. It was an important discovery that these notions coincide. That they do is the content of the \emph{soundness} and \emph{completeness theorems}. \end{explain} \begin{defn}[Theorems] A !!{sentence}~$!A$ is a \emph{theorem} if there is !!a{derivation} of~$!A$ in natural deduction in which all assumptions are !!{discharged}. We write $\Proves !A$ if $!A$ is a theorem and $\Proves/ !A$ if it is not. \end{defn} \begin{defn}[!!^{derivability}] !!^a{sentence} $!A$ is \emph{!!{derivable} from} a set of !!{sentence}s~$\Gamma$, $\Gamma \Proves !A$, if there is a !!{derivation} with conclusion~$!A$ and in which every assumption is either !!{discharged} or is in~$\Gamma$. If $!A$ is not !!{derivable} from $\Gamma$ we write $\Gamma \Proves/ !A$. \end{defn} \begin{defn}[Consistency] A set of !!{sentence}s~$\Gamma$ is \emph{inconsistent} iff $\Gamma \Proves \lfalse$. If $\Gamma$ is not inconsistent, i.e., if $\Gamma \Proves/ \lfalse$, we say it is \emph{consistent}. \end{defn} \begin{prop}[Reflexivity] \ollabel{prop:reflexivity} If $!A \in \Gamma$, then $\Gamma \Proves !A$. \end{prop} \begin{proof} The assumption $!A$ by itself is !!a{derivation} of~$!A$ where every !!{undischarged} assumption (i.e., $!A$) is in~$\Gamma$. \end{proof} \begin{prop}[Monotonicity] \ollabel{prop:monotonicity} If $\Gamma \subseteq \Delta$ and $\Gamma \Proves !A$, then $\Delta \Proves !A$. \end{prop} \begin{proof} Any !!{derivation} of $!A$ from $\Gamma$ is also !!a{derivation} of $!A$ from~$\Delta$. \end{proof} \begin{prop}[Transitivity] \ollabel{prop:transitivity} If $\Gamma \Proves !A$ and $\{!A\} \cup \Delta \Proves !B$, then $\Gamma \cup \Delta \Proves !B$. \end{prop} \begin{proof} If $\Gamma \Proves !A$, there is !!a{derivation}~$\delta_0$ of~$!A$ with all !!{undischarged} assumptions in~$\Gamma$. If $\{!A\} \cup \Delta \Proves !B$, then there is !!a{derivation}~$\delta_1$ of~$!B$ with all !!{undischarged} assumptions in~$\{!A\} \cup \Delta$. Now consider: \begin{prooftree} \AxiomC{$\Delta, \Discharge{!A}{1}$} \RightLabel{$\delta_1$} \DeduceC{$!B$} \DischargeRule{\Intro{\lif}}{1} \UnaryInfC{$!A \lif !B$} \AxiomC{$\Gamma$} \RightLabel{$\delta_0$} \DeduceC{$!A$} \RightLabel{\Elim{\lif}} \BinaryInfC{$!B$} \end{prooftree} The !!{undischarged} assumptions are now all among $\Gamma \cup \Delta$, so this shows $\Gamma \cup \Delta \Proves !B$. \end{proof} When $\Gamma = \{!A_1, !A_2, \ldots, !A_k\}$ is a finite set we may use the simplified notation $!A_1,!A_2,\ldots,!A_k \Proves !B$ for $\Gamma \Proves !B$, in particular $!A \Proves !B$ means that $\{!A\} \Proves !B$. Note that if $\Gamma \Proves !A$ and $!A \Proves !B$, then $\Gamma \Proves !B$. It follows also that if $!A_1, \dots, !A_n \Proves !B$ and $\Gamma \Proves !A_i$ for each~$i$, then $\Gamma \Proves !B$. \begin{prop} \ollabel{prop:incons} The following are equivalent. \begin{enumerate} \item \( \Gamma \) is inconsistent. \item \( \Gamma \Proves {!A} \) for every !!{sentence}~\( {!A} \). \item \( \Gamma \Proves {!A} \) and \( \Gamma \Proves \lnot {!A} \) for some !!{sentence}~\( {!A} \). \end{enumerate} \end{prop} \begin{proof} Exercise. \end{proof} \tagprob{FOL} \begin{prob} Prove \olref[fol][ntd][ptn]{prop:incons} \end{prob} \tagendprob \tagprob{notFOL} \begin{prob} Prove \olref[pl][ntd][ptn]{prop:incons} \end{prob} \tagendprob \begin{prop}[Compactness] \ollabel{prop:proves-compact} \begin{enumerate} \item If $\Gamma \Proves !A$ then there is a finite subset $\Gamma_0 \subseteq \Gamma$ such that $\Gamma_0 \Proves !A$. \item If every finite subset of~$\Gamma$ is consistent, then $\Gamma$ is consistent. \end{enumerate} \end{prop} \begin{proof} \begin{enumerate} \item If $\Gamma \Proves !A$, then there is !!a{derivation}~$\delta$ of~$!A$ from~$\Gamma$. Let $\Gamma_0$ be the set of !!{undischarged} assumptions of~$\delta$. Since any !!{derivation} is finite, $\Gamma_0$ can only contain finitely many !!{sentence}s. So, $\delta$ is !!a{derivation} of~$!A$ from a finite~$\Gamma_0 \subseteq \Gamma$. \item This is the contrapositive of (1) for the special case $!A \ident \lfalse$. \end{enumerate} \end{proof} \end{document}

Ссылаются нормы: CONSISTENCY, DERIVABILITY, NotionDefinedIn, notion_defined_in, proof_notion_of

en · official · sha256:8fa5cf2746510d6fdcf91e7c08e9881506ba9c03836f526225f498d74a3b5e0bEN

% Part: first-order-logic % Chapter: natural-deduction % Section: soundness \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \iftag{FOL} {\olfileid{fol}{ntd}{sou}} {\olfileid{pl}{ntd}{sou}} \olsection{Soundness} \begin{explain} !!^a{derivation} system, such as natural deduction, is \emph{sound} if it cannot !!{derive} things that do not actually follow. Soundness is thus a kind of guaranteed safety property for !!{derivation} systems. Depending on which proof theoretic property is in question, we would like to know for instance, that \begin{enumerate} \item every !!{derivable} !!{sentence} is \iftag{FOL}{valid}{a tautology}; \item if !!a{sentence} is !!{derivable} from some others, it is also a consequence of them; \item if a set of !!{sentence}s is inconsistent, it is unsatisfiable. \end{enumerate} These are important properties of !!a{derivation} system. If any of them do not hold, the !!{derivation} system is deficient---it would !!{derive} too much. Consequently, establishing the soundness of a !!{derivation} system is of the utmost importance. \end{explain} \begin{thm}[Soundness] \ollabel{thm:soundness} If $!A$ is !!{derivable} from the !!{undischarged} assumptions $\Gamma$, then $\Gamma \Entails !A$. \end{thm} \begin{proof} Let $\delta$ be !!a{derivation} of $!A$. We proceed by induction on the number of inferences in~$\delta$. For the induction basis we show the claim if the number of inferences is~$0$. In this case, $\delta$ consists only of a single !!{sentence}~$!A$, i.e., an assumption. That assumption is !!{undischarged}, since assumptions can only be !!{discharged} by inferences, and there are no inferences. So, any \iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$} that satisfies all of the !!{undischarged} assumptions of the proof also satisfies~$!A$. Now for the inductive step. Suppose that $\delta$ contains~$n$ inferences. The premise(s) of the lowermost inference are !!{derive}d using sub-!!{derivation}s, each of which contains fewer than~$n$ inferences. We assume the induction hypothesis: The premises of the lowermost inference follow from the !!{undischarged} assumptions of the sub-!!{derivation}s ending in those premises. We have to show that the conclusion~$!A$ follows from the !!{undischarged} assumptions of the entire proof. We distinguish cases according to the type of the lowermost inference. First, we consider the possible inferences with only one premise. \begin{enumerate} \item Suppose that the last inference is \Intro{\lnot}: The !!{derivation} has the form \begin{prooftree} \AxiomC{$\Gamma, \Discharge{!A}{n}$} \RightLabel{$\delta_1$} \DeduceC{$\lfalse$} \DischargeRule{\Intro{\lnot}}{n} \UnaryInfC{$\lnot !A$} \end{prooftree} By inductive hypothesis, $\lfalse$ follows from the !!{undischarged} assumptions $\Gamma \cup \{!A\}$ of~$\delta_1$. Consider \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !A}$. Suppose for reductio that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, but $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lnot !A}$, i.e., $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. This would mean that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma \cup \{!A\}}$. This is contrary to our inductive hypothesis. So, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !A}$. \item The last inference is \Elim{\land}: There are two variants: $!A$ or $!B$ may be inferred from the premise $!A \land !B$. Consider the first case. The !!{derivation}~$\delta$ looks like this: \begin{prooftree} \AxiomC{$\Gamma$} \RightLabel{$\delta_1$} \DeduceC{$!A \land !B$} \RightLabel{\Elim{\land}} \UnaryInfC{$!A$} \end{prooftree} By inductive hypothesis, $!A \land !B$ follows from the !!{undischarged} assumptions~$\Gamma$ of~$\delta_1$. Consider !!a{structure}~\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$}. We need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. Suppose $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$. By our inductive hypothesis ($\Gamma \Entails !A \land !B$), we know that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$. By definition, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$ iff $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ and $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$. (The case where $!B$ is inferred from $!A \land !B$ is handled similarly.) \item The last inference is \Intro{\lor}: There are two variants: $!A \lor !B$ may be inferred from the premise~$!A$ or the premise~$!B$. Consider the first case. The !!{derivation} has the form \begin{prooftree} \AxiomC{$\Gamma$} \RightLabel{$\delta_1$} \DeduceC{$!A$} \RightLabel{\Intro{\lor}} \UnaryInfC{$!A \lor !B$} \end{prooftree} By inductive hypothesis, $!A$ follows from the !!{undischarged} assumptions~$\Gamma$ of~$\delta_1$. Consider \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lor !B}$. Suppose $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$; then $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ since $\Gamma \Entails !A$ (the inductive hypothesis). So it must also be the case that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lor !B}$. (The case where $!A \lor !B$ is inferred from~$!B$ is handled similarly.) \item The last inference is \Intro{\lif}: $!A \lif !B$ is inferred from a subproof with assumption~$!A$ and conclusion~$!B$, i.e., \begin{prooftree} \AxiomC{$\Gamma, \Discharge{!A}{n}$} \RightLabel{$\delta_1$} \DeduceC{$!B$} \DischargeRule{\Intro{\lif}}{n} \UnaryInfC{$!A \lif !B$} \end{prooftree} By inductive hypothesis, $!B$ follows from the !!{undischarged} assumptions of~$\delta_1$, i.e., $\Gamma \cup \{!A\} \Entails !B$. Consider \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. The !!{undischarged} assumptions of~$\delta$ are just $\Gamma$, since $!A$ is discharged at the last inference. So we need to show that $\Gamma \Entails !A \lif !B$. For reductio, suppose that for some \iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$}, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ but $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$. So, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ and $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$. But by hypothesis, $!B$ is a consequence of $\Gamma \cup \{!A\}$, i.e., $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$, which is a contradiction. So, $\Gamma \Entails !A \lif !B$. \item The last inference is \FalseInt: Here, $\delta$ ends in \begin{prooftree} \AxiomC{$\Gamma$} \RightLabel{$\delta_1$} \DeduceC{$\lfalse$} \RightLabel{\FalseInt} \UnaryInfC{$!A$} \end{prooftree} By induction hypothesis, $\Gamma \Entails \lfalse$. We have to show that $\Gamma \Entails !A$. Suppose not; then for some~$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ we have $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ and $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$. But we always have $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lfalse}$, so this would mean that $\Gamma \Entails/ \lfalse$, contrary to the induction hypothesis. \item The last inference is \FalseCl: Exercise. \iftag{FOL}{ \item The last inference is \Intro{\lforall}: Then $\delta$ has the form \begin{prooftree} \AxiomC{$\Gamma$} \RightLabel{$\delta_1$} \DeduceC{$!A(a)$} \RightLabel{\Intro{\lforall}} \UnaryInfC{$\lforall[x][!A(x)]$} \end{prooftree} The premise $!A(a)$ is a consequence of the !!{undischarged} assumptions $\Gamma$ by induction hypothesis. Consider some structure, $\Struct{M}$, such that $\Sat{M}{\Gamma}$. We need to show that $\Sat{M}{\lforall[x][!A(x)]}$. Since $\lforall[x][!A(x)]$ is !!a{sentence}, this means we have to show that for every variable assignment~$s$, $\Sat{M}{!A(x)}[s]$ (\olref[syn][ass]{prop:sat-quant}). Since $\Gamma$ consists entirely of sentences, $\Sat{M}{!B}[s]$ for all $!B \in \Gamma$ by \olref[syn][sat]{defn:satisfaction}. Let $\Struct{M'}$ be like $\Struct{M}$ except that $\Assign{a}{M'} = s(x)$. Since $a$ does not occur in~$\Gamma$, $\Sat{M'}{\Gamma}$ by \olref[syn][ext]{cor:extensionality-sent}. Since $\Gamma \Entails !A(a)$, $\Sat{M'}{!A(a)}$. Since $!A(a)$ is !!a{sentence}, $\Sat{M'}{!A(a)}[s]$ by \olref[syn][ass]{prop:sentence-sat-true}. $\Sat{M'}{!A(x)}[s]$ iff $\Sat{M'}{!A(a)}$ by \olref[syn][ext]{prop:ext-formulas} (recall that $!A(a)$ is just $\Subst{!A(x)}{a}{x}$). So, $\Sat{M'}{!A(x)}[s]$. Since $a$ does not occur in~$!A(x)$, by \olref[syn][ext]{prop:extensionality}, $\Sat{M}{!A(x)}[s]$. But $s$ was an arbitrary variable assignment, so $\Sat{M}{\lforall[x][!A(x)]}$. \item The last inference is \Intro{\lexists}: Exercise. \item The last inference is \Elim{\forall}: Exercise. }{} \end{enumerate} Now let's consider the possible inferences with several premises: \Elim{\lor}, \Intro{\land}, \iftag{FOL}{\Elim{\lif}, and \Elim{\lexists}}{and \Elim{\lif}}. \begin{enumerate} \item The last inference is \Intro{\land}. $!A \land !B$ is inferred from the premises $!A$ and $!B$ and $\delta$ has the form \begin{prooftree} \AxiomC{$\Gamma_1$} \RightLabel{$\delta_1$} \DeduceC{$!A$} \AxiomC{$\Gamma_2$} \RightLabel{$\delta_2$} \DeduceC{$!B$} \RightLabel{\Intro{\land}} \BinaryInfC{$!A \land !B$} \end{prooftree} By induction hypothesis, $!A$ follows from the !!{undischarged} assumptions~$\Gamma_1$ of~$\delta_1$ and $!B$ follows from the !!{undischarged} assumptions~$\Gamma_2$ of~$\delta_2$. The !!{undischarged} assumptions of~$\delta$ are $\Gamma_1 \cup \Gamma_2$, so we have to show that $\Gamma_1 \cup \Gamma_2 \Entails !A \land !B$. Consider \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$} with $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup \Gamma_2}$. Since $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1}$, it must be the case that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ as $\Gamma_1 \Entails !A$, and since $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_2}$, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ since $\Gamma_2 \Entails !B$. Together, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$. \item The last inference is \Elim{\lor}: Exercise. \item The last inference is \Elim{\lif}. $!B$ is inferred from the premises $!A \lif !B$ and~$!A$. The !!{derivation}~$\delta$ looks like this: \begin{prooftree} \AxiomC{$\Gamma_1$} \RightLabel{$\delta_1$} \DeduceC{$!A \lif !B$} \AxiomC{$\Gamma_2$} \RightLabel{$\delta_2$} \DeduceC{$!A$} \RightLabel{\Elim{\lif}} \BinaryInfC{$!B$} \end{prooftree} By induction hypothesis, $!A \lif !B$ follows from the !!{undischarged} assumptions~$\Gamma_1$ of~$\delta_1$ and $!A$ follows from the !!{undischarged} assumptions~$\Gamma_2$ of~$\delta_2$. Consider \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup \Gamma_2}$, then $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$. Suppose $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup \Gamma_2}$. Since $\Gamma_1 \Entails !A \lif !B$, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lif !B}$. Since $\Gamma_2 \Entails !A$, we have $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. This means that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ (For if $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$, since $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$, we'd have $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$, contradicting~$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lif !B}$). \item The last inference is \Elim{\lnot}: Exercise. \tagitem{FOL}{The last inference is \Elim{\lexists}: Exercise.}{} \end{enumerate} \end{proof} \tagprob{FOL} \begin{prob} Complete the proof of \olref[fol][ntd][sou]{thm:soundness}. \end{prob} \tagendprob \tagprob{notFOL} \begin{prob} Complete the proof of \olref[pl][ntd][sou]{thm:soundness}. \end{prob} \tagendprob \begin{cor} \ollabel{cor:weak-soundness} If $\Proves !A$, then $!A$ is \iftag{FOL}{valid}{a tautology}. \end{cor} \begin{cor} \ollabel{cor:consistency-soundness} If $\Gamma$ is satisfiable, then it is consistent. \end{cor} \begin{proof} We prove the contrapositive. Suppose that $\Gamma$ is not consistent. Then $\Gamma \Proves \lfalse$, i.e., there is !!a{derivation} of $\lfalse$ from !!{undischarged} assumptions in~$\Gamma$. By \olref{thm:soundness}, any \iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$} that satisfies $\Gamma$ must satisfy $\lfalse$. Since $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lfalse}$ for every \iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$}, no \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} can satisfy $\Gamma$, i.e., $\Gamma$ is not satisfiable. \end{proof} \end{document}

Ссылаются нормы: SOUNDNESS, sound_for

en · official · sha256:2087831e8733431a2c1d03e82dfeeca9f6d6383b1d776a5790ff2596d9a9153bEN

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: assignments \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{ass} \olsection{Variable Assignments} \begin{explain} A !!{variable} assignment~$s$ provides a value for \emph{every} variable---and there are infinitely many of them. This is of course not necessary. We require !!{variable} assignments to assign values to all !!{variable}s simply because it makes things a lot easier. The value of a term~$t$, and whether or not !!a{formula}~$!A$ is satisfied in !!a{structure} with respect to~$s$, only depend on the assignments~$s$ makes to the !!{variable}s in~$t$ and the free !!{variable}s of~$!A$. This is the content of the next two propositions. To make the idea of ``depends on'' precise, we show that any two variable assignments that agree on all the variables in~$t$ give the same value, and that $!A$ is satisfied relative to one iff it is satisfied relative to the other if two variable assignments agree on all free variables of~$!A$. \end{explain} \begin{prop}\ollabel{prop:valindep} If the !!{variable}s in a term~$t$ are among $x_1$, \dots,~$x_n$, and $s_1(x_i) = s_2(x_i)$ for $i = 1$, \dots,~$n$, then $\Value{t}{M}[s_1] = \Value{t}{M}[s_2]$. \end{prop} \begin{proof} By induction on the complexity of~$t$. For the base case, $t$ can be !!a{constant} or one of the variables~$x_1$, \dots,~$x_n$. If $t = c$, then $\Value{t}{M}[s_1] = \Assign{c}{M} = \Value{t}{M}[s_2]$. If $t = x_i$, $s_1(x_i) = s_2(x_i)$ by the hypothesis of the proposition, and so $\Value{t}{M}[s_1] = s_1(x_i) = s_2(x_i) = \Value{t}{M}[s_2]$. For the inductive step, assume that $t = \Atom{f}{t_1, \dots, t_k}$ and that the claim holds for $t_1$, \dots, $t_k$. Then \begin{align*} \Value{t}{M}[s_1] & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_1] \\ & = \Assign{f}{M}(\Value{t_1}{M}[s_1], \dots, \Value{t_k}{M}[s_1]). \intertext{For $j = 1$, \dots,~$k$, the !!{variable}s of~$t_j$ are among $x_1$, \dots,~$x_n$. By the induction hypothesis, $\Value{t_j}{M}[s_1] = \Value{t_j}{M}[s_2]$. So,} \Value{t}{M}[s_1] & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_1] \\ & = \Assign{f}{M}(\Value{t_1}{M}[s_1], \dots, \Value{t_k}{M}[s_1]) \\ & = \Assign{f}{M}(\Value{t_1}{M}[s_2], \dots, \Value{t_k}{M}[s_2]) \\ & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_2] = \Value{t}{M}[s_2]. \end{align*} \end{proof} \begin{prop}\ollabel{prop:satindep} If the free !!{variable}s in $!A$ are among $x_1$, \dots,~$x_n$, and $s_1(x_i) = s_2(x_i)$ for $i = 1$, \dots,~$n$, then $\Sat{M}{!A}[s_1]$ iff $\Sat{M}{!A}[s_2]$. \end{prop} \begin{proof} We use induction on the complexity of $!A$. For the base case, where $!A$ is atomic, $!A$ can be: \iftag{prvTrue}{$\ltrue$,}{} \iftag{prvFalse}{$\lfalse$,}{} $\Atom{R}{t_1, \dots, t_k}$ for a $k$-place predicate $R$ and terms $t_1$, \dots,~$t_k$, or $\eq[t_1][t_2]$ for terms $t_1$ and~$t_2$. In the latter two cases, we only demonstrate the forward direction of the !!{biconditional}, since the proof of the reverse is symmetrical. \begin{enumerate} \tagitem{prvTrue}{% \indcase{!A}{\ltrue}{both $\Sat{M}{\indfrm}[s_1]$ and $\Sat{M}{\indfrm}[s_2]$.}}{} \tagitem{prvFalse}{% \indcase{!A}{\lfalse}{both $\Sat/{M}{!A}[s_1]$ and $\Sat/{M}{!A}[s_2]$.}}{} \item \indcase{!A}{\Atom{R}{t_1, \ldots, t_k}}{let $\Sat{M}{\indfrm}[s_1]$. Then \[ \langle \Value{t_1}{M}[s_1], \ldots, \Value{t_k}{M}[s_1] \rangle \in \Assign{R}{M}. \] For $i = 1$, \dots,~$k$, $\Value{t_i}{M}[s_1] = \Value{t_i}{M}[s_2]$ by \olref{prop:valindep}. So we also have $\langle \Value{t_i}{M}[s_2], \ldots, \Value{t_k}{M}[s_2] \rangle \in \Assign{R}{M}$, and hence $\Sat{M}{\indfrm}[s_2]$.} \item \indcase{!A}{\eq[t_1][t_2]}{suppose $\Sat{M}{\indfrm}[s_1]$. Then $\Value{t_1}{M}[s_1] = \Value{t_2}{M}[s_1]$. So, \begin{align*} \Value{t_1}{M}[s_2] & = \Value{t_1}{M}[s_1] & \text{(by \olref{prop:valindep})} \\ & = \Value{t_2}{M}[s_1] & \text{(since $\Sat{M}{\eq[t_1][t_2]}[s_1]$)}\\ &= \Value{t_2}{M}[s_2] & \text{(by \olref{prop:valindep}),} \end{align*} so $\Sat{M}{\eq[t_1][t_2]}[s_2]$.} \end{enumerate} Now assume $\Sat{M}{!B}[s_1]$ iff $\Sat{M}{!B}[s_2]$ for all !!{formula}s $!B$ less complex than~$!A$. The induction step proceeds by cases determined by the main operator of~$!A$. In each case, we only demonstrate the forward direction of the !!{biconditional}; the proof of the reverse direction is symmetrical. In all cases except those for the quantifiers, we apply the induction hypothesis to sub-!!{formula}s~$!B$ of~$!A$. The free variables of~$!B$ are among those of~$!A$. Thus, if $s_1$ and $s_2$ agree on the free variables of~$!A$, they also agree on those of~$!B$, and the induction hypothesis applies to~$!B$. \begin{enumerate} \tagitem{defNot}{}{% \iftag{probNot}{% \indcase!{!A}{\lnot !B}{}}{% \indcase{!A}{\lnot !B}{if $\Sat{M}{\indfrm}[s_1]$, then $\Sat/{M}{!B}[s_1]$, so by the induction hypothesis, $\Sat/{M}{!B}[s_2]$, hence $\Sat{M}{\indfrm}[s_2]$.}}} \tagitem{defAnd}{}{% \iftag{probAnd}{% \indcase!{!A}{!B \land !C}{}}{% \indcase{!A}{!B \land !C}{if $\Sat{M}{\indfrm}[s_1]$, then $\Sat{M}{!B}[s_1]$ and $\Sat{M}{!C}[s_1]$, so by induction hypothesis, $\Sat{M}{!B}[s_2]$ and $\Sat{M}{!C}[s_2]$. Hence, $\Sat{M}{\indfrm}[s_2]$.}}} \tagitem{defOr}{}{% \iftag{probOr}{% \indcase!{!A}{!B \lor !C}{}}{% \indcase{!A}{!B \lor !C}{if $\Sat{M}{\indfrm}[s_1]$, then $\Sat{M}{!B}[s_1]$ or $\Sat{M}{!C}[s_1]$. By induction hypothesis, $\Sat{M}{!B}[s_2]$ or $\Sat{M}{!C}[s_2]$, so $\Sat{M}{\indfrm}[s_2]$.}}} \tagitem{defIf}{}{% \iftag{probIf}{% \indcase!{!A}{!B \lif !C}{}}{% \indcase{!A}{!B \lif !C}{if $\Sat{M}{\indfrm}[s_1]$, then $\Sat/{M}{!B}[s_1]$ or $\Sat{M}{!C}[s_1]$. By the induction hypothesis, $\Sat/{M}{!B}[s_2]$ or $\Sat{M}{!C}[s_2]$, so $\Sat{M}{\indfrm}[s_2]$.}}} \tagitem{defIff}{}{% \iftag{probIff}{% \indcase!{!A}{!B \liff !C}{}}{% \indcase{!A}{!B \liff !C}{if $\Sat{M}{\indfrm}[s_1]$, then either $\Sat{M}{!B}[s_1]$ and $\Sat{M}{!C}[s_1]$, or $\Sat/{M}{!B}[s_1]$ and $\Sat/{M}{!C}[s_1]$. By the induction hypothesis, either $\Sat{M}{!B}[s_2]$ and $\Sat{M}{!C}[s_2]$ or $\Sat/{M}{!B}[s_2]$ and $\Sat/{M}{!C}[s_2]$. In either case, $\Sat{M}{\indfrm}[s_2]$.}}} \tagitem{defEx}{}{% \iftag{probEx}{% \indcase!{!A}{\lexists[x][!B]}{}}{% \indcase{!A}{\lexists[x][!B]}{if $\Sat{M}{\indfrm}[s_1]$, there is an $m \in \Domain{M}$ so that $\Sat{M}{!B}[\Subst{s_1}{m}{x}]$. Let $s_1' = \Subst{s_1}{m}{x}$ and $s_2' = \Subst{s_2}{m}{x}$. The free variables of~$!B$ are among $x_1$, \dots, $x_n$, and $x$. $s_1'(x_i) = s_2'(x_i)$, since $s_1'$ and $s_2'$ are $x$-variants of $s_1$ and~$s_2$, respectively, and by hypothesis $s_1(x_i) = s_2(x_i)$. $s_1'(x) = s_2'(x) = m$ by the way we have defined $s_1'$ and~$s_2'$. Then the induction hypothesis applies to $!B$ and $s_1'$, $s_2'$, so $\Sat{M}{!B}[s_2']$. Hence, since $s_2' = \Subst{s_2}{m}{x}$, there is an $m \in \Domain{M}$ such that $\Sat{M}{!B}[\Subst{s_2}{m}{x}]$, and so $\Sat{M}{\indfrm}[s_2]$.}}} \tagitem{defAll}{}{% \iftag{probAll}{% \indcase!{!A}{\lforall[x][!B]}{}}{% \indcase{!A}{\lforall[x][!B]}{if $\Sat{M}{\indfrm}[s_1]$, then for every $m \in \Domain{M}$, $\Sat{M}{!B}[\Subst{s_1}{m}{x}]$. We want to show that also, for every $m \in \Domain{M}$, $\Sat{M}{!B}[\Subst{s_2}{m}{x}]$. So let $m \in \Domain{M}$ be arbitrary, and consider $s_1' = \Subst{s}{m}{x}$ and $s_2' = \Subst{s}{m}{x}$. We have that $\Sat{M}{!B}[s_1']$. The free variables of~$!B$ are among $x_1$, \dots, $x_n$, and $x$. $s_1'(x_i) = s_2'(x_i)$, since $s_1'$ and $s_2'$ are $x$-variants of $s_1$ and~$s_2$, respectively, and by hypothesis $s_1(x_i) = s_2(x_i)$. $s_1'(x) = s_2'(x) = m$ by the way we have defined $s_1'$ and~$s_2'$. Then the induction hypothesis applies to~$!B$ and~$s_1'$, $s_2'$, and we have $\Sat{M}{!B}[s_2']$. This applies to every $m \in \Domain{M}$, i.e., $\Sat{M}{!B}[\Subst{s_2}{m}{x}]$ for all~$m \in \Domain{M}$, so $\Sat{M}{\indfrm}[s_2]$.}}} \end{enumerate} By induction, we get that $\Sat{M}{!A}[s_1]$ iff $\Sat{M}{!A}[s_2]$ whenever the free !!{variable}s in $!A$ are among $x_1$, \dots, $x_n$ and $s_1(x_i)=s_2(x_i)$ for $i = 1$, \dots,~$n$. \end{proof} \begin{probtag}{probNot,probOr,probAnd,probIf,probIff,probEx,probAll} Complete the proof of \olref[fol][syn][ass]{prop:satindep}. \end{probtag} \begin{explain} !!^{sentence}s have no free variables, so any two variable assignments assign the same things to all the (zero) free variables of any sentence. The proposition just proved then means that whether or not !!a{sentence} is satisfied in a structure relative to a variable assignment is completely independent of the assignment. We'll record this fact. It justifies the definition of satisfaction of !!a{sentence} in !!a{structure} (without mentioning a variable assignment) that follows. \end{explain} \begin{cor} \ollabel{cor:sat-sentence} If $!A$ is !!a{sentence} and $s$ a variable assignment, then $\Sat{M}{!A}[s]$ iff $\Sat{M}{!A}[s']$ for every variable assignment~$s'$. \end{cor} \begin{proof} Let $s'$ be any variable assignment. Since $!A$ is !!a{sentence}, it has no free variables, and so every variable assignment~$s'$ trivially assigns the same things to all free variables of~$!A$ as does~$s$. So the condition of \olref{prop:satindep} is satisfied, and we have $\Sat{M}{!A}[s]$ iff $\Sat{M}{!A}[s']$. \end{proof} \begin{defn} \ollabel{defn:satisfaction} If $!A$ is !!a{sentence}, we say that !!a{structure}~$\Struct M$ \emph{satisfies}~$!A$, $\Sat{M}{!A}$, iff $\Sat{M}{!A}[s]$ for all variable assignments~$s$. \end{defn} If $\Sat{M}{!A}$, we also simply say that \emph{$!A$ is true in~$\Struct{M}$.} The notion of satisfaction naturally extends from individual !!{sentence}s to sets of !!{sentence}s. \begin{defn} \ollabel{defn:sat} If $\Gamma$ is a set of !!{sentence}s~$\Gamma$, we say that !!a{structure}~$\Struct M$ \emph{satisfies}~$\Gamma$, $\Sat{M}{\Gamma}$, iff $\Sat{M}{!A}$ for all $!A \in \Gamma$. \end{defn} \begin{prop}\ollabel{prop:sentence-sat-true} Let $\Struct{M}$ be !!a{structure}, $!A$ be !!a{sentence}, and $s$ a variable assignment. $\Sat{M}{!A}$ iff $\Sat{M}{!A}[s]$. \end{prop} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[fol][syn][ass]{prop:sentence-sat-true} \end{prob} \begin{prop}\ollabel{prop:sat-quant} Suppose $!A(x)$ only contains $x$ free, and $\Struct M$ is !!a{structure}. Then: \begin{tagenumerate}{prvEx,prvAll} \tagitem{prvEx}{$\Sat{M}{\lexists[x][!A(x)]}$ iff $\Sat{M}{!A(x)}[s]$ for at least one variable assignment~$s$.}{} \tagitem{prvAll}{$\Sat{M}{\lforall[x][!A(x)]}$ iff $\Sat{M}{!A(x)}[s]$ for all variable assignments~$s$.}{} \end{tagenumerate} \end{prop} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[fol][syn][ass]{prop:sat-quant}. \end{prob} \begin{prob} \DeclareRobustCommand{\VDash}{\mathrel{||}\joinrel\Relbar} Suppose $\Lang L$ is a language without !!{function}s. Given a !!{structure}~$\Struct M$, $c$ !!a{constant} and $a \in \Domain M$, define $\Struct M[a/c]$ to be the !!{structure} that is just like~$\Struct M$, except that $\Assign{c}{M[a/c]} = a$. Define $\Struct M \VDash !A$ for !!{sentence}s~$!A$ by: \begin{enumerate} \tagitem{prvFalse}{% \indcase{!A}{\lfalse}{not $\Struct{M} \VDash \indfrm$.}}{} \tagitem{prvTrue}{% \indcase{!A}{\ltrue}{$\Struct{M} \VDash \indfrm$.}}{} \item \indcase{!A}{\Atom{R}{d_1, \dots, d_n}}{$\Struct M \VDash \indfrm$ iff $\langle \Assign{d_1}{M}, \dots, \Assign{d_n}{M} \rangle \in \Assign{R}{M}$.} \item \indcase{!A}{\eq[d_1][d_2]}{$\Struct M \VDash \indfrm$ iff $\Assign{d_1}{M} = \Assign{d_2}{M}$.} \tagitem{prvNot}{% \indcase{!A}{\lnot !B}{$\Struct{M} \VDash \indfrm$ iff not $\Struct{M} \VDash {!B}$.}}{} \tagitem{prvAnd}{% \indcase{!A}{(!B \land !C)}{$\Struct{M} \VDash \indfrm$ iff $\Struct{M} \VDash!B$ and $\Struct{M} \VDash !C$.}}{} \tagitem{prvOr}{% \indcase{!A}{(!B \lor !C)}{$\Struct{M} \VDash \indfrm$ iff $\Struct{M} \VDash !B$ or $\Struct{M} \VDash !C$ (or both).}}{} \tagitem{prvIf}{% \indcase{!A}{(!B \lif !C)}{$\Struct{M} \VDash \indfrm$ iff not $\Struct {M} \VDash !B$ or $\Struct M \VDash !C$ (or both).}}{} \tagitem{prvIff}{% \indcase{!A}{(!B \liff !C)}{$\Struct{M} \VDash {\indfrm}$ iff either both $\Struct{M} \VDash {!B}$ and $\Struct{M} \VDash {!C}$, or neither $\Struct{M} \VDash {!B}$ nor $\Struct{M} \VDash {!C}$.}}{} \tagitem{prvAll}{% \indcase{!A}{\lforall[x][!B]}{$\Struct{M} \VDash {\indfrm}$ iff for all $a \in \Domain{M}$, $\Struct{M[a/c]} \VDash \Subst{!B}{c}{x}$, if $c$ does not occur in~$!B$.}}{} \tagitem{prvEx}{% \indcase{!A}{\lexists[x][!B]}{$\Struct{M} \VDash {\indfrm}$ iff there is an $a \in \Domain M$ such that $\Struct{M[a/c]} \VDash \Subst{!B}{c}{x}$, if $c$ does not occur in~$!B$.}}{} \end{enumerate} Let $x_1$, \dots, $x_n$ be all free !!{variable}s in~$!A$, $c_1$, \dots, $c_n$ constant symbols not in~$!A$, $a_1$, \dots, $a_n \in \Domain M$, and $s(x_i) = a_i$. Show that $\Sat{M}{!A}[s]$ iff $\Struct M[a_1/c_1,\dots,a_n/c_n] \VDash \Subst{\Subst{!A}{c_1}{x_1}\dots}{c_n}{x_n}$. (This problem shows that it is possible to give a semantics for first-order logic that makes do without variable assignments.) \end{prob} \begin{prob} Suppose that $f$ is a function symbol not in~$!A(x,y)$. Show that there is !!a{structure}~$\Struct{M}$ such that $\Sat{M}{\lforall[x][\lexists[y][!A(x,y)]]}$ iff there is an~$\Struct M'$ such that $\Sat{M'}{\lforall[x][!A(x,f(x))]}$. (This problem is a special case of what's known as Skolem's Theorem; $\lforall[x][!A(x,f(x))]$ is called a \emph{Skolem normal form} of $\lforall[x][\lexists[y][!A(x,y)]]$.) \end{prob} \end{document}

Ссылаются нормы: TERM_VALUE, VARIABLE_ASSIGNMENT

en · official · sha256:443634b114eb8dcb8863c275cdd29a21ba63c2d489bf568e451e52e5c21aa083EN

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: substitution \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{ext} \olsection{Extensionality} \begin{explain} Extensionality, sometimes called relevance, can be expressed informally as follows: the only factors that bear upon the satisfaction of !!{formula}~$!A$ in !!a{structure}~$\Struct M$ relative to !!a{variable} assignment~$s$, are the size of the !!{domain} and the assignments made by~$\Struct M$ and~$s$ to the elements of the language that actually appear in~$!A$. One immediate consequence of extensionality is that where two !!{structure}s~$\Struct M$ and~$\Struct M'$ agree on all the elements of the language appearing in a sentence~$!A$ and have the same domain,~$\Struct M$ and~$\Struct M'$ must also agree on whether or not $!A$ itself is true. \end{explain} \begin{prop}[Extensionality] \ollabel{prop:extensionality} Let $!A$ be !!a{formula}, and $\Struct M_1$ and $\Struct M_2$ be !!{structure}s with $\Domain{M_1} = \Domain{M_2}$, and $s$ a variable assignment on $\Domain{M_1} = \Domain{M_2}$. If $\Assign{c}{M_1} = \Assign{c}{M_2}$, $\Assign{R}{M_1}=\Assign{R}{M_2}$, and $\Assign{f}{M_1} = \Assign{f}{M_2}$ for every !!{constant}~$c$, relation symbol~$R$, and !!{function} $f$ occurring in~$!A$, then $\Sat{M_1}{!A}[s]$ iff $\Sat{M_2}{!A}[s]$. \end{prop} \begin{proof} First prove (by induction on~$t$) that for every term, $\Value{t}{M_1}[s] = \Value{t}{M_2}[s]$. Then prove the proposition by induction on~$!A$, making use of the claim just proved for the induction basis (where $!A$ is atomic). \end{proof} \begin{prob} Carry out the proof of \olref[fol][syn][ext]{prop:extensionality} in detail. \end{prob} \begin{cor}[Extensionality for !!^{sentence}s] \ollabel{cor:extensionality-sent} Let $!A$ be !!a{sentence} and $\Struct{M_1}$, $\Struct{M_2}$ as in \olref{prop:extensionality}. Then $\Sat{M_1}{!A}$ iff $\Sat{M_2}{!A}$. \end{cor} \begin{proof} Follows from \olref{prop:extensionality} by \olref[ass]{cor:sat-sentence}. \end{proof} Moreover, the value of a term, and whether or not !!a{structure} satisfies !!a{formula}, only depend on the values of its subterms. \begin{prop}\ollabel{prop:ext-terms} Let $\Struct M$ be !!a{structure}, $t$ and $t'$ terms, and $s$ a variable assignment. Then $\Value{\Subst{t}{t'}{x}}{M}[s] = \Value{t}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}]$. \end{prop} \begin{proof} By induction on~$t$. \begin{enumerate} \item If $t$ is a constant, say, $t\ident c$, then $\Subst{t}{t'}{x} = c$, and $\Value{c}{M}[s] = \Assign{c}{M} = \Value{c}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}]$. \item If $t$ is a variable other than~$x$, say, $t \ident y$, then $\Subst{t}{t'}{x} = y$, and $\Value{y}{M}[s] = \Value{y}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}]$ since $\varAssign{s}{\Subst{s}{\Value{t'}{M}[s]}{x}}{x}$. \item If $t \ident x$, then $\Subst{t}{t'}{x} = t'$. But $\Value{x}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}] = \Value{t'}{M}[s]$ by definition of~$\Subst{s}{\Value{t'}{M}[s]}{x}$. \item If $t \ident \Atom{f}{t_1,\dots,t_n}$ then we have: \begin{multline*} \Value{\Subst{t}{t'}{x}}{M}[s] = \\ \begin{aligned}[b] & = \Value{\Atom{f}{\Subst{t_1}{t'}{x}, \dots, \Subst{t_n}{t'}{x}}}{M}[s]\\ & \qquad \text{ by definition of $\Subst{t}{t'}{x}$}\\ & = \Assign{f}{M}(\Value{\Subst{t_1}{t'}{x}}{M}[s], \dots, \Value{\Subst{t_n}{t'}{x}}{M}[s])\\ & \qquad \text{ by definition of $\Value{\Atom{f}{\dots}}{M}[s]$}\\ & = \Assign{f}{M}(\Value{t_1}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}], \dots, \Value{t_n}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}])\\ & \qquad \text{ by induction hypothesis}\\ & = \Value{t}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}] \text{ by definition of $\Value{\Atom{f}{\dots}}{M}[\Subst{s}{\Value{t'}{M}[s]}{x}]$} \end{aligned} \end{multline*} \end{enumerate} \end{proof} \begin{prop}\ollabel{prop:ext-formulas} Let $\Struct M$ be !!a{structure}, $!A$ !!a{formula}, $t'$~a term, and $s$~a variable assignment. Then $\Sat{M}{\Subst{!A}{t'}{x}}[s]$ iff $\Sat{M}{!A}[\Subst{s}{\Value{t'}{M}[s]}{x}]$. \end{prop} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[fol][syn][ext]{prop:ext-formulas} \end{prob} \begin{explain} The point of \cref{fol:syn:ext:prop:ext-terms,fol:syn:ext:prop:ext-formulas} is the following. Suppose we have a term $t$ or !!a{formula}~$!A$ and some term~$t'$, and we want to know the value of $\Subst{t}{t'}{x}$ or whether or not $\Subst{!A}{t'}{x}$ is satisfied in !!a{structure}~$\Struct M$ relative to !!a{variable} assignment~$s$. Then we can either perform the substitution first and then consider the value or satisfaction relative to $\Struct{M}$ and~$s$, or we can first determine the value~$m = \Value{t'}{M}[s]$ of $t'$ in $\Struct{M}$ relative to~$s$, change the !!{variable} assignment to~$\Subst{s}{m}{x}$ and then consider the value of~$t$ in $\Struct{M}$ and~$\Subst{s}{m}{x}$, or whether $\Sat{M}{!A}[\Subst{s}{m}{x}]$. \Cref{fol:syn:ext:prop:ext-terms,fol:syn:ext:prop:ext-formulas} guarantee that the answer will be the same, whichever way we do it. \end{explain} \end{document}

Ссылаются нормы: EXTENSIONALITY

en · official · sha256:01d043caff592a8b7637df6461104b054d480dffe3d77284383745c3c5e44472EN

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: satisfaction \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{sat} \olsection{Satisfaction of \article{formula} \printtoken{S}{formula} in \article{structure} \printtoken{S}{structure}} \begin{explain} The basic notion that relates expressions such as terms and !!{formula}s, on the one hand, and !!{structure}s on the other, are those of \emph{!!{value}} of a term and \emph{satisfaction} of !!a{formula}. Informally, the !!{value} of a term is an !!{element} of !!a{structure}---if the term is just a constant, its !!{value} is the object assigned to the constant by the !!{structure}, and if it is built up using !!{function}s, the !!{value} is computed from the !!{value}s of constants and the functions assigned to the functions in the term. !!^a{formula} is \emph{satisfied} in !!a{structure} if the interpretation given to the predicates makes the !!{formula} true in the domain of the !!{structure}. This notion of satisfaction is specified inductively: the specification of the !!{structure} directly states when atomic !!{formula}s are satisfied, and we define when a complex !!{formula} is satisfied depending on the main connective or quantifier and whether or not the immediate !!{subformula}s are satisfied. The case of the quantifiers here is a bit tricky, as the immediate !!{subformula} of a quantified !!{formula} has a free !!{variable}, and !!{structure}s don't specify the !!{value}s of !!{variable}s. In order to deal with this difficulty, we also introduce \emph{variable assignments} and define satisfaction not with respect to !!a{structure} alone, but with respect to !!a{structure} plus !!a{variable} assignment. \end{explain} \begin{defn}[Variable Assignment] A \emph{variable assignment}~$s$ for !!a{structure}~$\Struct{M}$ is a function which maps each !!{variable} to !!a{element} of~$\Domain M$, i.e., $s\colon \Var \to \Domain M$. \end{defn} \begin{explain} !!^a{structure} assigns !!a{value} to each !!{constant}, and a variable assignment to each variable. But we want to use terms built up from them to also name !!{element}s of the !!{domain}. For this we define the !!{value} of terms inductively. For !!{constant}s and variables the value is just as the !!{structure} or the variable assignment specifies it; for more complex terms it is computed recursively using the functions the !!{structure} assigns to the !!{function}s. \end{explain} \begin{defn}[!!^{value} of Terms] If $t$ is a term of the language~$\Lang L$, $\Struct M$ is a !!{structure} for~$\Lang L$, and $s$ is !!a{variable} assignment for~$\Struct M$, the \emph{!!{value}}~$\Value{t}{M}[s]$ is defined as follows: \begin{enumerate} \item \indcase{t}{c}{$\Value{\indfrm}{M}[s] = \Assign{\indcomplex}{M}$.} \item \indcase{t}{x}{$\Value{\indfrm}{M}[s] = s(\indcomplex)$.} \item \indcase{t}{\Atom{f}{t_1, \ldots, t_n}}{ \[ \Value{\indfrm}{M}[s] = \Assign{f}{M}(\Value{t_1}{M}[s], \ldots, \Value{t_n}{M}[s]). \]} \end{enumerate} \end{defn} \begin{defn}[$x$-Variant] If $s$ is !!a{variable} assignment for !!a{structure}~$\Struct M$, then any !!{variable} assignment~$s'$ for~$\Struct M$ which differs from~$s$ at most in what it assigns to~$x$ is called an \emph{$x$-variant} of~$s$. If $s'$ is an $x$-variant of~$s$ we write $\varAssign{s'}{s}{x}$. \end{defn} \begin{explain} Note that an $x$-variant of an assignment~$s$ does not \emph{have} to assign something different to~$x$. In fact, every assignment counts as an $x$-variant of itself. \end{explain} \begin{defn} If $s$ is !!a{variable} assignment for !!a{structure}~$\Struct M$ and $m \in \Domain{M}$, then the assignment~$\Subst{s}{m}{x}$ is the variable assignment defined by \[\Subst{s}{m}{x}(y) = \begin{cases} m & \text{if } y \ident x\\ s(y) & \text{otherwise}. \end{cases}\] \end{defn} In other words, $\Subst{s}{m}{x}$ is the particular $x$-variant of~$s$ which assigns the domain !!{element}~$m$ to~$x$, and assigns the same things to !!{variable}s other than~$x$ that $s$ does. \begin{defn}[Satisfaction] \ollabel{defn:satisfaction} Satisfaction of !!a{formula}~$!A$ in !!a{structure}~$\Struct M$ relative to !!a{variable} assignment~$s$, in symbols: $\Sat{M}{!A}[s]$, is defined recursively as follows. (We write $\Sat/{M}{!A}[s]$ to mean ``not $\Sat{M}{!A}[s]$.'') \begin{enumerate} \tagitem{prvFalse}{% \indcase{!A}{\lfalse}{$\Sat/{M}{\indfrm}[s]$.}}{} \tagitem{prvTrue}{% \indcase{!A}{\ltrue}{$\Sat{M}{\indfrm}[s]$.}}{} \item \indcase{!A}{\Atom{R}{t_1, \dots, t_n}}{$\Sat{M}{\indfrm}[s]$ iff $\langle \Value{t_1}{M}[s], \dots, \Value{t_n}{M}[s] \rangle \in \Assign{R}{M}$.} \item \indcase{!A}{\eq[t_1][t_2]}{$\Sat{M}{\indfrm}[s]$ iff $\Value{t_1}{M}[s] = \Value{t_2}{M}[s]$.} \tagitem{prvNot}{% \indcase{!A}{\lnot !B}{$\Sat{M}{\indfrm}[s]$ iff $\Sat/{M}{!B}[s]$.}}{} \tagitem{prvAnd}{% \indcase{!A}{(!B \land !C)}{$\Sat{M}{\indfrm}[s]$ iff $\Sat{M}{!B}[s]$ and $\Sat{M}{!C}[s]$.}}{} \tagitem{prvOr}{% \indcase{!A}{(!B \lor !C)}{$\Sat{M}{\indfrm}[s]$ iff $\Sat{M}{!B}[s]$ or $\Sat{M}{!C}[s]$ (or both).}}{} \tagitem{prvIf}{% \indcase{!A}{(!B \lif !C)}{$\Sat{M}{\indfrm}[s]$ iff $\Sat/{M}{!B}[s]$ or $\Sat{M}{!C}[s]$ (or both).}}{} \tagitem{prvIff}{% \indcase{!A}{(!B \liff !C)}{$\Sat{M}{\indfrm}[s]$ iff either both $\Sat{M}{!B}[s]$ and $\Sat{M}{!C}[s]$, or neither $\Sat{M}{!B}[s]$ nor $\Sat{M}{!C}[s]$.}}{} \tagitem{prvAll}{% \indcase{!A}{\lforall[x][!B]}{$\Sat{M}{\indfrm}[s]$ iff for every !!{element}~$m \in \Domain M$, $\Sat{M}{!B}[\Subst{s}{m}{x}]$.}}{} \tagitem{prvEx}{% \indcase{!A}{\lexists[x][!B]}{$\Sat{M}{\indfrm}[s]$ iff for at least one !!{element}~$m \in \Domain M$, $\Sat{M}{!B}[\Subst{s}{m}{x}]$.}}{} \end{enumerate} \end{defn} \begin{explain} The variable assignments are important in the last \iftag{notprvEx,notprvAll}{clause}{two clauses}.\iftag{prvAll}{ We cannot define satisfaction of $\lforall[x][!B(x)]$ by ``for all $m \in \Domain{M}$, $\Sat{M}{!B(m)}$.''}{}\iftag{prvEx}{ We cannot define satisfaction of $\lexists[x][!B(x)]$ by ``for at least one $m \in \Domain{M}$, $\Sat{M}{!B(m)}$.''}{} The reason is that if $m \in \Domain M$, it is not a symbol of the language, and so $!B(m)$~is not !!a{formula} (that is, $\Subst{!B}{m}{x}$ is undefined). We also cannot assume that we have !!{constant}s or terms available that name every !!{element} of~$\Struct{M}$, since there is nothing in the definition of !!{structure}s that requires it. In the standard language, the set of !!{constant}s is !!{denumerable}, so if $\Domain{M}$ is not !!{enumerable} there aren't even enough !!{constant}s to name every object. We solve this problem by introducing !!{variable} assignments, which allow us to link variables directly with !!{element}s of the domain. Then instead of saying that, e.g., \iftag{prvEx}{$\lexists[x][!B(x)]$}{$\lforall[x][!B(x)]$} is satisfied in~$\Struct M$ iff \iftag{prvEx}{for at least one $m \in \Domain{M}$}{for all $m \in \Domain{M}$, $\Sat{M}{!B(m)}$}, we say it is satisfied in~$\Struct M$ \emph{relative to}~$s$ iff $!B(x)$ is satisfied relative to~$\Subst{s}{m}{x}$ \iftag{prvEx}{for at least one}{for every} $m \in \Domain M$. \end{explain} \begin{ex} Let $\Lang{L} = \{a, b, f, R\}$ where $a$ and $b$ are !!{constant}s, $f$~is a two-place !!{function}, and $R$~is a two-place !!{predicate}. Consider the !!{structure}~$\Struct{M}$ defined by: \begin{enumerate} \item $\Domain M = \{1, 2, 3, 4\}$ \item $\Assign{a}{M} = 1$ \item $\Assign{b}{M} = 2$ \item $\Assign{f}{M}(x, y) = x+y$ if $x+y \le 3$ and $= 3$ otherwise. \item $\Assign{R}{M} = \{\tuple{1, 1}, \tuple{1, 2}, \tuple{2, 3}, \tuple{2, 4}\}$ \end{enumerate} The function $s(x) = 1$ that assigns $1 \in \Domain{M}$ to every !!{variable} is a variable assignment for~$\Struct{M}$. Then \begin{align*} \Value{f(a,b)}{M}[s] & = \Assign{f}{M}(\Value{a}{M}[s], \Value{b}{M}[s]). \intertext{Since $a$ and $b$ are !!{constant}s, $\Value{a}{M}[s] = \Assign{a}{M} = 1$ and $\Value{b}{M}[s] = \Assign{b}{M} = 2$. So} \Value{f(a,b)}{M}[s] & = \Assign{f}{M}(1, 2) = 1+2 = 3. \intertext{To compute the value of $f(f(a,b),a)$ we have to consider} \Value{f(f(a,b),a)}{M}[s] & = \Assign{f}{M}(\Value{f(a, b)}{M}[s], \Value{a}{M}[s]) = \Assign{f}{M}(3, 1) = 3, \intertext{since $3+1 > 3$. Since $s(x) = 1$ and $\Value{x}{M}[s] = s(x)$, we also have} \Value{f(f(a,b),x)}{M}[s] & = \Assign{f}{M}(\Value{f(a, b)}{M}[s], \Value{x}{M}[s]) = \Assign{f}{M}(3, 1) = 3, \end{align*} An atomic !!{formula}~$R(t_1, t_2)$ is satisfied if the tuple of values of its arguments, i.e., $\tuple{\Value{t_1}{M}[s], \Value{t_2}{M}[s]}$, is !!a{element} of~$\Assign{R}{M}$. So, e.g., we have $\Sat{M}{R(b,f(a,b))}[s]$ since $\tuple{\Value{b}{M}, \Value{f(a,b)}{M}} = \tuple{2, 3} \in \Assign{R}{M}$, but $\Sat/{M}{R(x, f(a,b))}[s]$ since $\tuple{1, 3} \notin \Assign{R}{M}[s]$. To determine if a non-atomic formula~$!A$ is satisfied, you apply the clauses in the inductive definition that applies to the main connective. For instance, the main connective in $R(a, a) \lif (R(b, x) \lor R(x, b))$ is the~$\lif$, and \begin{align*} & \Sat{M}{R(a, a) \lif (R(b, x) \lor R(x, b))}[s] \text{ iff }\\ & \qquad \Sat/{M}{R(a,a)}[s] \text{ or } \Sat{M}{R(b, x) \lor R(x, b)}[s] \intertext{Since $\Sat{M}{R(a,a)}[s]$ (because $\tuple{1,1} \in \Assign{R}{M}$) we can't yet determine the answer and must first figure out if $\Sat{M}{R(b, x) \lor R(x, b)}[s]$:} & \Sat{M}{R(b, x) \lor R(x, b)}[s] \text{ iff }\\ & \qquad \Sat{M}{R(b,x)}[s] \text{ or } \Sat{M}{R(x, b)}[s] \intertext{And this is the case, since $\Sat{M}{R(x, b)}[s]$ (because $\tuple{1,2} \in \Assign{R}{M}$).} \end{align*} Recall that an $x$-variant of~$s$ is a variable assignment that differs from $s$ at most in what it assigns to~$x$. For every !!{element} of~$\Domain{M}$, there is an $x$-variant of~$s$: \begin{align*} s_1 & = \Subst{s}{1}{x}, & s_2 & = \Subst{s}{2}{x},\\ s_3 & = \Subst{s}{3}{x}, & s_4 & = \Subst{s}{4}{x}. \end{align*} So, e.g., $s_2(x) = 2$ and $s_2(y) = s(y) = 1$ for all variables~$y$ other than~$x$. These are all the $x$-variants of~$s$ for the structure~$\Struct{M}$, since $\Domain{M} = \{1, 2, 3, 4\}$. Note, in particular, that $s_1 = s$ ($s$~is always an $x$-variant of itself). \iftag{prvEx}{To determine if an existentially quantified !!{formula}~$\lexists[x][!A(x)]$ is satisfied, we have to determine if $\Sat{M}{!A(x)}[\Subst{s}{m}{x}]$ for at least one $m \in \Domain M$. So, \[ \Sat{M}{\lexists[x][(R(b,x) \lor R(x,b))]}[s], \] since $\Sat{M}{R(b,x) \lor R(x, b)}[\Subst{s}{1}{x}]$ ($\Subst{s}{3}{x}$ would also fit the bill). But, \[ \Sat/{M}{\lexists[x][(R(b,x) \land R(x,b))]}[s] \] since, whichever $m \in \Domain{M}$ we pick, $\Sat/{M}{R(b,x) \land R(x,b)}[\Subst{s}{m}{x}]$.}{} \iftag{prvAll}{To determine if a universally quantified !!{formula}~$\lforall[x][!A(x)]$ is satisfied, we have to determine if $\Sat{M}{!A(x)}[\Subst{s}{m}{x}]$ for all $m \in \Domain M$. So, \[ \Sat{M}{\lforall[x][(R(x,a) \lif R(a,x))]}[s], \] since $\Sat{M}{R(x,a) \lif R(a,x)}[\Subst{s}{m}{x}]$ for all $m \in \Domain M$. For $m = 1$, we have $\Sat{M}{R(a,x)}[\Subst{s}{1}{x}]$ so the consequent is true; for $m = 2$, $3$, and~$4$, we have $\Sat/{M}{R(x,a)}[\Subst{s}{m}{x}]$, so the antecedent is false. But, \[ \Sat/{M}{\lforall[x][(R(a,x) \lif R(x,a))]}[s] \] since $\Sat/{M}{R(a,x) \lif R(x,a)}[\Subst{s}{2}{x}]$ (because $\Sat{M}{R(a, x)}[\Subst{s}{2}{x}]$ and $\Sat/{M}{R(x, a)}[\Subst{s}{2}{x}]$).}{} \iftag{defEx}{To determine if an existentially quantified !!{formula}~$\lexists[x][!A(x)]$ is satisfied, we have to determine if $\Sat{M}{\lnot \lforall[x][\lnot !A(x)]}[s]$. For instance, we have \[ \Sat{M}{\lexists[x][(R(b,x) \lor R(x,b))]}[s]. \] First, $\Sat{M}{R(b,x) \lor R(x, b)}[\Subst{s}{1}{x}]$ ($\Subst{s}{3}{x}$ would also fit the bill). So, $\Sat/{M}{\lnot(R(b,x) \lor R(x,b))}[\Subst{s}{1}{x}]$, thus $\Sat/{M}{\lforall[x][\lnot((R(b,x) \lor R(x,b))]}[s]$, and therefore $\Sat{M}{\lnot\lforall[x][\lnot((R(b,x) \lor R(x,b))]}[s]$. On the other hand, \[ \Sat/{M}{\lexists[x][(R(b,x) \land R(x,b))],}[s]. \] That's because $\Sat{M}{\lforall[x][\lnot(R(b,x) \land R(x,b))]}[s]$, since for no $m \in \Domain M$, $\Sat{M}{R(b,x) \land R(x,b)}[\Subst{s}{m}{x}]$. As you can probably guess from these examples, $\Sat{M}{\lexists[x][!A(x)]}[s]$ iff $\Sat{M}{!A(x)}[\Subst{s}{m}{x}]$ for at least one $m \in \Domain M$.}{} \iftag{defAll}{To determine if a universally quantified !!{formula}~$\lforall[x][!A(x)]$ is satisfied, we have to determine if $\Sat{M}{\lnot\lexists[x][\lnot !A(x)]}[s]$. For instance, \[ \Sat{M}{\lforall[x][(R(x,a) \lif R(a,x))]}[s], \] First, $\Sat{M}{R(x,a) \lif R(a,x)}[\Subst{s}{m}{x}]$ for all $m \in \Domain M$ ($\Sat{M}{R(a,x)}[\Subst{s}{1}{x}]$ and $\Sat/{M}{R(a,x)}[\Subst{s}{m}{x}]$ for $m = 2$, $3$, or~$4$). Thus, there is no $m \in \Domain M$ such that $\Sat{M}{\lnot(R(x,a) \lif R(a,x))}[\Subst{s}{m}{x}]$ and hence $\Sat/{M}{\lexists[x][\lnot(R(x,a) \lif R(a,x))]}[s]$. Therefore, $\Sat{M}{\lnot\lexists[x][\lnot(R(x,a) \lif R(a,x))]}[s]$. On the other hand, \[ \Sat/{M}{\lforall[x][(R(a,x) \lif R(x,a))]}[s], \] since $\Sat/{M}{R(a,x) \lif R(x,a)}[\Subst{s}{2}{x}]$, and so $\Sat{M}{\lexists[x][\lnot(R(a,x) \lif R(x,a))]}[s]$. As you can probably guess from these examples, $\Sat{M}{\lforall[x][!A(x)]}[s]$ iff $\Sat{M}{!A(x)}[\Subst{s}{m}{x}]$ for every $m \in \Domain M$.}{} For a more complicated case, consider \[ \lforall[x][(R(a,x) \lif \lexists[y][R(x,y)])]. \] Since $\Sat/{M}{R(a,x)}[\Subst{s}{3}{x}]$ and $\Sat/{M}{R(a,x)}[\Subst{s}{4}{x}]$, the interesting cases where we have to worry about the consequent of the conditional are only $m = 1$ and $ = 2$. Does $\Sat{M}{\lexists[y][R(x,y)]}[\Subst{s}{1}{x}]$ hold? It does if there is at least one $n \in \Domain M$ so that $\Sat{M}{R(x,y)}[\Subst{\Subst{s}{1}{x}}{n}{y}]$. In fact, if we take $n = 1$, we have $\Subst{\Subst{s}{1}{x}}{n}{y} = \Subst{s}{1}{y} = s$. Since $s(x) = 1$, $s(y) = 1$, and $\tuple{1,1} \in \Assign{R}{M}$, the answer is yes. To determine if $\Sat{M}{\lexists[y][R(x,y)]}[\Subst{s}{2}{x}]$, we have to look at the !!{variable} assignments $\Subst{\Subst{s}{2}{x}}{n}{y}$. Here, for $n = 1$, this assignment is~$s_2 = \Subst{s}{2}{x}$, which does not satisfy $R(x,y)$ ($s_2(x) = 2$, $s_2(y) = 1$, and $\tuple{2,1}\notin \Assign{R}{M}$). However, consider $\Subst{\Subst{s}{2}{x}}{3}{y} = \Subst{s_2}{3}{y}$. $\Sat{M}{R(x,y)}[\Subst{s_2}{3}{y}]$ since $\tuple{2,3} \in \Assign{R}{M}$, and so $\Sat{M}{\lexists[y][R(x,y)]}[s_2]$. So, for all $n \in \Domain M$, either $\Sat/{M}{R(a,x)}[\Subst{s}{m}{x}]$ (if $m = 3$, $4$) or $\Sat{M}{\lexists[y][R(x,y)]}[\Subst{s}{m}{x}]$ (if $m = 1$, $2$), and so \[ \Sat{M}{\lforall[x][(R(a,x) \lif \lexists[y][R(x,y)])]}[s]. \] On the other hand, \[ \Sat/{M}{\lexists[x][(R(a,x) \land \lforall[y][R(x,y)])]}[s]. \] We have $\Sat{M}{R(a,x)}[\Subst{s}{m}{x}]$ only for $m = 1$ and $m = 2$. But for both of these values of~$m$, there is in turn an $n \in \Domain M$, namely $n = 4$, so that $\Sat/{M}{R(x,y)}[\Subst{\Subst{s}{m}{x}}{n}{y}]$ and so $\Sat/{M}{\lforall[y][R(x,y)]}[\Subst{s}{m}{x}]$ for $m = 1$ and $m = 2$. In sum, there is no $m \in \Domain M$ such that $\Sat{M}{R(a,x) \land \lforall[y][R(x,y)]}[\Subst{s}{m}{x}]$. \end{ex} \iftag{defEx}{% \begin{prop}\ollabel{prop:sat-ex} $\Sat{M}{\lexists[x][!B(x)]}[s]$ iff there is an $x$-variant $s'$ of $s$ so that $\Sat{M}{!B(x)}[s']$. \end{prop} \begin{proof} Exercise. \end{proof} }{} \tagprob{defEx} \begin{prob} Prove \olref[fol][syn][sat]{prop:sat-ex} \end{prob} \tagendprob \iftag{defAll}{% \begin{prop}\ollabel{prop:sat-all} $\Sat{M}{\lforall[x][!B(x)]}[s]$ iff for every $x$-variant~$s'$ of $s$, $\Sat{M}{!B(x)}[s']$ \end{prop} \begin{proof} Exercise. \end{proof} }{} \tagprob{defAll} \begin{prob} Prove \olref[fol][syn][sat]{prop:sat-all} \end{prob} \tagendprob \begin{prob} Let $\Lang L = \{c, f, A\}$ with one !!{constant}, one one-place !!{function} and one two-place !!{predicate}, and let the !!{structure}~$\Struct{M}$ be given by \begin{enumerate} \item $\Domain M = \{1, 2, 3\}$ \item $\Assign{c}{M} = 3$ \item $\Assign{f}{M}(1) = 2, \Assign{f}{M}(2) = 3, \Assign{f}{M}(3) = 2$ \item $\Assign{A}{M} = \{\tuple{1, 2}, \tuple{2, 3}, \tuple{3, 3}\}$ \end{enumerate} (a) Let $s(v) = 1$ for all !!{variable}s~$v$. Find out whether \[ \Sat{M}{\lexists[x][(A(f(z), c) \lif \lforall[y][(A(y, x) \lor A(f(y), x))])]}[s] \] Explain why or why not. (b) Give a different structure and !!{variable} assignment in which the !!{formula} is not satisfied. \end{prob} \end{document}

Ссылаются нормы: FOL_SATISFACTION, NotComputedHere, execution_boundary, not_computed_here

en · official · sha256:b540a24f76227c816cdb8107f6d46bca476d4fe95fcf61b977d627d9cc341058EN

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: Semantic Notions \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{sem} \olsection{Semantic Notions} \begin{explain} Given the definition of !!{structure}s for first-order languages, we can define some basic semantic properties of and relationships between sentences. The simplest of these is the notion of \emph{validity} of a sentence. A sentence is valid if it is satisfied in every !!{structure}. Valid sentences are those that are satisfied regardless of how the non-logical symbols in it are interpreted. Valid sentences are therefore also called \emph{logical truths}---they are true, i.e., satisfied, in any !!{structure} and hence their truth depends only on the logical symbols occurring in them and their syntactic !!{structure}, but not on the non-logical symbols or their interpretation. \end{explain} \begin{defn}[Validity] A sentence $!A$ is \emph{valid}, $\Entails !A$, iff $\Sat{M}{!A}$ for every !!{structure}~$\Struct M$. \end{defn} \begin{defn}[Entailment] A set of sentences~$\Gamma$ \emph{entails} a sentence~$!A$, $\Gamma \Entails !A$, iff for every !!{structure}~$\Struct M$ with $\Sat{M}{\Gamma}$, $\Sat{M}{!A}$. \end{defn} \begin{defn}[Satisfiability] A set of sentences~$\Gamma$ is \emph{satisfiable} if $\Sat{M}{\Gamma}$ for some !!{structure}~$\Struct M$. If $\Gamma$ is not satisfiable it is called \emph{unsatisfiable}. \end{defn} \begin{prop} A sentence $!A$ is valid iff $\Gamma \Entails !A$ for every set of sentences~$\Gamma$. \end{prop} \begin{proof} For the forward direction, let $!A$ be valid, and let $\Gamma$ be a set of sentences. Let $\Struct M$ be !!a{structure} so that $\Sat{M}{\Gamma}$. Since $!A$ is valid, $\Sat{M}{!A}$, hence $\Gamma \Entails !A$. For the contrapositive of the reverse direction, let $!A$ be invalid, so there is !!a{structure}~$\Struct M$ with $\Sat/{M}{!A}$. When $\Gamma = \{ \ltrue \}$, since $\ltrue$ is valid, $\Sat{M}{\Gamma}$. Hence, there is !!a{structure}~$\Struct M$ so that $\Sat{M}{\Gamma}$ but $\Sat/{M}{!A}$, hence $\Gamma$ does not entail $!A$. \end{proof} \begin{prop} \ollabel{prop:entails-unsat} $\Gamma \Entails !A$ iff $\Gamma \cup \{\lnot !A\}$ is unsatisfiable. \end{prop} \begin{proof} For the forward direction, suppose $\Gamma \Entails !A$ and suppose to the contrary that there is !!a{structure}~$\Struct M$ so that $\Sat{M}{\Gamma \cup \{ \lnot !A \}}$. Since $\Sat{M}{\Gamma}$ and $\Gamma \Entails !A$, $\Sat{M}{!A}$. Also, since $\Sat{M}{\Gamma\cup \{ \lnot !A \}}$, $\Sat{M}{\lnot !A}$, so we have both $\Sat{M}{!A}$ and $\Sat/{M}{!A}$, a contradiction. Hence, there can be no such !!{structure}~$\Struct M$, so $\Gamma \cup \{ \lnot !A \}$ is unsatisfiable. For the reverse direction, suppose $\Gamma \cup \{ \lnot !A \}$ is unsatisfiable. So for every !!{structure}~$\Struct M$, either $\Sat/{M}{\Gamma}$ or $\Sat{M}{!A}$. Hence, for every !!{structure} $\Struct M$ with $\Sat{M}{\Gamma}$, $\Sat{M}{!A}$, so $\Gamma \Entails !A$. \end{proof} \begin{prob} \begin{enumerate} \item Show that $\Gamma \Entails \bot$ iff $\Gamma$ is unsatisfiable. \item Show that $\Gamma \cup \{!A\} \Entails \bot$ iff $\Gamma \Entails \lnot !A$. \item Suppose $c$ does not occur in $!A$ or $\Gamma$. Show that $\Gamma \Entails \lforall[x][!A]$ iff $\Gamma \Entails \Subst{!A}{c}{x}$. \end{enumerate} \end{prob} \begin{prop} If $\Gamma \subseteq \Gamma'$ and $\Gamma \Entails !A$, then $\Gamma' \Entails !A$. \end{prop} \begin{proof} Suppose that $\Gamma \subseteq \Gamma'$ and $\Gamma \Entails !A$. Let $\Struct M$ be a structure such that $\Sat{M}{\Gamma'}$; then $\Sat{M}{\Gamma}$, and since $\Gamma \Entails !A$, we get that $\Sat{M}{!A}$. Hence, whenever $\Sat{M}{\Gamma'}$, $\Sat{M}{!A}$, so $\Gamma' \Entails !A$. \end{proof} \begin{thm}[Semantic Deduction Theorem] \ollabel{thm:sem-deduction} $\Gamma \cup \{!A\} \Entails !B$ iff $\Gamma \Entails !A \lif !B$. \end{thm} \begin{proof} For the forward direction, let $\Gamma \cup \{ !A \} \Entails !B$ and let $\Struct M$ be !!a{structure} so that $\Sat{M}{\Gamma}$. If $\Sat{M}{!A}$, then $\Sat{M}{\Gamma \cup \{ !A \} }$, so since $\Gamma \cup \{ !A \}$ entails $!B$, we get $\Sat{M}{!B}$. Therefore, $\Sat{M}{!A \lif !B}$, so $\Gamma \Entails !A \lif !B$. For the reverse direction, let $\Gamma \Entails !A \lif !B$ and $\Struct M$ be !!a{structure} so that $\Sat{M}{\Gamma \cup \{ !A \}}$. Then $\Sat{M}{\Gamma}$, so $\Sat{M}{!A \lif !B}$, and since $\Sat{M}{!A}$, $\Sat{M}{!B}$. Hence, whenever $\Sat{M}{\Gamma \cup \{ !A \} }$, $\Sat{M}{!B}$, so $\Gamma \cup \{ !A \} \Entails !B$. \end{proof} \begin{prop}\ollabel{prop:quant-terms} Let $\Struct{M}$ be !!a{structure}, and $!A(x)$ !!a{formula} with one free variable~$x$, and $t$~a closed term. Then: \begin{tagenumerate}{prvEx,prvAll} \tagitem{prvEx}{$!A(t) \Entails \lexists[x][!A(x)]$}{} \tagitem{prvAll}{$\lforall[x][!A(x)] \Entails !A(t)$}{} \end{tagenumerate} \end{prop} \begin{proof} \begin{tagenumerate}{prvEx,prvAll} \tagitem{prvEx}{% \iftag{probEx}{Exercise.}{Suppose $\Sat{M}{!A(t)}$. Let $s$ be a variable assignment with $s(x) = \Value{t}{M}$. Then $\Sat{M}{!A(t)}[s]$ since $!A(t)$ is !!a{sentence}. By \olref[ext]{prop:ext-formulas}, $\Sat{M}{!A(x)}[s]$. By \olref[ass]{prop:sat-quant}, $\Sat{M}{\lexists[x][!A(x)]}$.}}{} \tagitem{prvAll}{% \iftag{probAll}{Exercise.}{Suppose $\Sat{M}{\lforall[x][!A(x)]}$. Let $s$ be a variable assignment with $s(x) = \Value{t}{M}$. By \olref[ass]{prop:sat-quant}, $\Sat{M}{!A(x)}[s]$. By \olref[ext]{prop:ext-formulas}, $\Sat{M}{!A(t)}[s]$. By \olref[ass]{prop:sentence-sat-true}, $\Sat{M}{!A(t)}$ since $!A(t)$ is !!a{sentence}.}}{} \end{tagenumerate} \end{proof} \begin{probtag}{probEx,probAll} Complete the proof of \olref[fol][syn][sem]{prop:quant-terms}. \end{probtag} \end{document}

Ссылаются нормы: FOL_CONSEQUENCE, FOL_SATISFIABLE, FOL_VALIDITY, TRUTH_IN_STRUCTURE

en · official · sha256:65fa63d1b3e84be752d07b9c148168febfdc7b1ccbd64bce7413519a9e5b0ee7EN

% Part: first-order-logic % Chapter: syntax-and-semantics % Section: Structures \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{fol}{syn}{str} \olsection{\printtoken{P}{structure} for First-order Languages} \begin{explain} First-order languages are, by themselves, \emph{uninterpreted:} the !!{constant}s, !!{function}s, and !!{predicate}s have no specific meaning attached to them. Meanings are given by specifying \article{structure} \emph{!!{structure}}. It specifies the \emph{domain}, i.e., the objects which the !!{constant}s pick out, the !!{function}s operate on, and the quantifiers range over. In addition, it specifies which !!{constant}s pick out which objects, how !!a{function} maps objects to objects, and which objects the !!{predicate}s apply to. !!^{structure}s are the basis for \emph{semantic} notions in logic, e.g., the notion of consequence, validity, satisfiability. They are variously called ``structures,'' ``interpretations,'' or ``models'' in the literature. \end{explain} \begin{defn}[!!^{structure}s] \Article{structure} \emph{!!{structure}}~$\Struct M$, for a language $\Lang{L}$ of first-order logic consists of the following elements: \begin{enumerate} \item \emph{Domain:} a non-empty set, $\Domain M$ \item \emph{Interpretation of !!{constant}s:} for each !!{constant}~$c$ of $\Lang{L}$, !!a{element} $\Assign{c}{M} \in \Domain M$ \item \emph{Interpretation of !!{predicate}s:} for each $n$-place !!{predicate}~$R$ of $\Lang{L}$ (other than $\eq$), an $n$-place relation $\Assign{R}{M} \subseteq \Domain{M}^n$ \item \emph{Interpretation of !!{function}s:} for each $n$-place !!{function}~$f$ of $\Lang{L}$, an $n$-place function $\Assign{f}{M} \colon \Domain{M}^n \to \Domain{M}$ \end{enumerate} \end{defn} \begin{ex} !!^a{structure}~$\Struct M$ for the language of arithmetic consists of a set, an element of $\Domain M$, $\Assign{\Obj 0}{M}$, as interpretation of the !!{constant}~$\Obj 0$, a one-place function $\Assign{\Obj \prime}{M} \colon \Domain{M} \to \Domain M$, two two-place functions $\Assign{\Obj +}{M}$ and $\Assign{\Obj \times}{M}$, both $\Domain M^2 \to \Domain M$, and a two-place relation $\Assign{\Obj <}{M} \subseteq \Domain{M}^2$. An obvious example of such a structure is the following: \begin{enumerate} \item $\Domain N = \Nat$ \item $\Assign{\Obj 0}{N} = 0$ \item $\Assign{\Obj \prime}{N}(n) = n + 1$ for all $n \in \Nat$ \item $\Assign{\Obj +}{N}(n, m) = n + m$ for all $n, m \in \Nat$ \item $\Assign{\Obj \times}{N}(n, m) = n\cdot m$ for all $n, m \in \Nat$ \item $\Assign{\Obj <}{N} = \Setabs{\tuple{n, m}}{n \in \Nat, m \in \Nat, n < m}$ \end{enumerate} The structure~$\Struct N$ for $\Lang L_A$ so defined is called the \emph{standard model of arithmetic}, because it interprets the non-logical constants of~$\Lang L_A$ exactly how you would expect. However, there are many other possible !!{structure}s for~$\Lang L_A$. For instance, we might take as the domain the set~$\Int$ of integers instead of~$\Nat$, and define the interpretations of $\Obj 0$, $\Obj \prime$, $\Obj +$, $\Obj \times$, $\Obj <$ accordingly. But we can also define structures for~$\Lang L_A$ which have nothing even remotely to do with numbers. \end{ex} \begin{ex} A structure~$\Struct M$ for the language~$\Lang L_Z$ of set theory requires just a set and a single-two place relation. So technically, e.g., the set of people plus the relation ``$x$ is older than $y$'' could be used as !!a{structure} for $\Lang L_Z$, as well as $\Nat$ together with $n \ge m$ for $n, m \in \Nat$. A particularly interesting !!{structure} for $\Lang L_Z$ in which the !!{element}s of the domain are actually sets, and the interpretation of $\Obj \in$ actually is the relation ``$x$ is !!a{element} of~$y$'' is the !!{structure}~$\Struct{{HF}}$ of \emph{hereditarily finite sets}: \begin{enumerate} \item $\Domain{{{HF}}} = \emptyset \cup \Pow{\emptyset} \cup \Pow{\Pow{\emptyset}} \cup \Pow{\Pow{\Pow{\emptyset}}} \cup \dots$; \item $\Assign{\Obj \in}{{{HF}}} = \Setabs{\tuple{x, y}}{x, y \in \Domain{{{HF}}}, x \in y}$. \end{enumerate} \end{ex} \begin{digress} The stipulations we make as to what counts as !!a{structure} impact our logic. For example, the choice to prevent empty domains ensures, given the usual account of satisfaction (or truth) for quantified sentences, that $\lexists[x][(!A(x) \lor \lnot !A(x))]$ is valid---that is, a logical truth. And the stipulation that all !!{constant}s must refer to an object in the domain ensures that the existential generalization is a sound pattern of inference: $!A(a)$, therefore $\lexists[x][!A(x)]$. If we allowed names to refer outside the domain, or to not refer, then we would be on our way to a \emph{free logic}, in which existential generalization requires an additional premise: $!A(a)$ and $\lexists[x][\eq[x][a]]$, therefore $\lexists[x][!A(x)]$. \end{digress} \end{document}

Ссылаются нормы: DOMAIN, MODEL_NOTION, STRUCTURE

en · official · sha256:e0a742f19dfc356e400ec9d1cca0aa6a386afb00e3cbc7774365b4ae4d8d3366EN

% Part: propositional-logic % Chapter: syntax-and-semantics % Section: semantic-notions \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{pl}{syn}{sem} \olsection{Semantic Notions} We define the following semantic notions: \begin{defn} \begin{enumerate} \item !!^a{formula}~$!A$ is \emph{satisfiable} if for some~$\pAssign{v}$, $\pSat{v}{!A}$; it is \emph{unsatisfiable} if for no $\pAssign{v}$, $\pSat{v}{!A}$; \item !!^a{formula}~$!A$ is a \emph{tautology} if $\pSat{v}{!A}$ for all !!{valuation}s~$\pAssign{v}$; \item !!^a{formula}~$!A$ is \emph{contingent} if it is satisfiable but not a tautology; \item If $\Gamma$ is a set of !!{formula}s, $\Gamma \Entails !A$ (``$\Gamma$ entails $!A$'') if and only if $\pSat{v}{!A}$ for every !!{valuation}~$\pAssign{v}$ for which $\pSat{v}{\Gamma}$. \item If $\Gamma$ is a set of !!{formula}s, $\Gamma$ is \emph{satisfiable} if there is !!a{valuation}~$\pAssign{v}$ for which $\pSat{v}{\Gamma}$, and $\Gamma$ is \emph{unsatisfiable} otherwise. \end{enumerate} \end{defn} \begin{prob} For each of the following four !!{formula}s determine whether it is (a)~satisfiable, (b)~tautology, and (c)~contingent. \begin{enumerate} \item \( ( \Obj p_0 \lif ( \lnot \Obj p_1 \lif \lnot \Obj p_0 ) ) \). \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 )) \). \item \( ( \Obj p_0 \liff \Obj p_1 ) \lif ( \Obj p_2 \liff \lnot \Obj p_1 ) \). \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 ))) \). \end{enumerate} \end{prob} \begin{prop} \ollabel{prop:semanticalfacts} \begin{enumerate} \item $!A$ is a tautology if and only if $\emptyset \Entails !A$; \item If $\Gamma \Entails !A$ and $\Gamma \Entails !A \lif !B$ then $\Gamma \Entails !B$; \item If $\Gamma$ is satisfiable then every finite subset of $\Gamma$ is also satisfiable; \item \ollabel{def:monotonicity} Monotonicity: if $\Gamma \subseteq \Delta$ and $\Gamma \Entails !A$ then also $\Delta \Entails !A$; \item \ollabel{def:Cut} Transitivity: if $\Gamma \Entails !A$ and $\Delta \cup \{ !A\} \Entails !B$ then $\Gamma \cup \Delta \Entails !B$. \end{enumerate} \end{prop} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[pl][syn][sem]{prop:semanticalfacts} \end{prob} \begin{prop}\ollabel{prop:entails-unsat} $\Gamma \Entails !A$ if and only if $\Gamma \cup \{\lnot !A\}$ is unsatisfiable. \end{prop} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[pl][syn][sem]{prop:entails-unsat} \end{prob} \begin{thm}[Semantic Deduction Theorem] \ollabel{thm:sem-deduction} $\Gamma \Entails !A \lif !B$ if and only if $\Gamma \cup \{!A\} \Entails !B$. \end{thm} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[pl][syn][sem]{thm:sem-deduction} \end{prob} \end{document}

Ссылаются нормы: LanguageNotion, PROP_ENTAILMENT, PROP_SATISFIABLE, TAUTOLOGY, language_notion, semantic_notion_of

en · official · sha256:67e8e59f40fa61cbc496aef3c3bd67a766a5fe34a9dfcd70fbb9751bfa2555f5EN

% Part: propositional-logic % Chapter: syntax-and-semantics % Section: valuations-sat \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{pl}{syn}{val} \olsection{\usetoken{P}{valuation} and Satisfaction} \begin{defn}[!!^{valuation}s] Let $\{\True, \False\}$ be the set of the two truth values, ``true'' and ``false.'' A \emph{!!{valuation}} for $\Lang{L_0}$ is a function~$\pAssign{v}$ assigning either $\True$ or $\False$ to the !!{propositional variable}s of the language, i.e., $\pAssign{v} \colon \PVar \to \{\True, \False \}$. \end{defn} \begin{defn} Given !!a{valuation}~$\pAssign{v}$, define the evaluation function $\pValue{v} \colon \Frm[L_0] \to \{\True, \False \}$ inductively by: \begin{align*} \iftag{prvFalse}{\pValue{v}(\lfalse) & = \False; \\}{} \iftag{prvTrue}{\pValue{v}(\ltrue) & = \True; \\}{} \pValue{v}(\Obj p_n) & = \pAssign{v}(\Obj p_n); \\ \iftag{prvNot}{\pValue{v}(\lnot !A) & = \begin{cases} \True & \text{if } \pValue{v}(!A) = \False;\\ \False & \text{otherwise.} \end{cases} \\ }{} \iftag{prvAnd}{\pValue{v}(!A \land !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \True$ and $\pValue{v}(!B) = \True$;}\\ \False & \text{if $\pValue{v}(!A) = \False$ or $\pValue{v}(!B) = \False$}. \end{cases}\\}{} \iftag{prvOr}{\pValue{v}(!A \lor !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \True$ or $\pValue{v}(!B) = \True$;}\\ \False & \text{if $\pValue{v}(!A) = \False$ and $\pValue{v}(!B) = \False$}. \end{cases}\\}{} \iftag{prvIf}{\pValue{v}(!A \lif !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \False$ or $\pValue{v}(!B) = \True$;}\\ \False & \text{if $\pValue{v}(!A) = \True$ and $\pValue{v}(!B) = \False$}. \end{cases}\\}{} \iftag{prvIff}{\pValue{v}(!A \liff !B) & = \begin{cases} \True & \text{if $\pValue{v}(!A) = \pValue{v}(!B)$;}\\ \False & \text{if $\pValue{v}(!A) \neq \pValue{v}(!B)$}. \end{cases}}{} \end{align*} \end{defn} \begin{explain} The clauses correspond to the following truth tables: \begin{center} \iftag{prvNot}{ \begin{tabular}{|c||c|} \hline $!A$ & $ \lnot !A$ \\ \hline \hline $\True$ & $\False$ \\ $\False$ & $\True$ \\ \hline \end{tabular} }{} \iftag{prvAnd}{ \begin{tabular}{|cc||c|} \hline $!A$ & $!B$ & $!A \land !B$ \\ \hline \hline $\True$ & $\True$ & $\True$ \\ $\True$ & $\False$ & $\False$ \\ $\False$ & $\True$ & $\False$ \\ $\False$ & $\False$ & $\False$ \\ \hline \end{tabular} }{} \iftag{prvOr}{ \begin{tabular}{|cc||c|} \hline $!A$ & $!B$ & $!A \lor !B$ \\ \hline \hline $\True$ & $\True$ & $\True$ \\ $\True$ & $\False$ & $\True$ \\ $\False$ & $\True$ & $\True$ \\ $\False$ & $\False$ & $\False$ \\ \hline \end{tabular} }{}% \iftag{notprvNot,notprvAnd,notprvOr,notprvIf}{}{\\[1em]} \iftag{prvIf}{ \begin{tabular}{|cc||c|} \hline $!A$ & $!B$ & $!A \lif !B$ \\ \hline \hline $\True$ & $\True$ & $\True$ \\ $\True$ & $\False$ & $\False$ \\ $\False$ & $\True$ & $\True$ \\ $\False$ & $\False$ & $\True$ \\ \hline \end{tabular} }{} \iftag{prvIff}{ \begin{tabular}{|cc||c|} \hline $!A$ & $!B$ & $!A \liff !B$ \\ \hline \hline $\True$ & $\True$ & $\True$ \\ $\True$ & $\False$ & $\False$ \\ $\False$ & $\True$ & $\False$ \\ $\False$ & $\False$ & $\True$ \\ \hline \end{tabular} }{} \end{center} \end{explain} \begin{prob} Consider adding to $\Lang{L_0}$ a ternary connective $\diamondsuit$ with evaluation given by \begin{gather*} \pValue{v}(\diamondsuit( !A , !B , !C ) ) = \begin{cases} \pValue{v}( !B ) & \text{if $\pValue{v}(!A) = \True$;}\\ \pValue{v}( !C ) & \text{if $\pValue{v}(!A) = \False $}. \end{cases} \end{gather*} Write down the truth table for this connective. \end{prob} \begin{thm}[Local Determination] \ollabel{thm:LocalDetermination} Suppose that $\pAssign{v_1}$ and $\pAssign{v_2}$ are !!{valuation}s that agree on the !!{propositional variable}s occurring in $!A$, i.e., $\pAssign{v_1}(\Obj p_n) = \pAssign{v_2}(\Obj p_n)$ whenever $\Obj p_n$ occurs in some !!{formula}~$!A$. Then $\pValue{v_1}$ and $\pValue{v_2}$ also agree on~$!A$, i.e., $\pValue{v_1}(!A) = \pValue{v_2}(!A)$. \end{thm} \begin{proof} By induction on $!A$. \end{proof} \begin{defn}[Satisfaction] \ollabel{defn:satisfaction} We can inductively define the notion of \emph{satisfaction of !!a{formula}~$!A$ by !!a{valuation}~$\pAssign{v}$}, $\pSat{v}{!A}$, as follows. (We write $\pSat/{v}{!A}$ to mean ``not $\pSat{v}{!A}$.'') \begin{enumerate} \tagitem{prvFalse}{% \indcase{!A}{\lfalse}{$\pSat/{v}{\indfrm}$.}}{} \tagitem{prvTrue}{% \indcase{!A}{\ltrue}{$\pSat{v}{\indfrm}$.}}{} \item \indcase{!A}{\Obj p_i}{$\pSat{v}{\indfrm}$ iff $\pAssign{v}(\Obj p_i) = \True$.} \tagitem{prvNot}{% \indcase{!A}{\lnot !B}{$\pSat{v}{\indfrm}$ iff $\pSat/{v}{!B}$.}}{} \tagitem{prvAnd}{% \indcase{!A}{(!B \land !C)}{$\pSat{v}{\indfrm}$ iff $\pSat{v}{!B}$ and $\pSat{v}{!C}$.}}{} \tagitem{prvOr}{% \indcase{!A}{(!B \lor !C)}{$\pSat{v}{\indfrm}$ iff $\pSat{v}{!B}$ or $\pSat{v}{!C}$ (or both).}}{} \tagitem{prvIf}{% \indcase{!A}{(!B \lif !C)}{$\pSat{v}{\indfrm}$ iff $\pSat/{v}{!B}$ or $\pSat{v}{!C}$ (or both).}}{} \tagitem{prvIff}{% \indcase{!A}{(!B \liff !C)}{$\pSat{v}{\indfrm}$ iff either both $\pSat{v}{!B}$ and $\pSat{v}{!C}$, or neither $\pSat{v}{!B}$ nor $\pSat{v}{!C}$.}}{} \end{enumerate} If $\Gamma$ is a set of !!{formula}s, $\pSat{v}{\Gamma}$ iff $\pSat{v}{!A}$ for every~$!A \in \Gamma$. \end{defn} \begin{prop}\ollabel{prop:sat-value} $\pSat{v}{!A}$ iff $\pValue{v}(!A) = \True$. \end{prop} \begin{proof} By induction on~$!A$. \end{proof} \begin{prob} Prove \olref[pl][syn][val]{prop:sat-value} \end{prob} \end{document}

Ссылаются нормы: PROP_SATISFACTION, VALUATION