%%% Set extensionality proves "xi" %%% %%% Kevin Watkins %%% August 2004 %%% %%% See "Higher order semantics and extensionality", Benzmüller, Brown, %%% Kohlhase, to appear in JSL. %%% 0. Preliminaries jg : type. |- : jg -> type. eqv = [J] [J'] {J''} ((|- J -> |- J') -> (|- J' -> |- J) -> |- J'') -> |- J''. %infix none 0 eqv. %abbrev eqvI : J eqv J = [J] [f] f ([x] x) ([x] x). %abbrev sym : J eqv J' -> J' eqv J = [eq] [J''] [f] eq J'' ([x] [y] f y x). %abbrev trans : J1 eqv J2 -> J2 eqv J3 -> J1 eqv J3 = [eq1] [eq2] [J'] [f] eq1 J' ([x1] [y1] eq2 J' ([x2] [y2] f ([z] x2 (x1 z)) ([z] y1 (y2 z)))). %%% 1. The base theory of simply-typed functions tp : type. --> : tp -> tp -> tp. %infix right 0 -->. tm : tp -> type. \ : (tm A -> tm B) -> tm (A --> B). @ : tm (A --> B) -> (tm A -> tm B). %infix left 10 @. apply = [x] [y] x @ y. beta : {Ctx:((tm A -> tm B) -> (tm A -> tm B)) -> jg} Ctx ([x] apply (\ x)) eqv Ctx ([x] x). %%% 2. Propositions as terms o : tp. true : tm o -> jg. pf = [A] |- (true A). %%% 3. Watkins-description (does not require an equality) int : ((tm A -> tm o) -> tm o) -> tm A. %abbrev lift : tm A -> ((tm A -> tm o) -> tm o) = [x] [p] p x. intax : {Ctx:(tm A -> tm A) -> jg} Ctx ([x] int (lift x)) eqv Ctx ([x] x). %%% 4. Boolean extensionality boolext : (true P eqv true Q) -> {Ctx:tm o -> jg} Ctx P eqv Ctx Q. %%% 5a. The eta rule eta : {Ctx:(tm (A --> B) -> tm (A --> B)) -> jg} Ctx ([x] \ (apply x)) eqv Ctx ([x] x). %%% 5b. The xi rule xi : ({x:tm A} {Ctx:tm B -> jg} Ctx (F x) eqv Ctx (G x)) -> {Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G. %%% 5c. Functional extensionality fext : ({x:tm A} {Ctx:tm B -> jg} Ctx (S @ x) eqv Ctx (T @ x)) -> {Ctx:tm (A --> B) -> jg} Ctx S eqv Ctx T. %%% Aside: Contextual equivalences of meta-functions can be reduced %%% to contextual equivalences of object functions. %abbrev lower : ({Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G) -> {Ctx:tm (A --> B) -> jg} Ctx (\ F) eqv Ctx (\ G) = [D] [Ctx] D ([f] Ctx (\ f)). %abbrev raise : ({Ctx:tm (A --> B) -> jg} Ctx (\ F) eqv Ctx (\ G)) -> {Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G = [D] [Ctx] trans (sym (beta ([h] Ctx ([x] h F x)))) (trans (D ([h] Ctx ([x] apply h x))) (beta ([h] Ctx ([x] h G x)))). % As a consequence, the rules intax, eta, xi can be restated % equivalently as follows: intax' : {Ctx:tm (A --> A) -> jg} Ctx (\[x] int (lift x)) eqv Ctx (\[x] x). eta' : {Ctx:tm ((A --> B) --> (A --> B)) -> jg} Ctx (\[x] \ (apply x)) eqv Ctx (\[x] x). xi' : ({x:tm A} {Ctx:tm B -> jg} Ctx (F x) eqv Ctx (G x)) -> {Ctx:tm (A --> B) -> jg} Ctx (\ F) eqv Ctx (\ G). % Of course, the beta rule cannot be similarly reduced, because % raise/lower themselves depend upon beta. %%% Aside: Contextual equivalences of meta-functions have weaker %%% variants. If xi is available, the weaker and stronger versions %%% collapse. %abbrev weaken : ({Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G) -> {T:tm A} {Ctx:tm B -> jg} Ctx (F T) eqv Ctx (G T) = [D] [T] [Ctx] D ([h] Ctx (h T)). %abbrev strengthen : ({T:tm A} {Ctx:tm B -> jg} Ctx (F T) eqv Ctx (G T)) -> {Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G = xi. % Hence, the intax and eta rules have weaker variants as follows, which % are equivalent to the stronger when xi is available. wkintax : {Ctx:tm A -> jg} Ctx (int (lift T)) eqv Ctx T. wketa : {Ctx:tm (A --> B) -> jg} Ctx (\ (apply T)) eqv Ctx T. % And the beta rule, being a contextual equivalence of meta-functionals % rather than meta-functions, has three weaker variants: wkbeta1 : {Ctx:((tm A -> tm B) -> tm B) -> jg} Ctx ([x] apply (\ x) T) eqv Ctx ([x] x T). wkbeta2 : {Ctx:(tm A -> tm B) -> jg} Ctx (apply (\ F)) eqv Ctx F. wkbeta3 : {Ctx:tm B -> jg} Ctx (apply (\ F) T) eqv Ctx (F T). % I have not explored the relation between intax/intax', eta/eta', xi/xi' % in these weaker systems. %%% 7. Set extensionality setext : ({x} true (P x) eqv true (Q x)) -> {Ctx:(tm A -> tm o) -> jg} Ctx P eqv Ctx Q. % "First-order" version setext' : ({x} true (P x) eqv true (Q x)) -> {Ctx:tm (A --> o) -> jg} Ctx (\ P) eqv Ctx (\ Q). %%% I. Set extensionality entails Boolean extensionality %%% (if some type is non-empty) sometype : tp. something : tm sometype. %abbrev boolext~ : (true P eqv true Q) -> {Ctx:tm o -> jg} Ctx P eqv Ctx Q = [D] [Ctx] setext ([x] D) ([f] Ctx (f something)). %%% II. Set extensionality entails xi, if Watkins-description %%% is available % Plan of proof: % a. Define ordered pairs (not necessarily surjective) % b. Use the ordered pairs to extend setext to binary relations % c. Construct a representation of functions by their graphs % (again, not necessarily surjective) % d. Prove xi using binary relation extensionality on graphs %%% IIa. Definition of pairs * = [A] [B] (A --> B --> o) --> o. %infix right 5 *. pair : tm A -> tm B -> tm (A * B) = [x] [y] \[f] f @ x @ y. pi1 : tm (A * B) -> tm A = [z] int [p] z @ (\[x] \[y] p x). pi2 : tm (A * B) -> tm B = [z] int [p] z @ (\[x] \[y] p y). %abbrev beta_pair1 : {Ctx:(tm A -> tm B -> tm A) -> jg} Ctx ([x] [y] pi1 (pair x y)) eqv Ctx ([x] [y] x) = [Ctx] trans (beta ([h] Ctx ([x] [y] int [p] h ([f] f @ x @ y) (\[x'] \[y'] p x')))) (trans (beta ([h] Ctx ([x] [y] int [p] h ([x'] \[y'] p x') x @ y))) (trans (beta ([h] Ctx ([x] [y] int [p] h ([y'] p x) y))) (intax ([h] Ctx ([x] [y] h x))))). %abbrev beta_pair2 : {Ctx:(tm A -> tm B -> tm B) -> jg} Ctx ([x] [y] pi2 (pair x y)) eqv Ctx ([x] [y] y) = [Ctx] trans (beta ([h] Ctx ([x] [y] int [p] h ([f] f @ x @ y) (\[x'] \[y'] p y')))) (trans (beta ([h] Ctx ([x] [y] int [p] h ([x'] \[y'] p y') x @ y))) (trans (beta ([h] Ctx ([x] [y] int [p] h ([y'] p y') y))) (intax ([h] Ctx ([x] [y] h y))))). % Aside: an alternate elimination form split : tm (A * B) -> (tm A -> tm B -> tm C) -> tm C = [z] [f] int [p] z @ (\[x] \[y] p (f x y)). %abbrev beta_pair : {Ctx:((tm A -> tm B -> tm C) -> (tm A -> tm B -> tm C)) -> jg} Ctx ([f] [x] [y] split (pair x y) f) eqv Ctx ([f] [x] [y] f x y) = [Ctx] trans (beta ([h] Ctx ([f] [x] [y] int [p] h ([f] f @ x @ y) (\[x] \[y] p (f x y))))) (trans (beta ([h] Ctx ([f] [x] [y] int [p] h ([x] \[y] p (f x y)) x @ y))) (trans (beta ([h] Ctx ([f] [x] [y] int [p] h ([y] p (f x y)) y))) (intax ([h] Ctx ([f] [x] [y] h (f x y)))))). %%% IIb. Binary relation extensionality %abbrev lemma : {Ctx:((tm A -> tm B -> tm C) -> (tm A -> tm B -> tm C)) -> jg} Ctx ([f] [x] [y] f (pi1 (pair x y)) (pi2 (pair x y))) eqv Ctx ([f] f) = [Ctx] trans (beta_pair1 ([h] Ctx ([f] [x] [y] f (h x y) (pi2 (pair x y))))) (beta_pair2 ([h] Ctx ([f] [x] [y] f x (h x y)))). %abbrev binext : ({x} {y} true (P x y) eqv true (Q x y)) -> {Ctx:(tm A -> tm B -> tm o) -> jg} Ctx P eqv Ctx Q = [D] [Ctx] trans (sym (lemma ([h] Ctx (h P)))) (trans (setext ([z] D (pi1 z) (pi2 z)) ([h] Ctx ([x] [y] h (pair x y)))) (lemma ([h] Ctx (h Q)))). %%% IIc. Definition of the graph of a meta-function %abbrev graph : (tm A -> tm B) -> (tm A -> tm (B --> o) -> tm o) = [f] [x] [p] p @ (f x). %abbrev ungraph : (tm A -> tm (B --> o) -> tm o) -> (tm A -> tm B) = [g] [x] int [p] g x (\[y] p y). %abbrev beta_graph : {Ctx:((tm A -> tm B) -> (tm A -> tm B)) -> jg} Ctx ([f] ungraph (graph f)) eqv Ctx ([f] f) = [Ctx] trans (beta ([h] Ctx ([f] [x] int [p] h ([y] p y) (f x)))) (intax ([h] Ctx ([f] [x] h (f x)))). %%% IId. The xi rule %abbrev lemma : ({x:tm A} {Ctx:tm B -> jg} Ctx (F x) eqv Ctx (G x)) -> {Ctx:(tm A -> tm (B --> o) -> tm o) -> jg} Ctx (graph F) eqv Ctx (graph G) = [D] [Ctx] binext ([x] [p] D x ([y] true (p @ y))) Ctx. %abbrev xi~ : ({x:tm A} {Ctx:tm B -> jg} Ctx (F x) eqv Ctx (G x)) -> {Ctx:(tm A -> tm B) -> jg} Ctx F eqv Ctx G = [D] [Ctx] trans (sym (beta_graph ([h] Ctx (h F)))) (trans (lemma D ([h] Ctx (ungraph h))) (beta_graph ([h] Ctx (h G)))). %%% 8. Equality == : tm A -> (tm A -> tm o). %infix none 2 ==. in : ({Ctx:tm A -> jg} Ctx S eqv Ctx T) -> pf (S == T). out : pf (S == T) -> ({Ctx:tm A -> jg} Ctx S eqv Ctx T). % The above is a symmetric description; the following simpler % axiom is equivalent to in: refl : pf (T == T). %abbrev in~ : ({Ctx:tm A -> jg} Ctx S eqv Ctx T) -> pf (S == T) = [D] D ([h] true (S == h)) _ ([f] [g] f refl). %abbrev refl~ : pf (T == T) = in ([Ctx] eqvI). %%% Aside: If equality is available, then the "first-order" contextual %%% equivalences can be stated in terms of it: boolext== : (true P eqv true Q) -> pf (P == Q). fext== : ({x:tm A} pf (S @ x == T @ x)) -> pf (S == T). intax'== : pf ((\[x] int (lift x)) == (\[x] x)). eta'== : pf ((\[x] \ (apply x)) == (\[x] x)). xi'== : ({x:tm A} pf (F x == G x)) -> pf (\ F == \ G). setext'== : ({x:tm A} true (P x) eqv true (Q x)) -> pf (\ P == \ Q). wkintax== : pf (int (lift T) == T). wketa== : pf (\ (apply T) == T). wkbeta3== : pf (apply (\ F) T == F T). %%% 9. Andrews-description % See "General models, descriptions, and choice in type theory", % Andrews, JSL 37(2):385--394, 1972. the : (tm A -> tm o) -> tm A. equal = [x] [y] x == y. desc : {Ctx:(tm A -> tm A) -> jg} Ctx ([x] the (equal x)) eqv Ctx ([x] x). %%% III. Andrews-description entails Watkins-description %%% (in the presence of equality) %abbrev int~ : ((tm A -> tm o) -> tm o) -> tm A = [f] the [x] f ([y] y == x). %abbrev intax~ : {Ctx:(tm A -> tm A) -> jg} Ctx ([x] int~ (lift x)) eqv Ctx ([x] x) = [Ctx] desc Ctx. %%% IV. Watkins-description is always available at o %abbrev into : ((tm o -> tm o) -> tm o) -> tm o = [f] f ([x] x). %abbrev intoax : {Ctx:(tm o -> tm o) -> jg} Ctx ([x] into (lift x)) eqv Ctx ([x] x) = [Ctx] eqvI. %%% V. If Watkins-description is available at B it's available %%% at A --> B (assuming eta). %abbrev int--> : (((tm B -> tm o) -> tm o) -> tm B) -> (((tm (A --> B) -> tm o) -> tm o) -> tm (A --> B)) = [i] [f] \[x] i ([p] f ([g] p (g @ x))). %abbrev int-->ax : ({Ctx:(tm B -> tm B) -> jg} Ctx ([x] I (lift x)) eqv Ctx ([x] x)) -> ({Ctx:(tm (A --> B) -> tm (A --> B)) -> jg} Ctx ([x] int--> I (lift x)) eqv Ctx ([x] x)) = [D] [Ctx] trans (D ([h] Ctx ([x] \[y] h (x @ y)))) (eta ([h] Ctx ([x] h x))).