(A) A negative number times a negative number always equals a positive number.

I have been trying to symbolize and prove (A) however I am not sure if I have got it right, transcription-wise and proof-wise as well.

Transcription of (A) in FOL: ∀x∀y∃z((Nx ∧ Ny ∧ Txy) → Nz); "T" stands for times, as in x times y.

An English version of the transcription above: For all negative numbers x and y, there exists an z, such that, if x and y are negative numbers and whenever x is multiplied by y, then there exists a value of x and y which is a negative number z

1. Assume: ~∀x∀y∃z((Nx ∧ Ny ∧ Txy) → Nz)
2. ∃x~∀y∃z((Nx ∧ Ny ∧ Txy) → Nz)
3. ~∀y∃z((Na ∧ Ny ∧ Tay) → Nz)
4. ∃y~∃z((Na ∧ Ny ∧ Tay) → Nz)
5. ~∃z((Na ∧ Nb ∧ Tab) → Nz)
6. ∀z~((Na ∧ Nb ∧ Tab) → Nz)
7. ~((Na ∧ Nb ∧ Tab) → Na)
8. ~((Na ∧ Nb ∧ Tab) → Nb)
9. (Na ∧ Nb ∧ Tab)
10. ~Na
11. Na
12. So, ∀x∀y∃z((Nx ∧ Ny ∧ Txy) → Nz)

Since I am unsure of its transcription adequacy, I've transcribed it in an alternative way: ∀x(Nx → ∀y∃z((Ny ∧ Txy) → Nz)), without proof, however. What seems to me to be the problem is my confusion in transcribing "x times y" and transcribing it such that it yields z. So it feels like I've mistakenly used a relation predicate instead of a function. This made me think of another possible transcription, namely: ∀x∀y∃z((Nx ∧ Ny ∧ T(x,y) = Nz), since that's how I've seen a function being symbolized, however, I am clueless as to how one would go about proving that proposition. I also thought about symbolizing "always" as a necessity symbol of Modal Logic or biconditional of FOL, but, again, I would be clueless as how to prove such propositions.

Can anyone kindly shed light on my present bewilderment?

  • 1
    See this lecture note – Mauro ALLEGRANZA Jun 13 '14 at 10:10
  • Steps 9 and 10 have been simplified from Step 7. Thanks for the link! – Kas Jun 13 '14 at 10:19
  • 2
    from Courant & Robbins, p. 55: "It took a long time for mathematicians to realize that [this] 'rule of signs', together with all the other definitions governing negative integers and fractions cannot be 'proved'. They are created by us in order to attain freedom of operation while preserving the fundamental laws of arithmetic. What can—and must—be proved is only that on the basis of these definitions the commutative, associative, and distributive laws of arithmetic are preserved." You cannot prove (A) because we can interpret 'N','T', etc. in it so that (A) becomes false. – Hunan Rostomyan Jun 13 '14 at 16:37

There's a problem in your translation. Let's forget about the quantifiers for the bit, and ask how to translate 'if a is negative and b is negative then a x b is positive'.

You have something like:

Na & Nb & Tab → ¬Nc

But where does c come from? We want to say that c is the result of multiplying a and b, and Tab doesn't tell us this.

Instead, we need a ternary relation to say 'a x b is c', let's call that 'Tabc'.

Then, we get as the translation of 'if a is negative and b is negative then a x b is positive' the following:

∀x(Na & Nb & Tabx → ¬Nx)

(Why do we need the quantifier? Because, for all we've said about T, it might be that more than one number is the result of multiplying a and b. Ideally, we'd want to write down some more sentences which tell us that there's always exactly one answer.)

Then to translate that the product of any negative numbers is positive, we do:

(1) ∀x∀y∀z(Nx & Ny & Txyz → ¬Nz)

A functional approach

Alternatively, we can consider versions of logic which feature function symbols. A n-ary function symbol f (compared with an n-ary predicate) is such that, whenever a1,...,an are terms (e.g. variables or constants) then f(a1,...,an) is a term as well.

It's then very natural to translate your sentence into a language with a function for multiplication. We let T be a binary function so that 'T(x,y)' means 'x times y' (in fact, given this, we can straightforwardly abbreviate this as x x y).

Then the translation of the sentence would be much simpler:

(2) ∀x ∀y( Nx & Ny → ¬N(T(x,y)))

Proving these

Now, how would we prove either of these? The answer is, we can't, not if we're trying to do a proof in pure logic, as you are trying to. That's because the fact that (1) and (2) are true is not a matter of pure logic – that is, it is not a matter purely of the form of the sentences. Instead, it depends on the details of what 'times' and 'negative' mean. (Suppose, for example, that 'N' meant 'is negative', but 'T' meant addition. Then (1) and (2) would be false.)

In order to prove (1) and (2), we need additional facts about negativeness and multiplication, probably in the form of axioms. These will tell us what the properties of these predicates and functions are. We would then use these axioms as additional premises in the proof.

We could try to give some such axioms directly, but it probably wouldn't be very interesting. The reason is that, if we want to give some very basic principles about how these interact, the chances are that something like (1) or (2) would appear in our axioms, so the proof would be a boring one liner.

A more interesting proof – and one which is much closer to how it would actually be done – would be to select some axioms for arithmetic in general, such as the [http://en.wikipedia.org/wiki/Peano_axioms][Peano Axioms].* From these, we then define 'negative' and 'times' [but see edit below], and then prove (1) or (2) (depending on whether we've defined 'times' as a predicate or a function).

.* Actually, the Peano Axioms won't really do without a lot of additional work. The reason is that they're only about positive numbers, but we obviously want to say something about negative numbers. We could either move towards a set of axioms which also tells us about negative numbers, or we could do some tricks to define negative numbers within the positive numbers (this sounds weird, but it can be done in strange ways).

EDIT: Rereading this old-ish answer of mine, I notice I've made a mistake. In particular, in the (first-order) Peano axioms we can't define multiplication. Instead, we need to take multiplication and primitive together with some corresponding axioms. In second-order Peano arithmetic, we can, however, define multiplication as repeated addition.

  • Very interesting. Seems like it slipped right out of my mind to prefix a negation sign to the third subformula (Nz), after all the end-result is supposed to be a positive number. Stuff about not being able to prove the proposition out of thin air so to speak made perfect sense. I have some reading to do now! Thanks a lot! – Kas Jun 13 '14 at 10:06
  • 1
    No problem! But note that the missing negation sign isn't the main point - its the need for a ternary relation or a binary function (which is why I glossed over the negation issue). – J.P. Jun 13 '14 at 10:09

Not the answer you're looking for? Browse other questions tagged or ask your own question.