Correction in proof that OpenAssum relation is primitive recursive

OpenLogicProject / OpenLogic

An open-source, customizable intermediate logic textbook

http://openlogicproject.org/

Creative Commons Attribution 4.0 International

1.04k stars 237 forks source link

Correction in proof that OpenAssum relation is primitive recursive #297

Closed beastaugh closed 2 years ago

beastaugh commented 2 years ago

Sub-derivations should get smaller as i increases, not larger. This commit corrects that in both the prose explanation and in the formal definition of the OpenAssum relation.

rzach commented 2 years ago

Thanks!