problem set 3 (axioms and models)
Axioms for propositional logic
Consider the axiom system that results from our official system when \(\textsf{A3}\) is replaced with the axiom:
\[ (\neg p \to \neg q) \to (q \to p) \tag{$\textsf{A3}^\ast$} \]
We write \(\Gamma \vdash^\ast \varphi\) to indicate that \(\varphi\) is derivable from \(\Gamma\) in the new system. Now, for all \(\Gamma\) and \(\varphi\):
\[ \Gamma \vdash \varphi \ \Leftrightarrow \ \Gamma \vdash^\ast \varphi. \]
Justify the claims below:
For all \(\Gamma\) and \(\varphi\):
\[ \Gamma \vdash \varphi \ \Rightarrow \ \Gamma \vdash^\ast \varphi. \]
Given \(\textsf{Proposition 4.3}\), all substition instances of \(\textsf{A3}^\ast\) are theorems of our official system. So, if \((\chi_1, \dots, \chi_n)\) is a proof of \(\varphi\) from \(\Gamma\) in the new system, then we obtain a proof in our system when we replace each occurrence of an instance of \(\textsf{A3}^\ast\) in the proof with a proof of the formula in the official system.
The Deduction Theorem for \(\vdash^\ast\):
For all \(\Gamma\), \(\varphi\), and \(\psi\):
\[ \Gamma, \varphi \vdash^\ast \psi \ \Leftrightarrow \ \Gamma \vdash^\ast \varphi \to \psi. \]
The proof of the Deduction Theorem for \(\vdash\) made use only of the fact that all substitution instances of \(\textsf{A1}\) and \(\textsf{A2}\) are axioms of the system. Since they are all axioms of the new system as well, the proof can be recast as a proof of the Deduction Theorem for \(\vdash^\ast\).
For all \(\varphi\), \(\vdash^\ast \varphi \to (\neg \varphi \to \bot)\).
From \(\textsf{A1}[\neg \varphi/p, \neg \bot/q]\), we obtain: \[ \vdash^\ast \neg \varphi \to (\neg \bot \to \neg \varphi). \] \[ \{\neg \varphi\} \vdash^\ast \neg \bot \to \neg \varphi \] Given \(\textsf{A3}^\ast[\bot/p, \varphi/q]\), we infer: \[ \{\neg \varphi\} \vdash^\ast \varphi \to \bot \] \[ \{\varphi, \neg \varphi\} \vdash^\ast \bot. \] By the Deduction Theorem for \(\vdash^\ast\): \[ \{\varphi \} \vdash^\ast \neg \varphi \to \bot \] \[ \vdash^\ast \varphi \to (\neg \varphi \to \bot) \]
For all \(\varphi\), \(\vdash^\ast (\neg \varphi \to \varphi) \to \varphi\).
\[ \{\neg \varphi \to \varphi, \neg \varphi\} \vdash^\ast \varphi \] \[ \{\neg \varphi \to \varphi, \neg \varphi\} \vdash^\ast \neg \varphi \] On the other hand: \[ \vdash^\ast \varphi \to (\neg \varphi \to \bot) \] Therefore: \[ \{ \neg \varphi \to \varphi, \neg \varphi\} \vdash^\ast \bot \] \[ \{ \neg \varphi \to \varphi, \neg \varphi\} \vdash^\ast \neg \top \] \[ \{\neg \varphi \to \varphi \} \vdash^\ast \neg \varphi \to \neg \top. \] Given \(\textsf{A3}^\ast[\varphi/p, \top/q]\), we infer: \[ \{\neg \varphi \to \varphi \} \vdash^\ast \top \ \to \varphi. \] Since \(\vdash^\ast \top\): \[ \neg \varphi \to \varphi \vdash^\ast \varphi \] \[ \vdash^\ast (\neg \varphi \to \varphi) \to \varphi \]
For all \(\Gamma\) and \(\varphi\):
\[ \Gamma \vdash \varphi \ \Rightarrow \ \Gamma \vdash^\ast \varphi. \] It will suffice to observe that all instances of \(\textsf{A3}\) are theorems of the new system. For we should then be able to turn a proof in the official system into a proof in the new system. Given the Deduction Theorem, it suffices to note:
\[ \{\neg \varphi \to \neg \psi, \neg \varphi \to \psi \} \vdash^\ast \psi \to \varphi \]
\[ \{\neg \varphi \to \neg \psi, \neg \varphi \to \psi\} \vdash^\ast \neg \varphi \to \varphi \]
\[ \{\neg \varphi \to \neg \psi, \neg \varphi \to \psi\} \vdash^\ast \varphi \]
\[ \{\neg \varphi \to \neg \psi\} \vdash^\ast (\neg \varphi \to \psi) \to \varphi \]
\[ \vdash^\ast (\neg \varphi \to \neg \psi) \to ((\neg \varphi \to \psi) \to \psi) \]
Possible worlds models
Provide possible worlds models in order to justify that not every substitution instance of the relevant formula is true in every world of the relevant class of models.
\(\Diamond p \to \Box p\) / euclidean
\(\Box (\Box p \to p)\) / symmetric
\(\Diamond (p \to q) \to (\Diamond p \to \Diamond q)\) / reflexive
\(\Box \Box p \to \Box p\) / transitive
\(\Diamond p \to \Box \Diamond p\) / reflexive and transitive