What is the correct reading of $\bot$?
You are mixing up different aspects of logic, also some parts of your question are more philosophical than mathematical.
First headline: $\bot$ and $\top$ are wellformed formulas.
(On purpose I mention them both here because in this aspect they are the same)
Different authors have different formulations of this fact:
- $\bot$ and $\top$ are propositional constants
- $\bot$ and $\top$ are a zero-place connectives
- $\bot$ and $\top$ are atomic formula
They all point to the same thing $\bot$ and $\top$ can be part of a formula, it can be used like a normal propositional variable in all rules of the logic. so if $ ( P \to (Q \to R )) \to ( (P \to Q )\to (P \to R )) $ is a theorem then so are $ ( \top \to (Q \to \bot )) \to ( (\top \to Q )\to (\top \to \bot )) $ and $ ( \bot \to (\bot \to R )) \to ( (\bot \to \bot )\to (\bot \to R )) $ and many more, they are not very helpful but that is beside the point)
This is all about being wellformed and how you can use them in formulas , it has nothing about what $\bot$ means.
Some logics just don't define $\bot$ or $\top$ as a wellformed formula, so in those logics they just do not exist.
What does $\bot$ mean?
This is a philosophical question.
If you see logic just as symbol manipulation (the philosophy of mathematics known as formalism) , no symbol means anything and so questioning what a particular symbol means is meaningless.
The above is I guess not very helpful, so different logicians come up with different ideas.
$\bot$ means absurd: $ P \to \bot$ means that P leads to absurdity ( and we don't want that)
$\bot$ means refutability: $ P \to \bot$ means that P is refutable ( and so P is false)
$\bot$ means non-demonstrability $ P \to \bot$ means that P is not demonstable (so not provably true)
The above is a rewriting from "Foundations of Mathematical logic" Curry (1963), chapter 6 "negation" , the chapter goes much deeper in it, there is a dover edition of it, highly recomended, but negation is much more complex than it looks, in another article I saw, I think 7 different negations appeared, and i do doubt that article mentioned them all.
Wittgenstein came up with " meaning follows from use " so maybe the only way you can find the meaning is to look at how it is used.
If $ \bot \to P $ is a theorem then $\bot$ means absurdity, it is quite absurd that every formula is true.
If $ ((P \lor R) \to ((P \to\bot) \to R) $ is a theorem then $\bot$ means refutability, P is refuted (and therefore R is true)
If $ (P \lor (P \to\bot) ) $ you have classical logic.
so it all depends, but can you expect anything else with a philosophical question.
There is one simple "universal" answer to this question which depends neither on proof theory nor on semantics.
Think of the set of formulas of logic as a term algebra freely generated over a syntactic signature that describes its collection of connectives (or think of the set of formulas, for all that matters, as a context-free grammar). Assume there are denumerably many variables (or propositional parameters) in the underlying language. An abstract consequence relation is then defined over such propositional language, as usual, so as to recover the properties of a closure operator. A logic system is then given by a language $L$ and a substitution-invariant consequence relation $\vdash\;\subseteq 2^L\times L$. By 'substitution-invariant' we mean that $\Gamma\vdash A$ implies $\sigma[\Gamma]\vdash\sigma[A]$, where $\sigma$ denotes a substitution mapping in $L$ (i.e., a homomorphic mapping from variables to formulas).
Now, in the above construction $\bot$ (or $\top$) may be either a propositional parameter or a nullary connective. In the former scenario, substitution would apply to such symbol; in the latter, it wouldn't. However, in practice, $\bot\vdash p$ is usually assumed to hold for every variable $p$, but $q\vdash p$ in general fails for every variable $q$ distinct from $p$. Consequence would thus not be preserved under substitution, if one insisted that $\bot$ is a propositional parameter. The simplest way out is to assume it to be a nullary connective.
Here's the big divide over the use and meaning of an absurdity symbol in natural deduction systems: which of the following ways of treating the symbol should we take?
(i) $\bot$ can be assigned a truth-value and can appear embedded like a subformula in more complex formulas, or
(ii) $\bot$ merely serves to "close off" a line of reasoning when it contains contradictory wffs, so using it is like saying "Stop! Trouble!! Aaaarghhhh!!!!!"
Approach (i) is explored a bit in @Willemien's answer. And, concerning the fine print details within approach (i), it surely doesn't matter too much whether you officially call $\bot$ a zero place connective, or a propositional atomic formula (or rather, which way you go will depend on the further fine print of what you say elsewhere about connectives and atomic formulae).
Of those who have argued that we should best treat an absurdity marker using approach (ii), I think the most persuasive is Neil Tennant: see e.g. his paper http://people.cohums.ohio-state.edu/tennant9/nac.pdf for further details.