Infinitary first-order categorical logic

TL;DR

This paper develops a unified categorical framework for completeness theorems in various infinitary logics, extending classical results and applying large cardinal assumptions to prove properties like disjunction and existence.

Contribution

It introduces a new categorical approach that unifies and generalizes existing completeness theorems for infinitary logics, including intuitionistic variants.

Findings

New completeness theorems for classical and intuitionistic infinitary logics

A unified categorical framework encompassing previous results

Proof of disjunction and existence properties under large cardinal assumptions

Abstract

We present a unified categorical treatment of completeness theorems for several classical and intuitionistic infinitary logics with a proposed axiomatization. This provides new completeness theorems and subsumes previous ones by G\"odel, Kripke, Beth, Karp, Joyal, Makkai and Fourman/Grayson. As an application we prove, using large cardinals assumptions, the disjunction and existence properties for infinitary intuitionistic first-order logics.