<div dir="ltr"><div>Oh wow, that's a pretty direct derivation of extensionality from my version of defineTypeOp. I stand corrected; certainly it's not desirable to have a "conservative extension" allow the derivation of an axiom before its introduction. And I guess that the next best thing if you want to maintain conservativity is exactly your version of the axiom. </div>Mario </div><div class="gmail_extra"> <div class="gmail_quote">On Thu, Nov 6, 2014 at 2:16 AM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Mario, As you say, extensionality is an axiom of the system, but the use of it is explicitly tracked. For example, you can see which theorems in bool theory depend on it using the following command: opentheory info --theory --show-assumptions --show-derivations bool If defineTypeOp produced this: ⊦ p = (\r. rep (abs r) = r) (1) then you could apply appThm, betaConv and absThm to get: ⊦ (\r. p r) = (\r. rep (abs r) = r) (2) and then sym and trans using (1) and (2) to get ⊦ (\r. p r) = p (3) which is an untracked application of extensionality for any non-empty predicate p. It seemed more elegant to reformulate the theorem to avoid this possibility. Cheers, Joe <div class="HOEnZb"><div class="h5"> On Wed, Nov 5, 2014 at 10:45 PM, Mario Carneiro <<a href="mailto:di.gama@gmail.com">di.gama@gmail.com</a>> wrote: > I was aware that equation (1) is stronger than (2) without extensionality, > but I'm curious why this is a problem, since it is an axiom of the system > and doesn't require proof. Any v5 proof that starts with (2) can easily be > rebuilt to use (1), while conversely for a v6 proof there are very few > theorems that follow from (1) but not (2) in the absence of extensionality > (mostly trivial restatements of (1) itself), and I expect that any proof > that starts from (1) will immediately wrap it with appThm, upon which point > it will again be equivalent to (2). > > Mario > > On Thu, Nov 6, 2014 at 1:31 AM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >> >> Now that there is a release of the opentheory tool for processing >> version 6 articles, and I am sitting on a release of the standard >> theory library that uses version 6 articles, I'd like to finalize >> version 6 of the article file format standard, which is currently in >> draft mode: >> >> <a href="http://www.gilith.com/research/opentheory/article.html" target="_blank">http://www.gilith.com/research/opentheory/article.html</a> >> >> The commands that are new in version 6 are highlighted in yellow and >> the command with changed semantics (defineTypeOp) is highlighted in >> red. We have discussed the changes on this list, so there shouldn't be >> any surprises in store. >> >> Actually, there is one minor change that hasn't been discussed before. >> During implementation work on defineTypeOp I discovered that one of >> Mario's proposed theorems >> >> ⊦ p = (\r. rep (abs r) = r) (1) >> >> required the axiom of extensionality to be logically equivalent to the >> same theorem produced by version 5 of defineTypeOp: >> >> ⊦ p r = (rep (abs r) = r) (2) >> >> Although it would be theoretically possible to invoke the axiom of >> extensionality to convert between the two versions of defineTypeOp, I >> thought it was more elegant to reformulate theorem (1) >> by eta-expanding p: >> >> ⊦ (\r. rep (abs r) = r) = \r. p r (3) >> >> [I also flipped the LHS and RHS so that theorem (3) has a pleasing >> similarity to the other theorem produced by defineTypeOp.] Now theorem >> (3) is logically equivalent to theorem (2) without requiring the axiom >> of extensionality, and retains the desirable property of having no >> free term variables. >> >> Anyway, there are no other "brown bag updates" to the standard, and >> I'd like to finalize it so we can start using it for real work. >> >> Does anybody have any objections or last-minute additions? >> >> Cheers, >> >> Joe >> >> _______________________________________________ >> opentheory-users mailing list >> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> > > > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> > _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div></blockquote></div> </div>