OpenLogicProject / OpenLogic

An open-source, customizable intermediate logic textbook
http://openlogicproject.org/
Creative Commons Attribution 4.0 International
1.02k stars 234 forks source link

Minor error in example 12.25 #367

Closed marethyu closed 2 months ago

marethyu commented 4 months ago

If I'm not mistaken, $\mathcal{Q}'\models\Gamma\cup\Delta_0$ should be $\mathcal{Q}'\models\Gamma_0\cup\Delta_0$ for some finite $\Gamma_0\subseteq\Gamma$, since $\Gamma$ could be infinite?

Also, \{0<c\} should be \{\Obj{0}<c\}.

capture1

beastaugh commented 2 months ago

I see this is fixed, but I'm not convinced this was ever actually a typo: the family of structures that interpret $c$ as $1/K$ for $K \geq 1$ do satisfy all of $\Gamma$, not just some finite $\Gamma_0 \subseteq \Gamma$, and hence satisfy $\Gamma_0$ by monotonicity (realising this is part of the exercise of "prove this in detail"). But perhaps presenting it in the updated way makes it easier to understand…

rzach commented 2 months ago

Yes, it was not actually a typo, but I also thought it would be easier to follow this way (as evidenced by @marethyu 's suggesting the change - thanks BTW Jimmy!)