Exercise 6
\[% Shared mathematical notation for CSC438. % % Keep this file limited to commands supported by both LaTeX and MathJax. % Quarto loads it through filters/shared-macros.lua; TeX preambles can use % \input{../macros} when compiled from a first-level project directory. \renewcommand{\subset}{\subseteq} \renewcommand{\iff}{\leftrightarrow} \newcommand{\N}{\mathbb{N}} \newcommand{\proves}{\vdash} \newcommand{\cA}{\mathcal{A}} \newcommand{\cF}{\mathcal{F}} \newcommand{\cL}{\mathcal{L}} \newcommand{\cP}{\mathcal{P}} \newcommand{\cM}{\mathcal{M}} \newcommand{\Var}{\mathrm{Var}} \newcommand{\FV}{\mathrm{FV}} \newcommand{\Z}{\mathbb{Z}} \newcommand{\TR}{\mathbf{TR}} \newcommand{\D}{\mathbf{D}} \newcommand{\R}{\mathbb{R}} \newcommand{\seq}{\Rightarrow} \newcommand{\RA}{\Longrightarrow} \newcommand{\LRA}{\Longleftrightarrow} \newcommand{\OI}{\{0,1\}} \renewcommand{\SS}{\Sigma^*} \newcommand{\powerset}{\mathcal{P}} \newcommand{\blank}{\sqcup} \newcommand{\angles}[1]{\left\langle #1\right\rangle} \newcommand{\enc}[1]{\left\ulcorner #1\right\urcorner} \newcommand{\Lang}{\mathcal{L}} \newcommand{\Th}{\operatorname{Th}} \newcommand{\Thm}{\operatorname{Thm}} \newcommand{\Prov}{\operatorname{Prov}} \newcommand{\Con}{\operatorname{Con}} \newcommand{\ATM}{A_{\mathrm{TM}}} \newcommand{\HALTTM}{\operatorname{HALT}_{\mathrm{TM}}} \newcommand{\HALTe}{\operatorname{HALT}_{\epsilon}} \newcommand{\AExp}{A_E} \newcommand{\AMult}{A_M} \newcommand{\green}[1]{\textcolor{green}{#1}} \newcommand{\red}[1]{\textcolor{red}{#1}} \newcommand{\st}[1]{\sout{#1}} \]
1 Tautologically implies and unsatsifiability for sequents
1.1
Let \(S\) be a set of formulas, and \(A\) be a formula.
We have the following lemma. \(S \models A\) if and only if \(S \cup \{\neg A\}\) is unsatisfiable.
Let \(\varphi = A_1,...,A_k \seq B_1,...,B_\ell\) be a sequent. State a similar lemma and prove it.
Solution
We have
\[ S \models \varphi \quad\text{if and only if}\quad S \cup \{A_1,\ldots,A_k,\neg B_1,\ldots,\neg B_\ell\} \text{ is unsatisfiable}. \]
Proof. An assignment \(v\) falsifies the sequent \(\varphi\) exactly when it makes every \(A_i\) true and every \(B_j\) false. Thus, an assignment satisfies
\[ S \cup \{A_1,\ldots,A_k,\neg B_1,\ldots,\neg B_\ell\} \]
exactly when it satisfies every formula in \(S\) and falsifies \(\varphi\). Consequently, this set is unsatisfiable exactly when every assignment satisfying \(S\) satisfies \(\varphi\), which is the definition of \(S\models\varphi\).
This also covers empty antecedents or succedents: the corresponding condition on the \(A_i\) or \(B_j\) is vacuous.
1.2
Prove the statement on slide 77:
If \(S \models \varphi\), then there is some finite subset \(S_0 \subseteq S\) such that \(S_0 \models \varphi\).
Solution
Write \(\varphi=A_1,\ldots,A_k\seq B_1,\ldots,B_\ell\) and put
\[ F=\{A_1,\ldots,A_k,\neg B_1,\ldots,\neg B_\ell\}. \]
By the preceding lemma, \(S\cup F\) is unsatisfiable. By the contrapositive of the Compactness Theorem, it has a finite unsatisfiable subset \(T\subseteq S\cup F\).
Let \(S_0=T\cap S\). Then \(S_0\) is a finite subset of \(S\), and \(T\subseteq S_0\cup F\). Since any assignment satisfying \(S_0\cup F\) would also satisfy \(T\), the set \(S_0\cup F\) is unsatisfiable. Applying the preceding lemma again gives \(S_0\models\varphi\), as required.
2 Inversion
One of the lemmas for the proof of completeness was inversion. We verified inversion for one of the rules in class. Make sure you’re convinced that inversion holds for the remainder of the logical rules.
3 The Craig Interpolation Lemma
3.1
Let \(A, B\) be propositional formulas. Let \(\Pi\) be the set of atoms that occur in both \(A\) and \(B\). Suppose \(\Pi\) is non-empty.
Show that if \(A \models B\). Then there exists \(C\) such that
- \(A \models C\),
- \(C \models B\), and
- \(C\) contains only atoms from \(\Pi\).
Solution
Let \(X\) and \(Y\) be the finite sets of atoms occurring in \(A\) and \(B\), respectively, so \(\Pi=X\cap Y\). Let \(T\) consist of the assignments \(s:\Pi\to\OI\) that extend to a satisfying assignment of \(A\) on \(X\).
For each \(s\in T\), let \(M_s\) be the conjunction containing \(P\) when \(s(P)=1\) and \(\neg P\) when \(s(P)=0\), for every \(P\in\Pi\). If \(T\neq\varnothing\), put
\[ C=\bigvee_{s\in T}M_s. \]
If \(T=\varnothing\), choose \(P\in\Pi\) and put \(C=P\land\neg P\). In either case, \(C\) uses only atoms from \(\Pi\) and is true exactly on the common-atom assignments that extend to models of \(A\).
Every model of \(A\) restricts to an element of \(T\), so \(A\models C\).
To prove \(C\models B\), let \(v\models C\). Its restriction to \(\Pi\) extends to an assignment \(u\) on \(X\) satisfying \(A\). Since \(u\) and \(v\) agree on \(X\cap Y\), combine \(u\) on \(X\) with \(v\) on \(Y\) into one assignment \(w\) (and assign arbitrary values elsewhere). Then \(w\models A\), so \(w\models B\) by hypothesis. But \(w\) agrees with \(v\) on every atom of \(B\), giving \(v\models B\). If \(T\) is empty, \(C\models B\) holds vacuously (since \(P \land \neg P\) is unsatisfiable)
3.2
Add to the set of propositional formulas, \(\top\), and \(\bot\). The semantics of \(\top\) and \(\bot\) are as follows: \(v(\top) = 1\), and \(v(\bot) = 0\). That is \(\top\) is always True and \(\bot\) is always false. The lemma above is still true when \(\Pi\) is empty (now \(C\) can be either \(\bot\) or \(\top\), before there were no possible propositional formulas in this case). What does the lemma mean in this case?
Solution
When the common-atom set \(\Pi\) is empty, the conclusion is:
If \(A\) and \(B\) share no atoms and \(A\models B\), then either \(A\) is unsatisfiable or \(B\) is a tautology.
An atom-free formula built from \(\top\), \(\bot\), and connectives has a constant truth value, so an interpolant \(C\) is equivalent to either \(\bot\) or \(\top\). If \(C\equiv\bot\), then \(A\models C\) says that \(A\) is unsatisfiable. If \(C\equiv\top\), then \(C\models B\) says that \(B\) is a tautology.
To see directly why one of these must hold, suppose instead that some assignment satisfies \(A\) and some assignment falsifies \(B\). Since their atom sets are disjoint, combine these assignments to obtain one that satisfies \(A\) and falsifies \(B\), contradicting \(A\models B\).
Conversely, choose \(C=\bot\) when \(A\) is unsatisfiable, and \(C=\top\) when \(B\) is a tautology. Each choice satisfies the required entailments.
4 Finitely Satisfiable (Enderton 1.7.1)
A set \(S\) Is finitely satisfiable if every finite subset of \(S\) is satisfiable
Let \(S\) be a set of formulas, and \(A\) be a formula. Suppose \(S\) is finitely satisfiable. Show that at least one of \(S \cup \{A\}\), and \(S \cup \{\neg A\}\) is finitely satisfiable.
Solution
Suppose, for a contradiction, that neither enlarged set is finitely satisfiable. Then there are finite subsets \(F,G\subseteq S\) such that
\[ F\cup\{A\}\quad\text{and}\quad G\cup\{\neg A\} \]
are unsatisfiable. The set \(F\cup G\) is a finite subset of \(S\), so it has a satisfying assignment \(v\). If \(v(A)=1\), then \(v\) satisfies \(F\cup\{A\}\), a contradiction. If \(v(A)=0\), then \(v\) satisfies \(G\cup\{\neg A\}\), also a contradiction.
5 PK Extension
Suppose we added \(\to\) as a primitive connective (as opposed to just shorthand). Write the corresponding left and right introduction rules for \(\to\), and make sure they satisfy local soundness, and inversion.
6 Read up on the resolution proof system
This will be the tutorial for this week.
See the section on DNF and CNFS and the resolution proof system here
Note. The rest of that document uses some different notation than what we used in class.