[opentheory-users] defineTypeOp underspecified? / opentheory be used as a proof verifier

[Joe Leslie-Hurd]

Hi Gunter and Ramana,

>> I guess the new type operator op with name n has
>> type parameters α1 ... αk in this order, and
>> the types of rep and abs are
>>  rep:: n α1 ... αk -> b
>>  abs:: b -> n α1 ... αk (using prefix notation for the type-operator)
>> where b is the type of t
>> Is that true?
>
> That is correct.

Thanks for the clarification, I have added a note to defineConst and
defineTypeOp to spell this out:

http://www.gilith.com/research/opentheory/article.html#defineConstCommand
http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand

> However, I think if you are using a type operator whose definition is known
> and supply the wrong number of arguments, article processing will fail. Joe
> can probably confirm and clarify this.

I don't believe this affects soundness, so I regard this as
implementation-dependent behaviour. In the opentheory logical kernel
you can use a defined type operator with the wrong number of arguments
or a defined constant outside of its principal type, but there won't
be much you can prove about such types/terms. The logical kernels of
other systems might throw an exception if you try to construct such
types/terms.

> Yes. The opentheory tool can be used to verify that articles obey the
> derivation rules of (OpenTheory's variant of) HOL.

Agreed, and not just the opentheory tool, but any tool that processes
articles (such as your python tool in development).

Cheers,

Joe