# Proving statements for individual and/or all sets of axioms

If something is proved for one set of axioms then you can use it for that set of axioms but wouldn't you have to prove it for another set of axioms before you could use if for the second set of axioms. So for instance must you prove 2+2=4 for every set of axioms before you can use it in any set of axioms, and is this for any piece of maths? P.S. Sorry about the title, could not think of an appropriate title, so feel free to change it or ask me to change it, thanks.

-
Nothing is true in any set of axioms, you can always take the opposite of your statement as an axiom... Moreover any proof assume a clear set of axioms, a proof working for "every set of axioms" at the same time makes no sense. – Denis Jul 24 '13 at 16:58
@dkuper that is wildly misleading. You can only take P or not P to be an axiom if it remains consistent with the existing set of axioms; in general, this won't be true of statements that seem naturally interesting. – Eric Tressler Jul 24 '13 at 16:59
I meant you can take the opposite of your statement as only axiom. – Denis Jul 24 '13 at 17:00
If its not true then what or how is it classified? – genty4321 Jul 24 '13 at 17:00
The "opposite" part of what dkuper said comes as wrong as you pointed out, however, I do agree with him that it makes no sense to claim anything as provable for every set of axioms. Just because you have axioms, that doesn't mean you have any rules of inference. And without any rules of inference only the axioms come as provable. But, no system has every axiom in it by default (even classical logic, since it doesn't have truth-functions of non-classical logic). So, nothing holds true for every set of axioms. – Doug Spoonwood Jul 25 '13 at 0:57

The following answer is under the working assumption that we are talking about classical first-order logic.

Suppose that we can prove $\varphi$ from $T$. If $S$ is a theory such that $S\vdash T$, that is every axiom in $t$ is provable from $S$, then $\varphi$ is provable from $S$.

For example, consider the language including $0,s$ and $+$, where $s$ is an unary function whose meaning is "$sx$ is the successor of $x$". We don't have symbols for $1$ and $2$, but we write $1$ as a shorthand for $s0$ and $2$ as a shorthand for $ss0$.

Now we write the axioms: 1. $\forall x(x+0=x)$, and 2. $\forall x\forall y(x+s(y)=s(x+y))$.

We can now write a proof that $1+1=2$:

1. $s0+s0=s(s0+0))$, that's the second axiom applied to $x=y=1$.
2. $s0+0=s0$, that's the first axiom applied to $x=s0$.
3. $s(s0+0)=ss0$, that's an application of a logical axiom about equality.
4. $s0+s0=ss0$, as a consequence of the above and the application of the previous axiom of equality.

Now whenever we have $T$ whose language includes $s,0,+$ and $T$ proves the two axioms, we know that $T$ proves that $1+1=2$. This goes even further. If we can define (for every model of $T$) a constant $0$, a function $s$ and an operation $+$, and $T$ can prove the two axioms hold for those definable objects, then $T$ proves that $1+1=2$ for those as well.

On the other hand, in some cases we want to take something much weaker than $T$, and see if it still suffices to prove something. In those cases we need to actually work out the proof, or show that the two axioms hold for the addition. Or we can talk about a theory which is not weaker or stronger, but it is not provable from $T$ nor vice versa. In that case, again, we need to give some proof - and it might be a different one, depending on theory and the language.

-
Can you write down logical axiom of equality? – Trismegistos Jul 25 '13 at 7:15
@Trismegistos: It's actually a schema (per language, of course) in which we state (informally) that whenever $t_1,t_2$ are terms in the language, and $F$ is a function symbol then $t_1=t_2\rightarrow Ft_1=Ft_2$, and similarly if $R$ is a predicate then $t_1=t_2\rightarrow Rt_1\leftrightarrow Rt_2$. In here we apply it for terms without free variables, so we don't care about those. This means that whenever two terms are equal we can replace one with the other. – Asaf Karagila Jul 25 '13 at 7:41
So now I understand this if there is no free variables but is this schema different where there are free variables in terms? – Trismegistos Jul 25 '13 at 8:14
@Trismegistos: $\forall x_1\ldots\forall x_n\forall y_1\ldots\forall y_n(x_1=y_1\land\ldots\land x_n=y_n\rightarrow R(x_1,\ldots,x_n)\leftrightarrow R(y_1,\ldots,y_n)$. Similarly for $F$ and so on. For the relevant case here we have $\forall x\forall y(x=y\rightarrow sx=sy)$ and $\forall x_1\forall x_2\forall y_1\forall y_2(x_1=y_1\land x_2=y_2\rightarrow x_1+x_2=y_1+y_2)$. – Asaf Karagila Jul 25 '13 at 8:26