Inverting Proofs using “Iff”s

Before you read my question, let me make it clear that I am new to proof theory and know almost nothing about it. This is just something that I thought of out of the blue.

When one writes a proof, the proof consists of a chain of statements that imply each other. For example, a proof of the statement $S_1 \implies S_n$ might look like $$S_1\implies S_2\implies ...\implies S_n$$ Where each of the theorems used in the proof of this theorem are the theorems $$S_1\implies S_2$$ $$S_2\implies S_3$$ $$...$$ $$S_{n-1}\implies S_n$$ Which must be established beforehand

If you wanted to prove that $S_1 \iff S_n$, (I will call this type of theorem a "symmetric theorem", for lack of a better term) you can write proofs for both $S_1\implies S_n$ and $S_n\implies S_1$. However, you can achieve this in a single proof by instead using a proof that looks like this: $$S_1\iff S_2\iff ...\iff S_n$$ Because to prove the converse, instead of starting a separate proof, you can just turn this proof "backwards" and it will still work, since all of the intermediate theorems are symmetric.

However, I am trying to prove that if a theorem is symmetric, then it must have a proof using all symmetric intermediate theorems. It seems fairly obvious, but how do I show that? Assume the opposite and look for a contradiction?

I thought that this would be an interesting thing to prove, because I believe that if it were true, it would imply that in a formal system with no symmetric axioms, no symmetric theorems can be proven to be true.

Also, can anybody point me towards any resources addressing this kind of thing? Perhaps a beginning course of proof theory?

Thanks!

• I'm not sure I understand your question. Do you mean to prove that : $$(S_1 \Leftrightarrow S_n) \Rightarrow (S_n\Leftrightarrow S_i, \forall i \in [1,n])$$ ? – Furrane Jul 24 '17 at 17:54
• Yeah, that's what it boils down to. – Frpzzd Jul 24 '17 at 17:56
• What is a symmetric axiom? – DanielWainfleet Jul 25 '17 at 5:02
• @DanielWainfleet I'm using it to refer to a theorem that "works forwards and backwards", or uses "if and only if". – Frpzzd Jul 25 '17 at 13:02
• Theorem: $\;\forall x\;(x=x)\iff \forall y\;(y=y).$ Axioms needed: None. – DanielWainfleet Jul 25 '17 at 13:30

When you say that your symmetric theorem is of the form $S_1 \Leftrightarrow S_n$ you are basically already assuming that there are already a bunch of intermediate results $S_i$ ... all standing in the $S_i \Leftrightarrow S_{i+1}$ relationship. I mean, why else do you have those indices?

So maybe that's not a very interesting question....

And maybe a more interesting question is: if we have a symmetric theorem $\varphi \Leftrightarrow \psi$, will it always be the case that there are statements $S_1 ... S_n$ such that there is a symmetrical proof $\varphi = S_1 \Leftrightarrow S_2 ... \Leftrightarrow S_n = \psi$? And, since we could of could of trivially course choose $S_1=\varphi$ and $S_2 = \psi$, let's make the restriction that $S_i \Leftrightarrow S_{i+1}$ must be a specific instance of some rule of our proof system.

Well, it turns out that there are in fact equivalence rules that are complete for both propositional logic and predicate logic, meaning that whenever you have $\varphi \Leftrightarrow \psi$, you are guaranteed to be able to step by step transform $\varphi$ into $\psi$ using the equivalence rules, and since those are equivalence rules, such a transformation counts as a symmetric proof.

If you only have inference rules, however (such as what most natural deduction systems have), then typically you cannot invert the proof, and you will have to give two proofs.

Ok so let's try to prove $$(S_1 \Leftrightarrow S_n) \Rightarrow (\forall i \in [1,n] :S_1\Leftrightarrow S_i)$$

Given :

$$\forall i \in [1,n-1] : S_i\Leftrightarrow S_i+1$$

We will procede by recurrence (I'm not sure it's the correct english term):

Let $P_k = \{(S_1\Leftrightarrow S_k) \Leftrightarrow (S_1 \Leftrightarrow S_{k+1}) \}$

• Let $k=1$ :

We know that $\tag{1}S_1 \Leftrightarrow S_2$ and $\tag{2}S_2 \Leftrightarrow S_3$ (those are given)

$(1)$ and (2) allow us to conclude that $(S_1\Leftrightarrow S_2) \Rightarrow (S_1 \Leftrightarrow S_3)$ and $(S_1\Leftrightarrow S_3) \Rightarrow (S_1 \Leftrightarrow S_2)$ which is $P_1$ is true.

• Now suppose we have $P_k$ true for $k\in [1,n-2]$ which is :

$$(S_1\Leftrightarrow S_k) \Leftrightarrow (S_1 \Leftrightarrow S_{k+1})$$

But we also know (given) that :

$$S_{k+1} \Leftrightarrow S_{k+2}$$

So we can conclude similary that :

$${\forall k \in [1,n-2] :P_k \Rightarrow P_{k+1}}$$

So now we proved $\forall k \in [1,n-1] : P_k$ (is true).

So we can conclude that if $S_1 \Leftrightarrow S_n$ then $\forall i\in [1,n] : S_1\Leftrightarrow S_i$