%%% Assignment 7
%%% Out: Mon 12 Nov
%%% Due: Mon 19 Nov 
%
% 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.
%
%
%
% 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.
%
%
%
% 3. Quantifier Laws.
%
% Give proofs and terms for the following entailments.
%
% 
 proof CEa : (A & ?x:t. B(x)) => (?x:t. A & B(x)) =
%
 term CEa : (A & ?x:t. B(x)) => (?x:t. A & B(x)) =
%
% 
 proof CEb : (?x:t. A & B(x)) => (A & ?x:t. B(x)) =
%
 term CEb : (?x:t. A & B(x)) => (A & ?x:t. B(x)) =
%
%
% 
 proof DUa : (A | !x:t. B(x)) => (!x:t. A | B(x)) =
%
 term DUa :  (A | !x:t. B(x)) => (!x:t. A | B(x)) =
%
% 
 proof DUb : (!x:t. A | B(x)) => (A | !x:t. B(x)) =
%
 term DUb :  (!x:t. A | B(x)) => (A | !x:t. B(x)) =
%
%
%
% 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)
%
%
% 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)
%
%
%%%