Resource-Bounded Higher-Order Logic and Truth Computation

This paper proposes a formal system based on higher-order logic with an alternative ontology oftruth, where the truth of every statement is identified with its derivability.A key element of the approach is the computational power parameter i, which restricts thespace of formulas and the length of derivations, defining the computational horizon of the system.Within this framework, the existence of true but unprovable statements is excluded.It is shown that for any arbitrarily large value of i, the space of formulas is finite and the derivability relation becomes algorithmically decidable. This makes possible to treat logical inferenceas a process of truth computation.Approach has applications in automated theorem proving, verification of generated text, andother artificial intelligence systems. It also provides a computational perspective for the foundationsof mathematics, when considering computational power parameter i → ∞.