Algorithmic Logic with Stacks and Its Model-Theoretical Properties

Abstract

In this paper we propose to transform the Algorithmic Theory of Stacks (cf. Salwicki [30]) into a logic for expressing and proving properties of programs with stacks. We compare this logic to the Weak Second Order Logic (cf. [11, 15]) and prove theorems concerning axiomatizability without quantifiers (an analogon of Łoś-Tarski theorem) and ${\mathit{\chi }}_0$ - categoricity (an analogon of Ryll-Nardzewski’s theorem).