@F.Zer That's right! If there are at least 5 vertices satisfying the given conditions, then there is a triangle.

So indeed, first prove that ∃x,y,z,w,t∈V ( true ) ⇒ ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x ), and then when you're done you can use that result to prove (Q9).

@F.Zer Do note that you technically cannot use x,y,z,w,t for that ∃elim since they are not fresh. But of course it's easy to fix that.

I need help regarding this question which is included in “A Friendly Introduction to Mathematical Logic”

Q.: Let’s work out a language for elementary trigonometry. To get you started, let us suggest that you start off with lots of constant symbols — one for each real number. It is tempting to use the symbol 7 to stand for the number seven, but this runs into problems. (Do you see why this is illegal? 7, 77, 7/3...)

Cont... Now, what functions would you like to discuss? Think of symbols for them. What are the arities of your functions symbols? Do not forget that you need symbols for addition and multiplication! What relation symbols would you like to use?

My attempt: I really cannot understand the problem that we will run into for using symbol 7 for number seven.

For the part “what functions would you like to discuss” my answer would be: < +, •, /> where • stands for multiplication and / for fraction. The trigonometry will involve lots of fractions, so, I included /

The arities of all of them is two, because they can be operated only with objects at a time.

And the relational symbols I would use are <, > (greater than and less than symbols)

@ConGovDeIn Whoever wrote that ("this runs into problems") does not make much sense. Obviously in any proper FOL language you do not have juxtaposition.

So there is absolutely nothing wrong with having "7" as a constant-symbol.

"77" would simply be illegal in a proper FOL language.

The author really has no valid argument here. If the author attempts to argue that we will have trouble with numerals beyond 9, that attempt is doomed because we can simply have a single symbol for each integer, even for those more than 9. There is absolutely no problem with that; encoding into ASCII strings is not a problem with FOL.

Moreover, the author failed to realize that we already face encoding issues with variable names if we want to encode FOL into ASCII strings, since FOL must support at least countably many distinct variable names.

@user21820 Because one symbol is contained in the other?

Read all my comments first.

It's not about "contained in another". "77" is simply not a single symbol in a proper FOL language.

Don't confuse FOL with an encoding of FOL.

As for the question itself (language for elementary trigonometry), I would say that it is too nebulous to have a good answer. It depends heavily on what really you want to achieve. But for sure you're missing something to express the basic trigonometric functions.

“Don’t confuse FOL with an encoding of FOL” would you explain that with an example?

@ConGovDeIn I already gave you an example; variable names...

In say ASCII you have 256 symbols, so you certainly need some form of encoding scheme to support infinitely many variable names.

This kind of thing is best learnt by actually doing. Come up with your own encoding scheme that allows you to represent every pure FOL formula by a unique ASCII string, such that you can (in theory) implement a proof checker for your encoding.

When you've actually done so, you'll grasp what I was telling you earlier.

I will surely follow your advice.

can you please let me have a look of how would you formulate a language for trigonometry?

@user21820 Thank you ! I see the predicate "c" does not appear in the antecedent "∃ x,y,z,w,t∈V ( true )". Is it possible to prove a sentence like "∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x )" using only that ?

Also, all of those five objects could be the same one, right ? The antecedent is not restricting that possibility.

@F.Zer Maybe what I wrote earlier was misleading. I said "satisfying the given conditions", so I meant you need to prove that statement under the given conditions.

@F.Zer Hang on; you're right, I forgot that all five could be the same, so that won't work.

So yea, your proof outline won't work, because you really need "at least 5 vertices satisfying the given conditions".

@user21820 Good. I will try another route. Which are the given conditions ?

In the question itself.

What do you mean by "another route"? As I said, it's because you mistranslated "at least 5".

@user21820 5 vertices that satisfy the antecedent ? ∀x,y∈V ( c(x,y) ⇒ c(y,x) ) ∧ ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) )

I am missing something, I think.

@user21820 Got it.

@user21820 I think the given conditions are those two.

@F.Zer Yes.

@ConGovDeIn As you noticed, we need basic arithmetic. Note that if you include division you will have to face the issue of allowing division by 0, because FOL demands that every binary function can be applied to any two objects in the domain. In your axiomatization you need at least the ordered field axioms for real numbers. If you add division, you could add the axiom ∀x ( x≠0 ⇒ x·(y/x)=y ). You also need function-symbols representing the trigonometric functions you want to talk about.

Note that there is no trouble if y/0 is defined, because the axiom I stated does not assert anything about y/0.

@user21820 My translation of "at least 5 (different) vertices satisfying the given conditions" would be: ∃ x,y,z,w,t∈V ( x ≠ y ∧ y ≠ z ∧ z ≠ w ∧ w ≠ t ∧ x ≠ z ∧ x ≠ w ∧ x ≠ t ∧ y ≠ w ∧ y ≠ t ∧ z ≠ t) ∧ ∀x,y∈V ( c(x,y) ⇒ c(y,x) ) ∧ ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) )

@F.Zer Very good. Yes.

Thank you.

@user21820, is there any restriction about using the same name for an object and a function symbol ? I mean, there is the "c" predicate; can I introduce the name "c" for an object of V ?

@F.Zer Well of course you can't. In the first place, variable names are distinct from function/predicate-symbols. In the second place, why would you want to confuse yourself by having the same name for different things?

But if you're asking about rules, yes that's certainly a rule in any complete description of a formal FOL deductive system. Things like that don't get mentioned in my post only because they would just bloat the whole thing up.

Excellent. Makes absolute sense.

I mean, when it comes down to actually implementing a formal system for FOL, you get plenty of headaches that have got nothing to do with FOL. So yea.

Anyway I'm off.

See you!

@user21820 Oh, I remember reading once about that. There is some setup like: variables are lower-case letters a...z, uppercase letters denote..., and so on

@user21820 Goodbye. See you !

@F.Zer That may be what you can get by for FOL used in a single book, but it certainly isn't full FOL. As I mentioned to the other visitor just now, true FOL needs to support infinitely many variable names, so just a to z isn't enough.

We're just lucky that we don't often need more than 26 variables.

Alright, bye!

@user21820 Perfect. Understood.

@user21820, just finished my first proof skeleton of the translated statement. Could you tell me what do you think ?

If ∃ x,y,z,w,t∈V ( x ≠ y ∧ y ≠ z ∧ z ≠ w ∧ w ≠ t ∧ x ≠ z ∧ x ≠ w ∧ x ≠ t ∧ y ≠ w ∧ y ≠ t ∧ z ≠ t) ∧ ∀x,y∈V ( c(x,y) ⇒ c(y,x) ) ∧ ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) ):
	∃ x,y,z,w,t∈V ( x ≠ y ∧ y ≠ z ∧ z ≠ w ∧ w ≠ t ∧ x ≠ z ∧ x ≠ w ∧ x ≠ t ∧ y ≠ w ∧ y ≠ t ∧ z ≠ t)
	∀ x,y∈V ( c(x,y) ⇒ c(y,x) )
	∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) )
	c(a, b) ⋁ c(b, c') ⋁ c(c', a)
	c(b, c') ⋁ c(c', a) ⋁ c(a, b)
	c(c', a) ⋁ c(a, b) ⋁ c(b, c')
	If c(a, b):
		If c(b, c'):
			If c(c', a):
			If c(a, b):
			If c(b, c'):