[opentheory-users] Status of derived syntax

[Rob Arthan]

Joe,

On 25 Nov 2013, at 18:35, Joe Leslie-Hurd wrote:

> Hi Rob,
> 
> I think you have worked out your problem, but I wanted to explain the origin of the monster assumption you found in the natural theory package.
> 
> There are 3 axioms used to set up the standard theory library (extensionality, choice and infinity), and two primitive constants (= and select). A problem I found is that the usual presentation of the basic axioms refers to other constants, for example extensionality contains a universal quantifier. If you were to assert an axiom in terms of a non-primitive constant you run the risk of a theory package defining the non-primitive constant in an unexpected way, and then the axiom might make the system inconsistent.
> 
> My resolution is to expand the standard axioms using the definition of the constants, and have little theory packages that prove the usual presentation of the axiom in terms of the expanded axiom and the definition of the non-primitive constants that it refers to.

I take it that for you only equality and choice are primitive.

> For example, here is the axiom-extensionality package:
> 
> $ opentheory info --summary --show-assumptions axiom-extensionality
> 2 external type operators: -> bool
> 3 external constants: = ! T
> 3 assumptions:
>   |- T <=> (\p. p) = \p. p
>   |- (!) = \p. p = \x. T
>   |- let a d <- (\e. d e) = d in a = \b. (\c. c) = \c. c
> 1 theorem:
>   |- !t. (\x. t x) = t
> 
> The "real" extensionality axiom is the third assumption, and the usual presentation is proved as a theorem in terms of the real axiom and the standard definition of logical quantifiers. So if you were to define the universal quantifier in a different way, it wouldn't match the assumptions of this package and so you wouldn't get access to the axiom of extensionality.
> 

ETA_AX and SELECT_AX only use outermost universal quantifier, so you could just have stripped that off, giving equivalent readable axioms with free variables. That approach doesn't help with INFINITY_AX.

> The monster assumption you found in the natural theory package is the expanded version of the axiom of the infinity, which refers to injectivity and surjectivity, the definition of which refer to other constants which must be recursively expanded. The resulting "real" axiom of infinity is indeed a real monster.
> 

Having imported the axioms into ProofPower and beta-reduced them, I do see your problem with INFINITY_AX as it is completely unreadable before and after beta-reduction. 

But I don't really understand the problem you are trying to guard against. In addition to the axiom of infinity, the package axiom-infinity inputs the logical connectives and the quantifiers and has assumptions that say these things and injective and surjective have their standard meaning. You use the quantifiers and logical connectives in the assumptions about injective and surjective, so why does it cause a problem to use them in the axiom of infinity?

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131128/6f7232f0/attachment.html>