Math 557 Sep 10

Logical Implication and Proof

Key Concepts

  • Logical consequence:

    • This is the semantical implication we are often working with in mathematical practice. We say \(T\) logically implies \(\varphi\), \(T \models \varphi\), if for structure \(\mathcal{M}\), \(\mathcal{M} \models T\) implies \(\mathcal{M} \models \varphi\).

  • Formal proof:

    • \(T \vdash \varphi\) means there is a formal (i.e. syntactical) derivation of \(\varphi\) from \(T\) using the formulas of \(T\), the three kinds of logical axioms (propositional tautologies, equality and quantifier axioms), and the inference rules Modus Ponens and Generalization.

Problems

Exercise 1 (Warmup - Logical Implication)
Let \(T\) be an \(\mathcal{L}\)-theory. We say a theory \(T'\) is an axiomatization of \(T\) if for any \(\mathcal{L}\)-structure \(\mathcal{M}\),

\[\mathcal{M} \models T \; \iff \; \mathcal{M} \models T'\]

Show that for any axiomatization \(T'\) of \(T\), for any \(\mathcal{L}\)-sentence \(\sigma\),

\[T \models \sigma \; \iff \; T' \models \sigma\]

Exercise 2 (Warmup 2)
Recall that a model of a theory \(T\) is a structure \(\mathcal{M}\) such that for any sentence \(\sigma \in T\), \(\mathcal{M} \models \sigma\). In this case we write \(\mathcal{M} \models T\).

Argue that if \(T\) does not have a model, every sentence is a logical implication of \(T\).

Exercise 3 (Formal notion of proof – Warmup)
Verify that

\[\{\varphi, \neg \psi\} \vdash \neg(\varphi \to \psi)\]

Exercise 4
Argue (semantically) that if \(x\) is not free in \(\psi\),

\[\{\varphi \to \psi\} \models \exists x \varphi \: \to \: \psi\]

Then prove this syntactically, i.e. show (under the same assumption) that

\[\{\varphi \to \psi\} \vdash \exists x \varphi \: \to \: \psi\]

Exercise 5
Prove the Soundness Theorem, i.e. show that

\[T \vdash \varphi \; \Rightarrow \; T \models \varphi\]

Take-home problem


Show that

\[\begin{aligned} \{\varphi \to \psi \} & \vdash \exists x \varphi \: \to \: \exists x \psi \\ \{\varphi \to \psi \} & \vdash \forall x \varphi \: \to \: \forall x \psi \\ \end{aligned}\]