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

Question

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.

Answer 1

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.