First-order natural deduction in Agda

TL;DR

This paper implements and verifies first-order natural deduction within Agda, a dependently-typed programming language, using Agda's type checker and proof assistant to ensure correctness and formalize natural deduction in constructive type theory.

Contribution

It provides a formalization of natural deduction in Agda, leveraging Agda's proof capabilities to verify proofs and properties within constructive type theory.

Findings

Natural deduction proofs are verified by Agda's type checker

Properties of natural deduction are formally proved within Agda

Implementation demonstrates correctness under Agda's assumptions

Abstract

Agda is a dependently-typed functional programming language, based on an extension of intuitionistic Martin-L\"of type theory. We implement first order natural deduction in Agda. We use Agda's type checker to verify the correctness of natural deduction proofs, and also prove properties of natural deduction, using Agda's proof assistant functionality. This implementation corresponds to a formalisation of natural deduction in constructive type theory, and the proofs are verified by Agda to be correct (under the assumption that Agda itself is correct).