# Is there Mathematical discipline that treats mathematical logic, axioms and relations as one big mathematical object?

Recently I was self studying the properties of the Wronskian $$W$$ using various lecture notes and Wikipedia

I knew that if $$W\ne0$$ for at least one x then the functions are linearly independent

I also knew that by contrapositive, if the functions are linearly dependent then $$W=0$$ everywhere in the interval

Putting all the known facts about the Wronskian, I got the following diagram which illustrates all the logical statements that relates linear independence and the values of the Wronskian

Q1. Is this diagram a sort of generalization of a commutative diagram, as the arrows are not really a mapping from one set to another, but how one logical statement is related to another?

Q2. Is there any math discipline that explore a bunch of logical statements (or more generally, axioms and relations) as one giant mathematical structure, and/or geometrically, graphically?

• Do you know mathematical logic? Mar 22 '15 at 13:04
• Category theory may be close to what you have in mind.
– mrp
Mar 22 '15 at 13:08
• Learnt some first order logic and set theory in my 1st year undeegrad Mar 22 '15 at 13:08
• When I read the title I thought universal algebra might be the answer. When I read the question I thought, oh I have no idea, let others answer it. Mar 22 '15 at 13:35
• Having seen the answers, I have no idea how to green tick answers for this question because I think one guy have basically nailed Q2 while another guy in the answer has the best answer to Q1. The answers also implies I have a lot of reading to do afterwards Mar 22 '15 at 14:22

Q2. Is there any math discipline that explore a bunch of logical statements (or more generally, axioms and relations) as one giant mathematical structure, and/or geometrically, graphically?

The most well-developed theory in the general area your diagram points towards may be something like boolean algebra, and its close relations in order and lattice theory. But those don't general put a lot of theoretical emphasis on graphical representations.

There's graph theory too, of course, but that has a vastly larger domain than your particular kind of diagram.

Q1. Is this diagram a sort of generalization of a commutative diagram, as the arrows are not really a mapping from one set to another, but how one logical statement is related to another?

Commutative diagrams belong to categories, but it is difficult to see a category where your diagram could live and say something interesting. You can always build a category out of a particular preorder by letting arrows stand for the order relation -- but every diagram in such a category commutes, so "commutative diagram" is not an interesting property there. And it is not clear where your labeled arrows would fit in.

All in all it is probably more productive simply to view your diagram as an informal mental overview technique, than to attempt to build a general formalized theory it could be an instance of.

In categorial logic (the application of category theory to logic) we often consider the category whose objects are statements (usually statements of logic) and which has an arrow $A\to B$ for each proof that $A$ implies $B$. This seems to me to be much more similar to your diagram than what the other answers have proposed.

To be a category, the arrows must satisfy two properties: If $f$ is an arrow from $A$ to $B$, and if $g$ is an arrow from $B$ to $C$, then there must be an arrow $g\circ f$ from $A$ to $C$ called the “composition” of $f$ and $g$. Since in logic you can compose a proof that $A$ implies $B$ with a proof that $B$ implies $C$ to obtain a proof that $A$ implies $C$, this structure does have compositions. The other required property is that for each object $A$ there must be a “identity” arrow from $A$ to itself with certain properties. In this case the identity arrows are empty proofs: you don't need any argument to show that $A$ implies itself!

(It transpires that this is more interesting to do in intuitionistic logic, rather than the classical logic you are used to, because in classical logic any true statement implies any other.)

I regret that I can't think of a reference offhand; perhaps someone else reading this answer will insert some.

• Even in classical logic, we have that $A$ implies $A\lor B$, but $A\lor B$ doesn't imply $A$, when $A$ and $B$ are propositional variables. So there is still an interesting implication structure between statements that are not necessarily true. Mar 22 '15 at 15:26
• Doesn't categorical logic usually want the category to be cartesian closed? In that case we can't take textual proofs to be morphisms; one needs to quotient out a nontrivial equivalence relation between proofs such that the various commuting diagrams for products and exponentials actually commute. (This is not directly relevant at the level the OP speaks at, though). Mar 22 '15 at 15:34
• Thanks for pointing out my error in comment #1; I have corrected my post accordingly. I forget what the answer to #2 is.
– MJD
Mar 22 '15 at 15:39
• @HenningMakholm: yes, you almost always do need to quotient the proofs a bit. (Depending on what logical system you’re looking at, you don’t always necessarily want cartesian closure; but you almost always do still want something a bit stricter than what the raw un-quotiented syntax satisfies.) Mar 22 '15 at 16:24

Q1: I think not, your diagram features bubbles and arrows but it seems the bubbles are not objects and the arrows do not look like structure preserving maps. It looks more like a mind map.

Q2: Model checking maps certain logical statements to finite automata, uses algorithms to determine properties of the finite automaton and maps those results back to the logical statements. The graphs of finite automaton can be represented as diagrams.