Treatment of mathematical logic with less bookkeeping?

Question

My only real experience with mathematical logic is an undergrad-level model theory class that I took some years ago. My (perhaps fair, perhaps unfair) take away from this class was that mathematical logic as it is usually presented involves a lot of bookkeeping: keeping track of enumeration of variables, arity of function and relation symbols, etc. My impression was also that this bookkeeping was in some sense superfluous. Though the potential for off-by-one errors in writing down some statement abound, nothing of great consequence ever really hinges on the arities or variable-enumerations involved (edit: except perhaps broad cardinality distinctions, finite/countably infinite/uncountable). Perhaps I am wrong about this—if so, I would greatly like to see an example of where these things really are pivotal. But my impression, again not so informed, is that a lot of this bookkeeping is simply a product of the language we use to talk about logic, which seems not to have changed much since the early twentieth centuries and which predates a lot of modern mathematical formalism.

It would seem to me that modern language, e.g. from category theory, has the potential to clarify the presentation a lot. For example, we might think of the set of terms and formulas in a given signature as being the object in a certain category freely generated by the variable symbols and the function- and relation-symbols viewed as partial functions. Indeed I think something like this is the view taken up in universal algebra. And while some might (fairly) view this as overcomplicating things, to my eye it is perhaps a less messy presentation than the traditional one in terms of literal strings of symbols. For instance, it makes it immediately obvious that one can make definitions recursively on terms and/or formulas.

This example is I suppose a bit trivial, but I'm not really wedded to this particular concern or this particular rewording of things. My more general question is just whether there is any text on any aspect of mathematical logic that attempts to cut away some of the bookkeeping by reframing things in more modern language, and if there is, if anyone could point me to it. Thanks!

Answer 1

My impression was also that this bookkeeping was in some sense superfluous.

Maybe. This is not the definitive answer, just some food for thought...

Define $(f,X,Y)$ as :

1. $\forall a:[ a\in X\to f(a)\in Y]~~~~~~~~~~~~~~~~~~~~~~($Equivalently $f:X\to Y~)$

Why can we not then also define $(f,X^2,Y)$ as:

2. $\forall a,b:[(a,b) \in X^2 \to f(a,b) \in Y]~~~~~~($Equivalently $f: X^2\to~Y)$

It might be a little confusing, but it would save on what the you call "bookkeeping." I don't think it would it lead to any internal contradictions.

$f(x)$ would obviously be defined by (1). And $f(x,y)$ would be defined by (2).

We could even make sense of $f(x)=f(x,y)$

Technically, changing the name of the binary version in (2) would make no logical difference AFAICT.