English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In this paper, we attempt to investigate the so-called constructive predicate logic with strong negation from a model-theoretical point of view. Strong negation was first introduced by Nelson [8] in connection with Kleene's recursive realizability. At the same time, Markov [7] showed independently that intuitionistic (Heyting) negation can be defined by strong negation and implication. Then Vorob'ev [14] formulated constructive propositional logic with strong negation. Polish logicians such as Rasiowa [9],[10] studied in terms of lattice theory. Additionally, we can find a Gentzen-type formulation by Almukdad and Nelson [1] and Ishimoto [5],[6], and a model-theoretic study by Thomason [13] and Routley [11], to cite only a few. Strong negation is a constructive negation different from Heyting negation. For example, in intuitionistic logic, -^(A r\B) is not equivalent to the derivability of at least one formula of -*A or ~^B. And we cannot prove the equivalence between -^VxA(x) and -^A(t). But these are equivalent in constructive logic with strong negation. In this paper, we research this system on the basis of Kripke's many worlds semantics (the so-called Kripke model), and try to provide a Henkin-type proof of the completeness theorem for the system. We will also inquire into the relationships among constructive predicate logic with strong negation, classical logic, and intuitionistic logic.

Constructive predicate logic with strong negation and model theory.