On evaluations of propositional formulas whose range is a subset of some fixed countable ordered field

Abstract

Let L be a countable first-order language such that its set of constant symbols Const(L) is countable. We provide a complete infinitary propositional logic (formulas remain finite sequences of symbols, but we use inference rules with countably many premises) for description of C-valued L-structures, where C is an infinite subset of Const(L). The main goal is to provide a formal framework for reasoning about F-valued evaluations of propositional formulas, where F is some countable ordered field. The prime examples of F are the field of rational numbers ℚ, its real closure ℚ and the field of fractions ℚ(ε), where ε is a positive infinitesimal.