# Very simple predicate logic deduction question

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!

-
IIRC, you are allowed to choose any constant/term for replacing the bound variable. In particular, you may pick $c = d$. – Lord_Farin Oct 19 '12 at 15:36
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 a basic tutorial and quick reference. There’s an ‘edit’ link under the question. – Brian M. Scott Oct 19 '12 at 15:38
You can but just to note, you cannot use a constant already in use for $\exists$ – hmmmm Oct 19 '12 at 18:59

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)$.

-

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).$$

-

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!

-
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. – kcrisman Oct 19 '12 at 15:49
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. – Lord_Farin Oct 19 '12 at 15:54