1
$\begingroup$

Related questions: Formally what is a mathematical construction? and What is a Universal Construction in Category Theory?

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?

$\endgroup$
  • 2
    $\begingroup$ 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). $\endgroup$ – Pece May 16 '18 at 8:08
  • $\begingroup$ 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. $\endgroup$ – Alberto Takase May 16 '18 at 14:16
6
$\begingroup$

Your question sort of mixes syntax, semantics, informal notions of constructions, and Platonism or other philosophical approaches.

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.

The truth is that a construction is an outline, which is accepted by other mathematicians as a correct algorithm for starting from something and ending up with something else.

The exact details of what is a construction are left to vary between one field and another. You might argue that a diagram chasing argument and appealing to a universal property is not "enough" to be called a construction. Others would tell you that a transfinite recursion which heavily relies on the choice of choice function/well-ordering is not a construction. And others would tell you that unless you can explicitly compute each and every object in the "constructed target", then it's not a construction.

Each of these are subject to the conventional jargon of the field of interest. If mathematics is what mathematicians do and other mathematicians agree to be mathematics, then a construction is something that mathematicians construct in their respective fields, and their colleagues agree to be a construction.

So at the end of the day, "construction" is context dependent. It might be one thing for a set theorist, and a whole other thing for a group theorist, and an entirely different thing for someone working in proof theory. I don't think you can fully quantify this into a mathematical definition, just like you can't quite quantify what it means for two proofs to be the same. This is more of a "pornography" thing: you can identify a construction when you see one, but it has no exact definition.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.