First, I'm going to answer this with a question: How would you know that the axioms of your formal deductive system capture all that needs to be captured so that your concept of (deductive) truth is all that matters to (some informal notion) of truth as a concept?
In other words (assuming the deductive method is all that there is to "truth"), how do you know your axioms are grounded and "useful enough"? (And the same can be said about the inference rules, really.) I.e. what is the (ultimate) point of defining truth in a syntactic way (as deriving from some axioms by some rules)?
(I'll also note here that one of the reasons why relevance logic falls on deaf
ears with [most] mathematicians is that they are very discerning about which
axioms to admit to begin with. If they were not so discerning and any random mathematician
you picked would readily accept that "Trump is president and Trump is not president"
is an axiom... they would have to worry about relevance in entailment [not] "blowing up" mathematics. But since mathematicians are very discerning about their axioms [see e.g. how the axiom of constructibility
has been debated], they can be a bit more "maximalist" about the rules of the deductive system that founds mathematics.)
Second, assuming ZFC, it's actually quite trivial to define truth (semantically) in an algebraic model (itself a ZFC-defined structure--an algebra in the sense/definition of universal algebra). This is even "grounded" enough that you can define a notion of logical consequence that way; see for instance how the definition a logic in the abstract algebraic logic (AAL) programme includes both syntactically and model-defined logics. (Font's 2016 book is a good read here.) For example, one can define some logics this way that have no known axiomatization. (IIRC, Medvedev's "logic of problems" was the example given.)
Yes, there is a subtle meta-logical point here: we assume FOL (e.g. by Hilbert-style axiom-schemas), in which we build ZFC (with some more axioms) and in which we then (can) "more generally" define what a logic (with some properties) means... and the latter notion can actually encompass not only non-classical (propositional) logics but also allows one to define (propositional) logics merely by their (algebraic) models!
(N.B. I once asked a mathematician--Carl Mummert, if I recall that correctly-- if the (various) axioms of non-well-founded set theory seem "fishy" because they rely on a notion of [pointed] graphs. But how do you define graphs if you don't yet have a notion of set, etc.? His answer was, again if I recall correctly, was that one needs to assume that notion of graph is built in another "mini-language" etc.)
But to get back to your question...
What could "true" really mean, if we lack a procedure for distinguishing truth from falsehood? [...] I suspect that a model is better viewed as just the provable results of a different, "larger" logic. For instance, we say a Godel sentence is true because it can be derived in our brain-logic [...]
Actually that can be made more precise:
Although the Gödel sentence of a consistent theory is true as a statement about the intended interpretation of arithmetic, the Gödel sentence will be false in some nonstandard models of arithmetic, as a consequence of Gödel's completeness theorem (Franzén 2005, p. 135). That theorem shows that, when a sentence is independent of a theory, the theory will have models in which the sentence is true and models in which the sentence is false.
(Also discussed in https://plato.stanford.edu/entries/goedel-incompleteness/#IncNonStaMod)
But surely the fact that we have an "intended interpretation" of arithmetic (when building a system like PA) does say something about us (if not about the world).
Also, although a bit "opinionated", I think the following take (by Raattkainen) (cited by Wikipedia) on misinterpretations of Godel's result is useful to recall here because it pertains to your saying that "we say a Godel sentence is true because it can be derived in our brain-logic":
The structure of Godel's proof is, very roughly, the following : Assume that the formal system F is consistent (otherwise it proves, by elementary logic, every sentence and is trivially complete). By Godel's self-reference lemma, one can then construct a sentence GF that is independent of F (i.e. neither provable nor refutable in F). Thus F is incomplete. So far so good. Yet how then can one conclude that GF is true?
Assuming that the formalized provability predicate used is normal, one can prove, even inside F, that GF is true if and only if F is consistent, although neither side of the equivalence can be proved in F. Therefore, the truth of the sentence GF is already implicitly assumed in the beginning of the proof, in the form of the assumption that F is consistent.
If it nevertheless turns out that F is inconsistent, one has to conclude that GF is, after all, false — and provable in F, because every sentence is. The proof also goes through for a theory that is in fact inconsistent. An amusing real historical example is Quine's original version of his system ML (Quine 1940). At the end of the book, Quine presented a proof of Godel's theorem for this system. But ML was later shown to be inconsistent by Rosser. Hence the Godel sentence GML was actually false, whatever one's intuitions were.
An unqualified anti-mechanist conclusion was drawn from the incompleteness theorems in a much read popular exposition, Godel's Theorem, by Nagel and Newman (1958). Shortly afterwards, J.R. Lucas (1961) famously proclaimed that Godel's incompleteness theorem "proves that Mechanism is false, that is, that minds cannot be explained as machines". He stated that "given any machine which is consistent and capable of doing simple arithmetic, there is a formula it is incapable of producing as being true ...but which we can see to be true". More recently, very similar claims have been put forward by Roger Penrose (1990,1994).
The basic error of such an argument is actually rather simply pointed out. This objection goes back to Putnam 1960; see also Boolos 1967. The argument assumes that for any formalized system, or a finite machine, there exists the Godel sentence (saying that it is not provable in that system) which is unprovable in that system, but which the human mind can see to be true. Yet Godel's theorem has in reality the conditional form, and the alleged truth of the Godel sentence of a system depends on the assumption of the consistency of the system. That is, all that Godel's theorem allows us humans to prove with mathematical certainty, of an arbitrary given formalized theory F, is: F is consistent => GF.
The anti-mechanists argument thus also requires that the human mind can always see whether or not the formalized theory in question is consistent. However, this is highly implausible. After all, one should keep in mind that even such distinguished logicians as Frege, Curry, Church, Quine, Rosser and Martin-Lof have seriously proposed mathematical theories that have later turned out to be inconsistent.
As for these parts of the question:
What could "true" really mean, if we lack a procedure for distinguishing truth from falsehood? [...] If neither a claim nor its negation is derivable using the implicit logic of the human brain, I don't see how it could be meaningful to call it "true" or "false."
Well, I'm not sure what to make of the "implicit logic of the human brain" part, or exactly what you mean by "procedure" in there, but if (as hinted in the comments) your concern is that proofs and models need a constructive approach; intuitionism has its own approach(es) to model theory; one could say perhaps that it has too many...
Intuitionistic systems have inspired a variety of interpretations, including [...] formulas-as-types, Kleene’s recursive realizabilities [...] Of all these interpretations Kripke’s  possible-world semantics, with respect to which intuitionistic predicate logic is complete and consistent, most resembles classical model theory. Recursive realizability interpretations, on the other hand, attempt to effectively implement the B-H-K explanation of intuitionistic truth.
That SEP article also details Kleene’s approach to realizability via partial recursive function (which Wikipedia also covers.)
There's yet another SEP article that more specifically deals with constructive set theories where the implications of model approaches are discussed in more detail. In particular, that page does a good job of contrasting IZF which only restrict the logic and CZF which has a "double restriction" approach to what sets are constructible as well.
Finally, regarding the formulas-as-types interpretation, which has yielded ITT (Intuitionistic Type Theory)... that has also been given various models, both classical e.g. in ZF (or CZF) and realizable. To quote an (explanatory) bit on that, again from (a 3rd) SEP article...
The set-theoretic model can be criticized on the grounds that it models the type of functions as the set of all set-theoretic functions, in spite of the fact that a function in type theory is always computable, whereas a set-theoretic function may not be.
To remedy this problem one can instead construct a realizability model whereby one starts with a set of realizers. One can here follow Kleene’s numerical realizability closely where functions are realized by codes for Turing machines. Or alternatively, one can let realizers be terms in a lambda calculus or combinatory logic possibly extended with appropriate constants. Types are then represented by sets of realizers, or often as partial equivalence relations on the set of realizers. A partial equivalence relation is a convenient way to represent a type with a notion of “equality” on it.
There are many variations on the theme of realizability model. Some such models tacitly assume set theory as the metatheory (Aczel 1980, Beeson 1985), whereas others explictly assume a constructive metatheory (Smith 1984).
So, if your worry is that e.g. the definition of a function in a classical model is non-procedural/non-constructive... then you have to use a constructive meta-theory as well for models/interpretations.