<div dir="ltr"><div><div><div><div><div><div>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.<br><br></div>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<br><br>defineConst: [] |- bad = T<br>defineConst: [] |- bad = F<br></div>sym,trans:  [] |- T = F<br></div>eqMp: [] |- F<br></div><br></div>(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.<br><br></div>Mario<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Oct 19, 2014 at 1:36 AM, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Mario,<br>
<br>
Your question inspired me to update the OpenTheory FAQ:<br>
<br>
<a href="http://www.gilith.com/research/opentheory/faq.html" target="_blank">http://www.gilith.com/research/opentheory/faq.html</a><br>
<br>
Please take a look at this question<br>
<br>
<a href="http://www.gilith.com/research/opentheory/faq.html#what-are-theorem-files" target="_blank">http://www.gilith.com/research/opentheory/faq.html#what-are-theorem-files</a><br>
<br>
and let me know if anything is unclear.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div class="h5"><br>
On Sat, Oct 18, 2014 at 6:13 PM, Mario Carneiro <<a href="mailto:di.gama@gmail.com">di.gama@gmail.com</a>> wrote:<br>
> Hello,<br>
><br>
> I'm trying to make sense of the file bool-def-1.10/bool-def-1.10.art, which<br>
> on line 49 defines [] |- (F = bool-def-1.10), where "bool-def-1.10" is a<br>
> constant term which has not been previously defined. This is followed by the<br>
> axiom [] |- (F = (! \p. p)) (118) and finally publishing the theorem [] |-<br>
> (F = (! \p. p)) on line 122. What kind of constant declaration is this? I<br>
> don't really understand what the literal string "bool-def-1.10" is doing in<br>
> all this math, and it strikes me as not being safe either. Later in the same<br>
> file we have [] |- (T = bool-def-1.10) (191), and [] |- (T = (\p. p = \p.<br>
> p)) (210); from these we can derive first [] |- T, then we can use 191 and<br>
> 49 to derive [] |- (T = F) and hence [] |- F, which is not good at all. What<br>
> is going on here?<br>
><br>
> Mario Carneiro<br>
><br>
</div></div>> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br></div>