A Method for Propositionalizing Prenex Normal Form Sentences under Inclusive Semantics and Testing the Validity of Inferences Formed from Such Sentences

Abstract

Quantifier expansion requires enumerating the objects in the domain one by one. Therefore, it can only handle finite domains. This paper proposes a different perspective on propositionalization: rather than counting objects in the domain, it focuses on the finite regions determined by the sentence. Therefore, within its scope of application, even if the domain contains infinitely many objects, this method can still produce a finite propositionalization. This paper distinguishes two kinds of FOL based on different semantics: basic FOL, which allows the domain to be empty, and strengthened FOL, which requires a non-empty domain. This paper focuses on the basic FOL. At present, the basic FOL method only applies to prenex normal form sentences. To propositionalize such sentences, this paper introduces the Region Table and uses it to translate prenex-normal-form sentences into TFL sentences. On this basis, FOL inferences composed of such sentences can also be translated into TFL inferences, allowing their validity to be tested using TFL rules. This method provides a new approach to propositionalizing some FOL sentences over infinite domains and testing the validity of inferences composed of them, and it may be applied to formal reasoning in mathematics and physics.