값은 n항 생성자가 n개의 값과 결합한 것임.
항은 변수이거나 n항 생성자가 n개의 항과 결합한 것임.
그러므로 모든 값은 항이고, 0항 생성자는 그 자체로 값임.
식은 n항 술어가 n개의 항과 결합한 것임.
공리는 0개 이상의 식들을 전제로 가지고 1개의 식을 결론으로 가짐.
인터프리터에 식을 질의하면, 질의 안에 있는 각 변수에 어떤 값을 배정했을 때 식이 유도될 수 있는가를 답함.
한 공리에 있는 모든 변수들에 값을 배정했을 때, 전제에 있는 식들이 모두 유도될 수 있다면, 결론에 있는 식이 유도될 수 있음.
즉, 값이 배정된 식 A가 유도될 수 있다면 어떤 공리와 그 공리에 대한 적당한 변수배정이 존재하여 값이 배정된 결론이 A와 같고 값이 배정된 모든 전제들이 유도될 수 있음.

- 희망의 등불