1
$\begingroup$

I am very new to logic and currently taking a course about it but unfortunately it's a weekend now so I can't get the answers I need!

Basically I am wondering a very basic thing. I want to prove something with natural deduction and let's say I have this premise:

Ok so let's start the question, here's an example but not a full example, just a short bit:

$$\forall x\forall y\big(A(x)\to B(y)\big)\qquad\text{(premise)}$$

So we got these two variables $x$ and $y$ and then just get rid of the quantifiers and replace the variables with two arbitrary constants just like the rule says:

$$A(c)\to B(d)$$

Okay now for the question... Let's also say that I have another premise, or perhaps just an assumption even, that says:

$$A(d)$$

Would it be usable with $A(c)$? Like, could I use the modus ponens rule like this:

$$A(d)\quad A(c) \to B(d)$$

The two constants $d$ and $c$ are different. I'mma guess the answer to this question is in fact "no" but it's something that keeps bothering me (because I always go like "Hmm but I can do this to appl--Oh... Guess not...)" and I just want to 100% make sure it's not possible since I am absolutely horrible at this subject!

  • 0
    IIRC, you are allowed to choose _any_ constant/term for replacing the bound variable. In particular, you may pick $c = d$.2012-10-19
  • 1
    You can use $\TeX$ on this site by enclosing formulas in dollar signs: single dollar signs for inline formulas and double dollar signs for displayed equations. You can see the source code for any math formatting you see on this site by right-clicking on it and selecting ‘Show Math As:TeX Commands’. [Here’s](http://meta.math.stackexchange.com/questions/5020/mathjax-basic-tutorial-and-quick-reference) a basic tutorial and quick reference. There’s an ‘edit’ link under the question.2012-10-19
  • 0
    You can but just to note, you cannot use a constant already in use for $\exists$2012-10-19

3 Answers 3

0

In natural deduction, you may deduce $P(t)$ from $\forall x\: P(x)$ for arbitrary terms $t$.

Thus, in your case, you can deduce $A(d) \rightarrow B(d)$ from $\forall x\forall y\: (A(x)\rightarrow B(y))$, and then use the premise $A(d)$ to deduce $B(d)$.

You can generalize that by instead deducing $A(d) \rightarrow B(t)$ from $\forall x\forall y\: (A(x)\rightarrow B(y))$ ($t$ is again some arbitrary term), and then use $A(d)$ to deduce $B(t)$.

0

Let's be absolutely clear. In a standard Natural Deduction system you can only "get rid of" -- better, instantiate -- one quantifier at a time (the outermost, initial one). However, from $$\forall y\big(A(x)\to B(y)\big)$$ you can infer e.g. $$ \forall y\big(A(d)\to B(y)\big)$$ And now you can use the universal quantifier instantiation rule again, and again -- just as in the first case -- that rule allows you to instantiate with any constant, so you can use $d$ again, to get $$\big(A(d)\to B(d)\big).$$

-1

Couldn't you just get rid of the quantifiers with $A(d) \to B(d)$ as well? I mean, it's true for ALL $x$ and $y$... but presumably $A(c)$ and $A(d)$ are different, so you couldn't just use what you wrote. Luckily your initial premise is very, very flexible!

  • 0
    Umm, i.e. I was trying to be gentle to the original poster. Note in particular that my answer has the identical solution to your comment, but phrased far more conversationally. I hope that isn't usually worth a demerit.2012-10-19
  • 1
    I apologise, then. My comment should give you an indication that you have been too vague, though. IMHO, being "conversational" can be very dangerous in logic; before one notices, things which are "intuitive" get phrased _just_ wrong, and aren't valid. Not to mention the problems with this approach when one delves into the realms of intuitionistic logic.2012-10-19