# Axiomatizing first-order consequences in inclusion logic

## TL;DR

This paper develops a natural deduction system that is sound and complete for deriving first-order consequences in inclusion logic, a dependence logic variant with fixed-point expressiveness.

## Contribution

It provides the first explicit partial axiomatization for first-order consequences in inclusion logic using a natural deduction system.

## Key findings

- The deduction system is sound for first-order consequences.
- The deduction system is complete for first-order consequences.
- The system enables formal reasoning within inclusion logic.

## Abstract

Inclusion logic is a variant of dependence logic that was shown to have the same expressive power as positive greatest fixed-point logic. Inclusion logic is not axiomatizable in full, but its first-order consequences can be axiomatized. In this paper, we provide such an explicit partial axiomatization by introducing a system of natural deduction for inclusion logic that is sound and complete for first-order consequences in inclusion logic.