You can certainly teach first-order logic and basic set theory to kids (highschoolers, I guess). This teaches both mathematical thinking and formalization. While it is not its primary goal, I think TLA+ (and TLC) is a _great_ way to play with FOL/ZFC. I'm sure a more basic UI can be built for TLC just for loading files and evaluating expressions.
Ron