I was going through these notes and wanted to prove the following:
if $\Sigma \vdash \varphi_i, i \in [n] \iff \Sigma \vdash \varphi_1 \land \dots \land \varphi_n$ (without completeness of predicate logic)
I assume that to do that we'd need only the axioms provided in the notes for predicate logic and inference rules:
- propositional axioms
- equality axioms
- quantifier axioms
- inference rules (modus ponens (MP) or generalized rule (G))
obviously we are not allowed to just appeal to the definition on page 33 that defines truth in an L-structure $\mathcal A = (A;(R^{\mathcal A})_{R \in L^r},(F^{\mathcal A})_{F \in L^f} )$ and then use the completeness theorem (since the notes say to not do that). Therefore, it must be that only using 1-4 (axioms + inference rules) is the way to prove it.
However, the only thing that seems to involve logical ANDs are the propositional axioms:
- T
- $\varphi \to (\varphi \lor \psi); \varphi \to (\psi \lor \varphi)$
- $\neg \varphi \to (\neg \psi \to \neg (\varphi \lor \psi) $
- $(\varphi \land \psi) \to \varphi; (\psi \land \varphi) \to \psi$
- $\varphi \to (\psi \to (\varphi \land \psi))$
- $(\varphi \to (\psi \to \theta)) \to ((\varphi \to \psi)\to (\varphi \to \theta))$
- $\varphi \to (\neg \varphi \to \bot)$
- $(\neg \varphi \to \bot) \to \varphi$
however, because the propositional rules are rule full of implications, it seems that we have a lot of things of the form $a \lor b$. Since we we are only talking about provability, then it must mean that we cannot simply cancel things out using normal logic rules that involve truth because provability is just a symbol game at this point of the course. Therefore, it wasn't clear where to even start to prove this.
How does one even start? The statement seems obvious intuitively but seems very tricky to start. How does one even start these kind of proofs just looking at bunch of cold axioms? Any hints/help?