How does one show that an intersection of set of propositions is provable iff each proposition is individually provable?

Question

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:

1. propositional axioms
2. equality axioms
3. quantifier axioms
4. 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:

1. T
2. $\varphi \to (\varphi \lor \psi); \varphi \to (\psi \lor \varphi)$
3. $\neg \varphi \to (\neg \psi \to \neg (\varphi \lor \psi) $
4. $(\varphi \land \psi) \to \varphi; (\psi \land \varphi) \to \psi$
5. $\varphi \to (\psi \to (\varphi \land \psi))$
6. $(\varphi \to (\psi \to \theta)) \to ((\varphi \to \psi)\to (\varphi \to \theta))$
7. $\varphi \to (\neg \varphi \to \bot)$
8. $(\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?

Answer 1

The key is to use axiom $5.$ We can prove this by induction on $n.$ $n=1$ is obvious. Then, for $n=2,$ we have $\varphi_1$ and $\varphi_2,$ and then invoke axiom 5 as $\varphi_1\to(\varphi_2\to(\varphi_1\land\varphi_2))$ and use modus ponens twice to get $\varphi_1\land\varphi_2.$ The $n=2$ case can be modified into a proof of the induction step.

Answer 2

If $n = 1$, then the statement is trivial. From now on, we suppose $n > 1$.

The idea to prove both sides of the equivalence is to extend the derivation(s) given by hypothesis by means of suitable logical axioms and modus ponens, in order to get the demanded derivation(s).

---

$\Leftarrow$: Let $\pi$ be a derivation of $\Sigma \vdash \varphi_1 \land \dots \land \varphi_n$, which exists by hypothesis. For every $i \in \{1, \dots, n\}$, let $C_i$ be the formula $\varphi_i \land \dots \land \varphi_n$. Note that $C_n = \varphi_n$ and $C_{i} = \varphi_i \land C_{i+1}$ for all $i \in \{1, \dots, n-1\}$. Note that $\pi$ is a derivation of $\Sigma \vdash C_1$ (this is our starting point to build new derivations extending $\pi$). Consider the $2n$ instances $A_1, B_1, \dots, A_n, B_n$ of the logical axiom 4.

$A_1 : (\varphi_1 \land C_2) \to \varphi_1$

$B_1 : (\varphi_1 \land C_2) \to C_2$

$A_2 : (\varphi_2 \land C_3) \to \varphi_2$

$B_2 : (\varphi_2 \land C_3) \to C_3$

$\dots$

$A_n : (\varphi_{n-1} \land C_n) \to \varphi_{n-1}$

$B_n : (\varphi_{n-1} \land C_n) \to C_n$

If you apply modus ponens to the formulas $A_1$ and $C_1 = \varphi_1 \land C_2$, you get $\varphi_1$; hence, $\Sigma \vdash \varphi_1$. If you apply modus ponens to the formulas $B_1$ and $C_1 = \varphi_1 \land C_2$, you get $C_2$; hence, $\Sigma \vdash C_2$.

If you apply modus ponens to the formulas $A_2$ and $C_2 = \varphi_2 \land C_3$, you get $\varphi_2$; hence, $\Sigma \vdash \varphi_2$. If you apply modus ponens to the formulas $B_2$ and $C_2 = \varphi_2 \land C_3$, you get $C_3$; hence, $\Sigma \vdash C_3$.

And so on. After $2n-2$ applications of modus ponens, you get $\Sigma \vdash C_n$ i.e. $\Sigma \vdash \varphi_n$. In this way, you prove that $\Sigma \vdash \varphi_i$ for all $i \in \{1, \dots, n\}$.

---

$\Rightarrow$: As above, for every $i \in \{1, \dots, n\}$, let $C_i$ be the formula $\varphi_i \land \dots \land \varphi_n$. In particular, $C_1 = \varphi_1 \land \dots \land \varphi_n$. Note that $\Sigma \vdash C_n$ by hypothesis, since $C_n = \varphi_n$. Our starting points are the derivations of $\Sigma \vdash \varphi_i$ for all $i \in \{1, \dots, n\}$, which exist by hypothesis. Consider the $n-1$ instances $D_1, \dots, D_{n-1}$ of the logical axiom 5.

$D_1 : \varphi_{1} \to (C_2 \to (\varphi_{1} \land C_2))$

$D_2 : \varphi_{2} \to (C_3 \to (\varphi_{2} \land C_3))$

$\dots$

$D_{n-1} : \varphi_{n-1} \to (C_n \to (\varphi_{n-1} \land C_n))$

If you apply modus ponens to the formulas $D_{n-1}$ and $\varphi_{n-1}$, you get $C_n \to (\varphi_{n-1} \land C_n)$. If you apply modus ponens to the formulas $C_n \to (\varphi_{n-1} \land C_n)$ and $C_{n}$, you get $\varphi_{n-1} \land C_n = C_{n-1}$. Hence, $\Sigma \vdash C_{n-1}$.

If you apply modus ponens to the formulas $D_{n-2}$ and $\varphi_{n-2}$, you get $C_{n-1} \to (\varphi_{n-2} \land C_{n-1})$. If you apply modus ponens to the formulas $C_{n-1} \to (\varphi_{n-2} \land C_{n-1})$ and $C_{n-1}$, you get $\varphi_{n-2} \land C_{n-1} = C_{n-2}$. Hence, $\Sigma \vdash C_{n-2}$.

And so on. After $2n - 2$ applications of modus ponens, you get a derivation of $\Sigma \vdash C_1$, i.e. $\Sigma \vdash \varphi_1 \land \dots \land \varphi_n$.