atomic sentence vs atomic forumla as used in logic Is there a difference between the two terms as used in introduciton logic or are they synonym? I couldn't find an example of atomic sentence on wikipedia. I don't think atomic senteces really exist because they are expressed as variables in propositional logic.
 A: Let us begin with some informal definitions:

*

*An atomic formula is one that can not be broken down into simpler formulas and thus, it does not contain any logical connectives (like $\neg$, $\wedge$, $\vee$, $\rightarrow$, $\leftrightarrow$, etc), neither quantifiers ($\forall$, $\exists$). So, an atomic formula is constructed by a predicate symbol, either nullary or with terms as arguments: $P$, $P(t_{1})$, $P(t_{1},t_{2})$, $P(t_{1},t_{2},t_{3})$, ...


*A term is a variable, a constant, or it has the form $f(t_{1},t_{2},...,t_{n})$, where $f$ is a function symbol and $t_{1}$, $t_{2}$, ..., $t_{n}$ are terms.


*An atomic sentence is an atomic formula containing no variables. Since there are no variables, either the sentence is made of a nullary predicate (a predicate that takes no arguments), or it contains constant terms.
In the language of ordinary first order predicate calculus, there are no constants or function symbols, as primitive symbols. That means, you can not form any constant term, using only the symbols of that language. However, some times the “always true” and “always false” symbols, “$\top$” and “$\bot$” respectively, are included in the language. Those can be seen as nullary predicates, and thus, as atomic sentences. If these are not included, then, indeed, there are no atomic sentences in the language of ordinary first order predicate calculus.
However, even if we leave aside “$\top$” and “$\bot$”, it is not correct to say that, there are not any atomic sentences in general. In order for the language to be useful in a field of mathematics (a different one than pure logic), it must be extended with symbols belonging to that field. Those are called “non logical” symbols. For example, the language of first order Peano arithmetic, contains, together with the symbols of predicate calculus, the non logical symbols “$s$”, “$+$”, “$\cdot$” and “$0$”. An example of an atomic sentence in that language, is:
$$0+0=0$$
[ The equality symbol, "$=$", is usually a primitive symbol for predicate
logic, although not always (see "logic without equality"). It is a binary
predicate symbol, which means, it takes two arguments, and it represents a relation. With binary relations, the syntax "$xPy$" is often allowed, as equivalent with the more strict "$P(x,y)$" form. Otherwise, "$x=y$" should be written as "$=(x,y)$". Similarly, with binary functions, the syntax "$xfy$" is often in use, instead of "$f(x,y)$". "$+$" is a binary function, and we usually write "$x+y$" instead of "$+(x,y)$". If these conventions do not apply, one should write: "$=(+(0,0),0)$" ].
