Intuitionistic Existential Instantiation and Epsilon Symbol

TL;DR

This paper introduces a natural deduction system for intuitionistic predicate logic incorporating Hilbert's epsilon symbol, extending existing systems, and provides completeness and normalization insights.

Contribution

It presents a conservative natural deduction system with epsilon, extending prior intuitionistic logic frameworks, and offers a completeness proof and discussion on normalization.

Findings

The system is conservative over standard intuitionistic predicate logic.

A completeness proof for Kripke semantics is provided.

An approach to normalization is sketched.

Abstract

A natural deduction system for intuitionistic predicate logic with existential \ instantiation rule presented here uses Hilbert's $\e$-symbol. It is conservative over intuitionistic predicate logic. We provide a completeness proof for a suitable Kripke semantics, sketch an approach to a normalization proof, survey related work and state some open problems. Our system extends intuitionistic systems with $\e$-symbol due to A. Dragalin and Sh. Maehara.