# What is a construction (in mathematics)?

Backstory: A question arose in a seminar that concluded with the statement that Bernoulli shifts with the same entropy are isomorphic (proven by Ornstein in 1970 paper here): "Did Ornstein construct an explicit isomorphism?" The reply was that Ornstein indeed outlined a procedure. I left wondering about the definition of construction. This leads to my question.

Question: What is a construction (in mathematics)?

The answer I instinctively came up with is that a construction is a set in Gödel's constructible universe

I feel that this cannot be the complete picture.

• Category theory has a notion of a "universal property" which wants to describe structures up to isomorphisms. Then the class of all such structures may not be a set. Then maybe a construction is instead a class of objects satisfying a "universal property" i.e. a definable class. This falls in line with What is a Universal Construction in Category Theory?

• Formal logic with a deductive apparatus has a notion of a "proof" which wants to describe "theorems". Then maybe a construction is instead a "proof." i.e. a finite sequence of steps in the construction. This falls in line with Formally what is a mathematical construction?

There are three main ideas (1) existence <Gödel's constructible universe> (2) universal property <What is a Universal Construction in Category Theory?> and (3) finite sequence of steps <Formally what is a mathematical construction?>

Should all three combined be the definition?

• Have you heard of Coquand and Huet's Calculus of (Inductive) Constructions ? This is more or less the core of Coq. Although I completely agree with Asaf's answer for the concept of a construction in everyday mathematics, it can still be interesting to come up with a formal object that behave like this concept (in the same manner everyday mathematicians does not write formal proofs and does recognize something as a proof even when not written in a formal system, but still the formal sequences called "proofs" in logic are interesting to study). – Pece May 16 '18 at 8:08
• I have not. Thank you! I wonder if this is the type theory analog of the set theory constructible universe. Being unfamiliar with type theory, I am instinctively resorting to finding a comparison with set theory. – Alberto Takase May 16 '18 at 14:16

Suppose that you work in $\sf ZF+AD$. That means that the reals are not well-orderable. But you can still construct them from $\Bbb Q$. But now $\Bbb R\notin L$, so can you construct it or not? What about the "real reals"? Are they in $L$ or not? Maybe Woodin's Ultimate $L$ instead? But whenever Platonism is involved, questions of choice-of-theory start to rear their ugly head.