# An exercise on first order logic formulas, terms and Polish notation

This is part of my homework (not mandatory and not accredited).

Please comment/answer if my reasoning for the exercises is correct, because I'd like to see if I understand the material.

I will start with the axioms to show what I am working with:

(T1) Every variable is a term
(T2) Every constant symbol is a term
(T3) An expression of the form $$F(t_1, \dots , t_n)$$ where $$f$$ is an $$n-$$ary function symbol and $$t_1, \dots , t_n$$ are terms, is again a term

(F1) Are $$t_1,t_2$$ terms, then $$t_1=t_2$$ is also a formula
(F2) Are $$t_1, \dots , t_n$$ terms and is $$R$$ an $$n-$$ary relation symbol, then $$R(t_1, \dots , t_n)$$ is a formula
(F3) Is $$\varphi$$ a formula, then $$\neg \varphi$$ is also a formula
(F4) Are $$\varphi, \phi$$ formulas, then so are $$(\varphi \wedge \phi) ,( \varphi \vee \phi), (\varphi \to \phi), (\varphi \leftrightarrow \phi)$$
(F5) Is $$\varphi$$ a formula and $$x$$ a variable, then $$\forall x \varphi$$ and $$\exists x \varphi$$ is a formula

Exercise: Let $$F_1$$ be a $$1$$-ary, $$F_2$$ a $$2$$-ary, and $$F_3$$ a $$3$$-ary Function symbol. Let $$R_2$$ be a $$2$$-ary Relation symbol, $$c$$ a constant symbol and $$x,y,z$$ variables. Which of the following are syntactic correct terms or formulas? \begin{align}a) \ &F_3xF_3yF_3zF_2xF_1zzcc \\ b) \ & \neg \neg \neg\exists x \neg (( y = F_3xF_1y) \vee (x=x)) \\ c) \ & \forall x \neg(c=x) \vee \exists c(c=x)\end{align} My answer (or ideas):

$$\cdot$$ For a) I thought because I have troubles reading the Polish notation I should convert it into the notation I am used to.

My problem is now I don't know the rules to do that, my intuitive approach was to go from the inside to the outside, meaning I'd start with $$F_1$$ and associate one term to it and then continue with $$F_2$$, associate two terms to it and so on. With that logic I'd obtain: $$F_3xF_3yF_3zF_2xF_1zzcc = F_3\Bigg(x,F_3\bigg(y,F_3\Big(z,F_2\big(x,F_1(z)\big),z\Big),c\bigg),c\Bigg)$$ Edit: So the above term should be correct, we obtain a term again.

$$\cdot$$ For b) Unlike as above, the Polish notation $$F_3xF_1y$$ seems not well defined

$$\cdot$$ c) This is a correct formula.

a) looks fine. Another method would consist of assigning

1. -1 to all constant and variable symbols.
2. 0 to $F_1$ or any 1-ary
3. 1 to $F_2$ or any 2-ary
4. 2 to $F_3$ or any 3-ary

Then you sum those values as they appear in the sequence. If the only sum which equals -1 occurs corresponding to the very last symbol, and the very last symbol corresponds to -1, then you have a formula or term. Otherwise you don't have a formula. For your string this works out as follows:

 F3|  x| F3| y| F3| z| F2| x| F1| z| z| c|  c

2 |  1| 3 | 2| 4 | 3| 4 | 3| 3 | 2| 1| 0| -1


And thus you have a term.

"b) Unlike as above, the Polish notation F3xF1y seems not well defined"

If you use the above suggestion we have

 F3  x  F1  y

2   1  1   0


And thus, F$_3$xF$_1$y is not well-defined. We could also reason that F3 is a 3-ary function symbol, but we only have two arguments for that function "x" and "F$_1$y", and thus F$_3$xF$_1$y is not well-formed.

"c) This is a correct formula. "

No, it's not. Notice that c) is "∀x¬(c=x)∨∃c(c=x)". You have an "V" symbol. The only time "V" gets mentioned in the definition lies in clause F4.

"Are φ,Φ formulas, then so are (φ∧Φ),(φ∨Φ),(φ→Φ),(φ↔Φ)"

There does not exist a left-parenthetical symbol "(" before "∀", and a right-parenthetical symbol ")" after the second ")" in "∀x¬(c=x)∨∃c(c=x)".

(∀x¬(c=x)∨∃c(c=x)) would qualify as correct.

• This is a great answer, I appreciate it, thanks a lot for pointing out the importance of the parenthesis! – Spaced Sep 24 '14 at 17:50
• I just realized that c) can't be correct due to (F5) as well, because $\exists c$ where $c$ is a constant symbol is not well defined. Is that right? – Spaced Sep 24 '14 at 18:52
• @Spaced It looks like it's not according to that definition. However, from what I can tell usually quantification over constant symbols is allowed. – Doug Spoonwood Sep 24 '14 at 20:07