[opentheory-users] Wrong certificates

[Joe Leslie-Hurd]

Hi Chantal,

I think Ramana has already covered the essential point here, which is
that free variables (both type and term variables) are implicitly
quantified at the theorem/assumption level.

So your assumption |- x <=> T is indeed equivalent to |- !x. x <=> T
which is equivalent to |- F.

In general a theorem/assumption consists of a set of hypotheses and a
conclusion, written

{ hypotheses } |- conclusion

and any free type or term variables in the hypotheses and conclusion
are implicitly universally quantified at this level:

!frees. ({ hypotheses } |- conclusion)

A side condition of absThm is that the variable being abstracted is
not free in the hypotheses, since that would lead to the inconsistency
you describe.

As Ramana said, it is considered bad form for a theory to contain a
theorem/assumption with a non-empty set of hypotheses or free term
variables in the conclusion. Free type variables are unavoidable,
because there's no way to bind them in higher order logic.

While we're on this subject, I should mention that there's a potential
for terminology confusion, because what I call "hypotheses" above are
sometimes called "assumptions". I try to avoid this in OpenTheory,
because it confuses the theorem-level and the theory-level.

Cheers,

Joe

On Mon, Nov 19, 2012 at 8:06 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> Dear Chantal,
>
> I believe the new understanding of OpenTheory theories you described is a
> good one (if the assumptions are valid, then the theorems are valid),
> although I'd be more inclined to think of it as "free variables are
> implicitly universally quantified" (which may be equivalent).
>
> There is also a convention to avoid free variables whenever possible, which
> is mentioned a little bit in these threads:
> http://www.gilith.com/opentheory/mailing-list/2011-January/000037.html
> http://www.gilith.com/opentheory/mailing-list/2011-September/000111.html
>
> Cheers,
> Ramana
>
>
> On Mon, Nov 19, 2012 at 3:05 PM, Chantal Keller <chantal.keller at wanadoo.fr>
> wrote:
>>
>> Dear Ramana,
>>
>> First excuse me for mistyping your name.
>>
>> If we treat free variables as universally quantified, I imagine we
>> should understand the answers given by opentheory as : if each
>> assumption is valid (ie. true for any interpretation), then each theorem
>> is valid. This is weaker than my previous understanding, but with this
>> one my example does not break consistancy.
>>
>>
>>
>>
>>
>>
>> Le 19/11/2012 15:34, Ramana Kumar a écrit :
>> > Dear Chantal,
>> >
>> > Now I agree your example is surprising and may point to a flaw in the
>> > inference kernel.
>> > However, I will wait for Joe to comment.
>> >
>> > One other possibility is that we're equivocating on the semantics of a
>> > theory package.
>> >>From the OpenTheory webpage: "A higher order logic theory package Γ ⊳ Δ
>> > consists of a proof that the theorems in Δ logically derive from the
>> > assumptions in Γ".
>> > In higher-order logic it's conventional to treat free variables as
>> > universally quantified.
>> > Hence it is reasonable to deduce falsity from the assumption |- x <=> T,
>> > just as it would be unsurprising if you were to assume |- !x. x <=> T
>> > and
>> > deduce falsity.
>> >
>> > To put it another way, is there any context in which you could use your
>> > test.art to prove falsity while only assuming the axioms of HOL? Is it
>> > possible to create an article that satisfies the assumption |- x <=> T,
>> > without again assuming something equivalent?
>> >
>> > Cheers,
>> > R[a]mana
>> >
>> >
>> >
>> > On Mon, Nov 19, 2012 at 2:14 PM, Chantal Keller
>> > <chantal.keller at wanadoo.fr>wrote:
>> >
>> >> Hi Rumana,
>> >>
>> >> I forgot to mention the key point leading to such a problem: it
>> >> consists
>> >> in applying [absThm] to an assumption with open terms. [absThm] check
>> >> that we do not abstract over a free variable of the context, but not
>> >> over a free variable of the assumptions.
>> >>
>> >> I do not understand your problem with the "x"s: the theorem is closed,
>> >> I
>> >> could as well have obtained
>> >>
>> >> 2 input type operators: -> bool
>> >> 2 input constants: = T
>> >> 1 assumption:
>> >>   |- x <=> T
>> >> 1 theorem:
>> >>   |- (\y. y) = \y. T
>> >>
>> >> (see attached).
>> >>
>> >> An interpretation that satisfies the assumptions but not the
>> >> theorems is simple : [x ↦ T].
>> >>
>> >>
>> >>
>> >> Le 19/11/2012 14:53, Ramana Kumar a écrit :
>> >>> Hi Chantal,
>> >>>
>> >>> I haven't looked at your article yet, but one possibility that comes
>> >>> to
>> >>> mind is that the two "x"s on the left hand side of the theorem are
>> >> distinct.
>> >>> What is your interpretation that satisfies the assumptions but not the
>> >>> theorem?
>> >>> Does it still work if the x under the binder has a variable type
>> >>> (while
>> >> the
>> >>> x in the body has type bool)?
>> >>>
>> >>> Ramana
>> >>>
>> >>>
>> >>> On Mon, Nov 19, 2012 at 1:46 PM, Chantal Keller
>> >>> <chantal.keller at wanadoo.fr>wrote:
>> >>>
>> >>>> Dear OpenTheory users and developers,
>> >>>>
>> >>>> It appears to me that opentheory checks as correct wrong
>> >>>> certificates.
>> >>>>
>> >>>> Attached is an example. opentheory answers:
>> >>>>
>> >>>> 2 input type operators: -> bool
>> >>>> 2 input constants: = T
>> >>>> 1 assumption:
>> >>>>   |- x <=> T
>> >>>> 1 theorem:
>> >>>>   |- (\x. x) = \x. T
>> >>>>
>> >>>> But I think this should be forbidden: there is an interpretation of
>> >>>> the
>> >>>> variables that satisfies the assumptions but not the theorems.
>> >>>>
>> >>>> Perhaps you should restrict assumptions to close terms, or add a side
>> >>>> condition to the absThm rule?
>> >>>>
>> >>>> Thanks,
>> >>>>
>> >>>>
>> >>>> _______________________________________________
>> >>>> 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
>> >>
>> >> --
>> >> Chantal KELLER
>> >>
>> >
>>
>> --
>> Chantal KELLER
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>