Inductive Relations

一个由数字（如ev）参数化的命题可以被认为是一个属性——也就是说，它定义了nat的子集，即命题可证明的那些数字。同样，一个双参数命题可以被认为是一种关系——也就是说，它定义了一组可证明命题的对。