Definition of “contradiction” and use of the term for “⊥” If one looks in Internet for definition of “contradiction” (including respective words in other languages), one finds a mess. See for example this index of Wikipedia articles in various languages. The meanings offered include:


*

*Logical incompatibility between two statements, i.e., in modern notation, a theorem of the form “ ¬ (P ∧ Q)”, “(P ∧ Q) → ⊥ ”, “ P → (Q → ⊥)”, or similar equivalent form.

*A theorem of the form “ ¬Q ” or, the same, “ Q → ⊥ ” (especially in the context of “proof by contradiction”), and the proposition “Q” in such theorem itself.

*The propositional constant “⊥”.


It is not bizarre to see that first two items are covered by the same term, as they are interchangeable. But the last item (as propositional calculi in general) isn’t very ancient invention. Whereas the term “contradiction” historically denoted a semantic falsity (we know that something is false), “⊥” is a syntactic falsity. I was frustrated when discovered this terminology for propositional constants in English; in Russian, the same words are used for truth values and propositional constants, so “⊥” is ложь (“false”), the same term as for “F” in truth tables.
You may say: I am accustomed to one terminology, English speakers to another, and there is no difference how to call things. But the aberration that only irritates me, becomes actually confusing for other people, as expressed in this comment in the A de-Morgan law for Heyting lattices
 thread.
My principal question is: how the term “contradiction” in English extended its denotation beyond “ ⊨ (Q → ⊥) ” stuff and became the common name for “⊥”? Why the term falsum (“false”) fell out of favour? Did some historical causes for it exist? Was such unification convenient for some (then broadly used) logical system? Or did some popular misconception (either of ages of George Boole, or of poorly educated public later) caused this change?
 A: I'm not sure about the "real" origin, but I think that the main source for the use of $\bot$ is Gerhard Gentzen : INVESTIGATIONS INTO LOGICAL DEDUCTION (ed or. Untersuchungen uber das logische Schliessen, Mathematische Zeitschrift 39 (1935) 176-210, 405-431); see english reprint : Gerhard Gentzen, The collected papers (1969), page 70 :

Symbols for definite propositions: $\top$ ('the true proposition'), $\bot$ ('the false 
  proposition'). 

This definitions license the name falsum for $\bot$.
I think that the term contradiction is more apt to a "metalogical" usage, like tautology.
See Gentzen, page 78 :

$\mathfrak A$ and $\lnot \mathfrak A$ signifies a contradiction and as such cannot hold true (law of contradiction). This is formally expressed by the inference figure $\lnot$-E where $\bot$ designates 'the contradiction', 'the false'. 

Thus, I agree with Zhen Lin's comment : $⊥$ [the falsum] is "the abstract contradiction".
Gentzen's introduction of $\bot$ as a primitive symbol allows him to define $\lnot$ through an abbreviation: $\lnot A$ stands for : $A \rightarrow \bot$.
A: First of all, what do (non-mathematical) vocabularies say about relevant meanings? Non-English vocabularies were chosen to avoid presumed semantic deviations.
French:

Opposition, incompatibilité entre deux ou plusieurs choses, ou entre les éléments d'une même chose.
«Être» et «n'être pas» implique contradiction. Il y a contradiction entre ces deux propositions. Cette contradiction n'est qu'apparente.
       Source: 1

“ Opposition, incompatibility between two or more things, or between elements of one, the same, thing.
‘To be’ and ‘not to be’ implies contradiction. There is a contradiction between these two propositions. This contradiction is not but apparent. ”
Russian:

Положение, при котором что-либо одно исключает другое, несовместимое с ним.
       Source: 2

“ A condition that makes one thing to exclude another thing, incompatible with it. ” («Противоречие» is a literal translation of “contradictio” from Latin.)
We see that vocabularies mainly support the first interpretation, to some extend the second (with one proposition), and there is only a slight hint about the third. The French one starts from a pure “ ⊨ ¬ (P ∧ Q)” and then passes to éléments d'une même chose (somewhat a special case where C ⊢ P, Q and, consequently, “ ⊨ ¬C ” ). In examples there is a statement like “ ⊨ (P ∧ ¬P) → contradiction” (the verb “implique” was used), so it is plausible that French authors thought about “contradiction” also as about abstract “⊥”, but this wasn’t explained. The Russian one gives the “ ⊨ (P → ¬Q) ” formulation, a variant of the first meaning.
Three questions remain:
1. How “ ⊨ ¬ (P ∧ Q)” and “  ⊨ ¬Q ” meanings are related?
2. Is contradiction an “incompatibility condition” or a proposition Q for which “ ⊨ ¬Q ”?
3. How “⊥” is related to all this?
Obviously, a contradiction between two or more proposition can be generalized to contradiction on one proposition. On the other hand, “ ⊨ ¬ (P ∧ Q)” and analogous things for more propositions are all partial cases of “  ⊨ ¬Q ”. So, more that one proposition are plainly redundant. Also, assumed we can prove P, we enjoy “ P, (P → (Q → ⊥)) ⊢ (Q → ⊥)”. In other words, if we had a contradiction between two propositions and proved one of them, then we naturally obtained a contradiction on one proposition. So is the point 1.
As for point 2., we probably had a synecdoche. When users of propositional calculus forgot that primary meaning of “contradiction” was “ ⊨ ¬ (something)”, they started to think about (something) itself as about a contradiction.
The point 3. admits two explications:

*

*As was suggested in comments, all “contradictions” (i.e. such Q that “  ⊨ ¬Q ”) are logically equivalent. Whereas in English language “a contradiction” can denote an arbitrary such Q, it is consistent with grammar to make “the contradiction” to denote a predefined symbol, such as “⊥”. Russian language hasn’t articles and such trick wouldn’t be possible – and we see the result. (But note that French examples omit articles for «contradiction», although the language has them, in principle.)


*“⊥” can be seen as the generalization of “ P → (Q → ⊥)” and “ Q → ⊥ ” for zero propositions. Although we can’t normally have it as a theorem, it is a valid statement that can appear as “ (something)  ⊨ ⊥ ”, for example in so named proofs by contradiction.
