$\newcommand\Con{\text{Con}}
\newcommand\Dec{\text{Dec}}$
Let $F$ be the formal system in which the proofs are to be carried
out, when it comes to your formal assertions of the form
$\Dec(\varphi)$. So we assume that $F$ is described by some
computable axiomatization. For example, perhaps $F$ is simply the
usual first-order PA axioms. Let me assume that $F$ is true in the
standard model $\mathbb{N}$, which is probably a case that you care most about. (But actually, I believe it is
sufficient in this argument to assume iterated consistency assertions about $F$.)
Let $A=\Con(F)$. I claim that this statement is
$\infty$-undecidable with respect to $F$.
To see this, argue as follows. By the incompleteness theorem,
since $\Con(F)$ is true, we know that $F$ does not prove $A$, and
since $F$ and $A$ are both true, it also follows that $F$ does not
prove $\neg A$. So $\neg\Dec(A)$ is true (that is, in the standard
model $\mathbb{N}$). But $F$ by itself cannot prove $\neg\Dec(A)$,
since $F$ proves $\neg\Dec(X)\to \Con(F)$, as an inconsistent theory has no undecidable statements, and so if it did it
would violate the incompleteness theorem. Note also that $F$
cannot prove $\Dec(A)$ either, since $\neg\Dec(A)$ is true. Thus,
$\neg\Dec(\Dec(A))$ is true. But $F$ cannot prove this, since then
again it would prove $\Con(F)$, violating incompleteness, and it
also cannot prove $\Dec(\Dec(A))$, since $\neg\Dec(\Dec(A))$ is
true. So $\neg\Dec(\Dec(\Dec(A)))$ is true. And so on.
For the general step, if $\Dec^n(A)$ is false, then $F$ cannot prove this, since then it would prove $\Con(F)$, contrary to the incompleteness theorem, and it cannot prove $\Dec^n(A)$ either since it was false and $F$ is true, and so $\Dec^{n+1}(A)$ is false.
This reasoning shows that $\Dec^n(A)$ will be false for every $n$,
and so $A=\Con(F)$ is $\infty$-undecidable, assuming that $F$ is
true in the standard model.
It seems likely to me that the content of what it was about "true
in the standard model" that the argument used should be covered by
the assumption merely that $\Con^n(F)$ holds for all $n$. But I
shall leave this to the proof-theoretic experts, who I hope will
shed light on things.
Update. More generally, I claim the following.
Theorem. Assume that the formal system $F$ is true in the standard
model of arithmetic $\mathbb{N}$. Then $\Dec(B)$ and $\Dec(\Dec(B))$ are equivalent for any statement $B$. So $\Dec(B)$ is equivalent to $\Dec^n(B)$ for any particular $n$ with respect to any such true formal system $F$.
Proof. Note that I am not claiming that this equivalence is
provable in $F$, only that it is true in the standard model. You had already noted that
$\Dec(B)$ implies $\Dec(\Dec(B))$. So assume $\Dec(\Dec(B))$ is
true. Thus, it is true in $\mathbb{N}$ that either there is a proof in $F$ of $\Dec(B)$ or a proof of
$\neg\Dec(B)$. It cannot be the latter, because then $F$ would
prove its own consistency, as we have noted, contrary to the incompleteness theorem.
Thus, it must be true in the standard model that "there is a proof
of $\Dec(B)$." In this case, there really is a (standard) proof of $\Dec(B)$,
and so $\Dec(B)$ is true. QED
Thus, once you have an undecidable statement, it is $\infty$-undecidable, with respect to any such system $F$ that is true in the standard model.
which parts of physics are axiomatized now, and which are not.
As an example, some fairly big fragments of classical physics have been formalized.
A significant part of Newton's Principia has been formalized by Fleuriot and Paulson using the proof assistant Isabelle.
General relativity is pretty trivial to formalize, basically because GR isn't so much a theory per se as a framework that we can plug other theories in to. If you want a concise formalization, it's not much more than this: spacetime is a Hausdorff differentiable manifold and it comes equipped with a nondegenerate metric (usually assumed to have signature +---). You can add in the Einstein field equations, but in a purely mathematical formulation restricted to GR itself, they are vacuous or work just as a definition of the stress-energy tensor, because GR itself says absolutely nothing about the stress-energy tensor or matter fields. You may want to add some subsidiary conditions about the integrability and differentiability of the metric, as discussed in Hawking and Ellis, p. 58. Hawking and Ellis also give some other axioms on pp. 60 (causality) and 61 (local conservation of energy-momentum), but again, these postulates become vacuous unless you plug in a separate theory for the matter fields. For a different approach to formalizing special and general relativity, see Andreka.
What is the status of the Hilbert 6th problem?
I think these two examples can help to clarify why Hilbert's sixth problem is not really very interesting in a modern context. Hilbert was operating in a Victorian era of optimism about physics, when it was believed that we were very close to understanding all the fundamental laws of nature, and all that was necessary was a little more cleaning up and investigation of the details. Totally wrong. Physics turned out to be a lot more complicated than he thought, and all we possess today is a bunch of pieces of a theory of everything (ToE). These pieces sometimes interlock nicely, but in other cases they don't, as in the case of quantum gravity. Since the Planck scale is inaccessible to any foreseeable human technology, it is likely that, even centuries from now, we will never have a ToE that can be tested by experiment. Only once we had a ToE would it even make sense to worry about Hilbert's sixth problem (and at that point I suspect it would be both trivial and of little interest to go ahead and carry it out).
Hilbert was searching for absolute certainty in the universe, and he was working before Godel. An interesting secondary question is whether, given a ToE and its formalization, we could make some sort of decision procedure for physics. The answer is not very clear, because the theory we're talking about might actually not describe enough of arithmetic for Godel's theorems to apply. After all, GR is basically a kind of geometry, and Tarski wrote down a decision procedure for Euclidean geometry. In any case, we wouldn't have absolute certainty, because the ToE itself would be based on experiments and therefore subject to revision.
References
Andreka et al., "On logical analysis of relativity theories," pdf, Hungarian Philosophical Review, 2010/4, pp.204-222
Fleuriot and Paulson, "A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia," pdf, Lecture Notes in Computer Science 1421 (2006) 3.
Hawking and Ellis, "The large scale structure of space-time"
Best Answer
As the other responders noted, you first need to find a formal setting in which what you call "co-implication" is operationally distinguished from ordinary implication. Emil Jeřábek mentioned non-commutative logic, but I think he might have been too quick to dismiss its relevance here. In particular the "right implication" of non-commutative logic (distinguished from "left implication") seems to me to be what you are looking for.
Have a look at the "Lambek calculus" (introduced by Lambek in his 1958 article, The mathematics of sentence structure), and then more generally "categorial type logics". Lambek's original motivation was syntax of natural language, but eventually (following a 1983 essay by van Benthem) this idea became part of a general approach to relating natural language syntax and semantics.