Automata Theory Approach to Predicate Intuitionistic Logic

TL;DR

This paper introduces an automata model for predicate intuitionistic logic that directly corresponds to proof construction, enabling analysis of proof languages and their properties within a formal automata framework.

Contribution

It presents a novel automata-based model for full intuitionistic first-order logic, linking automata runs to normal proofs and facilitating formal language analysis.

Findings

Automata runs correspond to normal proofs in intuitionistic logic.

The model allows analysis of closure properties of proof languages.

Connections established between automata and logical connectives.

Abstract

Predicate intuitionistic logic is a well established fragment of dependent types. According to the Curry-Howard isomorphism proof construction in the logic corresponds well to synthesis of a program the type of which is a given formula. We present a model of automata that can handle proof construction in full intuitionistic first-order logic. The automata are constructed in such a way that any successful run corresponds directly to a normal proof in the logic. This makes it possible to discuss formal languages of proofs or programs, the closure properties of the automata and their connections with the traditional logical connectives.