%%% 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.
}%
%
%
%%%