In The psychology of invention in the mathematical field, p. 53, Hadamard makes the following claim:
Is his point that there must, in any axiomatic theory, be undefined terms, and if you write the parallel postulate entirely expanded, i.e., with definiens substituted for definiendum , then you will see that its not a truth of logic? But that seems completely off. You may still "see" that its a truth for perceptual space (let us grant, for the sake of the argument), and moreover, you may still fail to see that it isn't implied by the other axioms+logic. Thus, while you may arguably conceive of the possiblity of non-Euclidean axiom systems, you might still not yet perceive that of non-Euclidean geometries (qua sciences of space); and in fact, without a proof of relative consistency of these systems, e.g. by an inner model in Euclidean geometry, or by a model in R, you aren't technically allowed to even assume so much as the possibility of these systems, since (lacking such proof), the PP might -- for all you know -- after all be a consequence of the other axioms.
Am I completely misunderstanding Hadamard's point here?
Let start from Euclid's definition:
The issue is not about substitution of definiens in place of definiendum in the statement of the postulate.
The original text of Euclid's Postulate 5 does not use the definiendum "parallel lines" but refers to the "meeting condition" of the definies:
The issue is to note that in Post.5 Euclid uses a property of lines: to meet that is not mentioned in any other postulates.
Thus, we cannot derive anything about "lines meeting" from them.
Obviously, it is not easy at all to note this fact: the modern concept of model (the intuitive one) dates from late XIX Century and was very far away from Ancient and Early Modern mathematics.
Hilbert's proof is a mathematical proof, and not an intuition (made with hindsight).
The question posed by Hadamard can be rewritten as: can Pascal have had that intuition without a development of mathematics comparable to that of Hilbert?