Return to Answer

Traditional foundations layer first-order logic at then a first-order theory on top. This only captures the case of a logical deduction during which we perform axuliary constructions (expressed as terms of the first-order language) that require no further justifications. However, in practice we need more than that. For example, in the theory of fields it is natural to think of inverse as an operation. Every time we write $x^{-1}$ we need to argue that $x \neq 0$, so inverse is a construction which requires justification. If you look at how the theory of fields is formalized, you will see that it is unsatisfactory: either inverses are treated abstractly as existentials (instead of having the operation $x \mapsto x^{-1}$ we only state $\forall x \,.\, x \neq 0 \Rightarrow \exists y \,.\, x y = 1$), or the justification of $x \neq 0$ is ignored and the operation $x \mapsto x^{-1}$ is made everywhere defined by fiat by stipulating that $0^{-1} = 0$ or some such non-sense.

Traditional foundations layer a term language at the bottom and first-order logic on top. This only captures the case of a logical deduction during which we perform axuliary constructions (expressed as terms of the first-order language) that require no further justifications. However, in practice we need more than that. For example, in the theory of fields it is natural to think of inverse as an operation. Every time we write $x^{-1}$ we need to argue that $x \neq 0$, so inverse is a construction which requires justification. If you look at how the theory of fields is formalized, you will see that it is unsatisfactory: either inverses are treated abstractly as existentials (instead of having the operation $x \mapsto x^{-1}$ we only state $\forall x \,.\, x \neq 0 \Rightarrow \exists y \,.\, x y = 1$), or the justification of $x \neq 0$ is ignored and the operation $x \mapsto x^{-1}$ is made everywhere defined by fiat by stipulating that $0^{-1} = 0$ or some such non-sense.

• $\prod_{n : \mathbb{N}} \sum_{b : \{0,1\}} \sum_{k : \mathbb{N}} n = 2 m + b$ means "a construction which decomposes a number into its least significant bit and the rest of the number".
• $\prod_{n : \mathbb{N}} \sum_{b : \{0,1\}} \big|\sum_{k : \mathbb{N}} n = 2 m + b\big|$ means "a construction which calculates the least significant bit of a number".
• $\prod_{n : \mathbb{N}} \big|\sum_{b : \{0,1\}} \sum_{k : \mathbb{N}} n = 2 m + b\big|$ means "every number is (abstractly) even or odd".

• $\prod_{n : \mathbb{N}} \sum_{b : \{0,1\}} \sum_{k : \mathbb{N}} n = 2 k + b$ means "a construction which decomposes a number into its least significant bit and the rest of the number".
• $\prod_{n : \mathbb{N}} \sum_{b : \{0,1\}} \big|\sum_{k : \mathbb{N}} n = 2 k + b\big|$ means "a construction which calculates the least significant bit of a number".
• $\prod_{n : \mathbb{N}} \big|\sum_{b : \{0,1\}} \sum_{k : \mathbb{N}} n = 2 k + b\big|$ means "every number is (abstractly) even or odd".

Theorem 4.2: $\exists x \,.\, \theta(x)$.  Proof. (Construction of $x$ is given here.) QED

and later refer to Theorem 4.2 as if it were a construction.

Theorem 4.2: There exists $x$ such that $\theta(x)$. 

Proof. (Construction of $x$ is given here.) QED

and later refer to Theorem 4.2 as if it were a construction. It is as if they were ashamed of saying

Problem 4.2: Give $x$ such that $\theta(x)$.

Construction. (Construction of $x$ is given here.) DEFINED

We should all go back to reading Euclid.