[opentheory-users] Why are theory names showing up as constants in article files?

[Mario Carneiro]

Well, I'm afraid my question is a little more basic, along the lines of why
these abbreviated article files are valid under the standard. As I
understand it, you would like these name-version.art article files to
contain nothing but axiom -> thm directives so that it can function as a
listing of theorems without proofs. However, I don't understand the purpose
of the defineConst directives that define every constant to be equal to an
otherwise-unspecified "bool-def-1.10" constant. It looks like those
definitional theorems are just thrown away (using pop) after construction,
which makes them even more mysterious, but I'm certain that you could
derive a contradiction if you made use of them.

This ability to derive a contradiction in a standards-compliant article
file is more worrisome. There is no restriction in defineConst that the
constant has never been defined before - from this you can easily derive a
contradiction using the trick

defineConst: [] |- bad = T
defineConst: [] |- bad = F
sym,trans: [] |- T = F
eqMp: [] |- F

(where I assume that T and F are defined the usual way and have some basic
theorems). Similarly, if you introduce a constant definition via an axiom,
then you can't also use defineConst for it, which is to say that no axiom
is allowed to use a constant that was defined via defineConst in the
article file itself - in these cases you have to also import the
definitions of those constants as more axioms. This should fix the
inconsistency problem here.

Mario

On Sun, Oct 19, 2014 at 1:36 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Mario,
>
> Your question inspired me to update the OpenTheory FAQ:
>
> http://www.gilith.com/research/opentheory/faq.html
>
> Please take a look at this question
>
> http://www.gilith.com/research/opentheory/faq.html#what-are-theorem-files
>
> and let me know if anything is unclear.
>
> Cheers,
>
> Joe
>
> On Sat, Oct 18, 2014 at 6:13 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> > Hello,
> >
> > I'm trying to make sense of the file bool-def-1.10/bool-def-1.10.art,
> which
> > on line 49 defines [] |- (F = bool-def-1.10), where "bool-def-1.10" is a
> > constant term which has not been previously defined. This is followed by
> the
> > axiom [] |- (F = (! \p. p)) (118) and finally publishing the theorem []
> |-
> > (F = (! \p. p)) on line 122. What kind of constant declaration is this? I
> > don't really understand what the literal string "bool-def-1.10" is doing
> in
> > all this math, and it strikes me as not being safe either. Later in the
> same
> > file we have [] |- (T = bool-def-1.10) (191), and [] |- (T = (\p. p = \p.
> > p)) (210); from these we can derive first [] |- T, then we can use 191
> and
> > 49 to derive [] |- (T = F) and hence [] |- F, which is not good at all.
> What
> > is going on here?
> >
> > Mario Carneiro
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141019/cf065dea/attachment.html>