Conversation

Brendan Zabarauskas
@brendanzab
In natural deduction, is there a word for a bunch of related formation, introduction, elimination, and computation rules? Examples would be: pairs, functions, records, etc. I think some would call these 'types' but somehow I feel that only covers the type constructor part.
6
2
Gus
@guhou
Isabelle organises proofs into ‘theories’, which are essentially modules, but that might be broader than what you mean here?
2
1
Gus
@guhou
I think it’s also analogous to the T in SMT- eg one might speak of the ‘theory of integers’ which is the type and related rules?
1
1