Proving \neg x \vee x in Hilbert System: A Logical Dilemma

AI Thread Summary
The discussion centers on proving the logical expression ¬x ∨ x using the Hilbert system. Participants express confusion over the appropriate axioms to use, noting that different sets may apply. One contributor highlights that the expression is always true regardless of the truth value of x, but struggles with how to construct a formal proof within the Hilbert framework. There is a call for clarification on which axioms are permissible for this proof. Overall, the conversation reflects a mix of frustration and a desire for guidance on applying the Hilbert system to this logical dilemma.
hamsterman
Messages
74
Reaction score
0

Homework Statement


Prove \neg x \vee x using Hilbert system.

Homework 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))

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.
 
Physics news on Phys.org
hamsterman said:

Homework Statement


Prove \neg x \vee x using Hilbert system.

Homework 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))

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.

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.
 
Mark44 said:
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.

There there is something called the Hilbert system, but it's actually called Hilbert–Ackermann system.
 
I know it is true. That fact does not interest me. The proof using Hilbert system does.
 
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.
 
Back
Top