Arché Logic Group
As I've mentioned earlier, this semester Arché has started a new logic group (boringly called 'Arché Logic Group', but unofficially named 'The Deviants'). There's now an Arché Twiki page for the seminar, although still quite provisional. The first part of the semester we're working through Graham Priest's "classic" An Introduction to Non-Classical Logic 
, preparing to go through a forthcoming publication by the same author. The usual (Scandinavian) suspects have been spending late office hours going through all of the exercises. True, there is quite a bit of tedious and repetitious work, but we have encountered a great deal of interesting material in some of the harder parts of the book.
However, this is only the warm-up: In early November we fly in the big guns. Then Priest himself will join in the fun when we proceed to uncharted terrain. By then there will hopefully be some comments on the first book on the Twiki page. I'll come back with more later.
Meanwhile: Today's session reminded me of a theorem that a friend of mine persistently has brought to my attention in another context. This is Glivenko's theorem (Glivenko 1929), which Priest has relegated to a footnote on p. 103.
Theorem. (a) If Gamma |- A in classical logic then ¬¬Gamma |- ¬¬A in intuitionistic logic, assuming that CL negations and implications are replaced by their IL counterparts. (b) If ¬Gamma,Sigma |- ¬A in CL then ¬Gamma,¬¬Sigma |- ¬A in IL.
Priest suggests that this theorem says that although IL is a sublogic of CL, CL is "in a sense" contained within IL. Of course, it is this "in a sense" which makes the theorem philosophically loaded - how are we to understand the resurfacing of classical truths within the intuitionistic system? Has it any bearing on the philosophical projects associated with the logics? Etc. I will not get into that here. Rather, I just want to point to a corollary of Glivenko's result that I was unaware of. Priest directs our attention to what he calls the "unobvious" fact that if |-A in classical logic, and A contains no logical notation except negation and conjunction, then |-A in intuitionistic logic as well (with intuitionistic conj. and neg.). Somewhat surprising perhaps, since intuitionistic and classical negation usually are thought to behave quite differently.
I checked out Priest's reference, which is to the standard Introduction to Metamathematics (1952) by Kleene (see pp. 492-493). The proof is something like this: Consider A as a conj. of n formulae (n is 1 or greater), where each conjunct is itself not a conjunction. Then, all conjuncts are either propositional variables or negated. Furthermore, if A is provable in CL, then all of its conjuncts are provable; but no propositional variables are provable. So, the conjuncts are all negated, and by Glivenko's theorem (b), they are provable in IL.
Any comments on this - philosophical or logical? (Paul Simon, if this isn't an invitation, nothing is.)
Hopefully, the ALG will prosper in the next few years, warranting the 'logic' part of the Arché research description. I'm already conspiring to make it into a proof-theory seminar next semester - one interesting suggestion was to read the manuscript for Greg Restall's forthcoming Proof-theory and Philosophy.
Update: Thanks to Aidan for this link.
, preparing to go through a forthcoming publication by the same author. The usual (Scandinavian) suspects have been spending late office hours going through all of the exercises. True, there is quite a bit of tedious and repetitious work, but we have encountered a great deal of interesting material in some of the harder parts of the book.However, this is only the warm-up: In early November we fly in the big guns. Then Priest himself will join in the fun when we proceed to uncharted terrain. By then there will hopefully be some comments on the first book on the Twiki page. I'll come back with more later.
Meanwhile: Today's session reminded me of a theorem that a friend of mine persistently has brought to my attention in another context. This is Glivenko's theorem (Glivenko 1929), which Priest has relegated to a footnote on p. 103.
Theorem. (a) If Gamma |- A in classical logic then ¬¬Gamma |- ¬¬A in intuitionistic logic, assuming that CL negations and implications are replaced by their IL counterparts. (b) If ¬Gamma,Sigma |- ¬A in CL then ¬Gamma,¬¬Sigma |- ¬A in IL.
Priest suggests that this theorem says that although IL is a sublogic of CL, CL is "in a sense" contained within IL. Of course, it is this "in a sense" which makes the theorem philosophically loaded - how are we to understand the resurfacing of classical truths within the intuitionistic system? Has it any bearing on the philosophical projects associated with the logics? Etc. I will not get into that here. Rather, I just want to point to a corollary of Glivenko's result that I was unaware of. Priest directs our attention to what he calls the "unobvious" fact that if |-A in classical logic, and A contains no logical notation except negation and conjunction, then |-A in intuitionistic logic as well (with intuitionistic conj. and neg.). Somewhat surprising perhaps, since intuitionistic and classical negation usually are thought to behave quite differently.
I checked out Priest's reference, which is to the standard Introduction to Metamathematics (1952) by Kleene (see pp. 492-493). The proof is something like this: Consider A as a conj. of n formulae (n is 1 or greater), where each conjunct is itself not a conjunction. Then, all conjuncts are either propositional variables or negated. Furthermore, if A is provable in CL, then all of its conjuncts are provable; but no propositional variables are provable. So, the conjuncts are all negated, and by Glivenko's theorem (b), they are provable in IL.
Any comments on this - philosophical or logical? (Paul Simon, if this isn't an invitation, nothing is.)
Hopefully, the ALG will prosper in the next few years, warranting the 'logic' part of the Arché research description. I'm already conspiring to make it into a proof-theory seminar next semester - one interesting suggestion was to read the manuscript for Greg Restall's forthcoming Proof-theory and Philosophy.
Update: Thanks to Aidan for this link.
Posts
20 comments:
Stephen Read's course on algebraic logic two years ago helped me a lot in seeing the 'sense' in which CL is contained in IL. It's really worth talking to him about it.
Philosophically, CL is going to be acceptable to the intuitionist so long as we have some guarentee that none of the statements in question are undecidable. So it would be interesting to be clearer on the relationship between the fragment involved in the proof of the corollary of Glivenko's result and decidability. If restricting our attention to this fragment guarentees decidability, then this fact may be "unobvious", but it wouldn't be surprising. (For some discussion of this partial acceptance of CL, see here.
Ps. The maths project spent a huge amount of time on the status of HOL, the modality conference has spent countless hours on modal logic, and the vagueness project gave a vast amount of time to exploring non-classical logics. If you want a proper challenge, try justifying the 'mind' in Arche's description....
Aidan:
Thanks for the link. I've put it as an update on the post.
Some questions:
"Philosophically, CL is going to be acceptable to the intuitionist so long as we have some guarentee that none of the statements in question are undecidable."
I assume that the 'statements in question' refer to the conj.-neg. formulae in the corollary? Logically, of course, the corollary itself ensures the decidability of these formulae, since provability in CL gives provability in IL. But are you perhaps alluding to a non-formal concept of decidability?
"So it would be interesting to be clearer on the relationship between the fragment involved in the proof of the corollary of Glivenko's result and decidability."
Or, are you rather refering to the decidability of the statements in the post, i.e., the proofs? I agree that it is interesting whether the proof is itself intuitionistically acceptable. I haven't looked into that in detail, but as far as I can see, there is only intuitionistically valid reasoning in the proofs (that is, both in Glivenko's theorem and in the corollary). But I'm prepared to be corrected.
I completely agree about the 'mind' part. Actually, I think they've decided to skip 'mind' in the description when the AHRC funding runs out. 'Logic', however, will still be in there.
Btw, do you know an elegant way of including logical symbols in html?
Sorry to have waited so long to comment on a very interesting post. I cannot access internet from home, so there goes.
As I'm working on an article (which you, Ole, have seen the first seed of) detailing the relationship IL-CL, I have too many thoughts on this subject. So I'll stick to a simple observation.
The reason why Glivenko's theorem works, algebraically, is that double pseudo-complement is a closure.
The "unobvious" fact you mention is interesting, but it is a corollary of the fact that all you need of intuitionistic logic to reconstruct classical logic is conjunction and intuitionistic negation.
So we could say that classical logic is the conjunction-negation-universal quantifier fragment of intuitinoistic logic: A rather symmetric sublogic of intuitionistic logic.
In any case, we should dispense entirely with the idea that intuitionistic logic is a sublogic of classical logic. It is simply false. More on this next week...
Yeah, sorry Ole, I wasn't being clear. When talking of decidability I meant the generalised notion that features heavily in Dummett's writings on anti-realism (and of course others like Wright and Tennant). By the 'statements in question' I meant some class of statements in dispute between the realist and the anti-realist (so mathematical statements, or statements about the past, etc).
When we have some domain of discourse where we are sure there aren't any potentially verification-transcendent (this is basically what I meant by undecidable) statements, the intuitionist can use classical logic and semantics. So this really was an answer to your request for philosophical comments rather than logic ones (sorry for being quite so inexplicit).
Sorry, no idea about how to put logical symbols in.
As a comment on Dummett on undecidability. Dummett has identified three kinds of undecidability that figures in the revisionary arguments: subjunctive conditionals, past tense and quantification of infinite totalities. Without undecidability, Dummett says, the debate between the intuitionist and the classicisit is of no practical consequences, since both their meaning-theories will correspond to the linguistic behaviour of the masters of the discourse in question. So, undecidability is usely taken as a premise in a revisionary argument, even though, e.g. Cogburn takes the possibility of undecidability to be sufficient for revisionary purposes.
Paul Simon:
"In any case, we should dispense entirely with the idea that intuitionistic logic is a sublogic of classical logic. It is simply false."
I take it that you don't propose that we revise the current def. of sublogic at large. That, of course, will have dramatic consequences for other systems, e.g., the order of modal logics. However, I wonder if you can make a general definition of when L is a sublogic L' s.t. CL is a sublogic of IL, but which avoids undesirable results for other systems. The problem, as I see it, is that such a definition must allow for the corresponding L' to be inside the scope of some L'-constant (e.g., IL negation) when it is *not* the case that the original L theorem is inside the scope of the corresponding L-constant.
Aidan & Pål:
Ad undecidability. Don't know about you, but I find the idea that the *actual* absence of undecidable statements warrants CL for the intuitionist a bit unsettling. I'm more comfortable with what seems to be Cogburn's position, that possibility of undecidability is sufficient for revisionary purposes. There could be, say, mathematical discourses where we don't know of any undecidable statements, but if the intuitionist allows himself CL resources when exploring the field, he might end up proving something he lacks philosophical warrant for.
I haven't really thought about how to formulate a general definiton of sublogic which puts CL inside IL. But hopefully such one already exists.
The two ways to answering this question proceeds along the stony road of syntax or the serene path of semantics.
On the one hand, given a logic L as a pair (S , T), where S is its signature and T is its set of provable formulae, we can think of a sublogic L' of L (i.e. L'{L )as a pair (S', T'), such that S'[S and T'[T, where '[' denotes inclusion. However, this approach leaves much to be desired. For example, when are two signatures equivalent? (E.g. when they produce the same set T?) Furthermore, the exclusive focus on syntax is perhaps not very illuminating (endless inductions, term-rewriting etc), seeing that there is always one more x \in T to prove...
On the other hand, one could say that the logic L whose models subsume those of L' also contains L'. I personally think this is good way to think of the ordering of logics. A sublogic L'{L is then the restricting of attention to only certain operations and elements of L. I don't think this will upset anything in e.g. the hierarchy of modal logics, as I think that ordering arose from investigating modal logics from the point of view of universal algebra. (I think Blackburn et. al. writes this in the first chapter of their "modal logic", but my memory has failed me before.)
So, if this semantical approach to sublogics is taken, CL turns out to be a sublogic of IL. The corresponding syntactical fact can of course also be proved. (See e.g. section 2.3 in Troelstra: Basic Proof Theory for a number of embeddings of CL into IL.) But since we almost never consider the syntax of CL as derived from the syntax of IL, the syntactic result is perhaps less convincing. And also, I think, more difficult to get a clear view of.
Still, I'm torn on this. I am hesitant to claim, for instance, that the higher up in the hierarchy L' { ... { L { ... one gets, the logics get more fundamental. In many instances, such orderings will not reflect anything but a notational convenience. On the other hand, I enjoy the idea of sublogics since it seems that given an ordering L' { ... { L, we can isolate a family, perhaps an entire species of logics.
Somebody has probably written a book about this stuff. Anybody know of any literature on this topic?
I assume we agree that there are at least to usual ways of ordering logics: one proof-theoretical (syntactical) and one semantical. The one which most frequently is used to define sublogicality is the proof-theoretic one: L' is a sublogic of L iff for every A s.t. |-A in L', |-A in L as well; and (if strict) there is an A in L such that |-A but not |-A in L'. This, for instance, is the definition on which the ordinary ordering of the modal systems from K and upwards are ordered (where K is, in a sense, the smallest logic). However, I perfectly agree that by looking at it semantically, the ordering is turned up-side-down: say that L' is a sublogic of L iff every L'-model is is an L-model; and (if strict) there is an L-model which is not an L'-model. In other words, the ordering would now have the modal system K as the "largest logic", model-theoretically containing the other systems.
This duality, however, is not what my challenge consists in. Needless to say, I grant that on the semantic conception CL is a sublogic of IL (I guess this was your point as well). But, claiming that CL is a sublogic of IL proof-theoretically as well (say, because of some mapping like that provided by Glivenko) seems like a more interesting claim. And - it is for this claim that I want a new def. of sublogicality, i.e. a revised proof-theoretical definition.
Why is this a challenge? Because the mappings you refer to (Troelstra 2.3) all seem to use the so-called negative fragment of CL. I see no reason why this particular relation between CL and IL should give rise to a general definition of sublogicality.
Philosophically, it seems that it is this fact, that the negation is essential, which load the dice.
I made a mess, alas. Busy weekend, also alas.
Long comment due on sunday.
Your challenge points directly to issues I have been obsessing over for a while. I will try to answer it, and make some additional comments in an attempt to present a perspective on the more general questions at stake.
"I assume we agree that there are at least to usual ways of ordering logics: one proof-theoretical (syntactical) and one semantical. The one which most frequently is used to define sublogicality is the proof-theoretic one: L' is a sublogic of L iff for every A s.t.
|-A in L', |-A in L as well... However, I perfectly agree that by looking at it semantically, the ordering is turned up-side-down"
The contravarians between syntax and semantics seems to me to be misleading in this case. That is, not in the isolated case of CL and IL, but in the question of how to order logics w.r.t. some sort of inclusion.
Now, why is this contravarians misleading? If the models M(L') of a logic L' is contained in the models M(L) of a logic L, then this fact should find a syntactic expression as well, if for no other reason than completeness, whenever that obtains.
I suggest we don't think of the ordering of logics as dependent on whether we induce an order from syntax or semantics. A logic should be considered as a pair, syntax and semantics. In doing this we should not be forced to accept dialogues like
a: "L' is a sublogic of L"
b: "... ah, I see, you mean from the syntactic perspective..."
because it seems that a and b have no clear notion of a logic. To put it bluntly, either IL is a sublogic of CL or CL is a sublogic of IL. It should depend at from which angle one is looking at the matter. Dialetism is not an option.
Our claim is semantical sublogicality obtains iff syntactic sublogicality obtains.
Why bother with completeness in the first place? If I remember correctly, Priest's argument that IL is a sublogic of CL is based on semantical (Kripke-style) considerations. This is then a common way to approach the issue of sublogicality, and, depending on the choice of models, one which may yield different results. As an aside, one can note that Kripke-semantics for IL produces wrong metalogical results. This may indicate that something is amiss with Kripke-semantics as a semantical framework.
But in what sense are we justified in holding that IL cannot be a sublogic of CL? in order to answer this we should consider the question what does it mean when a logic proves less formulae?. The sole reason for claiming that IL is a sublogic of CL is that there is some formula which CL proves but not IL, e.g. A v ~A. When CL proves "A v ~A" it claims that this can never fail to hold. I.e. it disregards all instances, all possible situations, where it might fail. This is to say that CL consider a limited range of possible situations. On the other hand, IL does not claim that "A v ~A" holds all the time, but maybe sometimes. One can think of this as the logics ability to make disctinctions. This points to the duality between syntax and semantics you refer to, but we interpret it differently. If L proves some formula A which L' does not, other things being equal, then there is a syntactic distinction which L is not aware of, which L' respects. Think of e.g. ~~A = A in Cl and the de Morgan dualities and so on. They are distinct to our eyes, notation-wise and so forth, but they are equivalent are far as provability goes. This is a part of the syntactic expression of the fact that the less formulae some logic proves, the more models does its semantics subsume.
Keeping this in mind, we can proceed to justifying our above claim. Though, perhaps this is only partially an answer to your challenge, which was a revised proof-theoretical definition of sublogicality, since semantics somehow jumped on the train too. But I think everything will be covered in the end.
"Why is this a challenge? Because the mappings you refer to (Troelstra 2.3) all seem to use the so-called negative fragment of CL. I see no reason why this particular relation between CL and IL should give rise to a general definition of sublogicality."
CL appear as a restriction on the negative fragment of IL. This relation is particular to CL and IL -- it is just the way things are between those logics. What makes the relation between them general and interesting, is the fact that the embedding of CL in IL is faithful. All of CL can be reconstructed from IL. We are less concerned with the particulars of the embedding, in the case of IL-CL, that negation is essential, so long as the embedding exists and is faithfull.
So, what is the syntactic counterpart of model-inclusion? Embeddability! And it must be faithful too.
SUBLOGIC:
A logic L' is a subglogic of L iff there exists a map m() s.t.
L' |- A iff L |- m(A)
I mean, this is bound to have been covered in the literature on abstract model-theory and institutions in one way or another, so I have no delusions of originality here, but it is in my mind the best way to think of the ordering of logics. This way, a sublogic is actually a living fragment of some other logic, not just a subset of a set of wffs.
For example, we get that CL is a sublogic of IL, that both CL and IL are sublogics of S4. Also, we have that CL and IL are sublogics of linear logic (LL). Also, LL and S4 share the same modalities, but with different handling of contexts, or "resources", so I don't really know what happens there, but S4 is probably a sublogic of LL. etc..
To be continued...
Paul Simon:
"If the models M(L') of a logic L' is contained in the models M(L) of a logic L, then this fact should find a syntactic expression as well, if for no other reason than completeness, whenever that obtains."
Precisely how do you figure that the model-theoretic inclusion will manifest itself? Take for instance the modal systems K and T: M(T) is a (proper) subset of M(K). So, if a sentence A has a T-model (is T-satisfiable), then it has a K-model (is K-satisfiable), but not vice versa. The only immediate syntactic upshot of this is that if the formula A is T-consistent, then it is K-consistent. This follows by soundness.
"As an aside, one can note that Kripke-semantics for IL produces wrong metalogical results. This may indicate that something is amiss with Kripke-semantics as a semantical framework."
What do you mean by "wrong" metalogical results. Granted, they are different from algebraic semantics, but does that make them wrong?
"If L proves some formula A which L' does not, other things being equal, then there is a syntactic distinction which L is not aware of, which L' respects. Think of e.g. ~~A = A in Cl and the de Morgan dualities and so on. They are distinct to our eyes, notation-wise and so forth, but they are equivalent are far as provability goes. This is a part of the syntactic expression of the fact that the less formulae some logic proves, the more models does its semantics subsume."
I more or less agree with this part.
"So, what is the syntactic counterpart of model-inclusion? Embeddability! And it must be faithful too.
SUBLOGIC:
A logic L' is a subglogic of L iff there exists a map m() s.t.
L' |- A iff L |- m(A)"
But I thought that this was satisfied both for CL = L', IL = L and for CL = L, IL = L'. In other words, that there is a faithful embedding both ways. Maybe I'm getting something wrong here, but if this is the case then it seems that it contradicts your statement earlier in the comments:
"To put it bluntly, either IL is a sublogic of CL or CL is a sublogic of IL. It should depend at from which angle one is looking at the matter. Dialetism is not an option."
I'm prepared to be corrected on this.
Last things first.
"To put it bluntly, either IL is a sublogic of CL or CL is a sublogic of IL. It should depend at from which angle one is looking at the matter. Dialetism is not an option."
should read
"To put it bluntly, either IL is a sublogic of CL or CL is a sublogic of IL. It should not depend at from which angle one is looking at the matter. Dialetism is not an option."
So, on to the meat.
""SUBLOGIC:
A logic L' is a subglogic of L iff there exists a map m() s.t.
L' |- A iff L |- m(A)"
But I thought that this was satisfied both for CL = L', IL = L and for CL = L, IL = L'. In other words, that there is a faithful embedding both ways"
There is only a faithful embedding of CL into IL. One can, however, embed IL into CL by some map m, but we cannot recover the distinctions collapsed in CL by this m. I think I gave a counterexample to show we lose faithfulness in my thesis, but I don't remember exactly how it got off the ground. The point of embeddings is to preserve the operational meaning of the logical constants. If the embedding is faithful, then we have identified a syntactic fragment L' of a logic L, s.t. all the logical operations (the rules!) are intact. This means that they are not weakened (in their "sense", so to speak). When we embed IL into CL, we are in effect weakening all the intuitionistic operations. Since CL is not fine grained enough, i.e. proves to many equivalences, we cannot reverse this weakening. This can also be thought of in terms of the non-invertibility of Weakening in sequent systems, though this is only a metaphor.
""As an aside, one can note that Kripke-semantics for IL produces wrong metalogical results. This may indicate that something is amiss with Kripke-semantics as a semantical framework."
What do you mean by "wrong" metalogical results. Granted, they are different from algebraic semantics, but does that make them wrong?"
My claim that Kripke-semantics produces wrong metalogical results is not based on the fact that algebraic semantics gives a different metalogical result. However, the upshot of the differences between Kripke-semantics and algebraic semantics, is that I think algebraic semantics produces the right metalogical results. I see it this way. A logic is a language used to describe some structure. The more distinctions the language is able to make, the more differences the language is able to discern -- then, if such a language, a logic L, admits a faithful embedding of another logic L', then I would think that L' is a sublogic of L, since L is able to describe all that L' describes, but at the same time make more distinctions. It appears we agree more or less that on the syntactic level, IL makes more distinctions than CL in that IL does not collapse e.g. ~~A and A. Also, since CL is faithfully embeddable in IL, but not the other way around, I think the coast is clear to say that CL is a sublogic of IL. It is from this line of thought I would argue that Kripke-semantics produces wrong metalogical results.
"Precisely how do you figure that the model-theoretic inclusion will manifest itself? (...)"
I'm not sure. I haven't really thought about it. Maybe my understanding of sublogicality (a very strict one indeed) is applicable and limited only to the class of logics closely related to IL: CL, S4, LL. However, I do not believe this to be the case.
"The only immediate syntactic upshot of this is that if the formula A is T-consistent, then it is K-consistent. This follows by soundness."
I think I can account for the relationship between CL, IL, S4 and LL. I don't know about S5, nor the smaller modal logics like K, T, K4 etc. My feeble attempt at defining sublogicality is probably too strong, and thus also likely to give us wrong metalogical results every now and then. But I think that behind the the hierarchy of modal logics, the intelligent way of defining sublogicality is probably already given. And I think semantics is indispensible in dealing with this question.
"My feeble attempt at defining sublogicality is probably too strong, and thus also likely to give us wrong metalogical results every now and then."
I withdraw this comment.
There is a certain amount of relativity in the talk about sublogics, e.g. as evidenced by the "less" tautologies, "more" models duality. It seems that we have some liberty in chosing along which dimensions we would like to measure the unit of sublogicality.
Should we start with the axiomatization, the semantics or perhaps with something else?
I think the right place to start when dealing with the notion of sublogicality, is logical strentgth.
This is what it boils down to: If some logic L' is expressible by another L, then we should say L' is a sublogic of L. Thus we measure sublogicality according to what structures can be described/named by the logics, which seems to me to be fair to the nature of Logic.
Embeddings is the natural way of establishing the syntactic result about logical strength. "Model theoretic inclusion" is the natural way of establishing the semantics result about logical strength. Both of these have non-trivial "methods" of verification, except for in the simplest cases.
One could argue that the notion of logical strength is at heart a semantical one. This is unproblematic to me, but if one so desires, one can counter this by pointing out that it is not a semantical notion exclusively. The whole point of ordering logics according to their expressive power, is to capture both their language and their models. Otherwise the relation between language and models, syntax and semantics, would appear fragmentary and to a certain degree arbitrary. If one by preference would like to work exclusively in the one realm at the expense of the other, one should nonetheless use notions which preserve the "good" qualities which lie inherent in Logic, and respects the nexus between syntax and semantics.
I must admit that I'm still puzzled. I take it that you want to have a proof-theoretic and a model-theoretic notion of sublogicality, such that these coincide (I assume, only when there is completeness and soundness).
So, according to the two points you have been discussing, such a relation would mean something along the following lines.
Let L, L' be two logics, and M(L), M(L') be their models:
M(L') is a subset of M(L) iff
there is a faithful embedding of L' into M. Is this what you suggest?
A further question: What about the relation between classical propositional logic and classical first-order logic? What is the sublogicality relation between these on your account?
For logical symbols in HTML, add this keyboard to your toolbar. The following is a tentative application.
Humberstone writes (The Connectives, p.275):
"One reaction to this [ie : the 'unobvious" corollary of Glivenko you mentionned in your post] has been to suggest that far from being a subsytem of CL, IL is actually an extension, every classical tautology being rewritten in terms of the functionally complete connectives ¬ and ∧ (thus giving a formula by classical lights equivalent to the original, with intuitionistic → and ∨ regarded as additional connectives, like the ⇑ of modal logic [...]. However the temptation is best resisted since the result in question does not extend to the consequence relation concerned (e.g. it is not an IL truth that : ¬¬p l- p ) " (Humbestone's emphasis)
Note also that Glivenko's theorem does not hold for predicate IL and CL logics :
It is classically true that : l- ∀ (Fx ∨ ¬ Fx)
but not intuitionistically true that l- ¬¬ ∀ (Fx ∨ ¬ Fx)
Finally, you have probably noticed that in the definition of the UNILOG 2007 (here) contest, reference is made to a result of Wojcicki and more generally to different notions of translation of a logic in another logic. I don't know what Wojcicki's result states, and I'd be interested in earing from someone having any lights on this.
Best
Thanks Henri,
This was very helpful. It is quite true that Glivenko's theorem is restricted, but although the provability relation (e.g., in your example ¬¬p |- p) is not within the scope of the corollary in question, extending Glivenko's theorem to a full translation (i.e., the Gödel-Gentzen translation), the above example becomes provable as ¬¬¬¬p |- ¬¬p since all atomic formulae are doubly negated.
Furthermore, the translation also works for the first-order case by devising a translation s.t. exists x (Ax) := ¬ forall ¬Ax. I'll have to see what more Humberstone has to say about this; it's definitely an interesting passage.
I have noticed the references on the UNILOG page, but I've had a hard time finding some of them. I would especially like to look at the Prawitz & Malmnäs paper from 1968, but so far I haven't been able to get the anthology it's printed in.
Best,
Post a Comment