[General boards] [Fall 2018 courses] [Summer 2018 courses] [Winter 2018 courses] [Older or newer terms]

A bit confused with the final question of the first test

#1

This is the answer to the final question.
Where is that “Let …” sentence coming from? I never see this syntax in a formal proof in the book or the lecture. (I haven’t read all the parts of the solution though)
I suppose I should write a formal proof and it should be proving

(All the comma here should be a dot)

While instead, the answer has two free variables here. The reason I think the proof in the solution cannot be used to prove the sentence above with quantifier is that as far as I know we have never been introduced some rules like below:

The only way to introduce the universal quantifier is at the back of the book.

#2

The English sentence “Let …” is not part of the formal proof. The way to say that formally is the first line of the formal proof. The first two conjuncts
0: nat ∧ (∀m: nat· 0≤m)
say that 0 is a smallest natural number, and the next two conjuncts say that ∅ is a smallest natural number. From that line we conclude on the last line that 0=∅ .

#3

So in the formal proof part, phi is a very specific natural number right? In other words, the proof is only talking about a specific element [with the property that it is not greater than any natural number] and the proof doesn’t talk about any other element [that is not greater than any natural number], right?

#4

So in the formal proof part, phi is a very specific natural number right?

Right.

In other words, the proof is only talking about a specific element [with the property that it is not greater than any natural number] and the proof doesn’t talk about any other element [that is not greater than any natural number], right?

The proof talks about 0 and ∅, each of which is not greater than any natural number. It concludes that 0=∅.

#5

Ah, I think I have just understood the reason for your question. You are considering ∅ to be a variable, but 0 to be a constant. Now I think I want to change my answer as follows.
§ Let a and b be smallest natural numbers.
a: nat ∧ (∀m: nat· a ≤ m) ∧ b: nat ∧ (∀m: nat· b ≤ m)
Specialize the first ∀ with b for m and specialize the last ∀ with a for m .
⇒ a ≤ b ∧ b ≤ a Now, from a generic law (antisymmetry) we have
⇒ a = b
Now it is clearer that the proof is talking about both a and b, the nonlocal variables of the proof. Thank you for your question.

#6

“Prove that there are not two different natural numbers that are tied for smallest.”
This is the final question of the test.

My question is that I should prove
while in the formal proof you just gave,
I think you can only prove the version without universal quantification, i.e.,
“a: nat ∧ (∀m: nat· a ≤ m) ∧ b: nat ∧ (∀m: nat· b ≤ m) ⇒ a=b”
This version doesn’t have universal quantification.

#7

t.pdf (43.0 KB)