Let's think about animals. Clearly every refrigerator is a monkey because, when we only think about animals, there are no refrigerators. domain: animals R(x): ____x is a refrigerator M(x): ____x is a monkey ∀ R(x) → M(x) The hospital will only hire a skilled surgeon. All surgeons are greedy. Billy is a surgeon, but is not skilled. Therefore, Billy is greedy, but the hospital will not hire him. domain: people G(x): ____x is greedy. H(x): The hospital will hire ____x. R(x): ____x is a surgeon. K(x): ____x is skilled. b: Billy ∀x. [¬(R(x) ∧ K(x)) → ¬H(x)] ∀x. (R(x) → G (x)) R(b) ∧ ¬K(b) ∴ G(b) ∧ ¬H (b) Carol is a skilled surgeon and a tennis player. Therefore, Carol is a skilled tennis player. domain: people G(x): ____x is greedy. H(x): The hospital will hire ____x. R(x): ____x is a surgeon. K(x): ____x is skilled. T(x): ____x is a tennis player. b: Billy c: Carol (R(c) ∧ K(c)) ∧ T(c) ∴ K(c) ∧ T(c) domain: people G(x): ____x is greedy. H(x): The hospital will hire ____x. R(x): ____x is a surgeon. K₁(x): ____x is a skilled surgeon. K₂(x): ____x is a skilled tennis player. T(x): ____x is a tennis player. b: Billy c: Carol (R(c) ∧ K₁(c)) ∧ T(c) ∴ K₂(c) ∧ T(c) If you go on a date with your soulmate, you'll get married. You've decided not to marry anyone other than your soulmate. If you date enough people, you'll marry one of them. Therefore, your soulmate must exists. domain: people S(x): ____x is your soulmate M(x): you'll marry ____x D(x): you go on a date with ____x ∀x. (S(x) ∧ D(x)) → M(x) ∄x. M(x) ∧ ¬S(x) ∃x. D(x) → M(x) ∴ ∃x. S(x) The sqrt function works for all non-negative integer inputs. If x is a non-negative integer, so is x². I just ran sqrt(50000 * 50000) and it crashed. Therefore x * x does not compute x². domain: numbers N(x): ____x is a non-negative integer t(x) = x * x q(x) = x² C(x): sqrt(____x) crashes b: 50000 ∀x. N(x) → ¬C(x) ∀x. N(x) → N(q(x)) N(b) C(t(b)) ∴ (t ≠ q) No program can, given an arbitrary other program as its input, always determine if that program will run forever or not. But there are programs that other programs can identify as running forever or not domain: programs H(x, y): ____x identifies if ____y runs forever ∄x. ∀y. H(x, y) ∃y. ∃x. H(x, y)