Investigation of Formulae in Predicate Calculus (3)

(nested quantifiers)

∀x[∀y( )]     ∀y[∀x( )]    ∀x[∃y( )]    ∀y[∃x( )]     ∃x[∀y( )]     ∃y[∀x( )]    ∃x[∃y( )]     ∃y[∃x( )]

¬∀x[∀y( )]   ∀x[¬∀y( )]   ∀x[∀y(¬ )]   ¬∀x[¬∀y( )]  ¬∀x[∀y(¬ )]   ∀x[¬∀y(¬ )]   ¬∀x[¬∀y(¬ )]
∀x[( ) ∧ ∀y( )]    ∀x[∀y( ) ∧ ( )]    ∀x{∀y[( ) ∧ ( )]}

∀x[( ) ∨ ∀y( )]    ∀x[∀y( ) ∨ ( )]    ∀x{∀y[( ) ∨ ( )]}

∀x[( ) ⇒ ∀y( )]    ∀x[∀y( ) ⇒ ( )]    ∀x{∀y[( ) ⇒ ( )]}

∀x[( ) ⇔ ∀y( )]    ∀x[∀y( ) ⇔ ( )]    ∀x{∀y[( ) ⇔ ( )]}

¬∀y[∀x( )]   ∀y[¬∀x( )]   ∀y[∀x(¬ )]     ¬∀y[¬∀x( )]  ¬∀y[∀x(¬ )]   ∀y[¬∀x(¬ )]   ¬∀y[¬∀x(¬ )]

∀y[( ) ∧ ∀x( )]    ∀y[∀x( ) ∧ ( )]    ∀y{∀x[( ) ∧ ( )]}

∀y[( ) ∨ ∀x( )]    ∀y[∀x( ) ∨ ( )]    ∀y{∀x[( ) ∨ ( )]}

∀y[( ) ⇒ ∀x( )]    ∀y[∀x( ) ⇒ ( )]    ∀y{∀x[( ) ⇒ ( )]}

∀y[( ) ⇔ ∀x( )]    ∀y[∀x( ) ⇔ ( )]    ∀y{∀x[( ) ⇔ ( )]}

¬∀x[∃y( )]   ∀x[¬∃y( )]   ∀x[∃y(¬ )]    ¬∀x[¬∃y( )]  ¬∀x[∃y(¬ )]   ∀x[¬∃y(¬ )]   ¬∀x[¬∃y(¬ )]

∀x[( ) ∧ ∃y( )]    ∀x[∃y( ) ∧ ( )]    ∀x{∃y[( ) ∧ ( )]}

∀x[( ) ∨ ∃y( )]    ∀x[∃y( ) ∨ ( )]    ∀x{∃y[( ) ∨ ( )]}

∀x[( ) ⇒ ∃y( )]    ∀x[∃y( ) ⇒ ( )]    ∀x{∃y[( ) ⇒ ( )]}

∀x[( ) ⇔ ∃y( )]    ∀x[∃y( ) ⇔ ( )]    ∀x{∃y[( ) ⇔ ( )]}

¬∀y[∃x( )]   ∀y[¬∃x( )]   ∀y[∃x(¬ )]   ¬∀y[¬∃x( )]  ¬∀y[∃x(¬ )]   ∀y[¬∃x(¬ )]   ¬∀y[¬∃x(¬ )]

∀y[( ) ∧ ∃x( )]    ∀y[∃x( ) ∧ ( )]    ∀y{∃x[( ) ∧ ( )]}

∀y[( ) ∨ ∃x( )]    ∀y[∃x( ) ∨ ( )]    ∀y{∃x[( ) ∨ ( )]}

∀y[( ) ⇒ ∃x( )]    ∀y[∃x( ) ⇒ ( )]    ∀y{∃x[( ) ⇒ ( )]}

∀y[( ) ⇔ ∃x( )]    ∀y[∃x( ) ⇔ ( )]    ∀y{∃x[( ) ⇔ ( )]}

¬∃x[∀y( )]   ∃x[¬∀y( )]   ∃x[∀y(¬ )]   ¬∃x[¬∀y( )]  ¬∃x[∀y(¬ )]   ∃x[¬∀y(¬ )]   ¬∃x[¬∀y(¬ )]

∃x[( ) ∧ ∀y( )]    ∃x[∀y( ) ∧ ( )]    ∃x{∀y[( ) ∧ ( )]}

∃x[( ) ∨ ∀y( )]    ∃x[∀y( ) ∨ ( )]    ∃x{∀y[( ) ∨ ( )]}

∃x[( ) ⇒ ∀y( )]    ∃x[∀y( ) ⇒ ( )]    ∃x{∀y[( ) ⇒ ( )]}

∃x[( ) ⇔ ∀y( )]    ∃x[∀y( ) ⇔ ( )]    ∃x{∀y[( ) ⇔ ( )]}

¬∃y[∀x( )]   ∃y[¬∀x( )]   ∃y[∀x(¬ )]   ¬∃y[¬∀x( )]  ¬∃y[∀x(¬ )]   ∃y[¬∀x(¬ )]   ¬∃y[¬∀x(¬ )]

∃y[( ) ∧ ∀x( )]    ∃y[∀x( ) ∧ ( )]    ∃y{∀x[( ) ∧ ( )]}

∃y[( ) ∨ ∀x( )]    ∃y[∀x( ) ∨ ( )]    ∃y{∀x[( ) ∨ ( )]}

∃y[( ) ⇒ ∀x( )]    ∃y[∀x( ) ⇒ ( )]    ∃y{∀x[( ) ⇒ ( )]}

∃y[( ) ⇔ ∀x( )]    ∃y[∀x( ) ⇔ ( )]    ∃y{∀x[( ) ⇔ ( )]}

¬∃x[∃y( )]   ∃x[¬∃y( )]   ∃x[∃y(¬ )]  ¬∃x[¬∃y( )]  ¬∃x[∃y(¬ )]   ∃x[¬∃y(¬ )]   ¬∃x[¬∃y(¬ )]

∃x[( ) ∧ ∃y( )]    ∃x[∃y( ) ∧ ( )]    ∃x{∃y[( ) ∧ ( )]}

∃x[( ) ∨ ∃y( )]    ∃x[∃y( ) ∨ ( )]    ∃x{∃y[( ) ∨ ( )]}

∃x[( ) ⇒ ∃y( )]    ∃x[∃y( ) ⇒ ( )]    ∃x{∃y[( ) ⇒ ( )]}

∃x[( ) ⇔ ∃y( )]    ∃x[∃y( ) ⇔ ( )]    ∃x{∃y[( ) ⇔ ( )]}

¬∃y[∃x( )]   ∃y[¬∃x( )]   ∃y[∃x(¬ )]   ¬∃y[¬∃x( )]  ¬∃y[∃x(¬ )]   ∃y[¬∃x(¬ )]   ¬∃y[¬∃x(¬ )]

∃y[( ) ∧ ∃x( )]    ∃y[∃x( ) ∧ ( )]    ∃y{∃x[( ) ∧ ( )]}

∃y[( ) ∨ ∃x( )]    ∃y[∃x( ) ∨ ( )]    ∃y{∃x[( ) ∨ ( )]}

∃y[( ) ⇒ ∃x( )]    ∃y[∃x( ) ⇒ ( )]    ∃y{∃x[( ) ⇒ ( )]}

∃y[( ) ⇔ ∃x( )]    ∃y[∃x( ) ⇔ ( )]    ∃y{∃x[( ) ⇔ ( )]}

Investigation of Formulae in Predicate Calculus 2

The most basic formula in Predicate Calculus is of the Form P. It is a true-false statement represented by an uppercase letter. Alternatively, P can have n terms written Pp1,...,pn. An infinite list of atomic formula can be generated and given the rules for constructing wff's the set of all meaningful formulae in Predicate Calculus can be constructed. However, not all wff's are of interest. Examine the following.

Px, Qx, Lxy ∀x(Px), ∃x(Px), ∀x(Px ⇒ Qx), ∀x[∃y(Lxy)]

To begin to understand what these formulas mean, first define the set of objects the terms in each formula can refer to. I like mathematics, so, I use numbers. I call this set the Universe.

Use the following interpretation:

The Universe: The natural numbers
Px: x is prime.
Qx: x is rational.
Lxy: x is less than y.

Thus ∀x(Px) means that everything is prime. Clearly this is a false statement. There exists at least one composite number. ∃x(Px) means a prime number exists. This is a true statement. ∀x(Px ⇒ Qx) means that any object in the universe is a rational if it is prime. This too is a true statement. ∀x[∃y(Lxy)] is perhaps the most interesting. It says there is no largest number. This is true because one can always find a number y such that for any choice of x, x is less than y. In this context the universe is infinite but there is no reason why we can't restrict our universe. Or change the universe to say the integers or maybe even go as far as the real numbers.

Investigation of Formulae in Predicate Calculus

These are the elements that I use for Predicate Calculus

Ø 

A ... Z (with or without scripts)

 a ... z (with or without scripts)

∈ , = 

∀ , ∃ 

¬ , ∧ , ∨ , ⇒ , ⇔ 

( , ) , [ , ] , { , }

Expressions in Predicate Calculus include any finite sequence of the elements listed above.

Examples:         Ø∃⇒⇒              ¬ [∈∀               A = B

An atomic formula in Predicate Calculus is either an atomic formula from Propositional Calculus or an expression of the form Q(q1, q2, ... ,qn) where Q is an n-place predicate with q1, q2, ... , qn as terms. However, in the special case of the two place predicates ∈ and =, terms are placed on the left and right side of the predicates.

Examples:         P         Ua         Yxz           X ∈ Y           A = B

The terms of a Predicate can be either a constant or a variable. I take u, v, w, x, y, z upper and lowercase with or without scripts to represent variables and the rest of the alphabet with or without scripts both upper and lowercase as constants. 

1.) Every atomic formula of Predicate Calculus is a wff of Predicate Calculus.

2.) If P is a wff, then ¬P is a wff.

3.) If P and Q are wff's, then P ∧ Q, P ∨ Q, P ⇒ Q, and P ⇔ Q are wff's.

4.) If P is a wff that contains at least one occurrence of x and no x-quantifier, then ∀x(P) and ∃x(P) are both wff's.

Nothing is a wff of Predicate Calculus unless it can be formed by repeated applications of 1 - 4.

Now it's time to make some wff's!

Predicate Calculus (0)

The symbol '∈' is a predicate according to set theory. It reads "is a member of" or "is an element of". A sequence of three symbols containing a variable or a constant, then the predicate ∈, and again a variable or a constant is an atomic formula. The only constant in set theory is Ø. So, there exist four atomic formulae.

Ø ∈ Ø , Ø ∈ X , X ∈ Ø , X ∈ Y

The truth value of X ∈ Y is indeterminate because different substitutions for the variables X and Y yield different values. 

⊨P indicates that the formula P is universally valid (is true regardless of its variables) and there exists a proof of P that may require not only the use of propositional calculus but also predicate calculus.

A variable is an individual variable if and only if it occurs in an atomic formula involving predicates. A variable is a propositional variable if and only if it occurs in a propositional form involving logical connectives.

The symbols ∀ and ∃ are quantifiers and only individual variables are permitted to immediately follow these symbols. Example: If P is a logical formula and X is an individual variable then ∀X(P) and ∃X(P) are valid constructions. 

If X is an individual variable that occurs in a logical formula P, then X is bound in P if and only if X occurs immediately after a quantifier, or between ∀X( or ∃X( and its corresponding parenthesis ). X is free in P if and only if X is not bound in P. A logical formula is closed if and only if it does not contain any free variables. A logical sentence is a closed logical formula.

Subf(X,Z)P is the formula that results from substituting every free occurrence of X in P by Z assuming that X is a variable that does not already occur in P. Subb(X,Z)P is the formula that results from substituting every bound occurrence of X in P by Z. 

Propositional Calculus Proofs (9)

Th31) ⊢ (H ⇒ K) ⇒ {(H ⇒ L) ⇒ [H ⇒ (K ∧ L)]}

1.) ⊢ {H ⇒ [K ⇒ (L ⇒ (K ∧ L))]} ⇒ {(H ⇒ K) ⇒ [H ⇒ (L ⇒ (K ∧ L))]}                    Lk2

2.) ⊢ [H ⇒ (L ⇒ (K ∧ L))] ⇒ [(H ⇒ L) ⇒ (H ⇒ (K ∧ L))]                                         Lk2

3.) ⊢ {H ⇒ [K ⇒ (L ⇒ (K ∧ L))]} ⇒ {(H ⇒ K) ⇒ [(H ⇒ L) ⇒ (H ⇒ (K ∧ L))]}       Th14

4.) ⊢ K ⇒ (L ⇒ (K ∧ L))                                                                                               Th30

5.) ⊢ H ⇒ {K ⇒ [L ⇒ (K ∧ L)]}                                                                                   Th1

6.) ⊢ (H ⇒ K) ⇒ {(H ⇒ L) ⇒ [H ⇒ (K ∧ L)]}                                                             MP 3,5

Th32) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ L)

1.) ⊢ (K ∧ L) ⇒ L                                                                          Th28

2.) ⊢ H ⇒ [(K ∧ L) ⇒ L]                                                              Th1

3.) ⊢ {H ⇒ [(K ∧ L) ⇒ L]} ⇒ {[H ⇒ (K ∧ L)] ⇒ (H ⇒ L)}        Lk2

4.) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ L)                                                   MP2,3

Th33) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ K)

1.) ⊢ (K ∧ L) ⇒ K                                                                          Th29

2.) ⊢ H ⇒ [(K ∧ L) ⇒ K]                                                              Th1

3.) ⊢ {H ⇒ [(K ∧ L) ⇒ K]} ⇒ {[H ⇒ (K ∧ L)] ⇒ (H ⇒ K)}        Lk2

4.) ⊢ [H ⇒ (K ∧ L)] ⇒ (H ⇒ K)                                                   MP2,3

Th34) ⊢ P ⇒ (P ∧ P)     Idempotency of ∧

1.) ⊢ (P ⇒ P) ⇒ {(P ⇒ P) ⇒ [P ⇒ (P ∧ P)]}                                  Th31

2.) ⊢ P ⇒ P                                                                                     Th3

3.) ⊢ (P ⇒ P) ⇒ [P ⇒ (P ∧ P)]                                                       MP 1,2

4.) ⊢ P ⇒ (P ∧ P)                                                                            MP 2,3