About formulas $\wedge \Phi$, $\vee \Phi$, where $\Phi$ is a set of formulas.

Question

I am reading some papers on game theory and mathematical logic. I have some questions about the formalized system in the papers. The following is the system.

Language:
Free variables :$a_0,a_1,\cdots $
Bounded variables :$x_0,x_1,\cdots $
Functions:$f_0,f_1 \cdots$
Predicates:$P_0,P_1,\cdots$
Knowledge operators: $K_1,K_2,\cdots$ (These are not important and I will ignore them in my questions.)
Logical connectives:$\neg ,\supset (implies),\wedge, \vee, \forall, \exists$
Parentheses:$(,)$

Then, terms are defined in the standard way. And so are formulas with respect to $\neg ,\supset , \forall, \exists$ . But things are different for $\wedge ,\vee$.

Let $ \mathcal{P}_0$ be the set of all formulas generated by the above standard definition with respect to $\neg ,\supset , \forall, \exists$ and $\Phi$ be a subset of $ \mathcal{P}_0$ (satisfying some property). The authors intended to introduce formulas $\wedge \Phi$ and $\vee \Phi$, whose intended meaning is "for all $A \in \Phi, A$ is true."

Here, I have a question. I think neither $\wedge \Phi$ nor $\vee \Phi$ is a expression. So, neither $\wedge \Phi$ nor $\vee \Phi$ can be a formula. $\Phi$ is a meta-level concept and then cannot be treated (easily) in the formalized system.

please give me some advices.

Answer 1

There are two possibilities:

1. If $\Phi$ is a finite set of formulas, $\land \Phi$ can be viewed simply as a recipe for constructing an actual formula by placing $\land$ between all of them. That is, $\land\Phi$ is an expression at the meta-level whose value is a logical formula. That's not too unlike writing, say, "$\varphi\land\psi$" in first-order logic even though our concept of formula doesn't recognize the symbols $\varphi$ and $\psi$ -- we understand that $\varphi$ and $\psi$ are names of particular formulas and we're supposed to join those by a $\land$.

2. If $\Phi$ is infinite that doesn't work. In that case we'll have to interpret $\land\Phi$ as a new kind of connective that has infinitely many subformulas. This leads to infinitary logic (link courtesy of Mauro). It brings with it some mostly trivial representational challenges -- a "formula" cannot be a linear string of symbols anymore, and we have to use some other way of representing an infinitely-branching tree for it -- but as long as the depth of formulas is still finite, you can define truth relative to structures for them in a quite recognizable way. Proofs must become infinitary objects too. Some of the results of ordinary finite proof theory carry over, while others do not (the compactness theorem goes down the drain, for example).