Craig's interpolation theorem for the intuitionistic logic and its extensions - a semantical approach (Q1821770): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
Import240304020342 (talk | contribs)
Set profile property.
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank

Revision as of 04:48, 5 March 2024

scientific article
Language Label Description Also known as
English
Craig's interpolation theorem for the intuitionistic logic and its extensions - a semantical approach
scientific article

    Statements

    Craig's interpolation theorem for the intuitionistic logic and its extensions - a semantical approach (English)
    0 references
    0 references
    1986
    0 references
    Craig's interpolation theorem for intuitionistic predicate logic was first proved by Schütte using syntactical methods. Other syntactical proofs were given by, among others, Prawitz and Maehara. Semantical proofs were given by Gabbay, Fitting and Ono. One more such proof is given here, along the lines of the Henkin-style proof of the completeness theorem. Using a generalized notion of inseparable pair of theories, the author clarifies the relationship between interpolation and (Robinson's) consistency. As a corollary, the author also gives a new proof of the interpolation property of the seven intermediate propositional logics listed in \textit{L. L. Maksimova}'s paper in Algebra Logika 16, 643-681 (1977; Zbl 0403.03047). Warning: in reference [14], H. Ono should be replaced by K. \((=\) Katuzi) Ono, H. Ono's father.
    0 references
    semantical proof
    0 references
    intuitionistic logic
    0 references
    intermediate logic
    0 references
    joint consistency
    0 references
    inseparable theories
    0 references
    Robinson's theorem
    0 references
    Craig's interpolation
    0 references
    intuitionistic predicate logic
    0 references
    inseparable pair of theories
    0 references
    intermediate propositional logics
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references