Gentzen Calculus: Proving $\vdash^G_\Sigma (E3_\cong),(E1),\Gamma\rightarrow \Delta, \forall x_1\forall x_2(x_1\cong x_2\supset x_2\cong x_1)$

Question

I am trying to prove some theorems using Gentzen calculus and have a few questions. For example:

Show that $$\vdash^G_\Sigma (E3_\cong),(E1),\Gamma\rightarrow \Delta, \forall x_1\forall x_2(x_1\cong x_2\supset x_2\cong x_1),$$ where $(E1)$ is the sentence $$\forall x(x\cong x)$$ and $(E3_p )$ is the sentence $$\forall x_1...\forall x_{n+n}((x_1\cong x_{n+1}\wedge...\wedge x_n\cong x_{n+n})\supset p(x_1,...,x_n)\supset p(x_{n+1},...,x_{n+n})).$$ My attempt:

$1\quad (E3_\cong),(E1),\Gamma\rightarrow \Delta, \forall x_1\forall x_2(x_1\cong x_2\supset x_2\cong x_1)\quad R\forall:2$
$2\quad (E3_\cong),(E1),\Gamma\rightarrow \Delta,\forall x_2(x_2\cong x_2\supset x_2\cong x_2)\quad R\forall :3$
$3\quad (E3_\cong),(E1),\Gamma\rightarrow \Delta, x_2\cong x_2\supset x_2\cong x_2\quad R\supset:4$
$4\quad x_2\cong x_2,(E3_\cong),(E1),\Gamma\rightarrow \Delta,x_2\cong x_2\quad \text{Ax}$

From step 1 to step 2 I changed $x_1$ to $x_2$ because $x_2$ is a fresh variable in the first sequent. Is this derivation correct?

Furthermore, there is another exercise:

Show that $$\vdash^G_\Sigma (E3_\cong),(E1),\Gamma\rightarrow \Delta,\forall x_1\forall x_2\forall x_3((x_1\cong x_2\wedge x_2\cong x_3)\supset x_1\cong x_3).$$ Here I probably have to use $(E1)$ and $(E3_\cong)$.

My question(s): what does $p(x_1,...,x_n)$ mean when $p$ is replaced by $\cong$ ? In this case, I don't really know how to work with $(E3_\cong)$. What I mean is: what happens if, for example, I apply the rule $L\forall$ to $(E3_\cong)$ ?; how many variables $(x_1,x_2,...)$ should I consider for $(E3_\cong)$ in this particular exercise?

I appreciate any answer/insight. And thank you very much.

Answer 1

See G.Takeuti, Proof Theory, page 37-on, for equality axioms:

$$\to x_1=x_1$$

$$x_1=y_1, \ldots x_n=y_n \to f(x_1,\ldots,x_n)=f(y_1,\ldots,y_n),$$

where $f(...)$ is an $n$-argument places function symbol, and

$$x_1=y_1, \ldots x_n=y_n, P(x_1,\ldots,x_n) \to P(y_1,\ldots,y_n),$$

where $P(...)$ is an $n$-argument places predicate ($=$ included).

Reading your proof bottom-up. the last step seems wrong to me: when we have $∀x_2(x_2 ≅ x_2 ⊃ x_2 ≅ x_2)$ there is no way to recover $x_1$.

To prove Symmetry, we need the Substitution axiom for formulas with formula $(z = x_1)$ as $P(...)$.

Thus, the substitution $P(z,x_1)[x_1/z]$ will get $(x_1=x_1)$ and the substitution $P(z,x_1)[y_1/z]$ will get $(y_1=x_1)$:

$$x_1=y_1, (x_1 = x_1) \to (y_1=x_1).$$

The proof must be:

$$\dfrac{ \dfrac{}{x_1=y_1 , x_1 = x_1 \to y_1 = x_1}}{x_1=x_1,x_1=y_1 \to y_1=x_1},$$

using suitable rules and interchanges.

Now, we have to use Reflexivity axiom: $\dfrac {}{\to x_1=x_1}$ to derive: $x_1=y_1 \to y_1=x_1$, using Cut.

The final result will need $(\text R \supset)$ followed by two $(\text R \forall)$ to get:

$$\to \forall x_1 \forall y_1 (x_1=y_1 \supset y_1=x_1).$$

---

Similar for second proof. We need the atomic formula $(z = x_3)$ with the following instance of the axiom:

$x_1 = x_2, (z=x_3)[x_2/z] → (z=x_3)[x_1/z]).$