[eru]

Agreed.

> Furthermore, even if "X OR NOT X" is true (regardless of what X is, as long as it is well-formed), that does not mean that either "X" must be true or "NOT X" must be true.

Independent of manipulating meaningless symbols, there's a whole branch of math called 'constructivism' where people try to find proofs without the 'law of the excluded middle'. Ideology / philosophy aside, the methods developed for this curiously handicapped game are of practical interest in computer science.