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

[Joe Leslie-Hurd]

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
>