I am reading the book: Volume 1: Logical Foundations
Inductively Defined Propositions
I am not able to understand how to solve next 2 tasks:
Exercise: 2 stars, standard, optional (total_relation) :
Define an inductive binary relation total_relation
that holds between every pair of natural numbers.
Exercise: 2 stars, standard, optional (empty_relation)
Define an inductive binary relation empty_relation (on numbers) that never holds.
I don’t understand the logic. I tried to solve somehow… please see the bottom of attached screenshot.
Please give me a hint if you can.
Is that correct that “total relation” is “less than” relation?
There are a lot of total relations on natural numbers, right? For example “more than” is also a total relation, right?
Is one constructor enough?
I destruct m. Is it enough? Or n should be considered too?
Is that correct that empty_relation can throw away parameters in constructor and return just couple of arbitrary numbers? Or maybe constructor here should not have parameters at all?