Definition: "A tautology is a propositional formula that is true under any truth assignment to each of the atomic propositions in the domain of propositional function."
Let $p$ be a simple (or atomic) proposition (e.g. "9 is a square root of 81").
I understand that a proposition may be either true or false (but not both true and false at the same time). That is, $p$ may be either true or false, exclusively. Under all possible truth assignments, $p$ is not always true. Therefore, from the definition of tautology, $p$ is not a tautology.
However, suppose I proved $p$ to be true. I am tempted to write $p \iff \top$, but this means "$p$ is a tautology". However, the previous paragraph's conclusions was that "$p$ is not a tautology".
What's going on here?
Using the notation in symbolic logic, how does one write that $p$ is indeed true?
Thanks in advance for your help.
Best Answer
No it doesn't. $p \Leftrightarrow \top$ is just another formula, one that happens to be true in exactly the same structures as $p$ is.
It also happens that $p \Leftrightarrow \top$ is a tautology exactly if $p$ itself is a tautology. So if you write, "$p\Leftrightarrow\top$ is a tautology", you're also implicitly asserting that $p$ is a tautology.
But simply writing "$p\Leftrightarrow \top$", without further, is either just putting the formula on the table for further study at the metalevel, or implicitly an assertion that "$p\Leftrightarrow \top$" happens to be true under a particular intended interpretation of the symbols -- even though we're often leaving it implicit what the intended interpretation means.
If you want to say that $p$ is a tautology, then you need to say "$p$ is a tautology"; there is no generally understood symbolic way of saying that. You can say, at the metalevel, $$ \vDash p $$ which asserts that $p$ is logically valid, and in some presentations "tautology" is used to mean "logically valid". With the definition you quote, however, that is not the case.