[opentheory-users] Status of derived syntax

[Joe Leslie-Hurd]

Hi Rob,

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

That is correct.

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.
>

Another OpenTheory convention is that theorems don't have any free
variables, so I was trying to find a solution that satisfied this
constraint (though doing so meant throwing out readability).

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?
>

The assumptions collectively enforce that the standard definition of basic
logical constants are used. Consider the following two assumptions of the
axiom-infinity theory package:

  |- (!) = \p. p = \x. T
  |- !f. surjective f <=> !y. ?x. y = f x

The first assumption enforces that universal quantification has the
standard definition, so it can't cause problems to use universal
quantification in the definition of surjectivity.

The real problem I was trying to solve is recognizing the 3 standard axioms
so that I don't falsely report them as "unsatisfied assumptions" of a
theory. This is much easier if the standard axioms are expressed solely in
terms of primitive constants and type operators, so that the tool doesn't
have to check any definitions. The little axiom-* theories translate from
the primitive versions of the axioms to readable versions, assuming that
the standard definitions are being used. And note that the opentheory tool
reports all their assumptions as being satisfied, even though the primitive
versions of the axioms are not satisfied by any required theories but are
recognized as standard axioms.

I was thinking of changing the OpenTheory pretty printer so that the
primitive versions of the axioms would simply print as "AXIOM OF INFINITY"
instead of the monster term, which would perhaps avoid some future
confusion. I'm also open to better ways of booting up the OpenTheory
standard theory library, if you have any ideas.

Cheers,

Joe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131202/93ada46e/attachment.html>