There is a similar thread below, but I think it is more appropriate to make a new thread because it asks totally different questions. I am new to category theory and thinking about its possible application to computer science. Deductive systems based on first order logic (sound and complete) have been successfully applied to A.I knowledge based systems and a wide variety of inference systems so far. My questions are 1. Do you think category theory, especially categorical logic, can be successfully applicable to deductive reasoning systems? 2. If we use a categorical logic for a possible deductive system, what advantages we can expect from it over traditional First Order Logic (FOL) based deductive systems? 3. What might be the possible theoretical limits for categorical logic? Any opinions will be appreciated.