[Math] Definition of “contradiction” and use of the term for “⊥”

logicpropositional-calculusterminology

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?

Best Answer

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

Related Question