We prove that the Gödel incompleteness theorem holds for a weak arithmetic Tₘ = IΔ₀ + Ωₘ, for m ≥ 2, in the form Tₘ ⊬ HCons(Tₘ), where HCons(Tₘ) is an arithmetic formula expressing the consistency of Tₘ with respect to the Herbrand notion of provability. Moreover, we prove , where is HCons relativised to the definable cut Iₘ of (m-2)-times iterated logarithms. The proof is model-theoretic. We also prove a certain non-conservation result for Tₘ.
The first-value operator assigns to any sequence of partial functions of the same type a new such function. Its domain is the union of the domains of the sequence functions, and its value at any point is just the value of the first function in the sequence which is defined at that point. In this paper, the first-value operator is applied to establish hierarchies of classes of functions under various settings. For effective sequences of computable discrete functions, we obtain a hierarchy connected...
The first-value operator assigns to any sequence of partial functions of the same type a new such function. Its domain is the union of the domains of the sequence functions, and its value at any point is just the value of the first function in the sequence which is defined at that point. In this paper, the first-value operator is applied to establish hierarchies of classes of functions under various settings. For effective sequences of computable discrete functions, we obtain a hierarchy connected...
Fuzzy logics based on t-norms and their residua have been investigated extensively from a semantic perspective but a unifying proof theory for these logics has, until recently, been lacking. In this paper we survey results of the authors and others which show that a suitable proof-theoretic framework for fuzzy logics is provided by hypersequents, a natural generalization of Gentzen-style sequents. In particular we present hypersequent calculi for the logic of left-continuous t-norms MTL and related...