 As it stands, Tarski’s definition of satisfaction is not an explicit definition, because satisfaction for one formula is defined in terms of satisfaction for other formulas. So to show that it is formally correct, we need a way of converting it to an explicit definition. One way to do this is as follows, using either higher order logic or set theory. Suppose we write \(S\) for a binary relation between assignments and formulas. We say that \(S\) is a satisfaction relation if for every formula \(G, S\) meets the conditions put for satisfaction of \(G\) by Tarski’s definition. For example, if \(G\) is ‘\(G_1\) and \(G_2\)’, \(S\) should satisfy the following condition for every assignment \(a\):