Sunday, May 15, 2016

About Proofs

Definition: A sequent is an expression (A ⊢ C) where C is a statement called the conclusion of the sequent and A is a set of statements called the assumptions of the sequent. (A ⊢ C) is read 'A entals C' and means that there is a proof whose conclusion is C and whose undischarged assumptions are all in the set A. (⊢ C) means there is a proof of C relying on no undischarged assumptions.

Sequent Rule (∧I): If (A ⊢ C) and (B ⊢ D), then [(A ⋃ B) ⊢ (C ∧ D)].

Sequent Rule (∧E): If  [A ⊢ (B ∧ C)], then (A ⊢ B) and (A ⊢ C).

Sequent Rule (⇒I): If [A ⋃ {b} ⊢ C], then [A ⊢ (b ⇒ C)].

Sequent Rule (⇒E): If (A ⊢ C) and [B ⊢ (C ⇒ D)], then [(A ⋃ B) ⊢ D]


Just Kidding

I found a more appropriate textbook than Hurley's. It's title is Mathematical Logic and it is written by Ian Chriswell. 

Friday, May 13, 2016

Examples of Proofs with Quantifiers

∀x(Ax ⇒ Bx), ∀x(Bx ⇒ Cx) ⊢ ∀x(Ax ⇒ Cx)
1.) ∀x(Ax ⇒ Bx)                   Hyp
2.) Ax ⇒ Bx                          UI
3.) ∀x(Bx ⇒ Cx)                   Hyp
4.) Bx ⇒ Cx                          UI
5.) Ax ⇒ Cx                          Th5
6.) ∀x(Ax ⇒ Cx)                   UG

∀x(Bx ⇒ Cx), ∃x(Ax ∧ Bx) ⊢ ∃x(Ax ∧ Cx)
1.) ∃x(Ax ∧ Bx)                        Hyp
2.) ∀x(Bx ⇒ Cx)                      Hyp
3.) Ac ∧ Bc                               EI
4.) (Ac ∧ Bc) ⇒ Bc                  Th28
5.) (Ac ∧ Bc) ⇒ Ac                   Th29
6.) Bc                                        mp 3,4
7.) Ac                                        mp 3,5
8.) Bc ⇒ Cc                               UI
9.) Cc                                        mp 6,8
10.) Ac ⇒ [ Cc ⇒ (Ac ∧ Cc)]    Th30
11.) Cc ⇒ (Ac ∧ Cc)                  mp 7,10
12.) (Ac ∧ Cc)                          mp 9,11
13.) ∃x(Ax ∧ Cx)                      EG

Rules of Inference for Quantifiers

Universal Instantiation (UI)
The operation of deleting the universal quantifier and replacing every variable bound by that quantifier with a constant or a variable. 

Universal Generalization (UG)
The operation of adding a universal quantifier to a formula possessing at least one occurrence of a variable to be quantified. This rule cannot be applied to constants.

Existential Instantiation (EI)
The operation of deleting the existential quantifier and replacing in each occurrence of the variable with a constant. The existential name or constant to be used must be a new name that has not occurred in any previous lines in the proof.

Existential Generalization (EG)
The operation of adding a existential quantifier to a formula possessing either a constant or a variable and replacing it with a new quantified variable.

Predicate Logic Translations (2)

19.) Whoever is a socialite is vain: ∀x(Sx ⇒ Vx)
20.) Any caring mother is vigilant and nurturing: ∀y[(Cy ∧ My) ⇒ (Vy ∧ Ny)]
21.) Terrorists are neither rational nor empathic: ∀z[Tx ⇒ (¬Rx ∧ ¬Ex)
22.) Nobody consumed by jealousy is happy: ¬∃y(Cy ∧ Hy)
23.) Everything is imaginable: ∀w(Iw)
24.) Ghosts do not exist: ¬∃z(Gz)
25.) A thoroughbred is a horse: ∀y(Ty ⇒ Hy)
26.) A thoroughbred won the race: ∃z(Tz ∧ Wz)
27.) Not all mushrooms are edible: ∃x(Mx ∧ ¬Ex)
28.) Not any horse chestnuts are edible: ∀w(Hw ⇒ ¬Ew)
29.) A few guests arrived late: ∃x(Gx ∧ Ax)
30.) None but gentlemen prefer blondes: ∀x(Px ⇒ Gx)
31.) A few cities are neither safe nor beautiful: ∃w[(Cw ∧ ¬Sw) ∧ ¬Bw]
32.) There are no circular triangles: ¬∃z(Cz ∧ Tz)
33.) Snakes are harmless unless they have fangs: ∀x[(Sx ∧ Fx) ⇒ ¬Hx]
34.) Some dogs bite if and only if they are teased: ∃y[(Dy ∧ By) ⇔ Ty]
35.) An airliner is safe if and only if it is properly maintained: ∀z[(Az ∧ Sz) ⇔ Pz]

Thursday, May 12, 2016

Predicate Logic Translations (1)

1.) Elaine is a chemist: Ce
2.) Nancy is not a sales clerk: ¬Sn
3.) Neither Wordsworth nor Shelley was Irish: ¬Iw ∧ ¬Is
4.) Rachel is either a journalist or a newscaster: (Jr ∨ Nr) ∧ ¬(Jr ∧ Nr)
5.) Intel designs a faster chip only if Micron does: Dm ⇒ Di
6.) Belgium and France subsidize the arts only if Austria or Germany expand museum holdings: (Ea ∨ Eg) ⇒ (Sb ∧ Sf)
7.) All maples are trees: ∀x(Mx ⇒ Tx)
8.) Some grapes are sour: ∃x(Gx ∧ Sx)
9.) No novels are biographies: ¬∃y(Ny ∧ By)
10.) Some holidays are not relaxing: ∃z(Hz ∧ ¬Rz)
11.) If Gertrude is correct, then the Taj Mahal is made of marble: Cg ⇒ Mt
12.) Gertrude is not correct only if the Taj Mahal is made of granite: Gt ⇒ ¬Cg
13.) Tigers exist: ∃z(Tz)
14.) Anything that leads to violence is wrong: ∀x(Lx ⇒ Wx)
15.) There are pornographic art works: ∃u(Pu ∧ Au)
16.) Not every smile is genuine: ¬∀x(Sx ⇒ Gx)
17.) Every penguin loves ice: ∀z(Pz ⇒ Lz)
18.) There is trouble in River City: ∃u(Tu ∧ Ru) 

Wednesday, May 11, 2016

Textbook Found

I finally found a textbook that I can trust. I've been through quite a few. The predicate logic presented in this textbook is user friendly and more for philosophy but is just as valid as any mathematical presentation. So, I'm going to go with my new textbook and trust it. Besides it's from Patrick J. Hurley. He's been writing textbooks for decades.