1. The problem statement, all variables and given/known data Prove [itex]\neg x \vee x[/itex] using Hilbert system. 2. Relevant equations The logical axioms. I'm not sure if I should state them, or whether there is a standard set. It seems to me that different sets are used. Anyway, the ones with disjunction in them are: [itex]a \rightarrow a \vee b[/itex] [itex](a \rightarrow c) \rightarrow ((b \rightarrow c) \rightarrow (a \vee b \rightarrow c))[/itex] 3. The attempt at a solution If I wanted to use the first axiom, I'd have to prove x, which can be false. If I used the second axiom, I'd get what I wanted on the wrong side of the arrow. I don't think there is a way to reverse an arrow, except for [itex](x \rightarrow y) \rightarrow (\neg y \rightarrow \neg x)[/itex], but then I'd have no way to get rid of the negation. I'm lost. I'd appreciate help.