environ
vocabularies PROPOSIT;
notations PROPOSIT;
constructors PROPOSIT;
begin
reserve x,y,z for set;
(for x holds P1(x) iff Q1(x)) implies
((for x holds P1(x)) iff (for x holds Q1(x)));
(for x holds P1(x) iff Q1(x)) implies ((ex x st P1(x)) iff (ex x st Q1(x)));
((for x holds P1(x)) or (for x holds Q1(x))) implies
for x holds (P1(x) or Q1(x));
(ex x st (P1(x) implies Q1(x))) iff
((for x holds P1(x)) implies (ex x st Q1(x)));
(ex x st (P1(x) & Q1(x))) implies ((ex x st P1(x)) & (ex x st Q1(x)));
(ex x st (P1(x) or Q1(x))) iff ((ex x st P1(x)) or (ex x st Q1(x)));
(for x holds for y holds P2 x,y) iff (for y holds for x holds P2 x,y);
(for x for y holds P2 x,y) iff (for y for x holds P2 x,y);
(for x,y holds P2 x,y) iff (for y,x holds P2 x,y);
(ex x,y st P2 x,y) iff (ex y,x st P2 x,y);
(ex x st for y holds P2 x,y) implies (for y holds ex x st P2 x,y);
(ex x st for y holds P2 x,y) implies (for y ex x st P2 x,y);
:: (ex x st for y holds P2 x,y) iff (for y holds ex x st P2 x,y);
:: (for y holds ex x st P2 x,y) implies (ex x st for y holds P2 x,y);
not (for x holds P1(x)) iff ex x st not P1(x);
not not (for x holds P1(x)) iff not ex x st not P1(x);
(for x holds P1(x)) iff not ex x st not P1(x);
not (ex x st Q1(x)) iff for x holds not Q1(x);
not not (ex x st Q1(x)) iff not for x holds not Q1(x);
(ex x st Q1(x)) iff not for x holds not Q1(x);
:: Drinker Paradox (simplified)
ex x st (Q1 x implies for y holds Q1 y);
:: Drinker Paradox (general case)
(ex x st P1 x & (Q1 x implies for y st P1 y holds Q1 y)) iff (ex x st P1 x)
proof
thus (ex x st P1 x & (Q1 x implies for y st P1 y holds Q1 y)) implies (ex x st P1 x);
thus (ex x st P1 x) implies (ex x st P1 x & (Q1 x implies for y st P1 y holds Q1 y))
proof
:: assume ex x st P1 x;
:: then consider x such that x: P1 x;
given x such that x: P1 x;
per cases;
suppose y: for y st P1 y holds Q1 y;
take x;
thus P1 x by x,y;
thus (Q1 x implies for y st P1 y holds Q1 y) by y;
end;
suppose not for y st P1 y holds Q1 y;
then consider y such that
y: P1 y & not Q1 y;
take x=y;
thus P1 x by y;
thus Q1 x implies for y st P1 y holds Q1 y by y;
end;
end;
end;
:: proof
:: thus (ex x st P1 x & (Q1 x implies for y st P1 y holds Q1 y)) implies
:: (ex x st P1 x);
:: thus (ex x st P1 x) implies
:: (ex x st P1 x & (Q1 x implies for y st P1 y holds Q1 y))
:: proof
:: given x such that x: P1 x;
:: per cases;
:: suppose y: for y st P1 y holds Q1 y;
:: take x;
:: thus P1 x by x;
:: thus (Q1 x implies for y st P1 y holds Q1 y) by y;
:: end;
:: suppose not for y st P1 y holds Q1 y;
:: then consider y such that y: P1 y & not Q1 y;
:: take x=y;
:: thus P1 x by y;
:: thus Q1 x implies for y st P1 y holds Q1 y by y;
:: end;
:: end;
:: end;