"Contradiction-free" in logic vs. "Contradiction-free" in plain mathematics 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.
 A: I think the explanation has two components, one relating to your considerations and one to your teacher's considerations.
What you wrote is a description of a proof by contradiction, which is not the same as a contradiction. The part about making an assumption to then derive a contradiction from it isn't part of what "contradiction" means.
What does survive from your considerations, though, is that a more simple and direct definition of "contradiction-free" would be to say that there is no formula $\beta$ such that both $\beta$ and $\neg\beta$ are provable from $T$ -- this is the part of your description that relates directly to contradictions.
A possible reason for the more complicated definition used in your course might be that it makes it easier to check whether a theory is contradiction-free. To apply the simpler definition, you'd have to check every possible formula $\beta$; to apply your course's definition, you only have to check all possible combinations of formulas in the theory.
I suspect that it can be shown that the two definitions are equivalent, but I can only show one direction of this equivalence: If a theory is contradiction-free in your sense, then it is also contradiction-free in the course's sense. This is because we can use the deductive calculus you linked to to prove $\alpha_1\&\ldots\&\alpha_n$ from $\alpha_1, \dotsc, \alpha_n$. Here's the proof for $n=2$: $\neg(A\&\neg\neg(B\&\neg(A\&B)))$ is a propositional tautology. Thus $\neg(\alpha_1\&\neg\neg(\alpha_2\&\neg(\alpha_1\&\alpha_2)))$ is in $\kappa$. Since $\alpha_1$ is in $\kappa$, by modus ponens $\neg(\alpha_2\&\neg(\alpha_1\&\alpha_2))$ is in $\kappa$. Then since $\alpha_2$ is in $\kappa$, again by modus ponens $\alpha_1\&\alpha_2$ is in $\kappa$. Thus, a contradiction in the course's sense leads to a contradiction in your sense, with $\beta=\alpha_1\&\ldots\&\alpha_n$.
To show the other direction of the equivalence, one would have to show that if there is any $\beta$ for which both $\beta$ and $\neg\beta$ are provable from $T$, then there is necessarily such a $\beta$ of the form $\alpha_1\&\ldots\&\alpha_n$, with $\alpha_1, \dotsc, \alpha_n\in T$.
A: Here is an answer using the compactness theorem. Normally we say a theory is consistent if is has a model. I will explain why a theory is consistent if and only if it is contradiction free in your sense.  Here we take the theory to be just an arbitrary set of axioms. 
First, assume the theory is inconsistent, so it has no model. Then, by the compactness theorem, some finite subset $\{ \alpha_1, \ldots, \alpha_n\}$ of the axioms is inconsistent (the compactness theorem applies to any set of sentences). Thus $\lnot (\alpha_1 \land \cdots \land \alpha_n)$ is logically valid, and so this formula is provable in any complete proof system.
Conversely, suppose that that theory is not contradiction-free, so there is a finite set $\{ \alpha_1, \ldots, \alpha_n\}$ of axioms of the theory such that $\lnot (\alpha_1 \land \cdots \land \alpha_n)$  is provable. Then this compound sentence is true in every model, so there is no model which satisfies $\alpha_1 \land \cdots \land \alpha_n$, and thus no model of the theory. 
A: 
Why is "contradiction-free" defined is
  this way and not is some other more
  obvious way ?

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.
