text:
Empirical Negation
- 1.1k Downloads
- Citations
An extension of intuitionism to empirical discourse, a project most seriously taken up by Dummett and Tennant, requires an empirical negation whose strength lies somewhere between classical negation ('It is unwarranted that. . . ') and intuitionistic negation ('It is refutable that. . . '). I put forward one plausible candidate that compares favorably to some others that have been propounded in the literature. A tableau calculus is presented and shown to be strongly complete.
KeywordsIntuitionistic negation Empirical negation Strong negation Verificationism Dummett
1 Introduction
In mathematical discourse a uniform treatment of negated and unnegated statements can be given by defining the former in terms of the latter. If A is a mathematical statement then its negation may be defined as A → ⊥ where ⊥ is either taken as primitive or as an abbreviation of some fixed absurdity such as 0 = 1. What counts as an "absurdity" will depend on the background formal theory. Notice that in the usual arithmetical setting, defining the negation of A as A → 0 = 1 gives us the constructive properties of negation we expect. For example, ex falso quodlibet —that from A and ¬A anything follows—is derivable from modus ponens and the fact that 0 = 1 implies everything. Negation introduction and elimination are then just special cases of implication introduction and elimination.
However, there are issues concerning the choice of absurdity. If a theory does not contain sufficient arithmetic then 0 = 1 may not do. Indeed, there may be no single sentence able to play the role of absurdity across all mathematical discourses. Instead we shall have to choose, for a given mathematical theory, some sentence able to assume the role of absurdity. In practice this poses no problem on the assumption—and this assumption seems safe enough—that we can effectively choose a suitable absurdity for any given theory we are likely to care about. For example in arithmetic we may choose 0 = 1, in the theory of strict linear orders 0 < 0, and so on.
Negation . . . is highly problematic. In mathematics, given the meaning of "if . . . then", it is trivial to explain "Not A" as meaning "If A, then 0 = 1"; by contrast, a satisfactory explanation of "not", as applied to empirical statements for which bivalence is not, in general, taken as holding, is very difficult to arrive at. Given that the sentential operators cannot be thought of as explained by means of the two-valued truth-tables, the possibility that the laws of classical logic will fail is evidently open: but it is far from evident that the correct logical laws will always be the intuitionistic ones. More generally, it is by no means easy to determine what should serve as the analogue, for empirical statements, of the notion of proof as it figures in intuitionist semantics for mathematical statements. (Dummett 1996, p.473)
A blanket term for the analogue of proof for empirical statements is warrant or verification. One need not spell out a precise theory of warrant in formulating a semantics whose primary semantic values are warrants. Indeed, there has been no precise spelling out of proof for the constructivist, since proof for them is taken as intuitive and not relative to a given formal theory. Of course this has not prevented the formulation of numerous semantics for constructive logics.2 A similar point is made by Kleene regarding the realizability interpretation of intuitionistic number theory when he states "[t]he analysis which leads to this truth definition is not to be regarded as more than a partial analysis of the intuitionistic meaning of the statements, since it takes over without analysis, or leaves unanalyzed, the component of evidence" (Kleene 1945, p. 110).
In what follows I shall be taking the notion of warrant or verification as primitive and assuming, moreover, that a naїve extension of a constructively acceptable semantics to empirical discourse is one which replaces proofs as semantic values with warrants (perhaps with other necessary modifications made as well).3 , 4 The verification of a statement A might be taken to be the holding in principle of sufficient empirical evidence in support of A, where what counts as evidence is either contextually determined or domain specific. For instance, seemings to John might count as evidence for 'John is hungry' whereas they may not, e.g. because John has a fever, for 'The temperature is above twenty degrees celcius'. In other words, a number of factors may serve to determine what counts as evidence for a given class of propositions. In the case of mathematics, proof then turns out to be a species of warrant.5
It is easy to see why the usual notion of constructive negation does not by itself suffice for expressing negation in empirical discourse. Suppose we wish to express that Goldbach's conjecture is undecided at present. According to the arrow-falsum definition, this statement is equivalent to 'If Goldbach's conjecture is decided (i.e. proved or refuted) at present, then 0 = 1'. But this is far too strong: it states that, with respect to any evidential state we may be in, that Goldbach's conjecture is decided is refutable.6 However, while it is vacuously true with respect to our present evidential state that a proof of Goldbach's conjecture—which we do not presently have—can be transformed into a proof of 0 = 1, this may not be true with respect to future evidential states at which the conjecture may turn out proved or refuted. To express such claims the constructivist needs a weak negation that, when appended to a statement, expresses that the statement lacks warrant at this evidential state, the state at present. Such a negation has been referred to as 'empirical' in (Williamson 1994)) and (DeVidi and Solomon 2006) and as 'factual' antecedently in (Heyting 1971, p. 18).
It follows that any negation stronger than intuitionistic negation will be too strong to express that a particular evidential state (e.g. the present one) fails to support a given statement. For if the negation is stronger than intuitionistic negation it will express at least that the statement fails to be supported in every extension of the given state. In particular then, strong negation cannot serve as an empirical negation in our intended sense, but not for the reasons Williamson (Williamson 1994) cites. In (Williamson 1994) Williamson suggests, but ultimately rejects, the use of any non-standard intuitionistic negation, and in particular strong negation, as an empirical negation. I discuss his argument in §7.
[w]e might regard the meanings of negations of numerical equations as being given directly in terms of the computation procedures by which those equations are verified or falsified: a proof of the negation of any arbitrary statement then consists of an effective method for transforming any proof of that statement into a proof of some false numerical equation. Such an explanation relies on the underlying presumption that, given a proof of a false numerical equation, we can construct a proof of any statement whatsoever. It is not obvious that, when we extend these conceptions to empirical statements, there exists any class of decidable atomic statements for which a similar presumption holds good; and it is therefore not obvious that we have, for the general case, any similar uniform way of explaining negation for arbitrary statements. It would therefore remain well within the spirit of a theory of meaning of this type that we should regard the meaning of each statement as being given by the simultaneous provision of a means for recognizing a verification of it and a means for recognizing a falsification of it, where the only general requirement is that these should be specified in such a way as to make it impossible for any statement to be both verified and falsified. (Dummett 1996, pp. 71-72)
A semantics which treats verification and falsification symmetrically along the lines just sketched by Dummett has been proposed by Thomason (Thomason 1969) for the strong negation of (Nelson 1949). Similarly, Gurevich (Gurevich 1977) motivates his semantics for strong negation by observing that "[i]n many cases the falsehood of a simple scientific sentence can be ascertained as directly (or indirectly) as its truth. An example: a litmus-paper is used to verify sentence [sic] "The solution is acid" " ((Gurevich 1977, p. 49)) by which he means 'verify the falsity of' when he says 'verify'. In the context of constructivism we see that symmetrical treatments of truth and falsity have been around for quite some time.
Our reluctance to say that pi was not transcendental before 1882, or, more generally, to construe mathematical statements as significantly tensed, is not merely a lingering effect of platonistic misconceptions; it is, rather, to speak in this way would be to admit into mathematical statements a non-intuitionistic form of negation, as will be apparent if one attempts to assign a truth-value to 'pi is not algebraic', considered as a statement made in 1881. This is not because the 'not' which occurs in '. . . is not true' or '. . . was not true' is non-constructive: we may reasonably view it as decidable whether or not a statement has been proved at a given time. But though constructive, this is an empirical type of negation that occurs in statements of intuitionistic mathematics. (Dummett 1977, p. 337, my emphasis)
If it is decidable whether or not a given statement A lacks warrant at present (or any given time more generally), it will always be true, for example, that 'either A is (now) warranted or it is not'.
Empirical negation cannot simply be classical negation if we wish to add it in a straightforward way to the usual proof systems for intuitionistic logic. For there is no straightforward way of introducing classical negation to intuitionistic logic without the two negations collapsing into classical negation.7 So on pain of collapse, empirical negation must forgo certain classical principles. The same issue arises within the setting of classical relevant logic (see (Meyer and Routley 1973) and (Meyer and Routley 1974)), where the familiar law of contraposition in "arrow-form" fails (though it holds in rule form) for "classical" negation, again, on pain of collapse. Precisely which principles our account of empirical negation forgoes is discussed in Section 4.
However, besides collapse, there is a host of other objections against classical and classical-like negations that any proposal for a constructively or relevantly acceptable negation will have to avoid. In the next section I look at these objections in turn and argue that none of them are a problem for the empirical negation to be introduced in Section 3, despite its close affinity to classical negation. Indeed the following section could serve double duty as a survey of the numerous objections to classical-like negations.
2 Constructivist Objections to Classical (and like) Negations
2.1 Conservativity
If L and L′ are logics in the respective languages L and L ′ with L ⊆ L ′,then L′ is a conservative extension of L when for every sentence A in L, if A is L′-provable then it is L-provable. Conservativity has been thought to be a necessary condition on meaning coherence in the sense that the rules governing a connective can only confer coherent meaning on that connective if they conservatively extend a given coherent base.8 There are a number of reasons for desiring conservativity having to do primarily with anti-holism, learnability, anti-realism and consistency (against e.g. tonk-like connectives), but whichever reasons one has in mind, classical negation is going to be problematic since the usual ways of proof-theoretically extending deductive systems for intuitionistic logic to include classical negation yield nonconservative extensions. A famous example witnessing this nonconservativity phenomenon (assuming that the meaning of → is determined by the usual arrow introduction and elimination rules) is famously Peirce's law, ((A → B) → A) → A, which is classically but not intuitionistically provable. As such, classical negation has been deemed incoherent, most notably by Dummett.
We need not enter the debate about whether conservativity is a necessary condition for coherence, since one can remain neutral on the issue in cases where a given connective meets the constraint. The empirical negation introduced in Section 3 yields a conservative extension to intuitionistic logic, and so failure of conservativity is no objection to it.
2.2 Harmony
Inferentialists, who hold that the meaning of certain expressions is determined completely by the rules which govern them, have been the initial defenders of conservativity. In the case of the logical connectives they hold that the introduction and elimination rules (sometimes just those of one type and not of the other) completely determine the meaning of a logical connective.9 But if conservativity fails as a requirement for coherence, the inferentialist will need to appeal to some other requirement to rule out classical negation as incoherent. Harmony has been thought to fill this role. Roughly, harmony is the constraint that introduction and elimination rules for a logical connective must be in harmony in the sense that the elimination rules warrant precisely what is warranted from the premises of the introduction rules alone.10 Some inferentialists have defended harmony while rejecting conservativity (e.g. see (Read 2000)). Inferentialism is typically restricted to the view that the meaning of the logical fragment of our vocabulary is given completely by inferential rules. This is sometimes referred to as moderate inferentialism. One might wish to extend inferentialism to language as a whole, but it is unlikely that an advocate of any such program would endorse harmony as a meaning-theoretic constraint since it is far too constraining.
Should we require of empirical negation that it be governed by harmonious introduction-elimination rules? If empirical negation is non-logical and we are moderate inferentialists, then the answer is clearly "No". On the other hand, if empirical negation is deemed logical on grounds of topic neutrality, then the familiar intuitionistic negation cannot be deemed logical on the same grounds and this seems implausible. For recall that empirical negation is an operation on warrants of which proofs are a special case, so in this sense it generalizes intuitionistic negation by applying to a broader class of propositions, the mathematical and empirical. Now it is unlikely that any inferentialist will accept this brief argument denying the logicality of intuitionistic negation on grounds of topic neutrality, in which case they must hold that, while topic neutrality may be a sufficient condition on logicality, it cannot be a necessary one. According to an inferentialist, being characterizable by rules satisfying certain proof-theoretic constraints (e.g. harmony, conservativity, etc.) will be necessary and sufficient for logicality. But whatever conditions end up being necessary and sufficient for logicality, it is dubious that empirical negation will turn out logical on those grounds. Thus the issue of harmony seems irrelevant to empirical negation.11
This is not to say empirical negation fails to satisfy proof-theoretic constraints necessary and sufficient for logicality. Indeed one might hold that the burden of proof lies on the opponent to show that empirical negation cannot be given harmonious rules, which is an extremely strong claim to establish. But it is also debatable whether the rules given in Section 5 for empirical negation are not harmonious. Read (Read 2008) argues that labeled natural deduction systems for a variety of normal modal logics provide a way of furnishing harmonious rules for intensional connectives, and if he is right then empirical negation, and a good deal of other connectives including non-logical ones, satisfy the harmony constraint.12
So far the objections to classical and like negations have been proof theoretic, but there is a long history of model-theoretic objections as well. A number of them have been voiced by relevantists in defending non-classical (paraconsistent) De Morgan negation as an alternative to classical negation. Exactly these objections are open also to the intuitionist. In the following section I will discuss these objections in their original relevantist formulations and show how they connect directly to the present topic of empirical negation.
2.3 Heredity
The formal semantics of relevant logic has taken a fair amount of criticism from its inception for not having an adequate informal interpretation and the collapse of the ordering that allows for boolean negation worsens that criticism.15 For the ordering is supposed to represent an intuitive notion corresponding to something like information gathering, so that a ≤ b when b is an informational extension of a. The restriction requiring that a ≤ b iff a = b claims that states have no proper extensions and embodies the unfounded Leibnizian optimism that each state is itself the best (in terms of informational content) amongst all possible ones.
The point is that states are not perfect—i.e. complete and consistent. Moreover propositions, construed as sets of states, are not just any such sets: they are the hereditary ones. Now it is clear that boolean negation defined according to (1) is not an operation on propositions in the sense that the class of propositions is closed under that operation. For there are states a and b with a ≤ b such that a does not support a proposition A, and hence supports its boolean negation, while b supports A. But then the boolean negation of A is not preserved ≤ -upward, and so the boolean negation of A is not a hereditary set (read 'proposition'). As boolean negation is just set-theoretic complementation in disguise, another way of putting this is to say that complementation is not an operation on propositions.
Notice that the same objection may be levelled against classical negation by any intuitionist who takes seriously a semantics on which boolean negation fails to be an operation on propositions intuitionistically conceived. In Kripke semantics for intuitionistic logic (see Section 3), propositions, being ≤ -closed (for ≤ a preorder), are not closed under boolean negation. That is, in a Kripke model M for intuitionistic logic we may have M, a ⊨ ∼A and yet M, b ⊭ ~A (equivalently, M, b ⊨ A) for some b ≥ a. Now the intuitionist might attempt the same move as the relevantist by collapsing the preorder to identity (obtaining the class of "sheer reflexive" frames) so that Heredity is preserved in the presence of boolean negation, but that will not work since the resulting logic is classical (i.e. the set of arguments valid on the class of sheer reflexive frames is classical logic). So the relevantist move is unavailable to the intuitionist who must instead reject boolean negation as a genuine propositional operation.
It is easy to see that Heredity holds for the language extended with ∼, that is, ∼ is a genuine propositional operation.
There are two serious problems with this "negation". The first is that it is too weak. Almost no properties thought characteristic of negation hold for it. In particular, the law of excluded middle, a property we should think holds for empirical negation if we follow Dummett's remark quoted earlier, fails as does the law of non-contradiction and various directions of the De Morgan equivalences (e.g. ∼(A ∧ B) |= ∼A ∨ ∼ B). Second, it does not get things right at the level of models for there will be states supporting ∼A for every A, i.e. states at which trivialism holds, a thesis rejected by any constructivist. This will be the case, e.g., when no later state is actualized in which case the truth conditions for ∼A will be vacuously satisfied for arbitrary A.
For these reasons the empirical negation to be defined in Section 3 is better motivated from a philosophical point of view and it also fairs much better in terms of getting correct the inferences that ought to intuitively hold of empirical negation.
2.4 Implicit vs Explicit Information
Relevantists (e.g. Greg Restall) have argued that there is a "difference between claims about states, and claims supported by states" (Restall 1999, p. 71). A state a's failing to support a proposition A should not imply that a supports some other proposition ⇁A expressing a's lack of support for A—for this other proposition is about a. That is, it should not be assumed generally that a state supports all the information about itself. An intuitionist who even only weakly endorses Kripke semantics could file the same charge against empirical negation if introducing it into the semantics requires making the unjustified identification of implicit and explicit information.
Of course some states might support all the information about themselves, but to say that all do is to make an unfair assumption about states. It would, however, be just as unfair to assume that states never support some or all of the information about themselves. Moreover, why not think that every model ought to possess at least one such state intended to represent a privileged state of the model, for example, the present state of available evidence (or warrant)? Such states will be complete in the sense that every statement will be either warranted or not.
Given Dummett's remark claims of the form 'A is warranted' are in principle decidable, we should think that the present state of available evidence either warrants or fails to warrant the assertion of a given proposition. That is, the present state of available evidence is complete relative to empirical negation ∼ in the sense that A ∨ ∼A holds good at it. In modeling empirical negation, then, we should include at least one state representing the present state of available evidence for any claim of the form ∼A asserts that, at present, A lacks sufficient evidence to be warranted. Such a state will form a classical model in the sense that the set of sentences in the language involving only the connectives ∧ and ∼ will be maximally classically-consistent.
3 The Semantics of Fixed Negation
Since we will be interpreting a connective ∼ to be read 'There is insufficient evidence at present16 to warrant the proposition that. . . ' (¬ will continue to be read 'It is refutable that. . . ') we must distinguish one state in each model as the present moment. Such a state will be further singled out by the truth conditions given to our empirical negation ∼. These informal ideas motivate the semantical clauses for the connectives of our language, to be specified in a moment, the only novel one being that for ∼ .
Our language L ∼ is a usual language L for IPC (Intuitionistic Propositional Logic) augmented with the logical symbol ∼ .17 Let F = (W, ≤) be a Kripke frame for the language L of IPC. That is, W is a non-empty set of states and ≤ is a partial order (reflexive, transitive and anti-symmetric relation) on W . We denote by W ↑ the set of all upsets in W , i.e. sets X s.t. y ∈ X whenever x ∈ X and x ≤ y. An L ∼-model M is a tuple (F,@,V) where @ ∈ W is a distinguished element representing the state of available evidence in M (other modally inequivalent states representing substates or states containing evidence unavailable in M ) and V : Prop → W ↑ is a propositional valuation assigning propositions (i.e. upsets in W ) to propositional letters.18
- 2.
\( M,a| = A \wedge B{\text{ \; iff \; }}M,a\left| { = A{\text{ \; and \; }}M,a\,} \right| = B; \)
- 3.
\( M,a| = A \vee B{\text{ \; iff \; }}M,a\left| { = A \;{\text{or \;}}M,a\,} \right| = B; \)
- 4.
\( M,\,a\, \ne \, \bot \,{\text{(i}}{\text{.e}} \;{\text{it \; is}}\,{\text{never \; the \; case \; that \; }}M,\,a\,| = \bot ); \)
- 5.
\( M,a| = A \to B{\text{ \; iff}}\;\forall \; b \geqslant a\,(M,b| = A \Rightarrow M,b| = B); \)
- 6.
\( M,\,a\,| = \sim A \;{\text{iff}} \;M,\,@\, \ne \,A. \)
Truth in a model is truth at @, validity on a frame is truth in every model based on that frame, and validity "simpliciter" is validity on every frame. We say that a sentence A is an L ∼-consequence of set Γ of sentences, in symbols Γ |=A, iff for every model M , A is true in M whenever every member of Γ is true in M . We denote the set of valid consequences {(Γ, A) : Γ |=A} by IPC ∼.
We might have required that all models be rooted, i.e. that there be a minimum with respect to the partial order, or, perhaps more in line with common informal interpretations of intuitionistic models, that the models be tree-like. In any case, one obtains the same semantic consequence relation so we have chosen not to restrict our models in any of these two ways. It is interesting to note, however, that there are differences immaterial to consequence: e.g. if @ is always the root then A ∨∼A holds at every point of every model, whereas this is not true otherwise.
There are two notions of truth in a model we may distinguish: (i) actual truth which is truth at the distinguished element, and (ii) global truth which is truth common to all points in the model. A sentence is actually true in M = (W, ≤, @, V) when it is true at @, and a sentence is globally true in M when it is true at every state a ∈ W of M . These notions of truth are obviously quite distinct. We may also distinguish between two types of consequence: local and actual consequence. A sentence A is a local consequence of a set Γ of sentences when for each model M = (W, ≤ , @, V ) and every b in M , if every member of Γ is true at b then so is A. And A is an actual consequence of Γ when A is true at @ whenever every member of Γ is. For the base intuitionistic language L, the distinction between actual and local truth is one without a difference.20 However, this is not true for L~ since now the distinguished element plays a significant role, where before it did not.
[i]f a sign is to be regarded a negation of p at all, it must be used in such a way as to be incompatible with the assertion that p. The semantic rule has to hold, which Dummett calls Exclusion, that p and its negation cannot both be true. (Hossack 1990, p. 216).
One possible objection to the semantics for negation introduced here is that we have states at which both A and ∼A are supported in apparent violation of Dummett's Exclusion condition. For instance let M = (W, ≤, V ) be the two element model with W = {@, a}, ≤ the reflexive closure of {〈@, a〉} and V (p) = {a}. Then M, a |=A ∧ ∼A. But what is crucial here is that it is never the case, in accordance with Exclusion, that both A and ∼A are true, for truth (relative to an IPC ∼-model) is truth at @. Notice that the empirical negation of (DeVidi and Solomon 2006) fails to satisfy the Exclusion condition and so would not be deemed a negation according to Hossack and Dummett.
…non-monotonicity naturally suggests itself as a logical characteristic definitive of [defeasible warrant]. At least, it is difficult to see how warrant could genuinely be defeasible if it is not the case that further information could be obtained to defeat an assertion so warranted. To allow that defeating information can turn up however is precisely to allow the possibility that while X defeasibly warrants Z, the conjunction of X and Y might warrant the negation of Z. . . there is no obvious way of capturing the non-monotonic character of defeasible warrant within the framework provided by Kripke semantics for intuitionist logic. (Tomassi 2006, p.37-38)
While I agree that defeasible warrant introduces an element of non-monotonicity, I do not think it manifests at the level of logical consequence. Defeasible warrant is non-monotonic over the progression of time relative to some partial ordering on states of evidence. That is, if a and b are states of evidence such that a ≤ b, where ≤ is some monotonic ordering of strength of evidence, and A is warranted at a, then A is warranted at b. What we do not have is that if A is warranted at some time t and t < u then A is warranted at u. One has to distinguish between the orderings over which empirical truth is preserved. A statement A is warranted, in our sense, at a particular time t if and only if all the available evidence at t warrants A; i.e. statements are warranted relative to bodies of evidence. We should not want statements to be warranted relative to sets of statements, as they would be if reasoning with a defeasible warrant operator were non-monotonic. If we know that A, ⊢ B but A, C ⊢ B, and both A and C are warranted, then B is not warranted relative to {A}—it is simply not warranted. Ideally one should distinguish in the model two separate orderings, one ≤ over evidence and another ≼ over temporal states, and introduce a future or past temporal operator □ into the language governed by ≼ such that A may hold according to some body of evidence at a moment t even though □ A may not hold according to that same body of evidence and moment because A fails at the relevant ≼ -successors of t.
4 Validities and Invalidities
Nearly all of the rule-forms of contraposition fail as well, a feature familiar to relevant logicians who have observed these sorts of failures for boolean negation in the setting of classical relevant logic.
It is worth noting that IPC ~ is not closed under substitution of provable equivalents, though it is obviously closed under uniform substitution. A logic is closed under substitution of provable equivalents when Γ ⊢ A, B ⊢ C and C ⊢ B imply Γ ⊢ A(B/C), where A(B/C) is the result of replacing some occurrences of B in A with occurrences of C. A logic is closed under uniform substitution when Γ ⊢ A implies Γ ⊢ A(p/q) for p, q atoms. For example p∧ ∼ p ⊢ p∧¬p and p∧¬p ⊢ p∧ ∼ p, but ⊢ (p∧¬p) → ⊥ while ⊢ (p∧ ∼ p) → ⊥. This is not a particularly uncommon phenomenon. For example, compare logics with "actually" operators21, temporal logics with "now" operators, and paraconsistent logics with non-truth-functional negations such as those of de Costa 1974, each of which fails to be closed under substitution of provable equivalents.
More importantly, A |= B is weaker than |=A → B since the latter implies the former but not conversely—in other words, conditional proof fails. This explains, e.g., the → -form failure of EFQ; → may take us to states at which both A and ∼A hold, and hence states where an arbitrary A (e.g. ⊥) need not (or in the case of the example, must not) hold. Often it is the implication from | = A → B to A |= B that fails. For instance, this is the case with Tennant's relevant logics CR and IR (see (Tennant 1997)). In particular, |=(A ∧ ¬A)→B holds but A, ¬A |≠ B which is quite the opposite from IPC ∼.
It appears the rules for → are no longer in harmony since the usual form of → -elimination (in sequent form, A → B, A ⊢ B) holds while → - introduction in its usual form (from Γ, A ⊢ B infer Γ ⊢ A → B) fails.22 But → -introduction is supposed to be (and is on proposed ways of making rigorous harmony) the unique rule harmonious with → -elimination. There are two things to say here. First, the elimination rule for → in the proof system for IPC ∼ of Section 5 is not the usual → -elimination rule and, moreover, it is harmonious with the introduction rule given in Section 5 in the sense of (Read 2008). There may be other worries concerning the proof system—in particular, whether its use of labels can be justified on inferentialist grounds—that is independent of issues regarding harmony. I must ignore these issues here. Second, it is essential to the failure of → -introduction that there be occurrences of ∼ which means that the usual harmonious rules can be given to → for the → -fragment of IPC ∼, whatever consolation that may count as. This is not always the case, e.g. with non-conservative extensions which introduce theorems no longer provable by the original harmonious rules of the base language.
4.1 Remarks
Given the failure of conditional proof, IPC ∼ is not an axiomatic extension of any finite axiomatization of IPC in the sense that the former is obtainable from the latter by the addition of axioms. For any axiomatic extension of a finitely axiomatized system satisfying conditional proof, i.e. the deduction theorem in the context of axiomatic systems, satisfies conditional proof. However, IPC ∼ is a conservative extension of IPC. This is easy to see semantically, a self-evidence not usually exuded on the proof-theoretic side. For if A does not contain ∼ then it receives the truth conditions it has in IPC-models and so if it were IPC ∼-valid then it would have already been IPC-valid. As a final remark we note that IPC ∼ is Tarskian in that it satisfies the structural rules of Reflexivity, Thinning and Cut.
Digression: It should not be surprising that the disjunction property, if Γ ⊢ A ∨ B then Γ ⊢ A or Γ ⊢ B, fails for IPC ∼. This sort of failure is notorious for extensions of IPC. (So notorious in fact that it was conjectured by Lukasiewicz that IPC is the strongest intermediate logic to have the disjunction property.23 Kreisel and Putnam proved this conjecture false by showing that the system obtained by adding (¬A → (B ∨ C)) → ((¬A → B) ∨ (¬A → C)) to IPC has the disjunction property.) However, given our intended interpretation of the language it is not hard to justify the failure of conditional proof and the disjunction property. The justification for the failure of the latter rests on the assumption that it is decidable whether or not a proposition is supported by the evidence available at present in which case we expect ⊢ A ∨ ∼A for arbitrary A without either of ⊢ A or ⊢ ∼A holding. So we focus our attention on the failure of conditional proof. End of digression.
There are two things to say about the failure of conditional proof. The first is that if we are to take seriously Kripke semantics for intuitionistic logic and if adding empirical negation is semantically acceptable then there is reason to reject conditional proof. After all, it falls out of an acceptable semantics for the language. Now most intuitionists do not find Kripke semantics acceptable primarily on the grounds that it is usually couched within a classical metatheory. But at the propositional level, this should not matter since IPC and its extension IPC ∼ to fixed negation are complete with respect to a recursive set of finitely recursive models (i.e. models with a finite set of states and a recursive accessibility relation and valuation defined on that set). Indeed, if Γ ⊬ IPC A then, via a filtration technique, one can construct a finite countermodel from the set of subformulae of Γ ∪ {A} (assuming Γ is finite). Restricting the class of models so, the metatheory being classical or intuitionistic then come to the same thing.
While this fact does not generalize to quantificational theories, one may still furnish such theories with a constructive metatheory employing Kripke models even though certain results classically provable will not be provable in the constructive metatheory. This will not be problematic for a constructivist who finds something appealing with an informal interpretation of Kripke structures for intuitionistic logic and who wishes to make use of those structures in providing a semantics for her constructive language while sticking to a constructively acceptable metatheory. I shall therefore suppose that there are constructively acceptable versions of Kripke semantics for intuitionistic logic.
Despite the failure of conditional proof for →, we may introduce other implication connectives satisfying conditional proof. One natural way to do this is to define A as being a consequence from Γ, where Γ is finite, just when |=⋀Γ → A. (Alternatively we could allow infinite sets of premises and infinitary conjunction, but this is unnecessary given compactness for IPC ∼.) Under this definition of consequence, consequence and implication coincide but the definition looks ad hoc. Moreover we lose important theorems that were motivated by our original concerns. For example EFQ for ∼ fails (since now ⊥ would not be a consequence of A ∧ ∼A) as do a number of other important consequences involving the conditional that were valid under the original definition. So the revised definition of consequence does not speak well to the informal interpretation we had originally given to the language.
A more interesting conditional that satisfies conditional proof exploits the fact that (the theory of) @ is essentially a classical model with an additional intensional connective →. Notice that all the classical connectives are definable at @ in a straightforward way, e.g. A ⊃ B := ∼A → ∼∼ B (or equivalently ∼A ∨ ∼∼B) says that at an arbitrary point, either A fails to be @. Then Γ ⊢ A (under the original definition of ⊢) iff ⊢ ⋀Γ ⊃ A for finite Γ. One with a strong liking for conditional proof might then think of material implication as the correct notion of implication for empirical discourse.
5 Tableaux
Several complications present themselves on the side of proof theory. The first, which we have already encountered, is that conditional proof fails. This means that in the setting of natural deduction, a → -introduction rule would, in our case, turn out quite cumbersome. (This of course is not true for any system for which conditional proof fails.) The second, more troubling, difficulty is that since A, ∼A |= ⊥ which, in a natural deduction setting, we might call ∼ E, and ¬A |= ∼A, it follows that any of the usual presentations of natural deduction would generate a consequence relation satisfying both ¬A ⊢ ∼A and ∼A ⊢ ¬A (the latter following by ∼ E and ¬I) which is clearly bad (in respect of the latter); for ∼ is supposed to be strictly weaker than ¬. Exactly the same problem emerges when adding classical negation to intuitionistic logic in the usual systems of natural deduction.
For this reason we have chosen to give a signed and labelled tableau system for IPC ∼. The system is standard for IPC for this style of tableau system and adds two additional rules for sentences of the form S ∼A where S is a sign in {T, F} representing the truth or falsity of a sentence at a state (e.g. 'TA ∧ B, i' expresses that A ∧ B is true at state i). For tableaux there are two types of sentences.
Definition 5.1
A signed labelled sentence has the form SA,i for S ∈ {T,F}, A an IPC ∼-sentence and i ∈ {@} ∪ \( {\text{N}} = Labels \) (the set of labels).
A relational sentence has the form i ≤ j for i, j ∈ Labels.
A tableau for an argument A 1, . . . A n ⇒ B, with A i the premises and B the conclusion, starts by listing the TA i, @ in their natural order proceeded by FB, @. More precisely we have the following definition of a tableau.
Definition 5.2 (Tableaux)
A tableau \( \mathcal{T} = \left( {X, \leqslant } \right) \) is a partially ordered, finite set of sentences (labelled or relational) with a minimum (root) such that for each α ∈ \( \mathcal{T} \) the set of predecessors of α under ≤ forms a linear order. If ≤ is a partial order on a set X then α is a minimum in X w.r.t. ≤ iff for all β ∈ X, α ≤ β.
A branch of a tableau \( \mathcal{T} \) is a maximal chain in \( \mathcal{T} \).
Definition 5.3 (Closure)
A branch closes iff there is an i ∈ Labels and sentence A such that both TA, i and FA, i occur on the branch.
A tableau closes iff each of its branches closes.
A branch (tree) is open if it is not closed.
A closed tableau for an argument is a proof of that argument. An argument A 1, . . . A n ⇒ B is provable when there exists a closed tableau for it, in which case we write A 1, . . . A n ⊢ IPC ∼ B, sometimes suppressing the subscript when it is clear.
The parenthetical '(new j)' indicates that the label j must be new to the branch; i.e. it must not occur as the label of any formula on the branch besides those introduced by the rule. In the second to last rule of the second row, governing the transitivity of r, jrk does not need to immediately follow irj on the branch. All that is required is that each occur on the branch.The same may be said about the conclusions of the other rules, though it need not be. For definiteness we understand the other rules to be read in the same light.
6 Completeness
The proof of completeness for the tableau system is given according to the usual recipe. We confine ourselves to systematic tableaux, which means that the rules are to be taken as "musts" rather than "cans": if a rule can be applied, it must be applied. A systematic tableau is one in which every branch β is downward saturated (defined below). The goal then is to show that every open branch of a systematic tableau forms a Hintikka set (defined below), and that every Hintikka set is satisfiable. Completeness then follows almost immediately.
Definition 6.1
- 7.
If TA ∧ B, i occurs on β then TA, i and TB, i occur on β.
- 8.
If TA ∨ B, i occurs on β then either TA, i occurs on β or TB, i occurs on β.
- 9.
If T¬A, i and irj occurs on β then FA, j occurs on β.
- 10.
If TA → B, i and irj occurs on β then either FA, j occurs on β or TA, j occurs on β.
- 11.
If T ∼A, i occurs on β then FA, @ occurs on β.
- 12.
If FA ∧ B, i occurs on β then either FA, i occurs on β or FB, i occurs on β.
- 13.
If FA ∨ B, i occurs on β then both FA, i and FB, i occur on β.
- 14.
If F¬A, i occurs on β then for some j, irj and TA, j occur on β.
- 15.
If FA → B, i occurs on β then for some j, irj, TA, j and FB, j occur on β.
- 16.
If F ∼A, i occurs on β then TA, @ occurs on β.
- 17.
For all i occurring on β, iri occurs on β.
- 18.
If irj and jrk occur on β then irk occurs on β.
Definition 6.2
A set H of formulas is a Hintikka set if it satisfies the conditions of Definition 6.1 by replacing 'occurs on' by 'is a member of' and 'β' by 'H', and the further condition that for no propositional letter p and i ∈ Labels are both Tp, i and Fp , i in H.
Lemma 6.3.
Every open branch β forms a Hintikka set. i.e. the set of formulas consisting of the nodes of β is a Hintikka set.
Immediate by Definitions 5.2 and 6.2.
Lemma 6.4
W = label(H)
I ≤ j iff irj ∈ H
@ = @
V(p) = {i ∈ W :Tp,i ∈ H}.
We do two things. The first is to verify that M H is indeed a model. The second is to show that the Fundamental Lemma 6.5 holds.
We claim that ≤ is a partial order. Clearly for all i ∈ W , i ≤ i by definition and the fact that for each i ∈ label (H), iri ∈ H by the "reflexivity" rule. Transitivity follows similarly by the definition of ≤ and the fact that irj, jrk ∈ H only if irk ∈ H by the "transitivity" rule and downward saturation. Anti-symmetry is vacuously satisfied since the rules never allow that irj, jri ∈ H for i ≠ j.
To finish verifying that the structure defined above is an IPC ∼-model we have only left to show that for no i ∈ W and A ∈ L ∼ do we have i ∈ V (A) and \( i \in \overline {V(A)} \),where \( \overline X \) is the W-complement of X. As the result follows trivially by the definition of V (as the reader may wish to verify), our verification that M H is a model is concluded.
All that is left is proof of the following "Fundamental Lemma".
Lemma 6.5
(Fundamental Lemma). If TA, i ∈ H then M H , i | = A, and if FA, i ∈ H then M H , i |≠ A.
We proceed by induction on formula complexity.
Base A is an atomic letter p or ⊥. The case for ⊥ is trivial, so suppose Tp, i ∈ H. Then i ∈ V (p), so M H , i |= p.
Now suppose Fp, i ∈ H. Then \( i \notin \,V\,(p) \) , so M H ,i |≠ p.
- Case 1
A is B ∧ C. Suppose TB ∧ C, i ∈ H. Then (TB, i), (TC, i) ∈ H, so By IH M H , i |= B and M H , i |=C. Hence M H , i |=B ∧ C.
Now suppose FB ∧ C, i ∈ H. Then either FB, i ∈ H or FC, i ∈ H. By IH either M H , i ≠ B or M H , i ≠ C whence MH , i |≠ B ∨ C
- Case 2
A is B ∨ C. Suppose TB ∨ C, i ∈ H. Then either TB, i ∈ H or TC, i ∈ H. By IH either M H , i |=B or M H , i |=C, whence M H ,i|=B ∨ C
Now suppose FB ∨ C, i ∈ H. Then both FB, i, C, i ∈ H. By IH M H , i ≠ B and M H , i ≠ B , whence M H , i ≠ B ∨ C
- Case 3
A is ¬B. Suppose T¬B, i ∈ H. Then for all j s.t. irj ∈ H and FB, j ∈ H. By IH, for all j s.t. i ≤ j, M H , j |= B. Hence M H ,i|=¬B.
Now suppose F¬B, i ∈ H. Then there is a j s.t. irj ∈ H and TB, j ∈ H. Then i ≤ j and by IH M H ,j |=B. Hence M H , i|≠¬B.
- Case 4
A is B → C. Suppose TB → C, i ∈ H. Then for each j s.t. irj ∈ H, either FB, j ∈ H or TC, j ∈ H. By IH either M H , j |= B or M H ,j |=C for each j ≥ i. Hence M H , i |= B → C.
Now suppose FB → C, i ∈ H. Then there is a j s.t. irj ∈ H, TB, j ∈ H and FC, j ∈ H. Thus i ≤ j and by IH M H , j |=B and M H , j ≠ C. Hence M H , i ≠ B → C.
- Case 5
A is ∼ B. Suppose T ∼ B, i ∈ H. Then FB, @ ∈ H, whence by IH MH,@≠B, so M H , i |=∼B.
Now suppose F ∼ B, i ∈ H. Then TB, @ ∈ H, whence by IH M H , @ |=B, so MH, i ≠ ~ B.
Theorem 6.6
(Completeness). If Γ ⊢ B then Γ |=B. (Recall that Γ |=B means that for every model M , if M |= Γ then M |= B.)
Suppose Γ ⊬ B. Then there is a systematic tableau T with open branch β s.t. for each γ ∈ Γ, Tγ, @ occurs on β and FB, @ occurs on β. Let H be the Hintikka set whose elements are the nodes of β. Then by the fundamental lemma, there is an IPC ∼-model M H s.t. M H , @ |=Γ and M H ,@ ≠ B, thus Γ ≠ B. Contraposing, if Γ|=B then Γ⊢B.
7 Final Remarks
We have considered an operation ∼ such that the truth of ∼A at an arbitrary point of evaluation is determined completely by the truth of A at a distinguished point representing all evidence available at present. When consequence is defined as preservation of truth in a pointed model, ∼ looks nearly classical. Moreover, it seems plausible that any semantics defined with respect to a class of models which distinguishes a point according to which truth in that model amounts to truth at that point, solicits the characterization of a family of connectives defined in terms of the distinguished point.
If verificationism is a theory about ordinary discourse, then any intuitively coherent connective used in such discourse ought to admit of a constructively acceptable semantics where expressive adequacy is a concern. A theory T is expressively adequate with respect to a connective ♣ picked out by natural language expressions if there is a connective ⊗ in the language of T which corresponds, in an intuitive sense given the ⊢ T -rules governing ⊗, to ♣. For instance, IPC is expressively adequate with respect to conjunction to which ∧ corresponds. IPC is clearly not expressively adequate with respect to weak and empirical negations, just as certain theories of truth (of e.g. Kripke) are not expressively adequate with respect to "exclusion negation" (as opposed to "choice negation"), the operation which takes an intermediate truth value to truth in a three-valued semantics such as Kleene's.
- 1.
A∧¬KA supposition
- 2.
K(A ∧ ¬KA) 1 BHK interpretation
- 3.
KA∧K¬KA 2 distribution
- 4.
KA∧¬KA 3 axiom T
- 5.
- 6.
¬KA → ¬A 5 intuitionistic propositional logic
If in line (1) we replace ¬ with ∼ we can obtain everything up to the penultimate line (even with intuitionistic negation out front), but we can not obtain the conclusion, line (6).24
Williamson rejects any solution to this paradox that uses a "non-standard negation" ⇁ on the grounds that (i) it must satisfy ⇁A → ¬A, and (ii) K⇁A but not K¬A will have to be treated as sufficient for a negative solution to 'A will one day be decided'. First, his argument for (i) relies on the use of principles that are questionable on the addition of an empirical negation and K to the language. One of these is ¬(A ∧ ⇁A) that he thinks should hold but which does not in IPC ∼. His reason for thinking so is that "[⇁A] should at least be inconsistent with A" (Williamson 1994, 139).
They are inconsistent in IPC ∼ (when ⇁ is ∼) but that need not imply the validity of ¬(A ∧ ⇁A) and when the intended discourse is empirical, I see little reason to think it should. Another questionable inference is closure under provable implications, in the form A ⊢ B rather than ⊢ A → B, which he makes liberal use of. But this inference may not be warranted in logics extending IPC to include K and ⇁. Indeed it is not warranted in both IPC ∼ and the logic Williamson himself defines on (Williamson 1994, p. 140), a logic of strong negation with a warrant operator.
Williamson's justification of (ii) assumes that the only consistent rendering of 'A will never be decided' for the intuitionist is ⇁(KA ∨ K⇁A) (for non-standard ⇁), a claim itself established on the assumption of (i), viz. that ⊢ ⇁A → ¬A (see (Williamson 1994, p. 139)). But we have already seen why (i) ought to be rejected and hence (ii) along with it.25
- 1.
It should be mentioned in passing that some (e.g. (Cook and Cogburn 2000)) have objected to the use of 0 = 1 in a definition of negation. I shall not enter into this debate here.
- 2.
Taking proof as proof-in-L, for some fixed logic L, has been thought to be problematic for constructivism for reasons having to do with Gödel's incompleteness theorems. They would seem to imply that, if constructive proof were just proof-in-L, there would be verification- or proof-transcendent truths, contra constructivism as it is typically conceived. See e.g. Martin-Löf's (Martin-Löf 1984, p. 11).
- 3.
Williamson (Williamson 1994) makes this suggestion regarding the BHK clauses in order to show that a semantics so extended cannot make sense of empirical statements of the form 'A may be undecided'. I briefly discuss his argument in section 7.
- 4.
While I have taken the notion of warrant as primitive, so that one may fill in their favorite theory of warrant in the discussion to follow, that discussion does highlight what basic properties warrants must have. For instance, in a constructivist setting the notion of warrant is regarded as monotonic in the sense that if A is warranted by a particular state a, and b stands in the relevant "inclusion" relation to a then A is warranted also at b.
- 5.
What counts as constructively acceptable when the language is extended to include empirical statements is unclear. For instance it is not clear that disjunction ought to satisfy the disjunction property, that if A ∨ B is warranted (recalling that the A and B may be empirical) then either A is or B is. This issue is raised again in section 4 but even more needs to be said concerning constructive acceptability.
- 6.
I am assuming that if a statement is intuitionistically refutable with respect to some evidential state s, it is refutable with respect to all (or at least all extensions of s), i.e. refutability is not a relative matter.
- 7.
There are ways of introducing classical negation without collapse, see e.g. [del Cerro and Herzig 1996], but they are not straightforward adaptations of the usual style of proofs systems (e.g. Hilbert or sequent calculi).
- 8.
Dummett is often thought to have held the conservativity constraint. There are a number of criticisms of the constraint which seem to settle the matter against it. One is that there may be two connectives each of which can be individually and conservatively added to a given logic though the addition of both yields a nonconservative extension. Is each of these connectives individually coherent until present together? That seems an implausible thing to say.
- 9.
Indeed, it has been suggested that an operator is logical when its meaning is determined completely by its rules of inference.
- 10.
Thanks to an anonymous referee for clarifying some important points concerning my formulation of harmony. The one given here corresponds to what Dummett (Dummett 1991, ch. 13) calls 'stability'.
- 11.
From a semantic perspective, empirical negation likely will not be counted logical either. For instance, relative to Kripke semantics, empirical negation is non-logical according to the criterion of permutation invariance which states that a connective is logical if the set of truths in a model having that connective as primary is invariant under permutations of the set of worlds, where truth in a Kripke model may be taken to be truth at every or some distinguished point.
- 12.
The use of labeled systems makes Read's approach controversial. The proof language makes explicit use of an "accessibility" relation and formula labels typically thought of corresponding to points in a Kripke structure. In fact, there are rules specifically for the accessibility relation. The question, then, is whether such proof languages presume a prior understanding of the Kripke semantics from which they arose and whether they are thereby anti-inferentialist in spirit.
- 13.
A model for relevant logic is a quadruple (W, 0, R, V ) where W is a non-emtpy set, 0 ∈ W, R is a ternary relation on W and V is a function from W to subsets of W.
- 14.
The literature on relevant logic refers to the negation defined by (1) as 'boolean' rather than 'classical', so I have stuck with this terminology. In a sense boolean negation is a natural characterization of classical negation for relational semantics, but I don't think it is the only natural one. Fixed negation seems to me to be just as natural.
- 15.
- 16.
The usual intensional semantics for temporal indexicals such as 'at present' (i.e. 'now') treats such expressions as non-indexical propositional operators, and this is how we have chosen to treat them here. The same is true of non-temporal expressions such as 'actually' which is taken, by e.g. Lewis, to be indexical.
- 17.
For definiteness, the set of logical symbols is {∧, ∨, →, ∼, ⊥}, and Prop is a denumerable set of propositional letters (constants) whose members we denote by p, q, etc. We define ¬A := A → ⊥.
- 18.
We may read ≤ in a number of different ways. My preferred way is in terms of informational containment so that a ≤ b reads 'b contains all of the information contained in a'. Even though @ is to be thought of as the present state of evidence, we need not read ≤ temporally, e.g. by reading a ≤ b as 'b is a state of evidence arrived at temporally later than a which contains all the information contained in a' for we might just think of each state in the model as representing a possible present state of evidence.
- 19.
One interesting application of∼is that it may also be seen as providing an alternative, but inequivalent, characterization of boolean negation in the setting of relevant logic. If we confine ourselves to the simplified semantics for R then we may introduce∼by letting '@' denote the sole base world. Valid consequence on the simplified semantics for R is already defined in the same way we have defined valid consequence for IPC ∼, viz. in terms of truth preservation at @. It would be interesting to compare ∼ and boolean negation in the setting of relevant logic, a curiosity I mention only to set aside.
- 20.
A proof showing local validity implies actual validity is easy; the converse is not much harder. L-models are L ∼-models and the truth conditions for L-sentences are the same as those for L ∼-sentences restricted to L, where L ⊂ L ∼. For reductio, suppose A is an actual but not local consequence of Γ. Then there is a model M = (W, ≤, @, V ) and a ∈ M s.t. M |= Γ but M, a |≠ A. But then the model M′ = (W, ≤ ,@′ ,V),where @′=a, is s.t. M ′, @′ |=Γ and M′ @ |≠ A, which contradicts our supposition that A is an actual consequence of Γ.
- 21.
For instance, see [Hodes, 1984] and his notion of "weak" consequence according to which A and @A, the latter read 'actually A', are provably equivalent but not intersubstitutable salva veritate.
- 22.
Thanks to a referee for pointing this out. As remarked below, harmonious rules can be given to all connectives with respect to a labelled proof system, but without unlabelled system for IPC ∼, it cannot be said whether the same is true of other styles of proof systems (e.g. unlabelled natural deduction). This is an interesting open problem.
- 23.
Technically, IPC ∼ is not an intermediate logic since its language is not L but a proper extension of it. It might be more appropriate to call it a 'superintuitionistic' logic though some authors use these terms synonymously.
- 24.
In fact, the paradox is blocked in a Kripke semantics for IPC with a standard-going S5-like epistemic operator K since A ∧ ¬KA will then be consistent.
- 25.
This liberates strong negation from Williamson's objection to its use in the paradox he presents. But it does not liberate it from the point made in §1 that it is too strong to capture that a given statement lacks evidence at a particular state and not necessarily all extensions of that state. For an application of strong negation to Fitch's paradox, see (Wansing, 2002).
Thanks to Stephen Read, Dick de Jongh, Lloyd Humberstone, Elia Zardini, Ole Hjortland, and Heinrich Wansing for helpful discussion. I would also like to thank a referee of this journal for their substantive and detailed comments, as well as Julia Langkau and the audience of the 3rd Cambridge Graduate Conference on the Philosophy of Logic and Mathematics.
Open Access
This article is distributed under the terms of the Creative Commons Attribution License which permits any use, distribution, and reproduction in any medium, provided the original author(s) and the source are credited.
- Cook, R. T., & Cogburn, J. (2000). What negation is not: Intuitionism and 0 = 1. Analysis and Metaphysics, 60(1), 5–12.CrossRefGoogle Scholar
- Copeland, B. J. (1979). On when a semantics is not a semantics: Some reasons for disliking the routley-meyer semantics for relevance logic. Journal of Philosophical Logic, 8, 399–413.CrossRefGoogle Scholar
- Copeland, B. J. (1983). Pure semantics and applied semantics. Topoi, 2(2), 197–204.CrossRefGoogle Scholar
- Copeland, B. J. (1986). What is a semantics for classical negation? Mind, 95(380), 478–490.CrossRefGoogle Scholar
- del Cerro, L. F. & Herzig, A. (1996). Combinig classical and intuitionistic logic, or: Intuitionistic implication as a conditional. In Frontiers of Combining Systems (FroCos), pages 93-102Google Scholar
- DeVidi, D., & Solomon, G. (2006). Empirical negation in intuitionisitic logic. In D. DeVidi & T. Kenyon (Eds.), A Logical Approach to Philosophy (pp. 151–168). Dordrecht, The Netherlands: Springer.CrossRefGoogle Scholar
- Dummett, M. (1977). Elements of Intuitionism (2nd ed.). USA: Oxford University Press.Google Scholar
- Dummett, M. (1991). The logical basis of metaphysics. Harvard University PressGoogle Scholar
- Dummett, M. (1996). The seas of language. Oxford university press.Google Scholar
- Gurevich, Y. (1977). Intuitionistic logic with strong negation. Studia Logica, 36(1/2), 49–59.CrossRefGoogle Scholar
- Heyting, A. (1971). Intuitionism: An Introduction (3rd ed.). Amsterdam: North Holland Publishing Co.Google Scholar
- Hodes, H. T. (1984). Some theorems on the expressive limitations of modal languages. Journal of Philosophical Logic, 13, 13–26.CrossRefGoogle Scholar
- Hossack, K. G. (1990). A problem about the meaning of intuitionist negation. Mind, 99(394), 207–219.CrossRefGoogle Scholar
- Kleene, S. (1945). On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic, 10(4), 109–124.CrossRefGoogle Scholar
- Martin-Löf, P. (1984). Intuitionistic Type Theory. Bibliopolis.Google Scholar
- Meyer, R. K., & Routley, R. (1973). Classical relevant logics i. Studia Logica, 32(1), 51–66.CrossRefGoogle Scholar
- Meyer, R. K., & Routley, R. (1974). Classical relevant logics ii. Studia Logica, 33(2), 183–194.CrossRefGoogle Scholar
- Nelson, D. (1949). Constructible falsity. The Journal of Symbolic Logic, 14(1), 16–26.CrossRefGoogle Scholar
- Read, S. (2000). Harmony and autonomy in classical logic. Journal of Philosophical Logic, 29, 123–154.CrossRefGoogle Scholar
- Read, S. (2008). Harmony and modality. In Dégremont, C., Keiff, L., and Rückert, H., editors, Dialogues, Logics and Other Strange Things: Essays in Honour of Shahid Rahman, pages 285-304. College Publications.Google Scholar
- Restall, G. (1999). Negation in relevant logics: how i stopped worrying and learned to love the routley star. Applied Logic Series. Kluwer Academic Publishers.Google Scholar
- Tennant, N. (1997). The Taming of the True. New York: Oxford University Press.Google Scholar
- Thomason, R. (1969). A semantical study of constructible falsity. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 15:247-257. Google Scholar
- Tomassi, P. (2006). Truth, warrant and superassertibility. Synthese, 148, 31–56.CrossRefGoogle Scholar
- Wansing, H. (2002). Diamonds are a philosopher's bestfriend. Journal of Philosophical Logic, 31, 591–612.CrossRefGoogle Scholar
- Williamson, T. (1994). Never say never. Topoi, 13(2), 135–145.CrossRefGoogle Scholar


text:
Home > Corruption > Political Corruption in India: An Analysis
[5/5] Total Votes [ 1 ]
"I would go to the length of giving the whole congress a decent burial, rather than put up with the corruption that is rampant." --- Mahatma Gandhi May 1939
This was the outburst of Mahatma Gandhi against rampant corruption in Congress ministries formed under 1935 Act in six states in the year 1937. The disciples of Gandhi however, ignored his concern over corruption in post-Independence India, when they came to power. Over fifty years of democratic rule has made the people so immune to corruption that they have learnt how to live with the system even though the cancerous growth of this malady may finally kill it. The recent Tehelka episode surcharged the political atmosphere of the country but it hardly exposed anything, that was unknown to the people of this biggest democratic polity.
Politicians are fully aware of the corruption and nepotism as the main reasons behind the fall of Roman empire, the French Revolution, October Revolution in Russia, fall of Chiang Kai-Shek Government on the mainland of China and even the defeat of the mighty Congress party in India. But they are not ready to take any lesson from the pages of history.
The history of corruption in post-Independence India starts with the Jeep scandal in 1948, when a transaction concerning purchase of jeeps for the army needed for Kashmir operation was entered into by V.K.Krishna Menon, the then High Commissioner for India in London with a foreign firm without observing normal procedure. Contrary to the demand of the opposition for judicial inquiry as suggested by the Inquiry Committee led by Ananthsayanam Ayyangar, the then Government announced on September 30, 1955 that the Jeep scandal case was closed. Union Minister G.B.Pant declared "that as far as Government was concerned it has made up its mind to close the matter. If the opposition was not satisfied they can make it an election issue. Soon after on February 3,1956 Krishna Menon was inducted into the Nehru cabinet as minister without portfolio.
In 1950, A.D.Gorwala, an eminent civil servant was asked by Government of India to recommend improvements in the system of governance. In his report submitted in 1951 he made two observations: One, quite a few of Nehru's ministers were corrupt and this was common knowledge. Two, even a highly responsible civil servant in an official report as early as 1951 maintained that the Government went out of its way to shield its ministers (Report on Public Administration, Planning Commission, Government of India 1951)
Corruption charges in cases like Mudgal case (1951), Mundra deals (1957-58), Malaviya-Sirajuddin scandal (1963), and Pratap Singh Kairon case (1963) were levelled against the Congress ministers and Chief Ministers but no Prime Minister resigned.
The Santhanam Committee, which was appointed by the Government in 1962 to examine the issue of corruption in its report submitted in 1964 observed: There is widespread impression that failure of integrity is not uncommon among ministers and that some ministers, who have held office during the last sixteen years have enriched themselves illegitimately, obtained good jobs for their sons and relations through nepotism and have reaped other advantages inconsistent with any notion of purity in public life.
The following comments of Nehru on the memorandum of charges against Pratap Singh Kairon submitted to the President of India by the non-Communist opposition in Punjab suggest his approach on corruption - The question thus arises as to whether the chief minister is compelled to resign because of adverse findings on some questions of fact by Supreme Court. The ministers are collectively responsible to the legislature. Therefore, the matter was one, which concerned the assembly. As a rule therefore, the question of removing a minister would not arise unless the legislature expressed its wish by a majority vote. (Pathology of Corruption by S.S.Gill)
Thus, we find that while Nehru's tolerance of corruption among his ministers legitimized this malady, his daughter Indira Gandhi institutionalized it by holding both the posts of the Prime Minister and party president. By doing so she was herself controlling the party funds, which gave birth to the money power in politics. The famous V.P.Malhotra (Chief Cashier of State Bank of India) case in which he got a telephone call believing from Indira Gandhi to pay Rs,60 lakhs to one Nagarwal remained a mystery. Corruption cases like Fairfax, HBJ Pipeline, and HDW Submarine deal came up since then. The famous Bofor's deal is well known. Narsimha Rao was the first Prime Minister being prosecuted in corruption charges. Cases like Rs.2500 crore -Airbus A-320 deal with France involving kickback (1990), Harshad Mehta security scam (1992), Gold Star Steel and Alloys controversy (1992), JMM bribery case, Hawala scam of Rs. 65 crore and Urea scam (1996) also came up during the period of Narsimha Rao Government.
Criminalisation of politics is another facet of corruption. N.N.Vohra, Union Home Secretary in his report (1995) on this issue observed:- A network of mafias is virtually running a parallel Government pushing the state apparatus into irrelevance. Quoting some DIB sources, he added,there has been a rapid spread and growth of criminal gangs, armed senas, drug mafias, smuggling gangs and economic lobbies in the country, which have over the years developed an intensive network of contacts with bureaucrats, government functionaries at local level, politicians, media persons and strategically located individuals in non-state sector. Some of these syndicates have also international linkages including the foreign agencies.
Against the above-discussed historical background of corruption during last fifty years, the only contribution of Tehelka is that the exposure has forfeited the right of the BJP to claim itself to be a party with difference. So long the BJP was in opposition, it was by and large known as a party with moral integrity, but when it aligned with the political leaders with shady background for the sake of power, the malady of corruption infected this party too. Once the moral integrity is compromised it opens the door of corruption. Perhaps the BJP leadership deliberately went for ideological compromise for capturing power at centre. L.K.Advani put the responsibility on middle class when he reacted to a suggestion by an important ex-National Executive member of the party against the dubious coalition politics. Advani reportedly said: The middle class does not like compromises and tends to be idealistic. At the same time, it is unhappy if we lose power. It wants power as well as ideological integrity. This is the dilemma of the party. ( Inside BJP by Dr. Jay Dubashi published in Times of India dated March 22,2001). Advani might have philosophised the situation but he cannot escape from the responsibility for the ideological compromise the BJP made for the sake of power.
Corruption is an abstract term. According to World Bank report 1997 abuse of public power for private gains is described as corruption. But this appears to be too simplistic explanation of corruption. In fact it is a multi-faceted evil, which gradually kills a system. A basic conflict between the ethos and system has weakened the Indian polity. The feudal outlook of the ruling class polluted the people's mindset, which judge the status of an individual on his capability to flout the law to favour them. This is the reason why corruption is no more viewed by people with abhorrence in Indian society. Leaders like Laloo, Jayalalitha, Sukhram and others, who are facing corruption charges, continue to have wide range of people's support. Transparency, responsiveness, accountability, probity in public life and good governance are now only slogans. The legislature has failed to make the judiciary, executive and even media sensitive to the cause of the common people. The failure of the political leadership to take a principled stand against corruption has clouded the system to the extent that it is now difficult to understand whether the system is alive or dead.
In the present context corruption is so much linked with power that our politicians have adopted a cynical attitude toward political morality. Maneuvering the anti-defection law for electoral politics with the help of both money and muscle power and other unfair means for the sake of power have affected the political morality of all the political parties and as such none of them can claim themselves to be faithful to nation in true sense. It was pathetic to see an excellent orator of congress struggling to brush away the past of the congress in the recent Big fight programme of Star TV.
The collapse of the Janata Party Government (1977-80), fall of V.P.Singh and Chandrashekhar Government (1990-91), turning his minority Government into majority by Narsimha Rao, split in Telugu Desam Party (1994), defection of Ajit Singh with his supporters to Congress (1993), defection of S.S.Vaghela from BJP, maneuvering defection by Kalyan Singh to keep the BJP led Government in power in UP are some of examples to prove that a sizeable number of our politicians are not immune to corruption.
With Tehelka exposure, we may like to refer to our ancient law book, which said, That monarch, whose subjects are carried from his kingdom by ruffians, while they call aloud for protection, and he barely looks on them with his ministers, is a dead, and not a living king. (Manusmriti VII/143) Tehelka is simply an addition to thousands of past and present eruptions in the cancerous body polity of the country.
Manu may not be relevant to the present century, but as human nature more or less remains same and states either in monarchy or democracy are governed by the same human beings, he is still relevant. License to govern does not mean license to be corrupt. Mahatma Gandhi believed in the need for creating a social climate against corruption, which meant creation of an atmosphere in which the corrupt could not thrive. The need of the hour therefore, is to wipe off the tormenting system, which could be possible only after its thorough overhaul. For this our national leadership is expected to devise a political mechanism to create a social atmosphere by empowering of people. The on going war cry against corruption, which is nothing but a mad fight to replace one corrupt system by another is not going to transform the beleaguered nation to a sustainable social order. -Source : southasiaanalysis.

subset: commoncrawl


text:
Thoughts following the comments that the CSS logo should show "text only" character of CSS. Shouldn't we plan, in the future, for style sheets to be a general linking of logical elements to physical properties? From this point of view, text is the initial application. For example, in object-oriented graphics, one frequently finds logical color schemes, with logical colors for, say, background foreground emphasis de_emphasis A style sheet could bind each of these logical categories to color, or linewidth or line style(dash, dotted, etc). The linewidth and line style alternatives would be useful for black on white printing, or for people with color impairments. Style sheets could also be used for functional objects. For example, if a web page contains a menu, the style sheet could specify what kind of menu to use: traditional rectangular, pie etc., via reference to a Java Class or Active-X object, and also specify the properties of the menu, e.g. how a selected menuj item appears in terms of font or color, or how it sounds when accessed under control of an audio style sheet. The short term implication of this argument is that a "graphics" look in the CSS logo is a desirable feature. Plus a few words are needed in the introductary paragraph of the CSS standard. Long term, I don't think the syntax will need to change (someone please jump in if I'm wrong), but new elements, attributes, etc. would need to be defined. As you may have gathered, my main interest here is the utility of this for people with disabilities, but it would carry the benefits of style sheet to the world of graphics and functional objects for everyone else as well. Len Kasday firstname.lastname@example.com (These are my personal opinions, not necessarily those of my employer.)Received on Thursday, 5 December 1996 05:52:19 UTC
This archive was generated by hypermail 2.3.1 : Monday, 2 May 2016 14:26:42 UTC


text:
Downtown RVA
Annual Events that Happen in this Area
- Richmond Folk Festival
- Que Pasa Festival
- Broad Appétit
- Dominion Riverrock
- Festival of India
What's Coming to Downtown RVA
If you enjoy urban living with historical flair, the Downtown area is for you. You can choose to live in a historic row/town home in Jackson Ward, a modern condo/loft residence with breathtaking rooftop views of the city and the Mighty James, or you can opt for a funky contemporary number for a standout dwelling. The city bustles during the day and then once the 9-5'ers have gone to happy hour and home, the denizens of downtown are enjoying the great dining and arts in the area. Shockoe Bottom is nightlife central on the weekends with its many guests looking for a stiff cocktail and some dancing. Bridal parties have been known to litter the streets from the nearby hotels. Monroe Ward is sprinkled with apartment buildings housing VCU students and is very pretty walk along Franklin Street.
Notable Neighborhoods
- Jackson Ward
- Shockoe Bottom/Slip/Valley
- Monroe Ward
- Midtown
- Condos/Lofts
- Contemporary/Modern
- Greek Revival Town and Row Houses
Fab 5 Features
- Valentine Museum
- Arts District
- The Jefferson Hotel
- Dominion Arts Center
- Richmond Ballet
5 and Dine
- Rappahanock
- Black Sheep
- Saison
- Cafe Rustica
- Comfort
5 Experiences
- Visit Quirk Hotel for their Wine Table Tuesdays
- Go to 1st Fridays and see local artists/galleries
- Visit The Jefferson Hotel and do Brunch or enjoy their Happy Hour specials in this historic hotel
- Walk or Run the Canal Walk, Belle Isle, Brown Island
- Go to a show at The National
5 and Firsty
- Wong Gonzalez
- Champion Brewery
- Penny Lane Pub
- Siné
- Rosie O'Connolly


text:
From the first day we opened our doors at FitnessSocial in 2012, giving back to the local community was always part of our mission and something we still hold very dear to our hearts five years later. On Friday, October 27th from 5:30pm to 7:00pm, we will be hosting Happy Hour Yoga at the studio in honor… Continue reading Sweat for a Cause!
Tag: blog
A Healthier Lifestyle with Heart & Soul
As women, we play different roles in life. We are moms, wives, hard-working business women and best friends. From the beginning, we have learned to take on these roles and succeed in them to the best of our abilities. As women, we are capable of anything and everything, and we could do it all. Therefore,… Continue reading A Healthier Lifestyle with Heart & Soul
Invest in Children…They are the Future
When Dina and I sat down in early 2012 to talk about opening a business together we both knew that we wanted to be able to give back to our local community and help make a difference. It was important to both of us to be able to help out the smaller, local non-profit organizations… Continue reading Invest in Children…They are the Future


text:
Podcast (podcasts): Download (29.6MB)
Podcast (podcasts): Download (29.6MB)
**Please be advised, the contents of this podcast may not be suitable for all audiences. If you are under the age of 17, you should check with your legal guardian before listening. Now…ENJOY!**
This is the ninth podcast from The Bobby D Show. Here's what's featured in this podcast: The music of Isreal Spain, How to Properly Fold Toilet Paper (See Below), Perverted Behaviors that You Need to Stop, National Masturbation Month, A PSA about ugly chicks and a lot more. Keep in mind that our podcast are 100% NEW material. We love to recycle but we're not doing it here! Now find out more about the featured musical guests.
Which is the Proper Way to Fold Toiler Paper?
In this podcast, Civi (from Sports W/ Civi) and I debated the proper techniques of folding your toilet paper properly. So…what way do you think is the best. I have provided the pictures of the Top 3 down below.
This is the first technique, called 'The Mummy.' Preferred by some, the mummy is all encompassing. It covers the whole hand and assures errors are small. Speed is usually the reason behind the mummy. This technique isn't used most often by Civi or Bobby D, as they like their own personal strategies.
This is the second technique, called 'The Bunch.' This is Civi's favorite way to get a good, adequate wipe of his back side. Bobby D disagrees with this way stating there this is too much room for error. Can you get an adequate wipe from this technique? Will you use more toilet paper when using this technique? These are all questions that come up when using 'The Bunch' technique.
The last technique is called 'The Classic.' This is the favored technique for Bobby D. He defends his position by saying that "on this first wipe, there is just an abundance of space, you pretty much can't miss and your hand will always be clean." Civi says taking the time to make these 'neat' little sheets is a waste of time. Civi really has a problem with the next thing that Bobby D does with this technique.
This is the 'Classic Fold-Over.' This technique is used in cooperation with 'The Classic.' After the first couple of wipes, Bobby D says that you can 'fold over again and just use that bad boy one more time.' This statement made Civi say that 'Bobby D pretty much plays with his poo and should be locked in a padded room.' Bobby D still thinks he's correct.
Who do YOU think is correct? Send us an email, call and leave a message on (253) 778-6727 or find us on Facebook to cast your vote.
Isreal Spain
During the birth of his music career, Isreal Spain honed his performance skills in plays on theater stages of his high school in Franklin, Louisiana all the way to Kent State University (in Kent, Ohio) where he attended on a scholarship. Although Spain began his music career recording and releasing tracks with a group of his friends from his hometown, his undeniable talent and his relocation to Ohio inevitably dictated his future as a Solo Artist. Isreal saw this as motivation to push his songwriting skills and creativity in his own Unique Direction.
With his small town Heritage and diverse list of musical influences (ranging from Mahalia Jackson, to Sam Cooke, to Nas), Isreal Spain seemingly has no choice but to tell his story in a manner that is different from his major city-raised peers. Even in sharing familiar themes, he possesses a tangibly distinctive style in conveying his messages. Upon hearing the album content, it becomes evident that there is more to his songs than simply baritione-tinged, southern articulated verses. His songs often incorporate themes of seeking truth, gratification, reality, and redemption: sometimes with conflicting moral protocol, but such themes are very inspiring and moving nonetheless. Isreal Spain humbly describes his songs as "real music from the pages of his life."
Find out more about Isreal Spain by heading to Twitter account or hear more of his music on Reverb Nation.


text:
Hawthorne Auto Clinic
4307 SE Hawthorne Blvd Portland, OR 97215
Tel: (503)234-2119
Fax: (503)234-4230
Hometown: Troy, Ohio
Education: Xavier University.
Certification: ASE Certified Master Technician, L-1 Advanced Level Engine Performance Specialist.
Certified Service Consultant.
Worked at Hawthorne Auto since: Its inception in January 1983.
In the automotive industry since: 1976
Hobbies: Meddling in my kid's affairs, meddling in my government's
affairs, hiking, "working in the yard," reading
Favorite car: Fiat Abarth 850 TC and Toyota Prius PHEV (Plug-in Hybrid Electric Vehicle).
Most challenging part of the job: Keeping
up with the changing technology, and with the vehicle manufacturers' need to
approach technology differently from one another.
Advice to customers: Learn to use and appreciate alternative forms of transportation.
Visit our Blog


text:
|Some of the names in this Article use an unofficial English translation of its official Japanese Name.
The name is obtained either by using Japanese translating programs or through previous existing English equivalent terms in the game. The names will be used as quick references around other articles in the Monster Hunter Wiki until Capcom reveals the official English names for them.
|Berukyurosu Topics:
Berukyurosu are Flying Wyverns introduced in Monster Hunter Frontier Season 4.0.
Berukyurosu is able to shoot a linear lightning beam from its mouth. The beam itself is very similar to that of the Rajang. Berukyurosu is highly adept in aerial combat, able to do even more difficult maneuvers than the Kushala Daora.
Berukyurosu has the ability to learn patterns of attack from hunters and will counter it, or will attack/evade accordingly. It will also change behavior depending on what weapons are used and what quest it's in. It bears a passing resemblance to Rathalos and may be related to it. When enraged, the yellow mane of Berukyurosu will turn orange, and it will fly into the air to attempt a dive bomb capable of unleashing a massive explosion of thunder.
Other Non-Subspecies Forms
Hardcore (HC) Berukyurosu
First able to be encountered at SR81
Changes in appearance including the majority of its body color is more blue along with all its hair, spikes are bright yellow tipped, its long quill-like appendages are more thick, all its spikes are longer and more developed, the claws at the tips are greatly increased in size and are double tipped.
A very powerful variation, HC Berukyurosu, is even more deadly than the common Berukyurosu.[1] Using more of its deadlier attacks more often and new attacks that devastate hunters who are unprepared including a combo where Berukyurosu follows a target while it sweeps the ground with its long whip like appendages twice followed by a jump into the air where it hooks its appendages into the ground and pulls itself down smashing the ground and making its Thunder Sky Slam previously only done when entering rage.
At SR100, HC Berukyurosu gains a new attack where it flies high into the air and a thin red light comes out of its mouth aiming down below, followed by a beam more wide than the monster itself that its moves horizontally attempting to kill its target. If it's not in rage mode, it will gently fly down or if it's in rage mode, it will crash down with its Thunder Sky Slam.
Game Appearances
In-Game Description
- Berukyurosu's horn, back, both wings, appendages and side tails can be broken, and the middle tail can be severed.
- If Berukyurosu's horn is broken along with its back and wings, it may begin to lose control of its own power and inflict itself with damage. This can cause random, lethal bursts and has been seen to run away and blow out without anyone being in the area it died in.
- Berukyurosu is known for rare suicide blow outs when near death, preventing its capture from hunters.
- Berukyurosu's roar requires HG Earplugs to block.
- Berukyurosu's wind pressure requires Windproof (Hi) to block.
- HC Berukyurosu's roar requires Super HG Earplugs to block.
- When Berukyurosu staggers while it's hovering, there is a chance that it might drop a shiny.
- Some of Berukyurosu's known common tactic changes include the addition of free roaming balls of thunder for Dual Sword and Sword and Shield users.
- The lightning bite attack can cause a hunter's weapon to lose a large amount of its sharpness instantly.
External Links


text:
Pancreatic Cancer Surgical Options
For many types and stages of pancreatic cancer, surgery is the treatment of choice.
What is the Goal of Surgery for Pancreatic Cancer?
The goal of surgical treatment for this disease depends on the likelihood of removing the tumor.
- If imaging test results suggest surgeons can excise the entire mass then the goal of surgery is to cure the pancreatic cancer.
- If the imaging test results suggest the tumor is too large or widespread for surgeons to remove then the goal of surgery is to relieve symptoms or prevent complications (palliative surgery).
Imaging tests can't always predict exactly what the surgeon will encounter. He or she may need to switch from curative to palliative surgery based on the situation at hand.
Surgery is often just one part of a complete treatment plan that may also include radiation and medical oncology.
Surgical Treatment Options for Pancreatic Cancer
The surgical oncologists at UPMC Hillman Cancer Center have extensive skill in a range of advanced pancreatic cancer surgery techniques.
Minimally invasive and robotic surgical methods — including the robotically assisted Whipple procedure — reduce risks and healing times.
Almost 80 percent of pancreatic cancer patients at UPMC who we recommend for surgery have the Whipple procedure. And, up to 85 percent of patients slated for the Whipple procedure are candidates for the robotic option.
UPMC is one of only a handful of hospitals in the United States to offer the robotic Whipple method.
Your care team and surgeon will:
- Explain your pancreatic cancer surgical treatment options.
- Recommend the option that takes into account the type and stage of pancreatic cancer, along with the goals of surgery.
- Discuss the risks and benefits of the procedure and describe the recovery process.
You will also make decisions together about adding radiation or medical oncology to your treatment plan either before or after surgery.
Types of pancreatic cancer surgeries we perform
- Distal pancreatectomy — this is the removal (resection) of the tail and some of the body of the pancreas. Used mainly for neuroendocrine (islet cell) tumors, this open surgery often includes removal of the spleen. Because the spleen helps fight infection, you may need a vaccination before surgery. This operation usually requires a hospital stay of six to eight days.
- Laparoscopic pancreatectomy — this minimally invasive procedure removes the tail and body of the pancreas through five or six small "keyhole" incisions. This can reduce risks and shorten hospital stay by a few days.
- Pancreas-sparing tumor resection — in this type of limited resection, the surgeon removes the tumor without removing the pancreas. Contained tumors that haven't invaded nearby structures may be entirely resectable. Sometimes, the surgeon will resect a tumor along with part of a structure (usually the duodenum) that it has invaded.
- Portal vein resection and reconstruction — at the head of the pancreas, the superior mesenteric vein meets the splenic vein. These form the hepatic portal vein, which transmits blood to the liver. If a tumor invades this meeting point, the surgeon may resect it and build a new pathway to the liver. Surgeons can perform portal vein resection along with the Whipple procedure or on its own.
- Whipple procedure (Pylorus preserving pancreaticoduodenectomy) — this open method removes a tumor in the head of the pancreas along with the attached duodenum and bile duct. Surgeons also remove the gallbladder and part of the stomach. The open Whipple procedure requires a large incision and usually entails a hospital stay of about ten days. The minimally invasive robotic Whipple method requires a few small incisions. This results in a shorter hospital stay, faster recovery, and reduced pain and scarring.
- Advanced Whipple — this surgery contains all aspects of the standard Whipple along with the removal if the portal or superior mesenteric veins.
- Appleby operation — this is the removal of locally advanced cancers of the body of the pancreas that have invaded the celiac or hepatic artery. Robotic methods are not available for this operation.
- Small bowel (small intestine) resection — this is the resection of the pancreatic tumor along with the part of the bowel that it has invaded.
- Total gastrectomy — extensive tumor involvement may require a total gastrectomy. This is when the surgeon removes some or all of the diseased pancreas along with the entire stomach and nearby lymph nodes. Often, this also involves removing the spleen and parts of the intestine as well. This radical surgery results in connecting the esophagus directly to the bowel.
Learn More About Surgery for Pancreatic Cancer
If you would like to learn more about pancreatic cancer care:
- Contact UPMC Hillman Cancer Center at 412-647-2811.


text:
Our technology partners are contracted to deliver and install technology products into the schools under the project and are required to provide warranty support for the designated warranty period. They may optionally be contacted for after warranty support where needed at the schools' cost. Please contact these Partners for first line warranty support, and escalate to the e-Learning Jamaica Company if you are having any difficulties. Please see partner details below.
DELL Inc. (Support Tel. 1-800-682-3639. Website: www.support.dell.com)
Dell provides warranty support for Computers, Printers, Network Equipment and UPS Units. Support can be accessed through their 1-800-number or website.
Massy Technologies (28 Balmoral Ave, Kgn 10. Tel. 876-926-3490 or 1-888-991-2271. Website: www.illuminatnm.com)
Massy Technologies provides warranty support and repairs for audio visual equipment including; Multimedia Projectors, Document Cameras, Scanners, DVD Players, Video Cameras, Televisions.
ModOffice by EHC Industries Ltd. (16 Retirement Rd. Kgn 5. Tel. 876-968-8000. Website: www.modoffice.com)
ModOffice provides warranty support for the Computer Desks and Chairs.
Computer Environmental Solutions (Tel. 876-926‑2935) e-mail: [email protected]
Computer Environmental Solutions provide support for the UPSes as a sub-contractor of Dell.
MediaNet Ltd. (19-22 Ballater Ave. Kgn 10. Tel. 876-754-5784 email: [email protected])
Medianet provides support for the Network infrastructure and Air-condition units as a subcontractor of Dell.
Fujitsu Transaction Solutions (Jamaica) Limited (18 Belmont Rd. Kgn 5. Tel. 876-926-7567 or 876-926-7573. Website: www.fujitsu.com/caribbean)
Fujitsu provides installation support for the computers on the project.


text:
Dance Class Summary
Pick a class that best suites your needs!
Pick a class that best suites your needs!
Sokkie/Informal Classes:
Informal says it all. Our aim is to make it as much fun as possible to learn how to dance (sokkie), now matter how much you might struggle! While we keep a positive environment we also focus on the minor details and ensure that not only can you dance when you finish with the classes, but that you can also dance in style!
With special teaching techniques we teach the men how to lead and ladies how to follow, all while having fun!
More about the informal dance classes
Wedding Dance Classes
Any style that you desire, whether its fast, fancy, slow or waltz! Let us know what your song is and we'll find the perfect dance for you and your partner. Your first dance together as husband and bride should be relaxed, enjoyable and give you time to focus on each other. While we can choreograph a dance, we prefer to teach you both how to dance and provide you with a more naturally enjoyable dance.
More about the wedding dance classes
Singles Class
Our singles class is new and starts in 2017. The Dance2Evolution website allows you to find a dance partner. At class however we encourage dancers to swap partners. On top of that we have our monthly social dance event as well as various dance school social events.


text:
Today was a good day, in that weird kind of way. Hey hey. I'll preface: The other day I noticed my back passenger tire (back left/right?) was pretty low on air, so I drove to a gas station, filled it, and didn't think anything of it – until today. My daughter and I walked out to the car, where I found the same tire in the same state, its rim barely off the pavement. I drove to the tire store and checked my car in, hoping it would not take long. Before I tell you the resolution, I must add one more fact. Today was supposed to officially be "no more diapers" day for my daughter. It would free her of the plastic, Pamperish binding, and free me of buying and changing them. So, back at the tire store, and diaper free, we sat waiting for the car to be fixed. I asked my daughter numerous times if she had to – you know what – and she said, "no." Finally the car was fixed (just a nail… just a patch… just twenty bucks), and Little Mary and I walked to the counter to pay our dues. I was talking to the guy, signing the paper, and looked down to find my daughter standing in a pool of liquid. Not thinking at all about what had happened, I said to the guy, "Oh, someone must have spilled something on the floor over here." Then I looked at Little Mary's pants, and my eyes went wide. Damnit. Trying not to cause a scene or draw attention to her, I handed the paper back to the guy, and placed myself strategically between him and my sprout, blocking his view of her wet (soaked) pants. So, that was the tire.
We went home, showered, and then ran around some more. I had to go to campus to settle some business, and grab a book.
We then met my girl for dinner, a trip to the comic book shop, and upon exiting I ran into an old co-worker. The situation, and the conversation after, with Katie, reminded me of how socially ridiculous I am. I have pretty poor social skills, but apparently only when my girlfriend is around. I don't get it.
So, at the comic book store, I got issue #9 in the Girls series by The Luna Brothers, TechJacket, and Tiny Giants by Nate Powell. I also got Little Mary and I some Strawberry Pocky. So yummy.
Then I came home, walked into my room, and decided to rearrange the entire place. So, I did. Day over.


text:
Handle complex legal requirements and warranty issues easily!
Our approach on Serial Number Handling is a benchmark for the entire Telecommunications industry. Serial numbers play a fundamental role in the logistics processes of high value goods as they identify the items individually and our high IT performance and date security standards allow us to handle all serial numbers in real time inlcuding validation during the pick. We offer you item-wise IT based transparency over the whole process including delivery and return.


text:
30.05 (Ascension Day)
Created on 16.05.2019
It's time for a short break: on 30.05. (Ascension Day) our printing presses will not be running. Delivery times will be delayed accordingly. Please take the public holiday into account when ordering.
Unfortunately our service team will also be unavailable on this day.
We apologise for any inconvenience.
Your FLYERALARM Team
Adobe Creative Cloud
15% discount
Save 15% on Adobe Creative Cloud products as a FLYERALARM customer.
Professional programs at attractive prices
Adobe is the leading provider of professional layout, graphics and image editing software. All Adobe applications are amalgamated in the Creative Cloud. This ensures that all programs are always up-to-date and can be used on various devices. You can also download Creative Cloud at a discount through FLYERALARM.
Here you can choose whether you qualify for the VAT exclusion according to HMRC. Detailed information can be found in our FAQs.