This system of quantified propositional logic is straightforward to interpret into first-order logic. We make a theory $T$ that has a single, unary relation symbol, say $P$, and no other symbols in the signature, not even equality. Then, to quantify over "propositional variables", we quantify over elements in first order logic as usual. For each element $x$ in a model of $T$, $Px$ is either true or false, so the elements of the model can be treated as if they were propositional variables.
Thus the quantified propositional sentence $(\exists Q)(\forall R)[R \lor Q]$ is interpreted into $T$ as $(\exists q)(\forall r)[Pr \lor Pq]$. In this way, every sentence of quantified propositional logic is interpreted as a sentence of $T$, and vice-versa.
If we wanted to add constant symbols to $T$, that would be equivalent to adding constant (i.e. non-variable) propositional variables to quantified propositional logic.
I would suggest that the main reason that we don't bother having quantified propositional variables in the "usual" framework for first-order logic is that they are not useful for formalizing the typical mathematical theories (group theory, linear orders, set theory, arithmetic, etc.), and a central goal in most presentations of first-order logic is to be able to formalize these theories. The same holds for $\lambda$ terms to define functions. There is no reason that they could not be included in first-order theories, and in fact they sometimes are, but most presentations have no use for them.
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.
Best Answer
First, we need to define a few terms:
$ \begin{array}{lll} 1.& \text{Statement}& \text{A sentence that is either true or false.}\\ && \text{For example, "Georgia is located north of Florida."}\\ 2.& \text{Proposition}& \text{The meaning, or information content, of a sentence.}\\ && \text{For example, "Georgia is located north of Florida"} \\ && \text{and "Florida is located south of Georgia" are two}\\ && \text{distinct statements but one and the same proposition.} \\ && \text{Note not all texts distinguish between statements and}\\ && \text{propositions.}\\ 3.& \text{Complex Proposition}& \text{A proposition consisting of one or more parts that are}\\ && \text{themselves propositions. For example, "The sky is blue}\\ && \text{and the grass is green."}\\ 4.& \text{Atomic Proposition}& \text{A proposition consisting of one and only one part that}\\ && \text{is a proposition. For example, "The sky is blue." Note}\\ && \text{all atomic propositions are complex propositions, but not}\\ && \text{all complex propositions are atomic propositions.}\\ \end{array} $
In the language of propositional logic, letters such as $A,B,C,...,P,Q,R,...$ and schematic letters such as $φ, ψ, χ$ all represent propositions.
The first few letters $A,B,C,...$ of the alphabet are generally used to represent particular propositions. In other words, they are used to represent specific propositions. For instance, $A$ may be used to represent the sepcifcally identified proposition "My brother is tall," and anywhere I see $A$ I know that specific proposition is being referred to. For this reason, the letters $A,B,C$ are known as propositional constants because the meaning of the letters is specific and constant.
The letters $P,Q,R,...$ of the alphabet range over the set of all atomic propositions. This means the letter $P$ represents any arbitrary proposition that is comoposed of one and only one proposition. For instance, $P$ can mean "My brother is tall" or "My neighbor is an alien" or ... In other words, it is a place holder for any atomic proposition analogous to how $x$ and $y$ are place holders for real numbers in the expression $x+1=y$. Since these letters can represent any proposition in general, they are known as propositional variables. Note that propositional variables and\or constants can be joined by logical connectives to construct formulas that represent complex propositions. For instance, $(P \wedge Q) \to R$ means "If $P$ and $Q$, then $R$."
The schematic letters $φ, ψ, χ, ...$ range over the set of all complex propositions. This means $φ$ represents any arbitrary proposition that is comoposed of one or more propositions. For instance, $φ$ can mean "The sky is blue during the day and it becomes mostly black at night" or "The dog is inside the house or the dog is outside the house" or ... In other words, it is a place holder for any complex proposition in the same way $P$ is a place holder for any atomic proposition.
NOTE: The choice of letters, symbols, and even vocabulary may vary from one text to the next, but the underlying concepts do not. For instance, some texts will utilize uppercase letters for propositional constants while using lowercase letters for propositional variables. Or, some texts may use the utilize the letters $P,Q,R$ to represent complex propositions and abandon the use of schematic letters altogether. Whatever text you're working with, make sure you understand the corresponding definitions and notation.