New APPS

Art, Politics, Philosophy, Science. Mostly Philosophy.

recent posts

about

    Is the Barwise/Etchemendy system unsound?

    I might be being an idiot here, but I can't for the life of me figure out how the following inference is disallowed in the Barker-Plummer/Barwise/Etchemendy textbook:

    1. Ex(Rax)

    2. ExEx (Rxx)   1, E introduction

    This is clearly invalid, because there are anti-symmetric relations (note that if it were valid one can prove ExEx (Rxx) from ExEy (Rxy), and that ExEx(Rxx) has the same truth conditions as Ex(Rxx)).

    Intuitively, Existential Introduction should be restricted so that one cannot replace a name or eigenvariable with a variable that is already bound in the sentence. But I can't find this restriction in Barker-Plummer/Barwise/Etchemendy. My friend couldn't find it in the old red Mates book either, so we think it's not unlikely that we're both missing something obvious.

    I turned to the soundness proof in Barker-Plummer/Barwise/Etchemendy and they leave the case of Existential Introduction as an excercise to the reader. It has a little star next to it showing that it is a difficult problem. I'm wondering if it's impossible. But, again, it's more likely that I'm missing something, so if anyone who teaches from the book could take a look my introductory logic students would appreciate it.

    Posted in ,

    11 responses to “Is the Barwise/Etchemendy system unsound?”

    1. Justin Vlasits Avatar
      Justin Vlasits

      Page 357 of LPL 2nd edition:
      E-Intro
      |S(c)
      |ExS(x)
      “Here x stands for any variable, c stands for any individual constant (or complex term without variables), and S(c) stands for the result of replacing free occurrences of x in S(x) with c. Note that there may be other occurrences of c in S(x) as well.”
      In your formula, there are no free occurrences of x in S(x) (since it is ExRxx), so S(c) should just be the same as S(x).

      Like

      Reply
    2. Mark Avatar
      Mark

      Here is the rule:
      Existential Introduction:
      S(c)
      …
      Ex S(x)
      Here too x stands for any variable, c stands for any individual constant (or
      complex term without variables), and S(c) stands for the result of replacing
      free occurrences of x in S(x) with c. Note that there may be other occurrences
      of c in S(x) as well.
      Now your example is
      Ex(Rax)
      This formula cannot be obtained by “replacing free occurences of x with a in Ex(Rxx), which has no free occurences of x.

      Like

      Reply
    3. Jon Cogburn Avatar
      Jon Cogburn

      Awesome. Thank you.

      Like

      Reply
    4. RF Avatar
      RF

      Jon,
      Here’s how B-P, B, & E introduce the rule (p. 357):
      “Existential Introduction (E Intro):
      S(c)
      …
      ◃ Ex S(x)
      Here too x stands for any variable, c stands for any individual constant (or complex term without variables), and S(c) stands for the result of replacing free occurrences of x in S(x) with c. Note that there may be other occurrences of c in S(x) as well.”
      So, take your 2, lop off the quantifier you introduced via E intro and you get ‘Ex(Rxx)’. But there’s no free variables in this formula (see p. 234 #8 in their definition of free and bound variables). Thus, 1 is not “the result of replacing free occurrences of” x in Ex(Rxx) with a, as the rule requires. Doesn’t this exclude your 1-2?

      Like

      Reply
    5. Chad Avatar
      Chad

      Also, it’s ok in the Mates book. Here’s Mates p. 120:
      “EG (Existential generalization) The sentence (Ea)P may be entered on a line if P a/b appears on an earlier line …”
      In your example, (Ea)P is ExExR(xx). So P will be ExR(xx). And P a/b (i.e., the result of replacing every free occurrence of a in P with an occurrence of b) will also be ExR(xx). Since that doesn’t appear on an earlier line in your example, the conclusion doesn’t follow by EG as stated here.

      Like

      Reply
    6. Jon Cogburn Avatar
      Jon Cogburn

      3, and 4-
      Cool!
      I’m going to see how the restriction works in sequent calculus and Prawitz style systems. If I remember right, the standard way in those kinds of systems is a little less Byzantine (at least to an undergraduate student), which is what goofed me and my friend up. I mean it’s a little bit weirdly backwards to state what can count as the premise of the rule in terms of it being a replacement instance of that rule’s conclusion. That’s not how you normally think while working through a Fitch style proof system, even with respect to Existential Introduction.
      As far as I can tell you can get the same restriction with something like I suggested above, in terms of replacing the constant or eigenvariable with a variable proper only if that variable isn’t already bound, which seems more straightforward to me. I think some Prawitz and sequent calculi people do something like that, but I need to look at the presentations, and also make sure that it’s equivalent.
      It’s a little bit of an abuse of newapps to get people to teach me logic. . . Thanks so much for helping out though.
      In any case, the Junior Paker song above is pretty great at least (I just discovered it today), one of the very, very few Beatles covers where the person makes it into something different (most Beatles covers just sound derivative) yet equally worthwhile. Los Lobos’ noble effort actually suffers considerably by comparison.

      Like

      Reply
    7. Michael Kremer Avatar
      Michael Kremer

      Jon: What you call “weirdly backward” is, I think, fairly standard, and has solid motivations. Here’s one way to think of this (which I was taught by Nuel Belnap): the key idea is that of the relation between a generalized formula (whether universal or existential) and its instances. Universal Instantiation takes you from universal formula to any instance; Existential Generalization takes you from any instance to an existential formula. And (x)A and (Ex)A have exactly the same instances. Intuitively a formula At is an instance of a formula (x)A, if At “says about t” exactly what (x)A “says about all x”; and At is an instance of a formula (Ex)A if At “says about t” what (Ex)A “says about some x”. This means that whatever way you have of expressing the relation of generalized formula to instance is going to show up as the relation of premise to conclusion in Universal Instantiation, but as the relation of conclusion to premise in Existential Generalization. More formally, an instance is what you get from a generalized formula by stripping off the outermost quantifier and uniformly replacing all occurrences of the variable that was previously bound with a suitable term. If we write A[x/t] for the result of replacing all the free occurrences of x in A with t, then the instances of (x)A, also the instances of (Ex)A, are the formulas A[x/t] for suitable terms t. [The reference to “suitable terms” is because we have to be careful in the case in which the term t itself contains variables, but if we only use terms without variables to make instances, as Barwise and Etchemendy do, we avoid those complications. The complications themselves fall out of the intuitive account I just gave: if t contains a variable y which would “get bound” in substituting t for x to yield A[x/t], then A[x/t] does not “say the same thing about t” that (Ex)A says about some x, so this is not an instance. For example, it we have (x)(Ey)~Rxy, then we can’t get an instance of this by substituting y for x in (Ey)~Rxy. (Ey)~Rxy[x/y] is (Ey)~Ryy which does not “say the same thing about y that (x)(Ey)~Rxy says about all x — because (Ey)~Ryy doesn’t say anything “about y” at all, as y is bound and not free in that formula. So we can’t use UI to argue (x)(Ey)~Rxy, therefore (Ey)~Ryy — which is good because this is invalid, as we can see by replacing “R” with “=”. Similarly, we can’t see (y)Rxy[x/y] as an instance of (Ex)(y)Rxy, because the first does not “say about y” what the second “says about some x” — again because the first is (y)Ryy, which says nothing at all “about y” since there is no free y in it. But again this blocks an invalid inference: we can’t infer from (y)Ryy to (Ex)(y)Ryy, which is again a good thing — again replace “R” with “=”.]
      Sorry for the lengthy explanation; I hope it helps to see the motivation for this way of looking at things. There is a model-theoretic reason for looking at it this way as well, which is found in the proof of the soundness of the rules of existential generalization and universal instantiation, through the substitution lemma. Another way to see that something like this is expected is through the duality of (Ex) and (x), and this is more proof-theoretical; if we define (Ex)A as ~(x)~A we can then derive EG from UI, and when we look at it this way we will again expect that the relationf premise to conclusion in UI should be the relation of conclusion to premise in EG.

      Like

      Reply
    8. jdkbrown Avatar
      jdkbrown

      Jon,
      Perhaps I’m misunderstanding your proposed restriction, but wouldn’t it invalidate the following?
      1. (Fa & ExGx)
      2. Ex(Fx & ExGx) 1, E intro

      Like

      Reply
    9. Michael Kremer Avatar
      Michael Kremer

      Addition to my previous comment: “fairly standard” (I think I said — my post isn’t up yet) is too strong; I realize many texts don’t do things this way. Maybe I am influenced by model theory too much. But the motivation I sketched is, I think, useful and sound.

      Like

      Reply
    10. Jon Cogburn Avatar
      Jon Cogburn

      jdkbrown,
      Yeah, that was sloppy. I should have said ExP[a/x] follows from P[a] as long as the replacing variable x is not bound in P[a/x].

      Like

      Reply
    11. Jon Cogburn Avatar
      Jon Cogburn

      Michael,
      Thank you. That’s extremely illuminating. Once the duality is clear the restriction doesn’t look backwards with respect to existential.
      I didn’t see the duality because (if I remember right) in systems like Barwise/Etchemendy there’s a strict divide between individual constants and eigenvariables on the one hand and variables which get bound by quantifiers on the other. Since universal elimination only allows you to replace variables with proper names/eigenvariables the analog that you illustrate above is prevented without having to make an explicit restriction (I think this is right, I need to check their universal elimination rule).

      Like

      Reply

    Leave a comment