Propositional Calculus Proofs (10)

Th35.) (I ⇒ J), (J ⇒ I) ⊢ (I ⇔ J)
1.) ⊢ I ⇒ J                                                                      Hyp
2.) ⊢ J ⇒ I                                                                      Hyp
3.) ⊢ (I ⇒ J) ⇒ [(J ⇒ I) ⇒ ((I ⇒ J) ∧ (J ⇒ I))]            Th30
4.) ⊢ (J ⇒ I) ⇒ ((I ⇒ J) ∧ (J ⇒ I))                                MP 1,3
5.) ⊢ (I ⇒ J) ∧ (J ⇒ I)                                                   MP 2,4
6.) ⊢ (I ⇔ J)                                                                  Definition of ⇔

Th36.) H ⇔ K ⊢ K ⇔ H  Symmetry of ⇔
1.) ⊢ H ⇔ K                                                                     Hyp
2.) ⊢ (H ⇒ K) ∧ (K ⇒ H)                                                 Definition of ⇔
3.) ⊢ [(H ⇒ K) ∧ (K ⇒ H)] ⇒ [(K ⇒ H) ∧ (H ⇒ K)]       Th27
4.) ⊢ (K ⇒ H) ∧ (H ⇒ K)                                                 MP 2,3
5.) ⊢ K ⇔ H                                                                     Definition of ⇔

Th37.) (H ⇔ K), (K ⇔ L) ⊢ (H ⇔ L)  Transitivity of ⇔
1.) H ⇔ K                                                                        Hyp
2.) K ⇔ L                                                                         Hyp
3.) ⊢ (H ⇒ K) ∧ (K ⇒ H)                                                 Definition of ⇔
4.) ⊢ (K ⇒ L) ∧ (L ⇒ K)                                                   Definition of ⇔
5.) ⊢ [(H ⇒ K) ∧ (K ⇒ H)] ⇒ (K ⇒ H)                            Th28
6.) ⊢ [(H ⇒ K) ∧ (K ⇒ H)] ⇒ (H ⇒ K)                            Th29
7.) ⊢ (K ⇒ H)                                                                    MP 3,5
8.) ⊢ (H ⇒ K)                                                                   MP 3,6
9.) ⊢ [(K ⇒ L) ∧ (L ⇒ K)] ⇒ (L ⇒ K)                                Th28
10.) ⊢ [(K ⇒ L) ∧ (L ⇒ K)] ⇒ (K ⇒ L)                              Th29
11.) ⊢ (L ⇒ K)                                                                    MP 4,9
12.) ⊢ (K ⇒ L)                                                                   MP 4,10
13.) ⊢ (H ⇒ L)                                                                   Th5
14.) ⊢ (L ⇒ H)                                                                   Th5
18.) ⊢ H ⇔ L                                                                     Th35

Investigation of Formulae in Predicate Calculus (5)

Allow the universe, to literally be the universe. Now consider the following formula: 

∃x{∃y[¬(x = y)]}. There exists something call it x and there exists something call it y, it turns out it is not the case that x is the same thing as y. This construction is a strange way to say the number two!

Investigation of Formulae in Predicate Calculus (4)

∀x[∀y(xRy)] states that everything in the universe bares the relationship R to everything else in the universe. If I switch the positions of x and y, then the formula still makes the same claim. ∀y[∀x(xRy)] switches x and y in the quantifiers but yet again the meaning remains the same.

∀x[∃y(xRy)] makes both a universal claim as well as an existential claim. It states that for any possible thing x in the universe, there exists another thing y such that x bares relation R to y. If R is taken to be the predicate <, then ∀x[∃y(x<y)] is true if our universe is the set of all natural numbers. Switching x and y yields ∀x[∃y(y<x)] which turns out to be false if our universe remains but is true if we expand our universe to be the set of all integers. Swapping x and y in the quantifiers produces ∀y[∃x(x<y)] which turns out to mean the same thing as ∀x[∃y(y<x)] because the variable associated with each quantifier is in the same position in the atomic formula.

∃x[∀y(xRy)] if R is taken to be =, then ∃x[∀y(x = y)]. This statement says at least one thing exists in the universe such that it is equal to everything else in the universe. This statement is true in a one element universe because that element is both something and everything.

∃x[∃y(xRy)] means that at least one x and at least one y exist such that x bares R to y. Replace R with ∈ and the formula claims that something is a member of something else.

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[( ) ⇔ ( )]}