Terence Tao's 'QED' is an interactive textbook for the web which teaches propositional and first-order logic

https://teorth.github.io/QED/