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.

-
Do you know about the deduction theorem? If you are defining $\lnot \alpha$ as $\alpha \to \bot$, then that should explain how proof by contradiction works in terms of formal logic. –  Zhen Lin Jul 7 '11 at 12:12
It might be more clear if you made it explicit in the question that you are taking $T$ to be the set of axioms for a theory, and are not assuming $T$ is deductively closed. That seems to be the heart of the issue. –  Carl Mummert Jul 7 '11 at 12:18

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.

-

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$.

-
The two versions are indeed equivalent. For the reverse direction, if $T$ proves $\beta$ and $\lnot \beta$ then just let $\alpha_1 = \beta$ and $\alpha_2 = \lnot \beta$. For the forward version, if $T$ proves each $\alpha_i$ and $T$ proves $\lnot ( \alpha_1 \land \cdots \land \alpha_n)$ then in particular, because $T$ proves $\alpha_1$, $T$ proves $\lnot (\alpha_2 \land \cdots \land \alpha_n)$. But $T$ also proves $\alpha_2 \land \cdots \land \alpha_n$ by assumption. This leaves open the question of getting all the $\alpha_i$ to be axioms of $T$. This can done with another step ... –  Carl Mummert Jul 7 '11 at 12:11
If $\gamma_1, \ldots, \gamma_m$ are axioms of $T$ and $\gamma_1, \ldots, \gamma_m \vdash \bot$ then $\lnot (\gamma_1 \land \cdots \land \gamma_m)$ is logically valid, and thus provable in any complete proof system. So, in a sense, if we can find a contradiction between consequences of axioms of $T$, then there is already a contradiction between the axioms themselves. –  Carl Mummert Jul 7 '11 at 12:16
@Carl: a) What is the "assumption" that you refer to -- is it part of an implicit induction argument? If not, where does it come from? b) Your argument makes essential use of the completeness of the proof system -- is it easy to see that the proof system in question is complete? –  joriki Jul 7 '11 at 13:09
The assumption was that $T$ proves all the $\alpha_i$, and hence it proves $\alpha_2 \land \cdots \land \alpha_n$. I have not verified the proof system in question is complete, but my sense was that it was introduced in some textbook, so it should be complete, and my comment assumes it is. If the proof system is not complete, the questioner ought to point that out explicitly. –  Carl Mummert Jul 7 '11 at 17:10
@Carl: I don't understand why you make the step from $\lnot ( \alpha_1 \land \cdots \land \alpha_n)$ to $\lnot (\alpha_2 \land \cdots \land \alpha_n)$ and then use that $T$ proves $\alpha_2 \land \cdots \land \alpha_n$ -- if you're going to use that, why not directly use that it proves $\alpha_1 \land \cdots \land \alpha_n$? Or am I missing something? –  joriki Jul 7 '11 at 17:21

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.

-