In our course we have defined a theory $T$ to be contradiction-free, if there are no formulas $\alpha_1,\ldots \alpha_n\in T$ such that $\neg ( \alpha_1 \& \ldots \ \& \alpha_n )$ is provable (but not necessarily still in $T$) (where provable means, that $\neg ( \alpha_1 \& \ldots \ \& \alpha_n ) \in \kappa$, where $\kappa$ is my deductive calculus defined here). My question is: Why is "contradiction-free" defined is this way and not is some other more obvious way ?
My idea of a contradiction would be the following: When doing the usual mathematical proof by contradiction, it usually means that in the area in which I'm doing the proof (for example number theory) I make an additional assumption (which is just the negation of what I what to prove - lets call this the sentence $\alpha$. I can thus think of as $\neg \alpha$ being added to the axioms, which define number theory) and by using different already proven lemmas/theorems I can somehow deduce that some other already proven sentence $\beta$ is actually false, meaning I get $\neg \beta$. So shouldn't "contradiction-free" be defined more in way to reflect to above procedure ? Because defining it like it was defined in our course, I don't find that it corresponds to what I think a contradiction in the usual mathematical sense is.
Because “contradiction-free” can be defined in several equivalent ways, and you decided to use this definition. ;)
I assume you take negation as a primitive connective. Then a contradiction is a formula $\alpha\land\lnot\alpha$ for some $\alpha$. Your definition is equivalent to “every contradiction is not provable from $T$”. You can find the definition of “provable from” somewhere else.
To prove equivalence of the definitions, I need the deduction theorem which implies that “$\beta$ is provable from $T$” is equivalent to “there exist formulas $\alpha_1,\ldots,\alpha_n\in T$ such that $\alpha_1\land\ldots\land\alpha_n\to\beta$ is provable”.
To prove equivalence of the definitions, I need to prove equivalence of “there exist formulas $\alpha_1,\ldots,\alpha_n\in T$ such that $\lnot(\alpha_1\land\ldots\land\alpha_n)$ is provable” and “some contradiction is provable from $T$”.
$\rightarrow$: For all $i$, $\alpha_i$ is provable from $T$ by a degenerate proof. Let $\beta:=\alpha_1\land\ldots\land\alpha_n$. Then $\beta$ is provable from $T$. $\lnot\beta$ is provable from $\varnothing$. Then $\beta\land\lnot\beta$ is the contradiction that is provable from $T$.
$\leftarrow$: Let $\beta\land\lnot\beta$ be the contradiction that is provable from $T$. By the deduction theorem there exist $\alpha_1,\ldots,\alpha_n\in T$ such that $\alpha_1\land\ldots\land\alpha_n \to \beta\land\lnot\beta$ is provable. Using the axiom schema $(A\to B) \to (A\to\lnot B) \to \lnot A$, $\lnot(\alpha_1\land\ldots\land\alpha_n)$ is provable.