An analytic tableaux calculus adequate for the logic of existence propositions

Abstract

In [Markin, 2021] we set out the formal system for logical analyses of reasonings with existence judgements and their Boolean combinations. Its language contains the constant of existence, atomic formulas are formed by the concatenation of this constant with any finite sequence of general terms (positive and negative), complex formulas are formed by means of propositional connectives. We formulated a natural semantics and an adequate axiomatic calculus for this language. In this paper we construct an analytic tableau version of the calculus of existential judgements. We postulate the rules of expansion of a tableau for the formulas with the constant of existence and their negations, define analytic tableau as a sequence of families of sets of the formulas and formulate the criterion for the tableau closure. A formula A is provable in this calculus iff there exists a closed analytic tableau with the root {{ ¬A }} . We prove soundness and completeness theorems for the analytic tableau calculus of existential judgements. The effective procedure, which makes it possible to answer the question whether a formula is provable, is proposed in the paper. We prove decidability theorem for the analytic tableau calculus.