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

[Mario Carneiro]

If the purpose of the "bool-def-1.10" constant in that file is to indicate
where the axioms are coming from, that is more appropriate as a pragma (say
["source", "bool-def-1.10"]) than a defineConst directive.

On Sun, Oct 19, 2014 at 2:18 AM, Mario Carneiro <di.gama at gmail.com> wrote:

> 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/c17f0100/attachment-0001.html>