Program

Knudstorp~\cite{Knudstorp} axiomatizes modal information logic (MIL) with a supremum operator on posets. Since infima naturally complement suprema, this raises the question: Can this result be extended to a modal logic that includes both operators and, if so, what axioms would govern the interaction between the two modalities? In this paper, we prove soundness and completeness of tense information logic (TIL)---a modal logic with two binary modalities, $\supp$ and $\inff$, interpreted as supremum and infimum operators over posets. Our axiomatization, which links $\supp$ and $\inff$ only through the standard tense-logic axioms, thereby resolves a question posed by van Benthem~\cite{Benthem-1}.Completeness is proven using the step-by-step method \cite{Burgess} and as a corollary, we obtain completeness of TIL on preorders. Furthermore, we prove the finite model property (FMP) of TIL with respect to a generalized class of structures, which in turn establishes decidability of the logic. By introducing both fusion ($\supp$) and refinement ($\inff$) within one logical framework, TIL provides an expressive paradigm for information dynamics.

We discuss an infinitary refinement type system for input-output temporal specifications of functions that handle infinite objects like streams or infinite trees. Our system is based on a reformulation of Bonsangue and Kok's infinitary extension of Abramsky's Domain Theory in Logical Form to saturated properties. We show that in an interesting range of cases, our system is complete without the need of an infinitary rule introduced by Bonsangue and Kok to reflect the well-filteredness of Scott domains.

We analyze computable algebras (in the sense of universal algebra) in terms of index set complexity, specifically as regards their congruence lattices. We characterize simplicity of lattices as complete at the level Pi^0_2, mirroring a result of Khoussainov and Morozov (2010) for groups. Finiteness of the congruence lattice is proved complete at the level Sigma^0_3; and subdirect irreducibility at the level Sigma^0_3.

We consider a sequence $L_n, n = 1, 2, 3,...$, of linear preorders, a finite relational signature $\sigma$ including the signature $\{\preceq\}$ of the linear preorders $L_n$, and the set $W_n$ of all expansions of $L_n$ to $\sigma$. A probability distribution $P_n$ is defined on each $W_n$ (it can be e.g. the uniform distribution, but other distributions are possible). We prove that if all equivalence classes of the preorder $L_n$ grow (as $n\to\infty$) faster than every logarithm but slower than some polynomial, then every first-order formula is almost surely equivalent to a (in general) simpler formula that only expresses distances between variables and which atomic formulas they satisfy. As a corollary we get a convergence law for formulas, and zero-one law for sentences, of first-order logic. If we also assume that for some positive integer $\lambda$ the number of equivalence classes of every $L_n$ is exactly $\lambda$ and that all equivalence classes have roughly the same size, then we can also almost surely eliminate ``proportion quantifiers'' that express, for some $0 < r < 1$, that the proportion of elements satisfying a formula is larger than $r$; and we get a convergence law for first-order logic extended by such quantifiers.

We study asymptotic probabilities of formal languages specified by logical formulas. We focus on first-order sentences. We prove several results related to the asymptotic tractability of the two-variable fragment. Those results amount to show that asymptotic reasoning with two variables is feasible. We study some applications that are related to temporal reasoning.

Partial (i.e. unfinished) proofs can be represented by partial proof terms. These are proof terms expressing gaps in incomplete derivations with the help of formal sequents, that is, sequents occurring as proper components of the syntax of proof terms. Our previous paper applied this methodology to intuitionistic propositional logic, to show that focusing in sequent calculus corresponds to intercalation in bidirectional natural deduction. The main goal of this paper is to extend these results to classical logic, using the same methodology. We consider the focused sequent calculus LKT and a bidirectional natural deduction system with alternative conclusions, NKT, where the admissible typing rule for structural substitution is in fact an elimination rule for alternative implications.

When evaluating a counterfactual statement, it is often convenient to specify conditions that ought to be kept unchanged. Formally, this can be done by associating to each counterfactual a ceteris paribus set of formulas, specifying the facts that “ought to be kept unchanged”. Ceteris paribus counterfactuals originate in the debate between D. Lewis and Fine in the 1970s, and have been captured in formal accounts. However, these accounts are merely based on ‘counting’ formulas, and can yield counterintuitive results. In this paper, we develop a novel approach to evaluate ceteris paribus counterfactuals at (weakly) centered spher models, by taking into account the ‘significance’ of formulas that ought to be kept unchanged. Hypothetical states that keep the most significant formulas unchanged will be prioritized in the evaluation of a counterfactual. We show that the resulting notion of validity coincides with theoremhood in Lewis’ conditional logics VC or VW.

Tabular intermediate logics are intermediate logics characterized by finite posets treated as Kripke frames. For a poset $\mathbb P$, let $L(\mathbb P)$ denote the corresponding tabular intermediate logic. We investigate the complexity of the following decision problem {\sf LogContain}: given two finite posets $\mathbb P$ and $\mathbb Q$, decide whether $L(\mathbb P) \subseteq L(\mathbb Q)$. By Jankov's and de Jongh's theorem, the problem {\sf LogContain} is related to the problem {\sf SPMorph}: given two finite posets $\mathbb P$ and $\mathbb Q$, decide whether there exists a surjective $p$-morphism from $\mathbb P$ onto $\mathbb Q$. Both problems belong to the complexity class NP.We present two contributions. First, we describe a construction which, starting with a graph $\mathbb G$, gives a poset ${\sf Pos}(\mathbb G)$ such that there is a surjective locally surjective homomorphism (the graph-theoretic analog of a $p$-morphism) from $\mathbb G$ onto $\mathbb H$ if and only if there is a surjective $p$-morphism from ${\sf Pos}(\mathbb G)$ onto ${\sf Pos}(\mathbb H)$. This allows us to translate some hardness results from graph theory and obtain that several restricted versions of the problems {\sf LogContain} and {\sf SPMorph} are NP-complete. Among other results, we present a 18-element poset $\Q$ such that the problem to decide, for a given poset $\P$, whether $L(\P)\subseteq L(\Q)$ is NP-complete. Second, we describe a polynomial-time algorithm that decides {\sf LogContain} and {\sf SPMorph} for posets $\mathbb T$ and $\mathbb Q$, when $\mathbb T$ is a tree.