Thanks for the answer, you are absolutely right, but it was not what I intended. I have edited the question. I mean $L + \phi \vdash \psi$. I think this will do.

Note that there are famous mathematical problems that can be written as halting problem. Like Fermat's last theorem, four color theorem, golbach conjecture and probably much more.

I think the question needs some eidt. You are talking about provable, but your definition is also about definable. You can have a function defined in a Turing complete language that returns 0 for every input, but is not provable total in PA (if you translate the function to a PA definition). Still a function can be defined in PA, that is provable to be total. That makes also a difference for comment above.

@NoahSchweber The system would be quite strong, because you can quantify over whatever you want. In the input strings you can also start using a complete different syntax. But for now, the idea (which I have for years) is a still a disaster, because I never was able to tackle paradoxes. But I will give it additional thoughts.

@NoahSchweber If you program a $\forall$ quantifier, then you want the property that $\forall x \forall y$ can be replaced by $\forall y \forall x$. This property should be initially be given, to make initial proofs possible. But when the system is strong enough, it can prove these properties by itself. The "input string" is syntactically. So, there is no expression structure in it. Numbers could be used and then Gödel numbering can be used to encode any string. However, if you really want to make a practical system, then real computer strings can be used, but that requires additional rules.

@NoahSchweber Thanks for your interest. I never detailed the system out, because that would be pointless if I couldn't fix the paradox. But essential in the system is that the computable functions work in two ways. You can generate theorems as stated earlier, but you can also add a new rule of inference if you can prove that from a certain theorem follows that all generated theorems from the computable theorem can be obtained in some way. This is a more general form of Hilbert's $\omega$-rule. For this it is necessary that all inference rules are formally specified.

@AndreasBlass Thanks for your comment, ramified type theory seems indeed interesting. Good material to read.

Properties of $\land$ and $\forall$ need to be given initially, but when the system is strong enough, those properties can be proven by itself. So, the system is pure syntactically. I never got the system right, because of the paradoxes. You can easily express the Liar's paradox in this system. It is just function that generates itself implicating $\bot$. But with the levels it might work.

Thanks for the comment. I had no knowledge about NF. The levels look like stratifying indeed. In my system (still in development), an expression consists of $\bot$, <expr> $\rightarrow$ <expr>, a triple (<computable function>, <level>, <input string>) or some arithmetic. If a theorem consists of the triple alone, the function can be executed with the input string and a number, to generate new theorems. Possibly, this can be an infinite number. With this the $\land$ and $\forall$ operators can be programmed, where the input string is the sub-expression.