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

[Joe Leslie-Hurd]

Hi Mario,

You're quite right that the purpose of putting the NAME-VERSION in the
definition is a way to track the origin of constants, but since the
theorems file is only used internally by the opentheory tool to
optimize certain calculations there should be no confusion for users.

There is no restriction on defineConst in the article standard that
the constant has not been defined before, but that check is instead
left to the article reader. In most theorem prover implementations
redefining a constant is disallowed (perhaps unless it is
alpha-equivalent to the existing definition), but the opentheory
logical kernel is purely functional and allows it. However, soundness
is preserved by storing the definition with the constant, so your
hypothetical example would go like this:

defineConst: [] |- bad{T} = T
defineConst: [] |- bad{F} = F
sym,trans: failure, because bad{T} is not alpha-equivalent to bad{F}

I recommend ignoring these theorem files, because the functionality
they offer is in most cases subsumed by the article file THEORY.art
output by the command

opentheory info --article -o THEORY.art NAME-VERSION

Cheers,

Joe

On Sat, Oct 18, 2014 at 11:26 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> 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
>>
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>