Independence questions in a finite axiom-schematization of first-order logic

TL;DR

This paper reviews independence results in a finite axiom-schematization of first-order logic and proves the independence of a specific axiom scheme despite its instances being derivable from others.

Contribution

It introduces new independence results in a finite axiom system for first-order logic and demonstrates the independence of a particular axiom scheme.

Findings

Certain axiom schemes are independent in the system

All instances of the independent axiom scheme are provable from others

The system maintains consistency despite the independence results

Abstract

We review some independence results in a finite axiom-schematization of classical first-order logic introduced by Norman Megill. We also prove that a certain axiom scheme of this system is independent although all of its instances are provable from the other axiom schemes.