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.