A simplified framework for first-order languages and its formalization in Mizar

TL;DR

This paper presents a simplified, set-theoretical framework for first-order logic aimed at formalizing key logical results in Mizar, focusing on minimal inference rules and practical implementation techniques.

Contribution

It introduces a streamlined, formal approach to first-order logic that reduces complexity and facilitates Mizar formalization of fundamental theorems.

Findings

Simplified framework for first-order logic

Minimal inference rules identified

Techniques for Mizar implementation developed

Abstract

A strictly formal, set-theoretical treatment of classical first-order logic is given. Since this is done with the goal of a concrete Mizar formalization of basic results (Lindenbaum lemma; Henkin, satisfiability, completeness and Lowenheim-Skolem theorems) in mind, it turns into a systematic pursue of simplification: we give up the notions of free occurrence, of derivation tree, and study what inference rules are strictly needed to prove the mentioned results. Afterwards, we discuss details of the actual Mizar implementation, and give general techniques developed therein.