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.

Free variables :$a_0,a_1,\cdots $
Bounded variables :$x_0,x_1,\cdots $
Functions:$f_0,f_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$

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.

  • 1
    $\begingroup$ You are right: Basically "... is true" is not part of the formal language but is a property of interpreted formulas: thus, it is a "meta-" property. The symbol is a way to state the usual $\mathcal M \vDash \Gamma$, where $\Gamma$ is a set of formulas and $\mathcal M$ is a model (a structure that intepret the language) $\endgroup$ May 24, 2021 at 12:25
  • 1
    $\begingroup$ Alternatively, if $\Phi$ is a finite set of formulas, $\land \Phi$ usually means the conjunction of the formulas of the set. $\endgroup$ May 24, 2021 at 12:26
  • 1
    $\begingroup$ You may consider also Infinitary Logic $\endgroup$ May 24, 2021 at 12:31
  • $\begingroup$ For more details, please give us the reference to the paper. $\endgroup$ May 24, 2021 at 12:31
  • $\begingroup$ @Mauro ALLEGRANZA Thank you for your remarks. I did not know about infinitary logic. I'm sorry for my misleading remarks. The authors intended to give ,for example, $\land \{ A_i| i = 0,1,2 \cdots \} $ a meaning like $A_0 \land A_1 \land \cdots$. So, I think this is infinitary logic. I am wrong. Thank you. This is the reference: Game logic and its applications I $\endgroup$
    – Saito
    May 24, 2021 at 13:26

1 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).


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .