Back to Basics (0)

The symbol '⇒' is a logical connective. It represents what is called a logical implication. If A and B are wff's (well-formed formulae pronounced whiff's or whiff for wff) and A ⇒ B, then A is called the antecedent of A ⇒ B and B is called the consequent. The converse of A ⇒ B is B ⇒ A. The contraposition  is ¬B ⇒ ¬A. The Law of Contraposition  states (¬B ⇒ ¬A) ⇒ (A ⇒ B).

The aphabet I use is as follows:

An atomic formula in set theory is a sequence of three symbols: variable or constant, relation, variable or constant. Infix notation places the connective or relation between the variable or constant, prefix the connective or relation to the left, and postfix to the right of the variable or constant.

Any variable can be a wff (well-formed formula) and each atomic formula is a wff, or if P and Q are wff's and for every variable X, then all of the following formulae are also wff's:

Only strings of symbols built from atomic formula and formulae F1 - F7 are wff's. Formulae F1 through F7 are component formula  and P and Q are the components. These component are called propositional variables. If X occurs after a quantifier, then X is an operator variable otherwise it is an individual variable. For each P, Q, and X, the symbols P and Q are propositional forms, the formulae F1 - F5 are propositional forms, and only formulae built from F1 - F5 are propositional forms. Lastly, a logical formula is either a wff or a propositional form.

Centering

Buchstaben

Gelegentlich ergreifen wir die Feder
Und schreiben Zeichen auf ein weisses Blatt,
Die Sagan dies und das, es kennt sie jeder,
Es ist ein Spiel, das seine Regeln hat.

                     H. Hesse, "Buchstaben"


We now and then take pen in hand
And make some marks on empty paper.
Just what they say, all understand.
It is a game with rules that matter.

                     H. Hesse, "Alphabet" (translated by Prof. Richard S. Ellis)

Proof Positive

CIC Proofs (4)

Th11) ⊢ (Q ⇒ R) ⇒ [(P ⇒ Q) ⇒ (P ⇒ R)]
2.) ⊢ (Q ⇒ R) ⇒ {[P ⇒ (Q ⇒ R)] ⇒ [(P ⇒ Q) ⇒ (P ⇒ R)]}                           Th1
3.) ⊢ {(Q ⇒ R) ⇒ [P ⇒ (Q ⇒ R)]} ⇒ {(Q ⇒ R) ⇒ [(P ⇒ Q) ⇒ (P ⇒ R)]}     Th2
4.) ⊢ (Q ⇒ R) ⇒ ( P ⇒ (Q ⇒ R))                                                                        Lk1
5.) ⊢ (Q ⇒ R) ⇒ [( P ⇒ Q ) ⇒ ( P ⇒ R )]                                                         MP 3,4

CIC Proofs (3)

Th8) (P ⇒ Q), (Q ⇒ R), (R ⇒ S) ⊢ (P ⇒ S)

1.) ⊢ P ⇒ Q                        Hyp

2.) ⊢ Q ⇒ R                       Hyp

3.) ⊢ P ⇒ R                       Th5

4.) ⊢ R ⇒ S                        Hyp

5.) ⊢ P ⇒ S                         Th5 

Th9) H ⇒ (K ⇒ L), H ⇒ [K ⇒ (L ⇒ M)] ⊢ H ⇒ (K ⇒ M)

1.) ⊢ H ⇒ [K ⇒ (L ⇒ M)]                                                   Hyp

2.) ⊢ [K ⇒ ( L ⇒ M )] ⇒ [( K ⇒ L ) ⇒ ( K ⇒ M )]           Lk2

3.) ⊢ H ⇒ [( K ⇒ L ) ⇒ ( K ⇒ M )]                                   Th5

4.) ⊢ [H ⇒ ( K ⇒ L )] ⇒ [H ⇒ ( K ⇒ M )]                       Th2

5.) ⊢ H ⇒ (K ⇒ L)                                                               Hyp

6.) ⊢ H ⇒ ( K ⇒ M )                                                          MP 4,5

Th10) ⊢ [P ⇒ (P ⇒ Q)] ⇒ (P ⇒ Q)
1.) ⊢ P ⇒ P                                                               Th3
2.) ⊢ [P ⇒ (P ⇒ Q)] ⇒ P ⇒ P                                Th1
3.) ⊢ [P ⇒ (P ⇒ Q)] ⇒ [(P ⇒ P) ⇒ (P ⇒ Q)]       Lk2
4.) ⊢ [P ⇒ (P ⇒ Q)] ⇒ (P ⇒ Q)                            Th4

CIC Proofs (2)

Th6) K, H ⇒ ( K ⇒ L ) ⊢ H ⇒ L
1.) ⊢ [H ⇒ ( K ⇒ L )] ⇒ [( H ⇒ K ) ⇒ ( H ⇒ L )]      Lk2
2.) ⊢ H ⇒ ( K ⇒ L )                                                        Hyp
3.) ⊢ ( H ⇒ K ) ⇒ ( H ⇒ L )                                          MP 1,2
4.) ⊢ K                                                                              Hyp
5.) ⊢ H ⇒ K                                                                     Th1
6.) ⊢ H ⇒ L                                                                     MP 3,5

Th7) P ⇒ Q, P ⇒ ( Q ⇒ R ), P ⇒ ( R ⇒ S ) ⊢ P ⇒ S
1.) ⊢ P ⇒ Q                                         Hyp
2.) ⊢ P ⇒ ( Q ⇒ R )                           Hyp
3.) ⊢ P ⇒ R                                         Th4
4.) ⊢ P ⇒ ( R ⇒ S )                            Hyp
5.) ⊢ P ⇒ S                                          Th4