×

The pleasures of anticipation: Enriching intuitionistic logic. (English) Zbl 1002.03012

Summary: We explore a relation we call ‘anticipation’ between formulas, where \(A\) anticipates \(B\) (according to some logic) just in case \(B\) is a consequence (according to that logic, presumed to support some distinguished implicational connective \(\to)\) of the formula \(A\to B\). We are especially interested in the case in which the logic is intuitionistic (propositional) logic and are much concerned with an extension of that logic with a new connective, written as “\(a\)”, governed by rules which guarantee that for any formula \(B\), \(aB\) is the (logically) strongest formula anticipating \(B\). The investigation of this new logic, which we call \(\text{IL}a\), will confront us on several occasions with some of the finer points in the theory of rules and with issues in the philosophy of logic arising from the proposed explication of the existence of a connective (with prescribed logical behaviour) in terms of the conservative extension of a favoured logic by the addition of such a connective. Other points of interest include the provision of a Kripke semantics with respect to which \(\text{IL}a\) is demonstrably sound, deployed to establish certain unprovability results as well as to forge connections with C. Rauszer’s logic of dual intuitionistic negation and dual intuitionistic implication, and the isolation of two relations (between formulas), head-implication and head-linkage, which, though trivial in the setting of classical logic, are of considerable significance in the intuitionistic context.

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)

Software:

PLINK
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Anderson, A. R. and Belnap, N. D.: Modalities in Ackermann’s ”Rigorous Implication”, J. Symbolic Logic 24 (1959), 107–111. · Zbl 0090.00903 · doi:10.2307/2964754
[2] Belnap, N. D.: Tonk, plonk, and plink, Analysis 22 (1962), 130–134. · doi:10.2307/3326862
[3] Bessonov, A. V.: New operations in intuitionistic calculus, Math. Notes of the Academy of Sciences of the USSR 22 (1977), 503–506. · Zbl 0421.03018 · doi:10.1007/BF01147689
[4] De Jongh, D. H. J.: A Class of intuitionistic connectives, in J. Barwise, H. J. Keisler and K. Kunen (eds.), The Kleene Symposium, North-Holland, Amsterdam, 1980, pp. 103–111. · Zbl 0479.03015
[5] De Jongh, D. H. J. and Chagrova, L. A.: The decidability of dependency in intuitionistic propositional logic, J. Symbolic Logic 60 (1995), 498–504. · Zbl 0836.03010 · doi:10.2307/2275844
[6] Fagin, R., Halpern, J. and Vardi, M.: What is an inference rule?, J. Symbolic Logic 57 (1992), 1018–1045. · Zbl 0761.03010 · doi:10.2307/2275447
[7] Gabbay, D.: Semantical Investigations in Heyting’s Intuitionistic Logic, Reidel, Dordrecht, 1981. · Zbl 0453.03001
[8] Gurevich, Y.: Intuitionistic logic with strong negation, Studia Logica 36 (1977), 49–59. · Zbl 0366.02015 · doi:10.1007/BF02121114
[9] Hazen, A. P.: An application of generalized natural deduction, Melbourne University Department of Philosophy Preprint Series (No. 5 for the year), 1996.
[10] Humberstone, L.: Valuational semantics of rule derivability, J. Philos. Logic 25 (1996), 451–461. · Zbl 0859.03005 · doi:10.1007/BF00257380
[11] Humberstone, L.: Singulary extensional connectives: A closer look, J. Philos. Logic 26 (1997), 341–356. · Zbl 0874.03010 · doi:10.1023/A:1004240612163
[12] Humberstone, L.: An intriguing logic with two implicational connectives, Notre Dame J. Formal Logic 41 (2000), 1–41. · Zbl 1005.03026 · doi:10.1305/ndjfl/1027953481
[13] Humberstone, L.: Contra-classical logics, Australas. J. Philos. 78 (2000), 438–474. · doi:10.1080/00048400012349741
[14] Humberstone, L.: Archetypal forms of inference, in preparation. · Zbl 1058.03008
[15] Humberstone, L. and Williamson, T.: Inverses for normal modal operators, Studia Logica 59 (1997), 33–64. · Zbl 0887.03015 · doi:10.1023/A:1004995316790
[16] Kabziński, J. and Wroński, A.: On equivalential algebras, in Proc. 1975 International Symposium on Multiple-Valued Logic, Auspices of the IEEE Computer Society, Indiana University, Bloomington, 1975, pp. 419–428.
[17] Komori, Y.: Logics without Craig’s interpolation property, Proc. of the Japan Academy (Ser. A) 54 (1978), 46–48. · Zbl 0399.03048 · doi:10.3792/pjaa.54.46
[18] Koslow, A.: A Structuralist Theory of Logic, Cambridge University Press, Cambridge, 1992. · Zbl 0813.03001
[19] Kreisel, G.: Monadic operators defined by means of propositional quantification in intuitionistic logic, Reports on Math. Logic 12 (1981), 9–15. · Zbl 0464.03051
[20] López-Escobar, E. G. K.: On intuitionistic sentential connectives. I, Revista Colombiana de Matemáticas 19 (1985), 117–130. · Zbl 0616.03035
[21] McKay, C. G.: A consistent propositional logic without any finite models, J. Symbolic Logic 50 (1985), 38–41. · Zbl 0566.03008 · doi:10.2307/2273785
[22] Prior, A. N.: Logicians at play; or Syll, Simp, and Hilbert, Australas. J. Philos. 34 (1956), 182–192. · doi:10.1080/00048405685200181
[23] Prucnal, T.: Interpretations of classical implicational sentential calculus into nonclassical implicational calculi, Studia Logica 33 (1974), 59–64. · Zbl 0309.02008 · doi:10.1007/BF02120866
[24] Rauszer, C.: Semi-Boolean algebras and their applications to intuitionistic logic with dual operations, Fund. Math. 83 (1974), 219–249. · Zbl 0298.02064
[25] Rauszer, C.: A formalization of the propositional calculus of H-B logic, Studia Logica 33 (1974), 23–34. · Zbl 0289.02015 · doi:10.1007/BF02120864
[26] Rauszer, C.: An algebraic approach to the Heyting–Brouwer predicate calculus, Fund. Math. 96 (1977), 127–135. · Zbl 0365.02047
[27] Rauszer, C.: Applications of Kripke Models to Heyting–Brouwer Logic, Studia Logica 36 (1977), 61–71. · Zbl 0361.02033 · doi:10.1007/BF02121115
[28] Rauszer, C.: Model theory for an extension of intuitionistic logic, Studia Logica 36 (1977), 73–87. · Zbl 0361.02034 · doi:10.1007/BF02121116
[29] Rauszer, C.: An algebraic and Kripke-style approach to a certain extension of intuitionistic logic, Dissertationes Math. 167 (1980). · Zbl 0442.03024
[30] Scott, D.: Rules and derived rules, in S. Stenlund (ed.), Logical Theory and Semantic Analysis, Reidel, Dordrecht, 1974, pp. 147–161. · Zbl 0296.02012
[31] Segerberg, K.: Propositional logics related to Heyting’s and Johansson’s, Theoria 34 (1968), 26–61. · doi:10.1111/j.1755-2567.1968.tb00337.x
[32] Skolem, T.: Consideraciones sobre los fundamentos de la matemática, Rev. Mat. Hispano-Americana 12 (1952), 169–200.
[33] Smiley, T. J.: Relative necessity, J. Symbolic Logic 28 (1963), 113–134. · Zbl 0125.00512 · doi:10.2307/2271593
[34] Shoesmith, D. J. and Smiley, T. J.: Deducibility and many-valuedness, J. Symbolic Logic 36 (1971), 610–622. · Zbl 0253.02015 · doi:10.2307/2272465
[35] Surma, S. J., (ed.): Mordchaj Wajsberg: Logical Works, Polish Academy of Sciences, Institute of Philosophy and Sociology, Ossolineum, 1977.
[36] Troelstra, A. S.: On a second order propositional operator in intuitionistic logic, Studia Logica 40 (1981), 113–139. · Zbl 0473.03022 · doi:10.1007/BF01874704
[37] Troelstra, A. S. and van Dalen, D.: Constructivism in Mathematics: An Introduction, Vols. I and II, North-Holland, Amsterdam, 1988. · Zbl 0661.03047
[38] Wójcicki, R.: Theory of Logical Calculi, Kluwer Academic Publishers, Dordrecht, 1988. · Zbl 0682.03001
[39] Wojtylak, P.: Independent axiomatizability of sets of sentences, Ann. of Pure Appl. Logic 44 (1989), 259–299. · Zbl 0687.03015 · doi:10.1016/0168-0072(89)90034-1
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.