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

[Mario Carneiro]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141018/f161a3de/attachment.html>