Briefly,
In a previous post, I explored the question of if logical systems have any way of distinguishing between true statements that are obvious or tautological, and thereby not ‘meaningful’, versus logical derivations that are non-trivial, like the assertion of the equivalence of two things that has deep propositional content, and therefore has meaning.
I am still very interested in this idea. I have read a definition of “a logic” in formal logic as “the set of all tautologies” - the set of all true expressions, formulable from the formation rules. Such a conception of logic seems to fail to acknowledge this intuitive idea, that some truths are trivially true, or true by definition, and therefore mean almost nothing, like 1 = 1, whereas some truths are non-obvious and connect two very seemingly different things, and are therefore deeply meaningful.
I have been thinking about different ways a formal logic could actually encode or model this distinction.
One really simple way might be counting the number of steps in the derivation of some expression - the number of rule applications. I believe in some things like sequent calculus, some logics have a property that every expression can be written in a “normal form”, basically, a most reduced form. So, maybe one could just count how many steps it takes to arrive at some “truth”, to quantify how “far” from the initial axioms - the starting truths provided - some truth is. (But honestly, this seems suspiciously trivial).
Another way of thinking about this is how could you distinguish between a priori truths and a posteriori truths, in formal logic? If we think of predicate logic as modeling real-world reasoning, it might be as simple as saying that a priori reasoning is what deductions can be made from the axioms, without being provided a meaning or semantics for the predicate operators. A posteriori truth requires access to some external, contingent thing to supply information or truth that is not inherently already available just by reasoning.
But again, I don’t think this is deep enough.
In cryptography, there are algorithms where if you know a numerical solution to an equation, you are able to do a certain function, like sign a blockchain transaction. But it’s almost like a “one-way flow”, in terms of information theory: it’s easy to verify what the correct answer (number) is, and statistically bordering on impossible to find out what it is, if you don’t know it. This is closer to the general intuition of “something that is true, perhaps by virtue of reason alone, but it is not exactly a priori knowledge.”
I have other ideas, which I can expand on later, but I’d like to get the ball rolling on this topic.
