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). A construction is in general a series of computational steps intertwined with deduction steps. (For example, while constructing a solution of a differential equation, we may have to argue that a certain sequence converges.)
Traditional foundations layer first-order logic at the bottom and set theory on top. In first-order logic there are no constructions, at least not of the kind that mathematicians often perform in practice. Because of this mathematicians often formulate constructions inappropriately as abstract existential statements (as there is no other kind in first-order logic). They say
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.
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 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".