hilbert's axiom

Stream: new members

[tica]

I'm trying to formalize hilbert's axioms and I have some questions about the order axioms.

structure Segment :=
  (A B : Point)
infix `⬝`:56 := Segment.mk

constant Between : Point → Segment → Prop
infix ` ∈ₚₛ `:50   := Between
notation a ` ∉ₚₛ `:50 s:50 := ¬ Between a s

--1
axiom between_comm (A B C : Point) : B ∈ₚₛ A⬝C → B ∈ₚₛ C⬝A

--2
axiom between_exist (A C : Point) (h : A ≠ C): ∃ B, B ∈ₚₛ A⬝C

--3
axiom between_only_one (A B C : Point) : B ∈ₚₛ A⬝C → ¬(C ∈ₚₛ B⬝A)

1) B must be different from A and C? A and C must be different ?
2) same question for axiom two
3) For the definition of the segment, the two points must be different ?

I use two sources, wikipedia and The Foundations of Geometry
What is complicated is that the axioms are not exactly said the same (sometimes not as complete) so I don't know which source has the correct axioms.

For example for axiom 1 there are two statements.
If a point B lies between points A and C, B is also between C and A, and there exists a line containing the distinct points A, B, C.
If A, B, C are points of a straight line and B lies between A and C, then B lies also between C and A.

Thanks

[Yaël Dillies]

cc @Bhavik Mehta

[tica]

I have tried to prove this theorem but I cannot prove either way.

example (A C : Point) (A_ne_C : A ≠ C) : A ∉ₚₛ A⬝C :=
begin
sorry
end

example (A C : Point) (A_ne_C : A ≠ C) : A ∈ₚₛ A⬝C :=
begin
sorry
end

I have the impression that there is indeed something missing in the axioms.

[Eric Wieser]

Wikipedia's description of the first axiom says "For every two points A and B there exists a line a that contains them both"

[Eric Wieser]

From which those two statements are trivially true. It sounds like you forgot to write down the "contains them both" axiom?

[tica]

No, it's not the same thing.
Here I am talking about a segment and not a line

[Reid Barton]

I hope they are not both true

[Reid Barton]

I think you can prove the first one, using between_only_one and probably also between_comm.

[Reid Barton]

proof

constant Point : Type
structure Segment :=
  (A B : Point)
infix `⬝`:56 := Segment.mk

constant Between : Point → Segment → Prop
infix ` ∈ₚₛ `:50   := Between
notation a ` ∉ₚₛ `:50 s:50 := ¬ Between a s

--1
axiom between_comm (A B C : Point) : B ∈ₚₛ A⬝C → B ∈ₚₛ C⬝A

--2
axiom between_exist (A C : Point) (h : A ≠ C): ∃ B, B ∈ₚₛ A⬝C

--3
axiom between_only_one (A B C : Point) : B ∈ₚₛ A⬝C → ¬(C ∈ₚₛ B⬝A)

example (A C : Point) : A ∉ₚₛ A⬝C :=
begin
  intro h,
  have h' : A ∈ₚₛ C⬝A := between_comm _ _ _ h,
  exact between_only_one _ _ _ h' h,
end

[tica]

@Reid Barton Thanks, I was going into much more complicated things...

Is this really intended or is it just a consequence of a badly written axiom?

[Reid Barton]

I'm not exactly sure what you mean but I believe the intended interpretation of between A B C is indeed that B lies on the open segment from A to C (which is not possible if any two of A, B, C coincide).

[Reid Barton]

Of course, it would have been helpful for the English explanation of the meaning of the axioms to say this explicitly.

[tica]

Okay great.
Yes it is not clearly stated and the two sources give slightly different axioms.

[tica]

I'm trying to prove this theorem:

example (A B : Point) (A_ne_B : A ≠ B) : {C : Point | C ∈ₚₛ A⬝B}.infinite:= by sorry

Normally we can prove it with the above axioms.

I'm completely lost with subset, subtype, set.finite, finset, fintype, ...
On paper it's obvious from the between_exist axiom but I don't understand how to do it with lean.

[Sebastien Gouezel]

Is it really obvious? What if your space is made of three points and a single line containing all of them?

[Sebastien Gouezel]

Sorry, I didn't read your axioms correctly.

[Sebastien Gouezel]

tica said:

On paper it's obvious from the between_exist axiom but I don't understand how to do it with lean.

Can you explain your paper proof?

[tica]

@Sebastien Gouezel Let A and C be two points such that A ≠ C.

By the axiom between_exist there exists a point B such that B ∈ₚₛ A⬝C.
From there, one can construct an infinite set of points by applying the axiom repeatedly.

[tica]

We could also define an order relation of the points on the segment AC (I don't know how to do that).
Assuming that the set is finite, one could prove that this is nonsense using the axiom between_exist.
It looks better this way but I don't know how to do it

[Kevin Buzzard]

How do you know that the 37th point you construct is not equal to the 42nd point? This is the kind of thing which you'll have to formalise. In fact if you are not careful with how you apply the axiom then perhaps the 37th point is equal to the 42nd point. So you have to write down very precisely how you are repeatedly applying this axiom and then prove that it gives an infinite set of points. It's just a case of writing down your argument, but carefully.

[Reid Barton]

In addition you need to prove that all the points you construct actually belong to the original interval

[Jireh Loreaux]

I think another axiom is necessary, but I might be wrong. In particular, I think you need something like this:

axiom between_of_between (A B C D : Point) : (B ∈ₚₛ A⬝C) → (C ∈ₚₛ B⬝D) → (B ∈ₚₛ A⬝D)

[kali]

(deleted)