Structural type theory is an extension of simple type theory that incorporates types for any kind of mathematical structure and allows isomorphic structures to be identified within them. In order to guarantee consistency, the system incorporates several syntactic restrictions. Modelling structural type theory in Tarski–Grothendieck set theory and extending the definition of transport functions, we show that some of these restrictions can be lifted, thus improving the expressive power of the system. In addition, we show how to treat axiomatic theories as first-class objects in our reformulation of structural type theory, and we state and prove within it a result analogous to the morphism theorem by Farmer.
This paper establishes the subformula property and the Craig interpolation theorem for sequent calculi of the indexed tense expansions of modal logics K , KT , KD , K4 , K4D , and S4 . Our sequent calculi are based on the ordinary notion of (non-labelled) sequents, and they are not cut-free, but all applications of the cut rule can be restricted to analytic ones. We prove the subformula property of all the calculi by Takano’s semantic argument and apply Maehara’s method to obtain the Craig interpolation theorem, which counts both propositional variables and indices of modal operators as common vocabulary.
This paper concerns the categoricity problems, or Carnap’s problems, of some non-classical logics. I first review the categoricity theorems of LP and K3 proved by Tabakci (2024) and give a counterexample to a proposition in his paper. Then I prove some categoricity results of FDE and a theorem connecting that of FDE and those of LP and K3. I also prove that FDE is categorical regarding the star models and that LP and K3 are not categorical regarding their star models.
Kernel contraction, introduced by Sven Ove Hansson, is a fundamental method for withdrawing information from belief bases. Through the Levi Identity —which defines revision in terms of contraction— kernel contraction also induces the corresponding revision operator known as kernel revision. Recent work has proposed a non-prioritized variant of kernel contraction which, unlike its classical counterpart, may violate the Success postulate, and thereby permits some non-tautological beliefs to be protected from removal. This article develops a corresponding notion of non-prioritized kernel revision. Building on the machinery of classical kernel revision and non-prioritized kernel contraction, we define a revision mechanism that need not always incorporate incoming evidence. The proposal is given both a constructive formulation, via a generalized Levi Identity, and an axiomatic (postulational) characterization. Finally, we analyse its epistemic impact by showing how non-prioritized kernel revision can weaken or reinforce the degree of firmness of selected beliefs within a belief base, and how these effects can accumulate under iteration, eventually yielding endorsement of the epistemic input and de-endorsement of its negation.
The well-known“slingshot” argument concludes that sentences designate neither facts, nor situations, nor propositions, but instead designate one of the two truth values. We find fault with the argument by laying it out in the context of Bressan’s (1972) improved version of Carnap’s (1947) “method of extension and intension”: The argument is fallacious inasmuch as it employs the “method of the name relation,” which awards each sentence only one semantic value instead of both an extension and an intension.
