Background
My grasp of propositional logic is pretty good, as is my ability to translate it to and from symbols. Quantificational logic however is a little more challenging. Mostly because I get lost in how to apply the inference rules. I struggle in particular when applying logic to mathematics. Let me give some examples and maybe my difficulties will jump out.
Problem
Use a direct proof to show every odd integer is the difference of two squares.
I translated this into symbols as, $\forall n(n = 2k +1 \implies \exists k,l(n = k^2 – l^2))$ where $n,\ k$ and $l$ are integers.
Some Initial Questions
- Did I translate this correctly?
- In my initial universal quantifier, I sometimes see people write $\forall n \in S\ P(n)$. Is this just another way of specifying the domain so I don't have to say what the domain is after writing everything down in symbols? A kind of shorthand?
- In the book I use they'll nest quantifiers explicitly like $\exists k \exists l\ Q(k, l)$. In my translation I did what I've seen elsewhere which is to do $\exists k,l\ Q(k, l)$ is this okay? And if the answer to Question 2 above was that using the $\in$ shorthand is acceptable, then I'm guessing I could also write this as $\exists k,\ l \in S\ Q(k, l)$.
These are just formatting questions, but they have been bothering me so I wanted to get your input. However, the following is why I'm really here:
I know to begin working on a universally quantified statement I can invoke universal instantiation. My book defines this as $\forall x P(x) \therefore P(c)$. It then goes on with an example of a formal proof using this on the form $\forall x (P(x) \implies Q(x)) \therefore P(a) \implies Q(a)$. How are they applying Universal Instantiation across the $\implies$, when the definition only has a single predicate $P(x)$? Is it that they've set $P(x)$ to mean $P(x) \implies Q(x)$?
I can accept that this is the case, since it appears to be so. However, how do I apply this when doing a mathematical proof? I have no difficulty proving a bunch of generic, non-math arbitrary predicates using these quantificational rules and the other inference rules, but as soon as I apply it to math proofs I don't see how it's used anymore. Especially given the informal nature of math proofs. So for the above problem, how do I instantiate the antecedent $n = 2k + 1$? Isn't this already instantiated? Moreover, according to this application of Universal Instantiation to conditionals, wouldn't I instantiate everything inside of the outermost $\forall n$ quantifier?
For example, I have $$\forall n(n = 2k +1 \implies \exists k,l(n = k^2 – l^2))$$
Using Universal Instantiation I'd have, $n = 2k + 1 \implies \exists k,l(n = k^2 – l^2)$? I think … or have I accidentally/already instantiated them before removing the universal quantifier? It's easy when the predicates are words like $x$ is a student, then I know Universal Instantiation just means I can pick some person (provided the domain is set right) and there I go, I've gotten rid of the universal quantifier and can proceed with the proof. In math, with symbols and such, I don't know when I've actually instantiated something.
The same goes for Existential Instantiation. For this problem, would I apply Universal instantiation first, then existential instantiation to the consequent? But doing so then leaves me begging the question doesn't it? Since using something like direct proof requires I "transform" the antecedent into the conclusion, but I can't just use the consequent out of nowhere to do so, and it seems like this would allow that.
Finally, for direct proof we assume the antecedent is true and try to deduce the consequent. But, doesn't this create the same problem as above? Begging the question that is. Say I have $\forall x (P(x) \implies Q(x))$. Then I use direct proof to assume $P(x)$ is true. Well wouldn't I use Universal instantiation here and have $P(a)$, then using Universal Modus Ponens I could automatically infer $Q(a)$ is true?
I apologize for the lengthy question, but I am really struggling to see the connection between all the logic we have to learn to do math proofs, and then using them for math. I know that we can use the rules of inference, replacement rules (logical equivalences), and mathematical axioms and theorems to make deductions, but the process loses me. I have the formal proof stuff down okay, but the informal stuff kills me. I don't know when I'm actually using or need to use the addition rule of inference or disjunctive syllogism, or whatever. Please help.
Best Answer
No. The oddness needs to be quantified too.
You want $\forall n~\big(\exists k~(n=2k+1)~\to~\exists k~\exists l~(n=k^2-l^2)\big)$
It might be helpful to emphasise that the existance establishing oddness is distinct from the existances establishing sum-of-squares.
$$\forall n~\big(\exists k~(n=2k+1)~\to~\exists a~\exists b~(n=a^2-b^2)\big)$$
You may wish to explicitly indicate the domain of the discussion. $$\forall n\in\Bbb Z~\big(\exists k\in\Bbb Z~(n=2k+1)~\to~\exists a\in\Bbb Z~\exists b\in\Bbb Z~(n=a^2-b^2)\big)$$
As you see, this can clutter the statement when every entity is drawn from the same domain. So if you have established in accompanying text that is the implicit domain is the Integers, there is no need to explicitly indicate it in the statement.
It is a style choice. I prefer explictly quantifying each variable, but again, abbreviating things can reduce clutter
It ... is accepted, as long as you take care to avoid ambiguity.
Yes, you substitute $c$ for $x$ everywhere in the scope of the quantification. Here that is $(P(x)\to Q(x))$. In Universal Elimination (or Instantiation) you are deducing that if something is true about the universal bound variable $x$, then it will be true for an unbound variable $c$. (Or $a$ or whatever.)
No. If $∀x~(P(x)\to Q(x))$ is what you are trying to prove, then you don't have it. You cannot assert that a conclusion is proven inside its own proof.
Your argument should go: Let $a$ be an arbitrary term. Assume $P(a)$ and derive $Q(a)$ by some valid logic. Thus deducing that $P(a)\to Q(a)$, and since $a$ is arbitrary therefore, by Universal Generalisation, $\forall x~(P(x)\to Q(x))$.
In this case:
$$\def\fitch#1#2{\begin{array}{|l}#1 \\\hline #2\end{array}} \fitch{}{\fitch{[m]}{\fitch{\exists k~(m=2k+1)}{\fitch{[b]~m=2b+1}{\fitch{[a]~ b+1}{a^2=b^2+2b+1\\a^2=b^2+m\\m=a^2-b^2\\\exists l~(m=a^2-l^2)\\\exists k~\exists l~(m=k^2-l^2)}\\\exists k~\exists l~(m=k^2-l^2)}\\\exists k~\exists l~(m=k^2-l^2)}\\\exists k~(m=2k+1)\to\exists k~\exists l~(m=k^2-l^2)}\\\forall n~(\exists k~(n=2k+1)\to\exists k~\exists l~(n=k^2-l^2))}$$
Time out ... that's enough for now ... maybe more to come later ...