%%% Assignment 7 %%% Out: Mon 12 Nov %%% Due: Mon 19 Nov %%% Author : Brigitte Pientka % % This assignment is to be submitted electronically using Tutch. % Comment out those parts of problems 1,2, and 4 that cannot % be checked by Tutch. % % % 1. Syllogism. % % Prove that the following argument is valid. % % No philosophers are Spartans. % Some Greeks are Spartans. % -------------------------------- % Some Greeks are not philosophers. % %{ Let P(x) denote "x is a philosopher." Let S(x) denote "x is a Spartan". Let G(x) denote "x is a Greek". The the argument is: !x:t. P(x) => ~S(x), ?x:t. G(x) & S(x) |- ?x:t. G(x) & ~P(x) }% proof syllogism : ((!x:t. P(x) => ~S(x)) & (?x:t. G(x) & S(x))) => (?x:t. G(x) & ~P(x)) = begin [(!x:t. P(x) => ~S(x)) & (?x:t. G(x) & S(x)); !x:t. P(x) => ~S(x); ?x:t. G(x) & S(x); [ c:t, G(c) & S(c); G(c); S(c); [P(c); P(c) => ~S(c); ~S(c); F]; ~P(c); G(c) & ~P(c); ?x:t. G(x) & ~P(x)]; ?x:t. G(x) & ~P(x)]; ((!x:t. P(x) => ~S(x)) & (?x:t. G(x) & S(x))) => (?x:t. G(x) & ~P(x)); end; % % % 2. Formalization. % % In Huth & Ryan section 2.2, do exercize 6 on p. 102, % and in section 2.3, do exercize 12 on p. 128. % %{ 6. a. !x:t. ?y:t. M(y, x) b. !x:t. (?y:t. M(y, x)) & (?z. F(z, x)) c. !x:t. (?y:t. M(y, x)) => (?z. F(z, x)) d. ?x:t. ?y:t. (F(x, y) | M(x,y)) & F(e, x) e. !x:t. (?y:t. F(x, y)) => (?z:t. F(x, z) | M(x, z)) f. !x:t. (?y:t. H(x, y)) => (?z:t. H(x, y) | H(y, x)) g. !x:t. (?y:t. ?z:t. (F(y, z) | M(y, z)) & B(x, y)) => ~(?a:t. ?b:t. (F(a, b) | M(a, b)) & S(x, a)) h. !x:t. !y:t. (B(x, y) & B(y, x)) => ((B(x, y) & B(y, x)) | (B(x, y) & S(y, x)) | (S(x, y) & B(y, x)) | (S(x, y) & S(y, x))) i. !x:t. (?y:t. ?z:t. (F(y, z) | M(y, z)) & M(x, y)) => ~(?w:t. F(x, w)) j. H(e, p) k. ?x. H(c, x) & S(x, m) [Assuming Carl's gender and traditional marriage conventions.] 12. Let T(x) denote "x is a tax payer". Let P(x) denote "x is a politician". Let F(x) denote "x is a philanthropist". (?x:t. T(x)) => (!x:t. P(x) => T(x)), (?x:t. F(x)) => (!x:t. T(x) => F(x)) |- (?x:t. T(x) & F(x)) => (!x:t. P(x) => F(x)) }% proof twelve : (((?x:t. T(x)) => (!x:t. P(x) => T(x))) & ((?x:t. F(x)) => (!x:t. T(x) => F(x)))) => ((?x:t. T(x) & F(x)) => (!x:t. P(x) => F(x))) = begin [ ((?x:t. T(x)) => (!x:t. P(x) => T(x))) & ((?x:t. F(x)) => (!x:t. T(x) => F(x))); (?x:t. T(x)) => (!x:t. P(x) => T(x)); (?x:t. F(x)) => (!x:t. T(x) => F(x)); [ ?x:t. T(x) & F(x); [ a:t, T(a) & F(a); T(a); ?x:t. T(x)]; ?x:t. T(x); !x:t. P(x) => T(x); [ b:t, T(b) & F(b); F(b); ?x:t. F(x)]; ?x:t. F(x); !x:t. T(x) => F(x); [ c:t; [ P(c); P(c) => T(c); T(c); T(c) => F(c); F(c)]; P(c) => F(c)]; !x:t. P(x) => F(x)]; (?x:t. T(x) & F(x)) => (!x:t. P(x) => F(x))]; (((?x:t. T(x)) => (!x:t. P(x) => T(x))) & ((?x:t. F(x)) => (!x:t. T(x) => F(x)))) => ((?x:t. T(x) & F(x)) => (!x:t. P(x) => F(x))); end; % % % 3. Quantifier Laws. % % Give proofs and terms for the following entailments. % % proof CEa : (A & ?x:t. B(x)) => (?x:t. A & B(x)) = begin [A & ?x:t. B(x); A; ?x:t. B(x); [c:t, B(c); A & B(c); ?x:t. A & B(x)]; ?x:t. A & B(x)]; (A & ?x:t. B(x)) => (?x:t. A & B(x)); end; % term CEa : (A & ?x:t. B(x)) => (?x:t. A & B(x)) = fn u => let (c, v) = snd(u) in (c, (fst(u), v)); % % proof CEb : (?x:t. A & B(x)) => (A & ?x:t. B(x)) = begin [?x:t. A & B(x); [c:t, A & B(c); A; B(c); ?x:t. B(x); A & ?x:t. B(x)]; A & ?x:t. B(x)]; (?x:t. A & B(x)) => (A & ?x:t. B(x)); end; % term CEb : (?x:t. A & B(x)) => (A & ?x:t. B(x)) = fn u => let (c, v) = u in (fst(v), (c, snd(v))); % % % proof DUa : (A | !x:t. B(x)) => (!x:t. A | B(x)) = begin [A | !x:t. B(x); [c:t; [A; A | B(c)]; [!x:t. B(x); B(c); A | B(c)]; A | B(c)]; !x:t. A | B(x)]; (A | !x:t. B(x)) => (!x:t. A | B(x)); end; % term DUa : (A | !x:t. B(x)) => (!x:t. A | B(x)) = fn u => fn c => case u of inl a => inl a | inr v => inr (v c) end; % % % % proof DUb : (!x:t. A | B(x)) => (A | !x:t. B(x)) = % % term DUb : (!x:t. A | B(x)) => (A | !x:t. B(x)) = % % this is not provable constructively -- however it is provable classically. % Constructively, there exists no normal proof for the conjecture DUb, % because we cannot instantiate the universal quantifier on the left % (!x:t. A | B(x)) before introducing a new parameter on the right (!x:t. B(x)). % The only way it would be possible is to first commit to (!x:t. B(x)) by OrIR % rule and obtain B(c) where c is new. Then we could instantiate the left side % (!x:t. A | B(x)) to obtain A | B(c). However, from this assumptions we will % never be able to prove B(c), because we need to prove B(c) under the % assumption A (which is not provable) and prove B(c) under the % assumption B(c) (which is of course provable). % % 4. Classical Versus Constructive Validity. % % a. Show that the following entailment is classically valid, % but not constructively so. % % ((!x:t. B(x)) => A) => (?x:t. B(x) => A) % % Note: Since classical rules are used, the style is all that is similar to tutch. %{ proof classical : ((!x:t. B(x)) => A) => (?x:t. B(x) => A) = begin [ (!x:t. B(x)) => A; [ A; [ c:t; ~B c | A; (~B c | A) => (B c => A); B c => A; ?x:t. B(x) => A]; ?x:t. B(x) => A]; [ ~A; [ !x:t. B(x); A; F]; ~!x:t. B(x); ?x:t. ~B x; [ c:t, ~B c; ~B c | A; (~B c | A) => (B c => A); B c => A; ?x:t. B(x) => A]; ?x:t. B(x) => A]; ?x:t. B(x) => A]; ((!x:t. B(x)) => A) => (?x:t. B(x) => A); end; }% % % % b. Give an (informal) interpretation to show that the following % is not even classically valid (and so not constructively). % % (?x:t. B(x) => A) => ((?x:t. B(x)) => A) % %{ Let the universe of quantification have two elements 0, 1. Let B(0) be false and B(1) be true. Let A be false. Then B(0) => A is true since B(0) is false. So ?x:t. B(x) => A is true. But (?x:t. B(x)) => A is false since A is false and B(1) is true. Therefore the entire conditional is false. }% % % %%%