There are many aspects to the question "does a logical formalism reflect mathematical practice?" I will focus just on a very simple but important detail that every mathematician is familiar with.
In mathematical practice we differentiate between
- $\phi$ or $\psi$, and we know which one, and
- $\phi$ or $\psi$, but we may not know which one.
We also differentiate between
- there is a given $x$ such that $\theta(x)$, and
- there is $x$ such that $\theta(x)$, but we may not be given one.
Let me call the first kind the concrete disjunction an existential, and the second kind the abstract disjunction and existential. (There is no established terminology.) Thus, "concretely $\exists x \,.\, \theta(x)$" is meant to convey that I have a particular $a$ such that $\theta(a)$, while "abstractly $\exists x \,.\, \theta(x)$" is meant to convey that we know there is an individual satisfying $\theta$, but we may not have a specific one.
First-order logic formalizes the abstract version, because the inference rule for existentials forgets the witness $a$:
$$\frac{\phi(a)}{\exists x \,.\, \theta(x)},$$
Martin-Löf type theory formalizes the concrete version because the witness $a$ is recorded in the proof term:
$$\frac{p : \theta(a)}{(a,p) : \sum_{x : A} \theta(x)}.$$
A formalism which captures both is Martin-Löf type theory with propositional truncation. This is an operation which hides witnesses of statements. If you are familiar with type theory then you can look it up in homotopy type theory. If you are an ordinary mathematician, then it can be described as a quotient: given a type $A$, its propositional truncation $|A|$ is the quotient $A/{\sim}$ by the trivial equivalence relation $\sim$ which relates every $x$ and $y$ in $A$. Thus, if $A$ has an element then $|A|$ has one element. If $A$ is empty, then $|A|$ is empty as well.
With propositional truncation we can get all four variants:
- concrete disjunction is $\phi + \psi$
- abstract disjunction is $|\phi + \psi|$
- concrete existential is $\sum_{x : A} \theta(x)$
- abstract existential is $|\sum_{x : A} \theta(x)|$
Propositional truncation can be defined in homotopy type theory as a higher inductive type. Thus, homotopy type theory reflects mathematical practice (in one respect) better than logic and Martin-Löf's propositions-as-types.
You are asking about "layers" of logic and mathematics, so let me address this as well. In mathematical practice we prove statements and perform constructions (an early reference of such activity would be Euclid's Elements). Moreover, deduction and construction steps are intertwined. During a proof we often consturct auxiliary objects, and a complicated construction may require justification of certain steps. (For example, while constructing a solution of a differential equation, we may have to argue that a certain sequence converges.)
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.
There are real-world consequences of the failure of logic to correctly capture the multi-layered nature of constructions and deductions: mathematicians often formulate constructions inappropriately as abstract existential statements (as there is no other kind in first-order logic). They say
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.
In contrast, Martin-Löf type theory is a theory of constructions, so there the problem arises when we want to state something without giving a specific construction. Once again, homotopy type theory comes to the rescue with the idea of propositional truncation. And we can precisely explain which bits of a statement are to be read as constructions and which ones as abstract existence. An example may help here:
- $\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".
