Monadic Predicate Calculus
So far, we have considered only logical arguments composed entirely of “atomic” declarative sentences connected by simple logical operators like “not,” “and,” “or” and so on. Such arguments fail to represent the essence of most issues worth discussing, which intrinsically rely on the logic of generalization and the application of such generalizations to specific cases.
Consider Aristotle’s classic syllogism:

All humans are mortal.

Socrates is human.

Therefore, Socrates is mortal.
Based solely on the preceding section describing the sentential calculus, one might attempt to represent this as a simple case of modus ponens but what should the antecedent and consequent be?
What is lacking from the simple version of modus ponens discussed so far is the essence of this particular syllogism, which is the idea of declaring that all members of a class or set have some property and then using modus ponens to infer that a particular member of that class has that property.
Here is how the preceding syllogism should be represented using the monadic predicate calculus:
$$ \begin{array}{l} \forall x \left( H x \rightarrow M x \right) \\ H s \\ \hline \\ M s \end{array} $$
where:

Hχ is understood to mean “χ is human”

Mχ is understood to mean “χ* is mortal’

s is understood to refer to Socrates
A logician would render the first formula in the preceding version of the syllogism into English as something like, “For every x, if H of x then M of x.” This is the same as saying that everything in the universe is such that if it has the property H then it also has the property M.
The word “predicate” in “monadic predicate calculus” refers to terms like Hx and Ms in the preceding formulas. They amount to declarative sentences like the atomic symbols P, Q etc. in the sentential calculus except in the specific case of a sentence that ascribes some property to some object or entity. All of the same axioms, inference rules and so on of the sentential calculus apply asis to such predicates in the monadic predicate calculus.
Another way of understanding a predicate is as a function whose domain is every object or entity in the universe and whose range is the set of truth values. Hence the Fx syntax and “F of x” terminology.
The symbol ∀ is known as the “universal quantifier” and is used to declare that some formula is true of every member of the domain of discourse of some argument. The symbol ∃, on the other hand, is the “existential quantifier” and is used to assert that a given formula is true of at least one member of the domain of discourse, as in:
$$ \exists x \left( F x \rightarrow G x \right) $$
A logician would render the immediately preceding formula into English as something like, “there is an x such that if F of x then G of x.” If one were to replace ∀ with ∃ in the preceding syllogism, the argument would not be valid. The antecedent formula would become something like, “Some human beings are mortal” with no guarantee that Socrates is one of those human beings who happen to be destined to die.
In other words, both ∀ and ∃ are “variable binding operators.” Each defines a context within which a given variable is defined to refer to a single object or entity throughout that context, but no other contexts. A given variable like x in the first formula in the syllogism is said to be “bound” within the context of such a quantifier, while a variable like s in the second and third formulas are said to be “free.” When the same free variable appears in more than one formula in a single logical argument, it is assumed to refer to the same object or entity throughout. In other words, all free variables in an argument behave as if the whole argument were wrapped in implicit existential generalizations binding its free variables in an internally consistent fashion.
When carrying out proofs involving formulas that use such variable binding operators, the transformations that are allowed for each “move” in the “game” include rules by which generalizations can be inferred from particular cases as well as rules for how particular instances can be inferred from generalizations.
For example, the following is a valid inference that could appear within a proof:
$$ \begin{array}{l} H s \\ \hline \\ \exists x H x \\ \end{array} $$
This inference is known as existential generalization and its validity should be obvious. The following is a case of universal instantiation:
$$ \begin{array}{l} \forall x H x \\ \hline \\ H s \end{array} $$
You may use any free variable when applying universal instantiation, since the whole point of the universal quantifier is that it makes statements that are true of everything in the universe.
Existential instantiation is far more restrictive. In this case, you may not use any free variable that appears in any unboxed or canceled line in a proof so as to avoid making false assumptions as to exactly which entities do and do not have a given property. For example, the following is valid:
$$ \begin{array}{l} \exists x H x \\ H s \\ \hline \\ H a \end{array} $$
Had the conclusion used the free variable s the result would not be a valid inference. Care must be taken to follow these kinds of logically valid rules when using variable binding operators in proofs, as in the preceding examples. As already alluded to, the hypothetical variant of the syllogism in which the universal quantifier were replaced with the existential quantifier would not be valid because the two quantifiers have different rules for how they can be instantiated.
Another way of saying this is that both the universal and existential quantifier symbols denote generalizations, but the logic of how each type of generalization can be applied to particular circumstances are different.
Formulas can contain more than one bound variable. For example:
$$ \forall x y \left( F x \rightarrow G y \right) $$
which reads as something like, “For every x and y, if F of x then G of y.”
Different variables in a single formula can be bound by different quantifiers, as in:
$$ \forall x \exists y \left( F x \rightarrow G y \right) $$
which reads as something like, “For every x there exists some y such that if F of x then G of y.”
When applying such complex generalizations to particular circumstances, the appropriate rules must be followed when instantiating each bound variable according to the rules for the particular quantifier by which it is bound. For example, when instantiating the immediately preceding formula one can substitute any free variable for x but must choose a new free variable that does not yet appear anywhere in the proof as a substitute for y.
Here is the proof for the syllogism using the preceding rules:
$$ \begin{array}{llll} 1. & \sout{Show} & M s & 5, \text{direct proof} \\ \end{array} $$
$$ \begin{array}{llll} \hline \\ 2. & & \forall x (H x \rightarrow M x) & \text{premise} \\ 3. & & H s & \text{premise} \\ 4. & & H s \rightarrow M s & 2, \text{universal} \\ 5. & & M s & 3, 4, \text{modus ponens} \\ \hline \end{array} $$
It is worth emphasizing: had line 3 been ∃x(Hx → Mx) then the inference in line 4 could have used any free variable except s and so the proof could not have proceeded and that proposed syllogism would have been invalid.
Let us return to the very first symbolic argument discussed earlier. In the text surrounding that example, it was pointed out that P → Q means that P implies Q according to the axioms of symbolic logic, but any attempt to apply from that overly simplistic interpretation of modus ponens to any argument about a state of affairs in the real world would likely prove unsatisfactory since a posteriori truth as described by natural language arguments is far messier and more complicated than can be captured by the sentential calculus. The monadic predicate calculus begins to flesh out symbolic logic with some tools necessary to mitigate at least some of these deficiencies.
In particular, consider the proposed identity of the natural language argument:

If it is raining, the streets are wet.

It is raining.

Therefore, the streets are wet.
with the symbolic argument:
$$ \begin{array}{l} P \rightarrow Q \\ P \\ \hline \\ Q \end{array} $$
The claim made by traditional logic is that one ought to be able to deduce whether or not the streets are actually wet by
 Confirming whether or not it is actually raining.
 Appealing to modus ponens as exemplified by the given argument expressed in the sentential calculus.
No need to risk a cold by going out and actually checking the state of the streets. It just doesn’t get more Aristotelian than that!
The trouble, of course, is obvious. Where is it raining, and what counts as “rain” to start with? (Is a “drizzle” sufficient? How about heavy dew?) And what about these “streets?” Is there no stretch of road anywhere that might be shielded from the rain by passing under a bridge, through a tunnel etc.?
To begin addressing these sorts of complexities and ambiguities, we need to deploy the machinery of the monadic predicate calculus. The following comes much closer to expressing the actual realworld situation for even this simplest of syllogisms:
$$ \begin{array}{l} \text{Let } & S \chi & = & \chi \text{ is a segment of a street} \\ & C \chi & = & \chi \text{ is shielded from the rain} \\ & W \chi & = & \chi \text{ is wet} \\ & R \chi & = & \chi \text{ is within a geographic region where} \\ & & & \text{the level of precipitation meets the} \\ & & & \text{criteria for "rain"} \end{array} $$
$$ \begin{array}{l} \forall x ((S x \wedge R x \wedge \neg C x) \rightarrow W x) \\ S a \wedge R a \wedge \neg C a \\ \hline \\ W a \end{array} $$
Even then, any good trial lawyer would be able to raise at least the specter of “reasonable doubt.” After all, what if it were only a very light rain and a work crew with leaf blowers were deployed to keep an exposed stretch of road dry?
We could fix this by changing Cx to mean something like “there is no covering or mechanism deployed to keep x dry.” Too many successive applications of this process, however, raises the danger of turning an empirical argument into a tautology along the lines of “when there is no possibility of a stretch of road being dry, it is wet.”