Hello
I've been trying to prove this, but I don't even know how to start.
Assuming, a, b, c € N, I wanted to prove that if
a < b and b < c then a < c.
I know that
a < b is the same as saying
there is a X for which a + x = b
Now, I've tried doing the same for b < c
there is a Y for which b + y = c
Now, is there anyway to "mix them" together? What bothers me is that I don't even know if it possible, as both equations are "inside" the existencial quantifier. Or are they not? If I could make the second equation
there is Y for which b = y - c
and could mix it into something like
there is X, Y such that a + x = -y + c
then it would be easy to prove this.
Any help is appreciated
What is also self-evident, is that unless you post your entire axiom set we have no way to help.
If you require rigor, we need exact axioms and definitions.
This material can be and has been developed in many different ways.
Here is a simple one. Define a<b to mean b-a>0.
Then a<b & b<c means b-a>0 & c-b>0.
Adding we get c-a>0 or a<c.
But that probably does you no good since it probably differs from the way your text material treats this topic.
I am quite surprised that transitive property of real numbers would require proving.
If and , then ; otherwise it would mean , which would be a contradiction to the hypothesis. If this does not satisfy you. We can try again. say
Assume to the contrary that and , then . Say , it follows that
implies . This, however, contradict to our assumption. Therefore . This should be more that sufficient to say .
Yes, there is a way to mix them. The formula is equivalent to , both in the sense that they are true in the same models and in the sense that each one is derivable from the other. In fact, the latter formula is a prenex normal form of the former.Now, is there anyway to "mix them" together? What bothers me is that I don't even know if it possible, as both equations are "inside" the existencial quantifier. Or are they not?
When we are talking about derivability, there is something similar to "existential elimination rule". It says that if is already derived and from the assumption with the free variable one derives , then is derived (from the assumption ). In fact, this is nothing but formalization of a common way we deal with an assumption that asserts existence of something. So, having and , we apply existential elimination twice to get with free variables . After that, we introduce, i.e., add, existential quantifiers back.
If your doubts are about something else, feel free to clarify.
One of the most natural ways to record derivations formally is called, well, Natural Deduction. Each inference rule is written as a line with assumptions written above and one conclusion below the line. Also, there are scoping rules: some assumptions are available up to some point, after which the are closed. E.g., in proving A -> B, we assume A and may use it to derive B. Then A is closed and we obtain A -> B. After that, A can no longer be used.
Existential elimination rule (using an assumption of the form has the following form.
Here the assumption is closed by the last line. It corresponds to regular mathematical practice: if we know , but don't know what exactly is, we could prove that implies for any . Then we would know .
In text form, it is convenient to write derivations showing scoping explicitly. The existential elimination rule is written as follows.
This means that, having , we temporarily introduce an assumption , deduce from it, and then close . The result is a derivation of from .Code:
Using this, the proof about < can be written as follows.
Code:(1) assumption (2) introducing a temporary assumption from (1) (3) assumption (4) introducing a temporary assumption from (3) (5) from (2), (4) (6) from (5) (7) from (6) (8) close (4) (9) close (2)
Will it be incorrect to write:
(1) assumption
(2) universal elimination of (1)
(3) assumption
(4) universal elimination of (3)
and replace with when introducing existential quantifier later?
?
Won't it be easier with universal elimination? It requires only 2 lines. What is the reason for choose the above instead?Code:
He did. He did. He stated that he was working in the natural number system.
I would not consider that a good proof because, generally "b- a" is not defined in the natural number system. Julius's proof avoids that.This material can be and has been developed in many different ways.
Here is a simple one. Define a<b to mean b-a>0.
Then a<b & b<c means b-a>0 & c-b>0.
Adding we get c-a>0 or a<c.
But that probably does you no good since it probably differs from the way your text material treats this topic.