$\newcommand{L}{\mathcal{L}} \newcommand{A}{\mathcal{A}} \newcommand{Trm}{\operatorname{Trm}} \newcommand{Frm}{\operatorname{Frm}}$
I am reading the first order logic (FOL) section in the Open Logic Project book, and I have three questions which are boldened below. So far, I have read up to where they have defined the syntax for a FOL: it consists of a set of logical symbols, non-logical symbols, and punctuation symbols.
The logical symbols are:
- The logical connectives: $\neg, \land, \lor, \to, \leftrightarrow, \forall, \exists$
- The true and false constants: $\top$ and $\bot$, respectively.
- The 2-place identity predicate: $=$
- A countable set of variables: $v_0, v_1, v_2, \dots$
The non-logical symbols are:
- For each positive integer $n$, a countable set of $n$-place predicates $A_0^n, A_1^n, A_2^n, \dots$
- A countable set of constants $c_0, c_1, c_2, \dots$
- For each positive integer $n$, a countable set of $n$-place functions $f_0^n, f_1^n, f_2^n, \dots$
The punctuation symbols (which I separate with ${\color{red},}$ for clarity) are $({\color{red},} ){\color{red},} ,$
Question #1: Is it true that the logical symbols are common to all FOLs (and hence is a requirement for a language to be considered a FOL) and the non-logical symbols are up to a particular FOL's choosing (in which case, the non-logical symbols specified above are those of the standard first-order language's)?
Once a first order language $\L$ is specified, one inductively defines the set of terms $\Trm(\L)$ and (well-formed) formulas $\Frm(\L)$ of the language. Specifically, a term is defined by:
- Every variable in $\L$ is a term of $\L$.
- Every constant in $\L$ is a term of $\L$.
- If $f$ is an $n$-place function of $\L$ and $t_1, \dots, t_n$ are terms of $\L$, then $f(t_1, \dots, t_n)$ is a term of $\L$.
and a formula is defined by:
- $\top$ and $\bot$ are both (atomic) formulas of $\L$.
- If $R$ is an $n$-place predicate of $\L$ and $t_1, \dots, t_n$ are terms of $\L$, then $R(t_1, \dots, t_n)$ is a (atomic) formula of $\L$.
- If $t_1$ and $t_2$ are terms of $\L$, then ${=}(t_1, t_2)$ is a (atomic) formula of $\L$. It is commonly written as $t_1 = t_2$, and the same is common with other $2$-place predicates/functions.
- If $\varphi, \psi$ are formulas of $\L$ and $v_n$ is a variable of $\L$, then the following are all also formulas of $\L$: $\neg \varphi$, $(\varphi \land \psi)$, $(\varphi \lor \psi)$, $(\varphi \to \psi)$, $(\varphi \leftrightarrow \psi)$, $\forall x~\varphi$, $\exists x~\varphi$.
Question #2: How easily extendable are the above definitions to those of a second-order logic? Is it a matter of adding quantifying over predicates to (4) above?
Once these are defined, the following lemma is given:

Question #3: What is a property? Up until now this was never defined.
Edit: I apologize for including three questions in one post, I was not aware this was bad practice, and so I will not do this in the future. Though for the time being, I am more than happy with answers to individual questions if anyone has them.