Module: Predicate logic
Quote of the page

Popular pages
In these tutorials we will work with a simpler version of predicate logic (using only oneplace predicate letters). We will call this monadic predicate logic, or MPL. Let us first define the language of MPL more precisely:
The language of MPL contains the following symbols:
An expression of MPL is a string of one or more symbols of MPL.
The syntactic rules, or formation rules (rules of formation), for MPL are as follows :
Rule #1 tells us that expressions such as "R", "Pa", "Qb", "Gc" are wffs.
Rule #2 tells us that expressions such as "R", "P", "Q" are sentence letters, and "Pa", "Qb", "Gx" are not.
Rules #3 and #4 are just like rules from SL. We can apply them to form new wffs such as "~~Pa", "~((Pa&Sc)↔(~Q∨Ka))".
Part (b) of rule #4 is meant to rule out cases such as "(Pa&P)" as wff. Reason: This expression is formed from "Pa" and "P". They include the same predicate letter "P". But the first occurrence of "P" is not a sentence letter even though the second one is. So according to 4(b) they cannot be combined to form a wff. But the rule allows "(Pa&Pb)" to be a wff. "(P&P)" is also a wff.
Rule #5 is a little complicated. It applies only to wffs that include at least one name. So it applies to expressions such as "Qa", "(~Pa→Qb)", "(Pa&Qa)", but not "∃xFx". The rule says that we can pick a name in a wff, replace one or more occurrences of that name by a single variable, and then add either an existential or universal quantifier to the front. Here are some examples:
A complex wff in MPL is any wff that contains a quantifier or a connective. To show how a complex wff is constructed, we can draw a construction tree for that wff. A construction tree is a tree diagram with arrows linking wffs. Starting with noncomplex wffs at the top, the diagram shows how a complex wff can be built up stepbystep using the formation rules of MPL. Here for example is a construction tree for "~(P&~Fa)" :
We started off with "P" and "Fa" which are not noncomplex wffs. An arrow from X to Y indicates that Y can be constructed from X by applying one of the formation rules. Similarly, an arrow from X and Y to Z indicates that Z can be constructed from X and Y. By drawing a construction tree for a wff we show clearly how the formation rules are used to build up the wff. As a second example here is a construction tree for "~∀x(P&~Fx)" :
Of course, in this second example, we could have started off with "Fb" instead. So sometimes (not always) a wff can have more than one construction tree.
If any of these expressions is a WFF of MPL, draw its construction tree:
Do wffs in MPL have unique construction trees? In other words, given any wff in MPL, is it true that there is only one single construction tree that can be drawn for the wff? Why or why not?