### 5.1.1 Syntax of Propositional Calculus

A **proposition** is a sentence, written in a language, that has a truth value
(i.e., it is true or false) in a world. A proposition is built from
atomic propositions using logical connectives.

An **atomic proposition**, or just an **atom**, is a
symbol that starts with a lower-case
letter. Intuitively, an atom is something that is
true or false.

For example, *ai_is_fun*, *lit_l _{1}*,

*live_outside*, and

*sunny*can all be atoms.

In terms of the algebraic variables of the preceding chapter, an atom can be
seen as a statement that a variable has
a particular value or that the value is in a set of values. For
example, the proposition *classtimeAfter3* may mean *ClassTime>3*, which is true when the variable *ClassTime* has
value greater than 3 and is false otherwise. It is traditional in propositional
calculus not to make the variable explicit and we follow that tradition.
A direct connection exists to **Boolean variables**, which are
variables with domain *{true*, *false}*. An assignment
*X=true* is written as the proposition *x*, using the variable name, but in lower case. So the
proposition *happy* can mean
there exists a Boolean variable *Happy*, where *happy* means *Happy=true*.

Propositions can be built from simpler propositions using logical
connectives. A **proposition** is either

- an atomic proposition or
- a
**compound proposition**of the form*¬p*(read "not*p*")--the**negation**of*p**p∧q*(read "*p*and*q*")--the**conjunction**of*p*and*q**p∨q*(read "*p*or*q*")--the**disjunction**of*p*and*q**p→q*(read "*p*implies*q*")--the**implication**of*q*from*p**p←q*(read "*p*if*q*")--the**implication**of*p*from*q**p ↔q*(read "*p*if and only if*q*" or "*p*is equivalent to*q*")where

*p*and*q*are propositions.

The precedence of the operators is in the order they are given above. That is, a compound proposition can be disambiguated by adding parentheses to the subexpressions in the order the operations are defined above. Thus, for example,

¬a ∨ b ∧c →d ∧¬e ∨ f

is an abbreviation for

((¬a) ∨ (b ∧c)) →((d ∧(¬e)) ∨ f).