How to prove a mathematical logical problem with predicates?

[Xamaa]

1 Prove that the following argument is coherent, that is, based on the premises, draw the conclusion: Every city with more than 5 million inhabitants is a metropolis. ABC is a city with more than 5 million inhabitants. There is some city that is a metropolis.

I'm trying this:

∀x (City with more than 5 million inhabitants (ABC, x) → is a metropolis (x, ABC)
(metropolis (ABC)

1.∀x (City with more than 5 million inhabitants (ABC, x) → is a metropolis premise (x, ABC)

City with more than 5 million inhabitants (ABC) premisse
(ABC) is a metropolis premisse

City with more than 5 million inhabitants (ABC) → is a metropolis S x over ABC (1)
4, (ABC) is metropolis MP(3.2)

 

[TeethWhitener]

A few things:
1. The form of your post is very difficult to follow. You have a 1, a 4, but no 2 or 3. You have things labeled as premises in very odd (and likely incorrect) ways. I would lay out everything a little more cleanly than this if I were you.
2. This looks like a homework problem. I'll ping a mentor to get it moved into the homework section.
3. For problems where you have quantifiers with no free variables along with specific instantiations, you're going to need to do introduction and elimination of quantifiers at some point in your argument.

 

[Kavi]

I cant remember the exact syntax rules but I think you have to use contradiction to prove these. It will go like this:

1. Premise: ForAll x If x pop > 5mill then x is a metro
2. Premise: ThereExist y such that pop y > 5mill
3. ASSUME: Not Exists z such that z is a metro
4. From 3 therefore, For All z z is not a metro
5. From 3,1 For all z, z <= 5mill
6. From 5,2 Contradiction
7. Therefore NOT 3

This is a box proof where you make an assumption and show it leads to a contradiction.

 

[TeethWhitener]

I cant remember the exact syntax rules but I think you have to use contradiction to prove these. It will go like this:

1. Premise: ForAll x If x pop > 5mill then x is a metro
2. Premise: ThereExist y such that pop y > 5mill
3. ASSUME: Not Exists z such that z is a metro
4. From 3 therefore, For All z z is not a metro
5. From 3,1 For all z, z <= 5mill
6. From 5,2 Contradiction
7. Therefore NOT 3

This is a box proof where you make an assumption and show it leads to a contradiction.

You definitely don't need to assume a contradiction. Also, 2 is not a premise. 2 can be derived from the premise "ABC is a city with more than 5 million inhabitants" by using existential introduction:
##P(a)\vdash\exists x P(x)##
but this is also not necessary in the proof.

 

[Kavi]

You definitely don't need to assume a contradiction. Also, 2 is not a premise. 2 can be derived from the premise "ABC is a city with more than 5 million inhabitants" by using existential introduction:
##P(a)\vdash\exists x P(x)##
but this is also not necessary in the proof.

It was a long time since I studied this but from the OPs wording

PREMISE1: Every city with more than 5 million inhabitants is a metropolis.
PREMISE2: ABC is a city with more than 5 million inhabitants.
CONCLUSION: There is some city that is a metropolis.

(Edit: Ok I understand, I think I maybe missed a formal step, I just took 2. as a premise instead of deriving it from the rule you posted but as I mentioned I cant remember all the exact details)

I still think it must be proven by contradiction but i cant remember for sure...

 

[Xamaa]

Thanks guys for your precious time, the query has been solved now. Really Appreciated.... .

 

[WWGD]

IIRC, you need to use instantiation, as used in FOL.