Combining linear-time temporal logic with constructiveness and paraconsistency

It is known that linear-time temporal logic (LTL), which is an extension of classical logic, is useful for expressing temporal reasoning as investigated in computer science. In this paper, two constructive and bounded versions of LTL, which are extensions of intuitionistic logic or Nelson's paraconsistent logic, are introduced as Gentzen-type sequent calculi. These logics, $\mathrm{IB}[l]$ and $\mathrm{PB}[l]$, are intended to provide a useful theoretical basis for representing not only temporal (linear-time), but also constructive, and paraconsistent (inconsistency-tolerant) reasoning. The time domain of the proposed logics is bounded by a fixed positive integer. Despite the restriction on the time domain, the logics can derive almost all the typical temporal axioms of LTL. As a merit of bounding time, faithful embeddings into intuitionistic logic and Nelson's paraconsistent logic are shown for $\mathrm{IB}[l]$ and $\mathrm{PB}[l]$, respectively. Completeness (with respect to Kripke semantics), cut–elimination, normalization (with respect to natural deduction), and decidability theorems for the newly defined logics are proved as the main results of this paper. Moreover, we present sound and complete display calculi for $\mathrm{IB}[l]$ and $\mathrm{PB}[l]$.In [P. Maier, Intuitionistic LTL and a new characterization of safety and liveness, in: Proceedings of Computer Science Logic 2004, in: Lecture Notes in Computer Science, vol. 3210, Springer-Verlag, Berlin, 2004, pp. 295–309] it has been emphasized that intuitionistic linear-time logic (ILTL) admits an elegant characterization of safety and liveness properties. The system ILTL, however, has been presented only in an algebraic setting. The present paper is the first semantical and proof-theoretical study of bounded constructive linear-time temporal logics containing either intuitionistic or strong negation.     

Reasoning about negligibility and proximity in the set of all hyperreals

We consider the binary relations of negligibility, comparability and proximity in the set of all hyperreals. Associating with negligibility, comparability and proximity the binary predicates N, C and P and the connectives $[N]$, $[C]$ and $[P]$, we consider a first-order theory based on these predicates and a modal logic based on these connectives. We investigate the axiomatization/completeness and the decidability/complexity of this first-order theory and this modal logic.     

A family of Gödel hybrid logics

In this paper, we define a family of fuzzy hybrid logics that are based on Gödel logic. It is composed of two infinite-valued versions called ${\mathsf{GH}}_{\infty }$ and ${\mathsf{WGH}}_{\infty }$, and a sequence of finitary valued versions ${({\mathsf{GH}}_n)}_{0<n<\infty }$. We define decision procedures for both ${\mathsf{WGH}}_{\infty }$ and ${({\mathsf{GH}}_n)}_{0<n<\infty }$ that are based on particular sequents and on a set of proof rules dealing with such sequents. As these rules are strongly invertible the procedures naturally allow one to generate countermodels. Therefore we prove the decidability and the finite model property for these logics. Finally, from the decision procedure of ${\mathsf{WGH}}_{\infty }$, we design a sound and complete sequent calculus for this logic.     

Bridging Curry and Church's typing style

There are two versions of type assignment in the λ-calculus: Church-style, in which the type of each variable is fixed, and Curry-style (also called “domain free”), in which it is not. As an example, in Church-style typing, ${\lambda }_{x:A}.x$ is the identity function on type A, and it has type $A\to A$ but not $B\to B$ for a type B different from A. In Curry-style typing, ${\lambda }_x.x$ is a general identity function with type $C\to C$ for every type C. In this paper, we will show how to interpret in a Curry-style system every Pure Type System (PTS) in the Church-style without losing any typing information. We will also prove a kind of conservative extension result for this interpretation, a result which implies that for most consistent PTSs of the Church-style, the corresponding Curry-style system is consistent. We will then show how to interpret in a system of the Church-style (a modified PTS, stronger than a PTS) every PTS-like system in the Curry style.     

The psychology of inferring conditionals from disjunctions: A probabilistic study

There is a new probabilistic paradigm in the psychology of reasoning that is, in part, based on results showing that people judge the probability of the natural language conditional, if $A$then $B$, $P\left(ifAthenB\right)$, to be the conditional probability, $P(B\mid A)$. We apply this new approach to the study of a very common inference form in ordinary reasoning: inferring the conditional if not-$A$then $B$ from the disjunction $A$ or $B$. We show how this inference can be strong, with $P$(if not-$A$then $B$) “close to” $P\left(AorB\right)$, when $A$ or $B$ is non-constructively justified. When $A$ or $B$ is constructively justified, the inference can be very weak. We also define suitable measures of “closeness” and “constructivity”, by providing a probabilistic analysis of these notions.