I would like to suggest a way of reconciling this situation for your consideration. I have no proof as yet but if accepted and then used as a vehicle of exploration and understanding of context I have found it to be a useful.
A formal logic (an arbitrary calculus) is defined by 4 basic constituents: 1) signs 2) rules of formation 3) rules of inference 4) rules of transformation Basically it's a formally specific grammar of signs. A formal proof is a collection of (3) transformed according to (4) that takes the original inference from a starting state to an end state. Whatever state results is necessarily true according to the language. The concept that I have found useful is that if you imagine that in some context in the universe, the natural behaviour of it happens to correspond to a virtual definition of items 1, 2, 3, 4 above, then what will be found is the universe behaving like formal logic of a certain type. Voila, mathematical decriptions are found to be 'unreasonably effective' ways of characterising the universe. In different contexts in the natural world, difference sets of formal logic happen to be 'virtually reified' by the circumstances. In each case a different set of rules will be found. A slithly differrent set of mathematical rules will be found and we will tend to think that the 'laws' thus 'discovered' are somehow driving the universe. In formal mathematics, though, one set of formalities can be transformed into anouther. Arithmetic can be done using formal logic, for example. Extraordinalrily tedious..but can be done...In a sense there is no 'native tongue', there are only 'tongues'. When you think about it this way you end up wondering what is the 'calculus' of the natural world, which is selectively mapped into other calculii we find so useful? This brings in the idea of the universe as a reified calculus. Indeed the _only_ reified calculus. If it is, then what are its signs, rules of formation, inference, transformation? I have been looking into this and I have been able to make on. I wonder if others can. Try it. I called mine 'entropy calculus'. The idea brings with it one unique aspect: none of the calculii we hold so dear, that are so wonderful to play with, so poweful in their predictive nature in certain contexts, are ever reified. None of them actually truly capture reality in any way. They only appear to in certain contexts. The only actual mathematics that captures the true nature of the universe is the universe itself as a calculus. It doesn't invalidate the maths we love. It just makes it merely a depiction in a certain context. Very useful but thats all. But there's a further subtlelty to this. In mathematics there is a cultural assumption born of the history of mathematics. ...imagine Leibniz or Newton sitting there with their new toy calculus. They start with one set of symbols and work in a single line, transformation after transformation. A single linear proof emerges. Wonderment ensues. If the universe is a calculus, how many Newtons and Leibniz's are there _All_ working at once? How many 'proofs' are being evaluated at once, all with direct relationships to each other? Nobody ever thinks about that. If 100,000,000,000,000 leibnizs all started with their own sign and then connected with each other, formed, inferred transformed, each finding the results of the other 99,999,999,999,999 Leibniz's results in some way available to use in their own next transformation, what would the resulting calculus look like? What would it be like to 'be' one the proofs being enacted by Leibniz 145,735,365,268? Leibniz 145,735,365,268's proof could be an electron. Leibniz 567,145,735,365,268's proof could be Bruno Marchal. Our mathematics, as we see it, thinking about it from this perspective, is rather lame, n'est pas? Food for thought, anyway. That's my handle on the relationship between mathematical models and reality. It's been a useful way of thinking for me and I commend it to you for a little amusement. cheers colin hales