Axiom talk:Hilbert's Axioms

Work to be done

Obviously, this is not the final version, but this is the form of the axioms I found in my source. I understand that every axiom should go to a separate page which will be done in the near future. I will probably need to introduce a shorthand notation for primitive relations, because any other presentation I find online so far is very verbal. I've seen betweenness relation in Tarski's axioms, and I think others should have their shorthand notations as well. Also the names of individual axioms and groupings have not settled yet. Some sources provide better suggestions than others.--Julius (talk) 20:24, 22 August 2022 (UTC)

Well overdue, and big thanks for taking it on. --prime mover (talk) 21:48, 22 August 2022 (UTC)

I guess these axioms are for planar Euclidean geometry? Good to make that explicit. — Lord_Farin (talk) 09:31, 23 August 2022 (UTC)

Nice catch. Planar geometry indeed.--22:33, 23 August 2022 (UTC)

Incidentally, before we travel too far down the road, I moved this page to the Axiom namespace. I think it better belongs there. --prime mover (talk) 18:38, 23 August 2022 (UTC)

Presentation

I wonder whether it would make the page prettier if we were to make the axioms heading-3 rather than heading-2? --prime mover (talk) 09:36, 26 August 2022 (UTC)

Whatever suits you better. At the moment I am focused on rewriting everything with fewer words and making it look more like Tarski's axioms. It seems that various sources introduce their own notation, and the number of axioms seems to vary as well. Hence, mapping their ideas on what I have here is not so trivial.Julius (talk) 22:13, 27 August 2022 (UTC)

$p$ is a point

Depends on what we want to do. For a simple description this is sufficient. But if we ever plan to make strict connections with the first- or second- order logics then we need this notation.--Julius (talk) 22:21, 27 August 2022 (UTC)

Yes, absolutely, But I would say we need it in describing the connection, not in the axioms itself. So only in the translation to 1OL/2OL does it become relevant, or at least that's how I see it.

We just have to be careful about applying set-theoretic machinery because a priori this translation might not be 100% faithful. — Lord_Farin (talk) 08:52, 28 August 2022 (UTC)

Oh, I only now saw the edit you made. In my view adding the "sets" convolutes the exposition because instead of just working with points and lines, we have to talk about sets and stuff. Before you know it you will assume stuff like $l = \{p: I(p,l)\}$ and write $p\in l$.

If we want to discuss point and lines, then we should not bother with sets. That comes when we want to interpret planar geometry in terms of set theory. But not before that moment.

So I would really like to suggest that the exposition be modified to exclude the $\in$ symbol and "set" word. — Lord_Farin (talk) 08:59, 28 August 2022 (UTC)

Let's see how I see this problem. We are trying to write down an axiomatic system which is a sort of digest of abstract notions pertaining to the Euclidean geometry. For that we have to write down basic notions of various elements and their relations. We can write this with words or with symbols whose meaning we explain somewhere earlier. At the moment we are not considering any connection to 1OL or 2OL, so any symbols or notions we introduce here are independent of standard axiomatics. So even if here we use a word "set", until we show that this maps to the standard set, the term should have no problem existing within the context of these axioms (except for the confusion using the same string of symbols denote apriori two different things). However, you suggest avoiding using the notion of sets and, by extension, the entire set builder notation. Most likely this can be done. Just at the moment I am interpolating between several texts, and set theory for me was a good starting point to condense everything. I will see what I can do. But along the way I may need to introduce some new notation so please bare with me.--Julius (talk) 18:04, 28 August 2022 (UTC)

Unfortunately upon closer inspection the axioms and formulation are just lacking and I had to put a {{Questionable}} template. I also tried to fix some of the most obvious issues but was probably not complete.

I think in part this arose exactly because symbols and set notation were taken instead of words. Why not include some text at least to describe what you are trying to do?

Your specifications lack things like "distinct points" instead of "points" and mix up quantifier order. I can't stress enough that all these troubles would be avoided by simply using words. Words are more clear than symbols. It is kind of frustrating to witness. — Lord_Farin (talk) 18:25, 30 August 2022 (UTC)

The fact that the exposition is questionable is not questionable, hence the WIP template. The text will reappear in due time. My initial goal was to rewrite all of this in a way similar to Tarski's axioms. However, the primitive notions and relations are different so differences are bound emerge. Simple text is not enough because "lie on" was defined for points on lines, but then they also "lie on" segments, and the problem remains. I am also comparing these axioms with a number of other sources and I am very familiar with differences between all of them. This is why the progress is not a simple convergence to a nice result and why one should not jump to conclusions.--Julius (talk) 20:38, 30 August 2022 (UTC)

I finished my first run. Indeed not everything is well defined. Since, as the source states, this was a simplified presentation, I am moving to the original Hilbert's axioms. What is more, in parallel I am reading an article on formalization of the axioms on Isabele/Isar. What is nice is that in the process they translate text into rather formal language, so we do not have to start from scratch. Also, they introduce "distinct points","lies on line", "lies on segment", "lies on ray" as separate relations that we noticed as well. Finally, they conclude that some of the axioms are ambiguous and implicitly rely on pictures (worth mentioning here, preferably with pictures explaining this). This is supported by various conversations concluding that, strictly speaking, Hilbert's axioms are in some sense incomplete, although a great deal of them are derivable from Tarski's axioms.--Julius (talk) 07:48, 31 August 2022 (UTC)

I think I have almost converged to what I would like to present. I removed symbolic exposition for now, since logical sentences sometimes are a bit lengthy. If there is a demand, we can always reinstatiate them. What is lacking now is mostly the appearance. The floor is open for discussion.--Julius (talk) 21:33, 28 September 2022 (UTC)

Presentation

Couple of things:

Any reason to add the NOTOC? Makes it hard to see what's on the page.

I used Axiom:Tarski's Axioms as a starting point for this page, so I tried to follow its style. It these auxiliaries are unnecessary, feel free to remove them.--Julius (talk) 07:27, 29 September 2022 (UTC)

Can the axiomata be numbered? --prime mover (talk) 05:15, 29 September 2022 (UTC)

They can be numbered, but usually they are presented in groups, those being: incidence (or connection), order, congruence, parallels, and continuity. But we can choose, whether to reset numbering for each group or just count them to ~20. Definitions for composite notions usually are not numbered. Some people present them together in the beginning, others - just before they need them.--Julius (talk) 07:27, 29 September 2022 (UTC)