search

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

Need to clarify explanation of last tableau in the example in tableaux/identity.tex #312

Closed furcyd closed 2 years ago

furcyd commented 2 years ago

I think that the last paragraph (and possibly the tableau itself; see below) in the example within tableaux/identity.tex needs to be rewritten. That is the paragraph that explains the tableau for proving that equality is transitive.

The reason I find this paragraph confusing is because the terms t_1 and t_2 used in this tableau do not line up with the ones used in the =T inference rule. Namely, in this example, t_2 (resp. t_3) plays the role of t_1 (resp. t_2) in the rule. So when, reading the current text, it is not clear whether the terms in the text refer to those in the rule or those in the tableau. Rewriting the tableau with t' through t''' instead t_1 through t_3 would be one way to solve this issue.

rzach commented 2 years ago

fixed in ec6994c893e6c298997831741b217dea85a3ec1c