Wyniki wyszukiwania - BazTech

1

A note on Humberstone's constant Ω

Niki Satoru, Omori Hitoshi

Reports on Mathematical Logic

|

2021

|

Vol. 56

75--99

EN

We investigate an expansion of positive intuitionistic logic obtained by adding a constant Ω introduced by Lloyd Humberstone. Our main results include a sound and strongly complete axiomatization, some comparisons to other expansions of intuitionistic logic obtained by adding actuality and empirical negation, and an algebraic semantics. We also briefly discuss its connection to classical logic.

2

What Are Justification Logics?

Fitting Melvin

Fundamenta Informaticae

|

2019

|

Vol. 165, nr 3-4

193--203

EN

Justification logic began with Sergei Artemov’s work providing an arithmetic semantics for intuitionistic logic. As part of that work, a small number of explicit modal logics were introduced—logics in which there was a structure of terms that kept track of not just what was a necessary truth, but why it was necessary. These explicit modal logics were connected with standard modal logics such as S4, T, K, and others using Realization Theorems, essentially saying that modal operators concealed an underlying informational structure. Since Artemov’s work, the phenomenon of justification logic has turned out to be very broad. For instance, I have shown that infinitely many modal logics have justification counterparts. In this paper I will sketch the basics and try to give some of the ideas behind formal justification proofs, justification semantics, and realization theorems.

3

Strong Normalization for Truth Table Natural Deduction

Geuvers Herman, van der Giessen Iris, Hurkens Tonny

Fundamenta Informaticae

|

2019

|

Vol. 170, nr 1-3

139--176

EN

We present a proof of strong normalization of proof-reduction in a general system of natural deduction called truth table natural deduction. In previous work, we have defined truth table natural deduction, which is a method for deriving intuitionistic derivation rules for a connective from its truth table. This yields natural deduction rules for each connective separately. Moreover, these rules adhere to a standard format which gives rise to a general notions of detour and permutation conversion for natural deductions. The aim is to remove all convertibilities and obtain a deduction in normal form. In general, conversion of truth table natural deductions is non-deterministic, which makes it more challenging to study. It has already been shown that this conversion is weakly normalizing. To prove strong normalization, we construct a conversion-preserving translation from deductions to terms in an extension of simply typed lambda calculus which we call parallel simply typed lambda calculus and which we prove to be strongly normalizing. This makes it possible to get a grip on the non-deterministic character of conversion in the intuitionistic truth table natural deduction system.

4

Multi-Agent Dialogues and Dialogue Sequents for Proof Search and Scheduling in Intuitionistic Logic and the Modal Logic S4

Sticht M.

Fundamenta Informaticae

|

2018

|

Vol. 161, nr 1/2

191--218

EN

Dialogical games as introduced by Lorenzen and Lorenz describe a reasoning technique for intuitionistic and classical predicate logic: two players (proponent and opponent) argue about the validity of a given formula according to predefined rules. If the proponent has a winning strategy then the formula is proven to be valid. The underlying game rules can be modified to have an impact on proof search strategies and increase the efficiency of such a searching process. In this paper, a multi-agent version of dialogical logic is introduced that corresponds more to multiconclusion sequent calculi for propositional intuitionistic logic rather than single-conclusion ones which are more related to two-player dialogues. We also consider an extension for the normal modal logic S4. The rules lead us to a normalization of a proof, let us focus on the proponents' relevant decisions, and therefore give explicit directives that increase compactness of the proofsearching process. This allows us to perform parts of the proof in a parallel way. We prove soundness and completeness of these multi-agent systems.

5

An alternative intuitionistic version of Mally's deontic logic

Lokhorst G. J. C.

Reports on Mathematical Logic

|

2016

|

Vol. 51

35--41

EN

Some years ago, Lokhorst proposed an intuitionistic reformulation of Mally's deontic logic (1926). This reformulation was unsatisfactory, because it provided a striking theorem that Mally himself did not mention. In this paper, we present an alter- native reformulation of Mally's deontic logic that does not provide this theorem.

6

An axiomatization of Wansing's expansion of Nelson's logic

Omori H.

Reports on Mathematical Logic

|

2015

|

Vol. 50

41--51

EN

The present note offers an axiomatization for an expansion of Nelson’s logic motivated by Heinrich Wansing which serves as a base logic for the framework of nonmonotonic reasoning considered by Dov Gabbay and Raymond Turner. We also show that the expansion of Wansing is not conservative over intuitionistic logic, but at least as strong as Jankov’s logic.

7

Explicit Constructive Logic ECL : a New Representation of Construction and Selection of Logical Information by an Epistemic Agent

Gentilini P., Martelli M., Rosolini G.

Fundamenta Informaticae

|

2015

|

Vol. 140, nr 3/4

357--372

EN

One of the main goals of Explicit Constructive Logic (ECL) is to provide a constructive formulation of Full (Classical) Higher Order Logic LKω that can be seen as a foundation for knowledge representation. ECL is introduced as a subsystem Zω of LKω. The first order case Z1 and the propositional case Z0 of ECL are examined as well. A comparison of constructivism from the point of view of ECL and of the corresponding features of Intuitionistic Logic, and Constructive Paraconsistent Logic is proposed.

8

Circular Causality in Event Structures

Bartoletti M., Cimoli T., Pinna G. M., Zunino R.

Fundamenta Informaticae

|

2014

|

Vol. 134, nr 3/4

219--259

EN

We propose a model of events with circular causality, in the form of a conservative extension of Winskel’s event structures. We study the relations between this new kind of event structures and Propositional Contract Logic. Provable atoms in the logic correspond to reachable events in our event structures. Furthermore, we show a correspondence between the configurations of this new brand of event structures and the proofs in a fragment of Propositional Contract Logic.

9

Characterising Strongly Normalising Intuitionistic Terms

Santo J. E., Ivetić J., Likavec S.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

83-120

EN

This paper gives a characterisation, via intersection types, of the strongly normalising proof-terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary λ-calculus. The completeness of the typing system is obtained from subject expansion at root position. Next we use our result to analyze the characterisation of strong normalisability for three classes of intuitionistic terms: ordinary λ-terms, ΛJ-terms (λ-terms with generalised application), and λx-terms (λ-terms with explicit substitution). We explain via our system why the type systems in the natural deduction format for ΛJ and λx known from the literature contain extra, exceptional rules for typing generalised application or substitution; and we show a new characterisation of the β-strongly normalising l-terms, as a corollary to a PSN-result, relating the λ-calculus and the intuitionistic sequent calculus. Finally, we obtain variants of our characterisation by restricting the set of assignable types to sub-classes of intersection types, notably strict types. In addition, the known characterisation of the b-strongly normalising l-terms in terms of assignment of strict types follows as an easy corollary of our results.

10

Extensions of Intuitionistic Logic Without the Deduction Theorem: Some Simple Examples

Humberstone L.

Reports on Mathematical Logic

|

2006

|

Nr 40

45-82

EN

We provide some illustrations of consequence relations extending that associated with intuitionistic propositional logic but lacking the Deduction Theorem, together with a discussion of issues of some interest in their own right raised by these examples. There are two main examples, with some minor variations: one in which the language of intuitionistic logic is retained, and one in which this language is expanded.