# Proof of theorems (First Order Logic)

Considering the list of axioms:

$(A1)$ - All Tautologies.

$(A2)$ - $(\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta))$.

$(A3)$ - $(\forall x \alpha) \rightarrow [\alpha]^{t}_{x}$ if x is free for t in $\alpha$.

$(A4)$ - $\alpha \rightarrow (\forall x \alpha)$ if x is not free in $\alpha$.

$(A5)$ - $x = x$

$(A6)$ - $(x=y) \rightarrow (\alpha \rightarrow \beta)$ if $\beta$ if obtained by substitution of at least one occurrence of x free for y in $\alpha$.

I am trying to write a proof for some theorems. However, I am a little confused.

$\vdash (\forall x_1(R_1^1(x_1) \lor R_2^1(x_1))) \rightarrow (R_2^1(x_1) \lor R_1^1(x_1))$

For this one, could I use (A3), given that $\forall x_1$ on the left side of $\rightarrow$?

$\vdash R_1^1(c_1) \rightarrow (R_1^1(c_2) \rightarrow (R_1^1(c_1) \land R_1^1(c_2)))$

For this one, could I use the tautology $\alpha \rightarrow (\beta \rightarrow(\alpha \land \beta))$, given that $R_1^1(c_1)$ is the same relational symbol, but applied to different constants?

$\vdash \forall x_1(\forall x_2(R_1^1(x_1) \rightarrow (R_1^1(x_2) \rightarrow R_1^1(x_1))))$

Same question as before (combining the first ones), could I use the tautology $\alpha \rightarrow (\beta \rightarrow \alpha)$ and then (A4)?

First: Yes, though you have to combine (A3) with a tautology in order to get to swap the $R_2^1$ and $R_1^1$ disjuncts in the conclusion.

Second: Yes, this is an instance of (A1).

Third: No, (A3) will let you remove a $\forall$ from something you've already proved, not add it. In fact I'm almost sure your axioms are not enough to prove this, if all you have is Modus Ponens. Specifically, the axioms would all be true under a variant semantics where $\forall x\alpha$ always evaluates to false when $x$ is free in $\alpha$ (and MP preserves this truth). Since your goal is not true in this that variant semantics, it can't be proved.

Are you sure you don't have a separate Generalization rule in addition to your axioms and MP?

• Sorry, i meant (A4) on that one, will edit. So, even with A4, I can't use it there, do I need the Generalization Theorem (GT) on that one? Considering the first, (A3) should change $x_1$ to $x_1$, is that correct? – Bruno A Aug 21 '16 at 15:27
• @LuizS.: I'm not exactly sure what your "Generalization Theorem" says, but if it says what it sounds like it ought to, then it is not true if all you have is tha axioms you have shown here plus MP. – Henning Makholm Aug 21 '16 at 15:38
• It says: Let $\Gamma$ be a subset of formulas of a first order logic language such that the variable x is not free in all formulas of $\Gamma$. Then $\Gamma \vdash \alpha$ whenever $\Gamma \vdash \forall x \alpha$ – Bruno A Aug 21 '16 at 15:51
• @LuizS.: Ah, that looks true, but it goes in the wrong direction -- it also requires you already to have proved $\forall x\alpha$ before it applies. (In fact what it states is just a simple application of A3 with $t=x$). – Henning Makholm Aug 21 '16 at 15:52
• So I can't use it directly on the third case? – Bruno A Aug 21 '16 at 15:56