Notes - Logic MT24, Proofs in propositional logic
Flashcards
@Define the proof system $L _ 0$.
Here $\mathcal L _ 0 := \mathcal L _ \text{prop}(\lnot, \to)$.
Axioms: Any formula of the following form, where $\alpha, \beta, \gamma \in \text{Form}(\mathcal L _ 0)$:
- A1: $(\alpha \to (\beta \to \alpha))$ (“if A, then anything implies A”)
- A2: $((\alpha \to (\beta \to \gamma)) \to ((\alpha \to \beta) \to (\alpha \to \gamma)))$ (“if A shows that B implies C, then if A implies B, A also implies C”)
- A3: $((\lnot \alpha \to \beta) \to ((\lnot \alpha \to \lnot \beta) \to \alpha)))$ (“contradiction”)
Rules of inference:
- Modus ponens (MP): For any $\phi, \psi \in \text{Form}(\mathcal L _ 0)$, from $\phi$ and $(\phi \to \psi)$ infer $\psi$.
Suppose:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0$)
- $\phi \in \text{Form}(\mathcal L _ 0)$
@Define what it means for $\phi$ to be provable from hypotheses $\Gamma$, written
\[\Gamma \vdash \phi\]
There is a sequence of $\mathcal L _ 0$ formulaus $\phi _ 1, \ldots, \phi _ n$ with $\phi _ n = \phi$ such that for each $i \le n$, at least one of the following holds:
- (A1-A3): $\phi _ i$ is an axiom
- (Hyp): $\phi _ i \in \Gamma$
- (MP): $\phi _ k = (\phi _ j \to \phi _ i)$ for some $j, k < i$
Suppose $\phi \in \mathcal L _ 0$. What does the notation
\[\vdash \phi\]
mean?
so $\phi$ is a theorem of $L _ 0$, i.e. $\phi$ is provable from no hypotheses.
What does it mean for some $\phi \in \mathcal L _ 0$ to be a theorem of $L _ 0$?
What is the difference between $\mathcal L _ 0$ and $L _ 0$?
- $\mathcal L _ 0$ is $\text{Form}(\mathcal L [\lnot, \to])$
- $L _ 0$ is $\mathcal L _ 0$ with a proof system
@State the soundness theorem for $L _ 0$.
$L _ 0$ is sound, i.e. suppose:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
- $\phi \in \text{Form}(\mathcal L _ 0)$
- $\Gamma \vdash \phi$
Then:
- $\Gamma \models \phi$.
@Prove the soundness theorem for $L _ 0$, i.e. that if
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
- $\phi \in \text{Form}(\mathcal L _ 0)$
- $\Gamma \vdash \phi$
then:
- $\Gamma \models \phi$.
We prove the following for all $m$:
If $\phi$ has a proof of length $m$ from $\Gamma$ in $L _ 0$, then $\Gamma \models \phi$. $(\star)$
Induct on $m$. In the base case, $m = 0$. This is immediate as no proof has length $0$.
In the inductive step, we can assume $m \ge 1$ and ($\star$) holds for all $m’ < m$. Suppose $\alpha _ 1, \ldots, \alpha _ m$ is a proof in $L _ 0$. We want to show that $\Gamma \models \alpha _ m$. There are several cases:
Case 1: $\alpha _ m$ is an axiom. By truth tables, the axioms are logically valid, so $\Gamma \models \alpha _ m$.
Case 2: $\alpha _ m \in \Gamma$. Then $\Gamma \models \alpha _ m$ is immediate.
Case 3: $\alpha _ m$ is obtained by MP. Hence $\exists i, j < m$ and $\alpha _ j = (\alpha _ i \to \alpha _ m)$. By the inductive hypothesis, since $\alpha _ i, \ldots, \alpha _ i$ is a proof of length $i < m$, we have $\Gamma \models \alpha _ i$. Similarly, $\Gamma \models \alpha _ j$, i.e. $\Gamma \models (\alpha _ i \to \alpha _ m)$.
Then by the lemma which says:
\[\Gamma \cup \\{\psi\\} \models \phi \text{ iff } \Gamma \models (\psi \to \phi)\]Suppose $\Gamma$ is a set of formulas and $\psi$, $\phi$ are formulas (not necessarily in $\Gamma$). Then:
$\{\alpha _ i, (\alpha _ i \to \alpha _ m)\} \models \alpha _ m$. But then by the transitivity of “$\models$”, $\Gamma \models \alpha _ m$, as required.
The soundness theorem for $L _ 0$ states that if:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
- $\phi \in \text{Form}(\mathcal L _ 0)$
- $\Gamma \vdash \phi$
Then:
- $\Gamma \models \phi$.
In particular, can you translate this statement into one about the validity of a certain class of formulas?
Any theorem of $L _ 0$ is logically valid.
@State the deduction theorem for $L _ 0$.
Suppose:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
- $\phi, \psi \in \text{Form}(\mathcal L _ 0)$
Then:
- If $\Gamma \cup \{\phi \} \vdash \psi$, then $\Gamma \vdash (\phi \to \psi)$
…or, equivalently the result could be stated as…
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
- $\phi, \psi \in \text{Form}(\mathcal L _ 0)$
- $\Gamma \cup \{\phi \} \vdash \psi$
Then:
- $\Gamma \vdash (\phi \to \psi)$
@Prove the deduction theorem for $L _ 0$, i.e. that if
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
- $\phi, \psi \in \text{Form}(\mathcal L _ 0)$
then:
- If $\Gamma \cup \{\phi \} \vdash \psi$, then $\Gamma \vdash (\phi \to \psi)$
We prove the family of statements
If $\psi$ has a proof of length $m$ from $\Gamma \cup \{\phi\}$ in $L _ 0$, then $\Gamma \vdash (\phi \to \psi)$. $(\star)$
Induct on $m$. Suppose that $\alpha _ 1, \ldots, \alpha _ m$ is a proof in $L _ 0$ from $\Gamma \cup \{\phi\}$. We want to show that $\Gamma \vdash (\phi \to \alpha _ m)$, assuming inductively that $\Gamma \vdash (\phi \to \alpha _ i)$ for all $i < m$. There are several cases:
Case 1: $\alpha _ m$ is an axiom. Then $\vdash (\phi \to \alpha _ m)$ by the following proof:
- Axiom: $\alpha _ m$
- A1: $(\alpha _ m \to (\phi \to \alpha _ m))$
- MP1, 2: $(\phi \to \alpha _ m)$
But as $\{\} \subseteq \Gamma$, $\Gamma \vdash (\phi \to \alpha _ m)$.
Case 2: $\alpha _ m \in \Gamma \cup \{\phi\}$. Then the proof in case 1 goes through almost exactly the same, except line 1 is an axiom rather than a hypothesis.
- Hypothesis: $\alpha _ m$
- A1: $(\alpha _ m \to (\phi \to \alpha _ m))$
- MP1, 2: $(\phi \to \alpha _ m)$
Case 3: $\alpha _ m$ is obtained by MP for earlier $\alpha _ j, \alpha _ k$. So there are $j, k < m$ such that $\alpha _ j = (\alpha _ k \to \alpha _ m)$. By the inductive hypothesis:
- $\Gamma \vdash (\phi \to \alpha _ k)$
- $\Gamma \vdash (\phi \to \alpha _ j)$, i.e. $\Gamma \vdash (\phi \to (\alpha _ k \to \alpha _ m))$.
We can glue these two proofs together to form a proof for $\Gamma \vdash \alpha _ m$:
Suppose:
\[\beta_1, \ldots, \beta_{r-1}, (\phi \to \alpha_k)\]is a length-$r$ proof of $\Gamma \vdash (\phi \to \alpha _ k)$ from $\Gamma$ and
\[\gamma_1, \ldots, \gamma_{s-1}, (\phi \to (\alpha_k \to \alpha_m))\]is a length-$s$ proof of $\Gamma \vdash (\phi \to (\alpha _ k \to \alpha _ m))$ from $\Gamma$. But then:
\[\beta_1, \ldots, \beta_{r-1}, (\phi \to \alpha_k), \gamma_1, \ldots, \gamma_{s-1}, (\phi \to (\alpha_k \to \alpha_m))\]followed by
\[\begin{aligned} &((\phi \to (\alpha_k \to \alpha_m)) \to ((\phi \to \alpha_k) \to (\phi \to \alpha_m))), \\ &((\phi \to \alpha_k) \to (\phi \to \alpha_m)), \\ &(\phi \to \alpha_m) \end{aligned}\]is a proof of $(\phi \to \alpha _ m)$ in $L _ 0$ from $\Gamma$.
@Prove (very quickly) the converse of the deduction theorem for $L _ 0$, i.e. that if
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
- $\phi, \psi \in \text{Form}(\mathcal L _ 0)$
then:
- If $\Gamma \vdash (\phi \to \psi)$, then $\Gamma \cup \{\phi \} \vdash \psi$
Let $\beta _ 1, \ldots, \beta _ {r-1}, (\phi \to \psi)$ be the proof of $(\phi \to \psi)$ from $\Gamma$. Then
\[\beta_1, \ldots, \beta_{r-1}, (\phi \to \psi), \phi, \psi\]Gives $\Gamma \cup \phi \vdash \psi$, where MP is used in the last step.
@State the completeness theorem for $L _ 0$.
Suppose:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
- $\phi \in \text{Form}(\mathcal L _ 0)$
- $\Gamma \models \phi$
Then:
- $\Gamma \vdash \phi$
What equivalence does the combination of completeness and soundness give you?
@Define what it means for $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ to be inconsistent.
There exists $\chi \in \text{Form}(\mathcal L _ 0)$ such that
\[\Gamma \vdash \chi \text{ and } \Gamma \vdash \lnot \chi\]@Justify why $\emptyset \subseteq \mathcal L _ 0$ is consistent.
- $\mathcal L _ 0$ is sound, so anything proved from $\emptyset$ must be a logical validity
- If $\mathcal L _ 0$ were inconsistent, it could prove $\chi$ and $\lnot \chi$ for some $\chi$
- But both of these would have to be logical validities, however no formula and it’s negation can be both logically valid
- Therefore $\emptyset$ is consistent
@Prove that $\Gamma \vdash \phi$ iff $\Gamma \cup \{\lnot \phi\}$ is inconsistent.
$\Gamma \vdash \phi$ implies $\Gamma \cup \{\lnot \phi\}$:
Suppose $\Gamma \cup \{\lnot \phi\}$ is inconsistent, so that
\[\Gamma \cup \\{\lnot \phi\\} \vdash \chi \text{ and } \Gamma \cup \\{\lnot \phi\\} \vdash \lnot \chi\]for some $\chi$. But then by the deduction theorem,
\[\Gamma \vdash (\lnot \phi \to \chi) \text{ and } \Gamma \vdash (\lnot \phi \to \lnot \chi)\]so
\[((\lnot \phi \to \chi) \to ((\lnot \phi \to \lnot \chi) \to \phi))\]is an instance of the axiom A3. By modus ponents twice, we can conclude $\Gamma \vdash \phi$.
$\Gamma \cup \{\lnot \phi\}$ implies $\Gamma \vdash \phi$:
Suppose $\Gamma \vdash \phi$. Then $\Gamma \cup \{\lnot \phi\}$ is inconsistent, since $\Gamma \cup \{\lnot \phi\} \vdash \phi$ and $\Gamma \cup \{\lnot \phi\} \vdash \lnot \phi$.
@State a lemma that characterises provability in terms of inconsistency for $L _ 0$.
$\Gamma \vdash \phi$ iff $\Gamma \cup \{\lnot \phi\}$ is inconsistent.
@State a lemma that characterises entailment in terms of satisfiability.
$\Gamma \models \phi$ iff $\Gamma \cup \{\lnot \phi\}$ is unsatisfiable.
@Define what it means for $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ to be complete/maximally consistent.
- $\Gamma$ is consistent (you can’t prove a statement and it’s negation)
- For every $\phi \in \text{Form}(\mathcal L _ 0)$, either $\Gamma \vdash \phi$ or $\Gamma \vdash \lnot \phi$.
@State a lemma which lets you “expand” a consistent set $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$.
Suppose:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ is consistent
- $\phi \in \text{Form}(\mathcal L _ 0)$
Then either:
- $\Gamma \cup \{\phi\}$ is consistent, or
- $\Gamma \cup \{\lnot \phi\}$ is consistent.
@Prove that if:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ is consistent
- $\phi \in \text{Form}(\mathcal L _ 0)$
then either:
- $\Gamma \cup \{\phi\}$ is consistent, or
- $\Gamma \cup \{\lnot \phi\}$ is consistent.
Suppose $\Gamma \not\vdash \phi$, then $\Gamma \cup \{\lnot \phi\}$ is consistent by the lemma that says
$\Gamma \vdash \phi$ iff $\Gamma \cup \{\lnot \phi\}$ is inconsistent.
Otherwise, $\Gamma \vdash \phi$. Suppose for a contradiction that $\Gamma \cup \{\phi\}$ is not consistent, then
- $\Gamma \cup \{\phi\} \vdash \chi$ implies $\Gamma \vdash (\phi \to \chi)$ by the deduction theorem.
- $\Gamma \cup \{\phi\} \vdash \lnot\chi$ implies $\Gamma \vdash (\phi \to \lnot\chi)$ by the deduction theorem.
But then $\Gamma \vdash \phi$ implies by modus ponens that both $\Gamma \vdash \chi$ and $\Gamma \vdash \lnot \chi$, a contradiction since $\Gamma$ is assumed to be consistent.
@State a theorem about extending a consistent set of formulas $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ to a complete set $\Gamma’$.
Suppose:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ is consistent
Then:
- There exists a complete $\Gamma’ \supseteq \Gamma$
@Prove that if
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ is consistent
then:
- there exists a complete $\Gamma’ \supseteq \Gamma$.
Note that $\text{Form}(\mathcal L _ 0) = \{\phi _ 0, \phi _ 1, \ldots\}$ is countable. Construct a chain of consistent sets like so:
\[\Gamma = \Gamma_0 \subseteq \Gamma_1 \subseteq \cdots\]where:
$\Gamma _ 0 := \Gamma$ and given a consistent $\Gamma _ n$, let
\[\Gamma_{n+1} := \begin{cases} \Gamma_n \cup \\{\phi_n\\} &\text{ if } \Gamma_n \cup \\{\phi_n\\} \text{ is consistent} \\\\ \Gamma_n \cup \\{\lnot \phi_n \\} &\text{otherwise} \end{cases}\]Then consider
\[\Gamma' := \bigcup^\infty_{n = 0} \Gamma_n\]Then $\Gamma’$ is consistent: if $\Gamma’ \vdash \chi$ and $\Gamma’ \vdash \lnot \chi$, then proofs witnessing this use only finitely many formulas from $\Gamma’$, so for some $n$,
\[\Gamma_n \vdash \chi\]and
\[\Gamma_n \vdash \lnot \chi\]which contradicts the consistency of $\Gamma _ n$. And by construction $\Gamma’$ is complete.
@State and @prove a lemma which gives two results about the kinds of statements you can prove when $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ is complete.
Suppose:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ is complete
Then:
- $\Gamma \vdash \lnot \psi$ iff $\Gamma \not\vdash \psi$
- $\Gamma \vdash (\psi \to \chi)$ iff either:
- $\Gamma \not\vdash \psi$, or
- $\Gamma \vdash \chi$
For (1), consistency of $\Gamma$ handles the forward direction and completeness handles the backwards direction.
For (2):
- Forward direction: Suppose $\Gamma \vdash (\psi \to \chi)$ but that $\Gamma \vdash \psi$ and $\Gamma \not\vdash \chi$. But by MP, $\Gamma \vdash \chi$ contradicts consistency.
- Backwards direction: Suppose $\Gamma \not\vdash \psi$. Then $\Gamma \vdash \lnot\psi$ by (a). But then $\Gamma \vdash (\psi \to \chi)$ by the deduction theorem. If $\Gamma \vdash \chi$, then $\Gamma \vdash (\psi \to \chi)$ by A1 and MP.
@State a theorem which connects completeness and satisfiability of a set of formulas $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$.
@Prove that if:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
- $\Gamma$ is complete
then:
- $\Gamma$ is satisfiable
Define a valuation $v$ by:
\[v(p_i) = T \text{ iff } \Gamma \vdash p_i\]We prove by induction of the length of any formula $\phi \in \text{Form}(\mathcal L _ 0)$:
\[v(\phi) = T \text{ iff } \Gamma \vdash \phi\]There are several cases:
Case 1: $\phi = p _ i$ for some $i$. Then we are done by the definition of $v$.
Case 2: $\phi = \lnot \psi$. Then:
\[\begin{aligned} \tilde v(\phi) = T &\text{ iff } \tilde v(\psi) = F &&(\text{tt}\lnot) \\\\ &\text{ iff } \Gamma \not\vdash \psi &&(\text{by inductive hypothesis}) \\\\ &\text{ iff } \Gamma \vdash \lnot \psi &&(\text{by completeness}) \\\\ &\text{ iff } \Gamma \vdash \phi \end{aligned}\]Case 3: $\phi = (\psi \to \chi)$. Then:
\[\begin{aligned} \tilde v(\phi) = T &\text{ iff } \tilde v(\psi) = F \text{ or } \tilde v(\chi) = T &&(\text{tt}\lnot) \\\\ &\text{ iff } \Gamma \not\vdash \psi \text{ or } \Gamma \vdash \chi &&(\text{by inductive hypothesis}) \\\\ &\text{ iff } \Gamma \vdash (\psi \to \chi) &&(\text{by completeness}) \\\\ &\text{ iff } \Gamma \vdash \phi \end{aligned}\]as required.
@State a theorem which connects the consistency of a set of formulas $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ to its satisfiability.
@Prove that if:
- $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
then:
\[\Gamma \text{ consistent} \iff \Gamma\text{ satisfiable}\]
- Forward direction: If $\Gamma$ is consistent, it extends to a complete set, which is satisfiable, and hence $\Gamma$ is also satisfiable
- Backward direction: If $\Gamma$ is inconsistent, then $\Gamma \vdash \chi$ and $\Gamma \vdash \lnot \chi$, then $\Gamma \models \chi$ and $\Gamma \models \lnot \chi$ by soundness. But no valuation can satisfy both $\chi$ and $\lnot \chi$.