The foundations of Suslin logic
Erik Ellentuck · Journal of Symbolic Logic · 1975
LetLbe a first order logic and the infinitary logic (as described in [K, p. 6] overL. Suslin logic is obtained from by adjoining new propositional operators and . Letfrange over elements ofωωandnrange over elements of ω.Seqis the set of all finite sequences of elements of ω. If θ:Seq→ is a mapping into formulas of then and areformulasofLA. If is a structure in which we can interpret andhis an -assignment then we extend the notion ofsatisfactionfrom to by defining wheref∣nis the finite sequence consisting of the firstnvalues off. We assume that hasωsymbols for relations, functions, constants, andω1variables. θ is valid if θ ⊧ [h] for everyhand isvalidif -valid for every . We address ourselves to the problem of finding syntactical rules (or nearly so) which characterize validity .