When writing little proofs to write a larger one, I often try to make a chain of $\iff,$ to get to an obviously true statement. I feel like it would be nice to do just another $\iff$ to an symbol that stands for "true statement," a boolean constant, if you like. Is there such a thing?
2 Answers
You can use $\top$ for true and $\bot$ for false.
Note that I'm not going to provide such a symbol, but rather argue that it shouldn't be introduced in the first place.
Something is never simply "true" without context. A statement can be true if another statement that implies the first statement is considered true, which is again only true if it is implied by a third true statement, etc. This chain in principle goes all the way down to the axioms of your theory.
In practice, however, one often stops (or starts) a proof at some well-known assertion. But introducing a whole symbol for just that part would probably just be confusing; instead, you should explain (with words) why that assertion should be considered true, or give some reference.
