Sentential Calculus
Overview
The sentential calculus is a formal language for expressing simple logical arguments. Consider the following:

If it is raining then the streets are wet.

It is raining.

Therefore, the streets are wet.
The first two sentences are premises that are simply stipulated to be true for the purposes of the given argument. The third sentence is the conclusion that is derived from the premises by the application of inference rules (modus ponens in this case). The whole argument is a theorem, i.e. it is a valid argument. An argument is valid if and only if it is possible to show that the conclusion must be true when making no assumptions other than that the explicitly cited premises are true and then applying a sequence of one or more transformations that are supported by the axioms of symbolic logic.
Note: The terminology and motivation for symbolic logic predates the modern distinction between a formal system and its metamathematical interpretation. It is critical to understand that when logicians pronounce formal expressions like
$$ P \rightarrow Q $$
as “if P then Q,” they are simply using the common oral terminology for a formal expression involving a conditional connective. It is a metamathematical notion to equate such formal expressions with the meaning of the natural language phrases to which they have traditionally been said to correspond. Such metamathematical notions are not the domain of discourse for symbolic logic.
Another way of understanding the distinction is by the following observation: any attempt to prove a point about the real world by representing an argument as expressions of symbolic logic must reduce all of the terms of the argument to absolutely unambiguous declarative statements with objectively determined truth values and completely incontestable compositions of those terms using the connectives as they are defined by the axioms of symolic logic and not as they are commonly understood in natural language. Only then can the proof procedures discussed below actually apply to any given argument concerning the state of things in the real world.
Good luck with that!
The preceding naturallanguage argument could be expressed as a sequence of wellformed formulas (WFF’s) of the sentential calculus, as follows:
Argument 1:
$$ \begin{aligned} &P \rightarrow Q \\ &P \\ \hline \\ \therefore &Q \\ \end{aligned} $$
where
$$ \begin{aligned} P & = \text{``It is raining.''} \\ Q & = \text{``The streets are wet.''} \end{aligned} $$
The primitive terms in a formula of the sentential calculus are represented by upper case letters of the Latin alphabet, P and Q in this example. They evaluate to one of exactly two possible values, true (T) or false (F). When interpreting an expression in natural language, such primitive terms correspond to complete declarative sentences – hence the “sentential” in “sentential calculus” – such as “It is raining,” “Two plus two equals four,” and so on.
The symbol → is one of a number of connectives that can be used to combine terms to express a logical relationship – “if … then …” in this case. The statements above the horizontal line are the premises of an argument and the statement below the line its conclusion. Such an argument is valid if the conclusion is necessarily true assuming that its premises are true.
There are a number of connectives or “operators.” Each is defined by its truth table and has a commonly used natural language formulation like “and,” “or,” “if … then …” etc.
Note: Conventionally, greek letters like Φ and Ψ are used when documenting axioms and inference rules which apply to any combination of wellformed formulas. E.g.
$$ \Phi \rightarrow \Psi $$
is used when discussing the truth table for or inference rules involving the conditional connective as it could be applied to any combination of wellformed formulas while
$$ P \rightarrow Q $$
is a particular conditional formula and
$$ (P \vee \neg Q) \rightarrow \neg (R \wedge S) $$
is another.
Here, for example, is the truth table for ∧, “and”:
$$ \begin{array}{ccc} \Phi & \Psi & \Phi \wedge \Psi \\ \hline \\ T & T & T \\ T & F & F \\ T & T & F \\ T & F & F \end{array} $$
See Connectives for a complete set of such truth tables for all of the connectives in traditional logic and a more detailed explanation of their meaning.
The validity of argument 1, above, should be fairly intuitive. Assuming that the symbol ¬ means “not” (logical negation) and the symbol ∨ means “or”, consider this argument:
$$ \begin{aligned} &\neg P \vee Q \\ &P \\ \hline \\ \therefore &Q \end{aligned} $$
This is less immediately intuitive, but is also valid. In fact, according to the rules of the sentential calculus it is entirely equivalent to the first argument involving the → symbol, as will be discussed further below. For now, consider the following translation into the corresponding natural language argument:

Either the weather is fair or the streets are wet.

The weather is not fair.

Therefore, the streets are wet.
That the sentence, “Either the weather is fair or the streets are wet,” is logically equivalent to the sentence, “If it is raining then the streets are wet,” is a theorem of traditional logic – but only assuming that “the weather is fair” means exactly the same thing as “it is not raining” and vice versa. The whole point of symbolic logic as it was originally conceived is to divorce purely logical arguments from that sort of ambiguity of natural language. It is from that point view that we can assert the equivalence:
$$ (\Phi \rightarrow \Psi) \leftrightarrow (\neg \Phi \vee \Psi) $$
which could be rendered into English as, “Φ implies Ψ if and only if either Φ is false or Ψ is true.”
Basic Syntax
This informal syntax describes the sentential calculus as it is actually written by human beings on white boards and the like. See BackusNaur Form for the formal definition of the syntax of the sentential calculus, which is far more strict than described here but which is amenable to automatic proof procedures of the sort that could be carried out by computer algorithms.

An uppercase letter is a wellformed formula of the sentential calculus representing a primitive term that evaluates to a truth value, i.e. true (T) or false (F).

Any wellformed formula may be enclosed in parentheses for grouping purposes; when enclosed in parentheses, an entire formula can be used as an “inner” term in an “outer” formula involving other connectives.

A negation symbol (¬) followed by a term (a primitive term denoting an “atomic” sentence or a formula enclosed in parentheses) is a wellformed formula whose truth value is the opposite to that of the term following the negation symbol.

The sequence of a term, one of the connectives corresponding to axioms of symbolic logic and another term is a wellformed expression.
Examples
The sentence P, which may be true (T) or false (F):
$$ P $$
Another sentence, Q, which also may be true or false independently of the value of P:
$$ Q $$
The negation of P, i.e. ¬P is false if P is true, and viceversa:
$$ \neg P $$
Two sentences joined by a connective (“inclusive or”, in this case):
$$ P \vee Q $$
Grouping using parentheses:
$$ \neg \left( P \wedge Q \right) $$
A vacuously true statement (i.e. a tautology):
$$ \left( \neg P \vee \neg Q \right) \leftrightarrow \neg \left( P \wedge Q \right) $$
A way to visualize the grammar of the sentential calculus is by drawing formulas as tree diagrams. Here is such a tree diagram for the example of De Morgan’s Law just cited:
graph TB P1((P)) Q1((Q)) P2((P)) Q2((Q)) NOT1(("¬")) NOT2(("¬")) NOT3(("¬")) OR(("∨")) AND(("∧")) BICONDITIONAL(("→")) BICONDITIONAL > OR BICONDITIONAL > NOT3 OR > NOT1 OR > NOT2 NOT1 > P1 NOT2 > Q1 NOT3 > AND AND > P2 AND > Q2
If a node in such a tree corresponds to a primitive term, the truth value of the node is that of the primitive term. Otherwise, the truth value of a node is calculated by first evaluating the truth value(s) of the term(s) to which it is directly connected and then applying the appropriate row from the truth table for the nonterminal node. Applying such a procedure to the preceding diagram shows that the root node is always true without regard to the values of the terminal nodes.