<div dir="ltr"><div>Hello,<br><br>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?<br><br></div>Mario Carneiro<br></div>