Abstract
Intermediate logics are logics stronger than intuitionistic logic I but weaker than classical logic C. Most of them are motivated by their semantical characterization. In this chapter we see how the goal-directed approach can be extended to this area by analysing two case-studies. We have seen in the previous chapter that intuitionistic logic is complete with respect to the class of finite Kripke models. One can refine the completeness theorem and show that intuitionistic logic is complete with respect to Kripke models whose possible-worlds structure form a finite tree. Given a Kripke model M = (W, ≤, w 0, V), we can concentrate on the structure (W, ≤, w 0), which is a finite tree, and forget about the evaluation function V for atoms. We write λ(E) for the set of labels occurring in E. Changing the terminology a bit, we will speak about models based on a given finite tree (W, ≤, w 0), since varying V we will have several models based on it. The completeness result can then be re-phrased to assert that intuitionistic logic is complete with respect to the class of finite trees, that is to say, with respect to Kripke models based on finite trees. This change of terminology matters as we are naturally lead to consider subclasses of finite trees and ask what axioms we can add to obtain a characterization of valid formulas in these subclasses. For instance here are two natural subclasses:
-
(1)
for any n, the class of finite trees of height ≤ n; a finite tree T = (W, ≤, w 0) is in this class if there are not n + 1 different elements w 0, w 1, ... , w n , such that
$${w_o} \leqslant {w_1} \leqslant ... \leqslant {w_n}hold.$$This means that all chains are of length ≤ n. Valid formulas in these subclasses are axiomatized by the axioms BH n of the next section.
-
(2)
for any n, the class of finite trees of width ≤ n; a finite tree T = (W, ≤, w 0) is in this class if there are not n different elements which are pairwise incomparable. Valid formulas in these subclasses are axiomatized by taking the axiom schema
$$V_{i = 1}^n({A_i} \to {V_{i \ne j}}{A_j})$$for finite width trees of width ≤ n. Notice that for n = 2, we have the axiom
$$({A_1} \to {A_2}) \vee ({A_2} \to {A_1})$$which gives the well known logic LC introduced independently by Dummett [1959] and Gödel [1932] that we have already mentioned in the previous chapter. This axiom corresponds to the property of linearity: the models are finite ordered sequence of worlds (i.e. there are not two incomparable points).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Gabbay, D.M., Olivetti, N. (2000). Intermediate Logics. In: Goal-Directed Proof Theory. Applied Logic Series, vol 21. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-1713-7_3
Download citation
DOI: https://doi.org/10.1007/978-94-017-1713-7_3
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5526-2
Online ISBN: 978-94-017-1713-7
eBook Packages: Springer Book Archive