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?


\[\emptyset \vdash \phi\]

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$?


\[\vdash \phi\]

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:

Suppose $\Gamma$ is a set of formulas and $\psi$, $\phi$ are formulas (not necessarily in $\Gamma$). Then:

\[\Gamma \cup \\{\psi\\} \models \phi \text{ iff } \Gamma \models (\psi \to \phi)\]

$\{\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:

  1. Axiom: $\alpha _ m$
  2. A1: $(\alpha _ m \to (\phi \to \alpha _ m))$
  3. 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.

  1. Hypothesis: $\alpha _ m$
  2. A1: $(\alpha _ m \to (\phi \to \alpha _ m))$
  3. 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?


\[\Gamma \models \phi \text{ iff } \Gamma \vdash \phi\]

@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.


  1. $\Gamma$ is consistent (you can’t prove a statement and it’s negation)
  2. 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:

  1. $\Gamma \vdash \lnot \psi$ iff $\Gamma \not\vdash \psi$
  2. $\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)$.


\[\Gamma \text{ is complete} \implies \Gamma \text{ is satisfiable}\]

@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.


\[\Gamma \text{ consistent} \iff \Gamma\text{ satisfiable}\]

@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$.



Related posts