In this note we study the effect of adding fixed points to justification logics. We introduce two extensions of justification logics: extensions by fixed point (or diagonal) operators, and extensions by least fixed points. The former is a justification version of Smory\`{n}ski’s Diagonalization Operator Logic, and the latter is a justification version of Kozen’s modal μ -calculus. We also introduce fixed point extensions of Fitting’s quantified logic of proofs, and formalize the Knower Paradox and the Surprise Test Paradox in these extensions. By interpreting a surprise statement as a statement for which there is no justification, we give a solution to the self-reference version of the Surprise Test Paradox in quantified logic of proofs.

The papers gathered in this collection were presented at the 8th International Workshop on Nonmonotonic Reasoning, NMR2000. The series was started by John McCarthy in 1978. The first international NMR workshop was held at Mohonk Mountain House, New Paltz, New York in June, 1984, and was organized by Ray Reiter and Bonnie Webber. In the last 10 years the area of nonmonotonic reasoning has seen a number of important developments. Significant theoretical advances were made in the understanding of general abstract principles underlying nonmonotonicity. Key results on the expressibility and computational complexity of nonmonotonic logics were established. The role of nonmonotonic reasoning in belief revision, abduction, reasoning about action, planing and uncertainty was further clarified.

We prove that the expressive power of first-order logic with team semantics plus contradictory negation does not rise beyond that of first-order logic (with respect to sentences), and that the totality atoms of arity k +1 are not definable in terms of the totality atoms of arity k. We furthermore prove that all first-order nullary and unary dependencies are strongly first order, in the sense that they do not increase the expressive power of first order logic if added to it.

We seize the opportunity of the publication of selected papers from the \emph{Logic, categories, semantics} workshop in the \emph{Journal of Applied Logic} to survey some current trends in logic, namely intuitionistic and linear type theories, that interweave categorical, geometrical and computational considerations. We thereafter present how these rich logical frameworks can model the way language conveys meaning.

In work of Fokkinga and Meertens a calculational approach to category theory is developed. The scheme has many merits, but sacrifices useful type information in the move to an equational style of reasoning. By contrast, traditional proofs by diagram pasting retain the vital type information, but poorly express the reasoning and development of categorical proofs. In order to combine the strengths of these two perspectives, we propose the use of string diagrams, common folklore in the category theory community, allowing us to retain the type information whilst pursuing a calculational form of proof. These graphical representations provide a topological perspective on categorical proofs, and silently handle functoriality and naturality conditions that require awkward bookkeeping in more traditional notation.

We prove an extensionality theorem for the “type-in-type” dependent type theory with Sigma-types. We suggest that the extensional equality type be identified with the logical equivalence relation on the free term model of type theory.

In recent years, a number of researchers have suggested that the extensional equality in type theory is the canonical logical relation defined by induction on type structure (Tait [1998], Altenkirch et al [2008], Coquand [2010], Harper et al [2013]). Here we make this position explicit in the statement of Extensionality Thesis.

Simple and useful classical logic is unfortunately defective with its problematic definition of material implication. This paper presents an implication relation defined by a simple equation to replace the traditional material implication in classical logic. Common “paradoxes” of material implication are avoided while simplicity and usefulness of the system are reserved with this implication relation.

Recursive maps, nowadays called primitive recursive maps, PR maps, have been introduced by G\”odel in his 1931 article for the arithmetisation, g\”odelisation, of metamathematics. For construction of his undecidable formula he introduces a non-constructive, non-recursive predicate beweisbar, provable. Staying within the area of categorical free-variables theory PR of primitive recursion or appropriate extensions opens the chance to avoid the two (original) G\”odel’s incompleteness theorems: these are stated for Principia Mathematica und verwandte Systeme, “related systems” such as in particular Zermelo-Fraenkel set theory ZF and v. Neumann G\”odel Bernays set theory NGB. On the basis of primitive recursion we consider \mu-recursive maps as partial pr maps. Special terminating general recursive maps considered are complexity controlled iterations. Map code evaluation is then given in terms of such an iteration. We discuss iterative pr map code evaluation versus termination conditioned soundness and based on this decidability of primitive recursive predicates.

We extend the polynomial time algorithms due to Buss and Mints(APAL 1999) and Ferrari, Fiorentini and Fiorino(LPAR 2002) to yield a polynomial time complete disjunction property in intuitionistic propositional logic.