La logica categorica è la branca della matematica in cui strumenti e concetti della teoria delle categorie vengono applicati allo studio della logica. In termini generali, la logica categoriale rappresenta sia la sintassi che la semantica mediante una categoria e un'interpretazione mediante un funtore. Il quadro categorico fornisce un ricco background concettuale per le costruzioni logiche e di tipo teorico.[1][2]
La logica categorica introduce la nozione di struttura valutata in una categoria C con la classica nozione teorica del modello di una struttura che compare nel caso particolare in cui C è la categoria degli insiemi e delle funzioni. Il sistema utilizza un linguaggio interno che nomina i componenti rilevanti di una categoria, quindi applica la semantica categoriale per trasformare le asserzioni in una logica sul linguaggio interno in corrispondenti affermazioni categoriche. Spesso la semantica categoriale di una logica fornisce una base per stabilire una corrispondenza tra teorie nella logica e istanze di un tipo appropriato di categoria. Ciò ha permesso di dimostrare proprietà metateoriche di alcune logiche mediante un'appropriata algebra categoriale.[2][3][4]
- ^ J. Marquis, G. Reyes "The History of Categorical Logic 1963–1977". Gabbay, Kanamori & Woods 2012. pp. 689–800.
- ^ a b J. Goguen, T. Mossakowski, et al. "An Institutional View on Categorical Logic". International Journal of Software and Informatics. 2007 1 (1): 129–152.
- ^ Francis William Lawvere "Functorial Semantics of Algebraic Theories". Proceedings of the National Academy of Sciences 1963. 50 (5): 869–872.
- ^ Bell, John Lane "The Development of Categorical Logic". In Gabbay, D.M.; Guenthner, Franz (eds.). Handbook of Philosophical Logic. 2001 Vol. 12