# Using Hilbert logic axioms

1. May 4, 2012

### hamsterman

1. The problem statement, all variables and given/known data
Prove $\neg x \vee x$ 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:
$a \rightarrow a \vee b$
$(a \rightarrow c) \rightarrow ((b \rightarrow c) \rightarrow (a \vee b \rightarrow c))$

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 $(x \rightarrow y) \rightarrow (\neg y \rightarrow \neg x)$, but then I'd have no way to get rid of the negation. I'm lost. I'd appreciate help.

2. May 4, 2012

### Staff: Mentor

This seems like a lot of work to evaluate a very simple logical expression that is always true.
If x is true, then ~x is false, in which case ~x V x is true.
If x is false, then ~x is true, in which case ~x V x is again true.

How this fits into the Hilbert system, I have no idea, since that's a new one on me. I'm familar with Hilbert space, but not the Hilbert system.

3. May 4, 2012

### mtayab1994

There there is something called the Hilbert system, but it's actually called Hilbert–Ackermann system.

4. May 5, 2012

### hamsterman

I know it is true. That fact does not interest me. The proof using Hilbert system does.

5. May 11, 2012

### scurty

Can you list all of the axioms you are allowed to use? Like you said sometimes different sets are used, it'd be easier if we knew what ones you could use.