2

The formal definition of ${\forall}$ is $\left({\forall}x\,{\in}S:P(x)\right)=true :\Leftrightarrow \{x:P(x)=true\}=S$.

This uses $P(x)$, propositional function, whose definition uses the concept of a function.

The definition of function uses the concept of ${\forall}$, however.

So is this definition of ${\forall}$ circular?

Is there any other, non-circular definition of ${\forall}$?

hxcb
  • 21
  • Im not sure if this can help in set-theory, but in Logic, the definition says that if you chose an arbitrary $x$ and then deduce some statement about $x$, say $P(x)$, then you may deduce $P(x)$ for all $x$ – Connor Bishop Mar 19 '16 at 09:33
  • I have never defined $\forall$, and I don't think this makes much sense, since it relies on the definition of equality of sets. But equality of sets is defined using $\forall$. – Crostul Mar 19 '16 at 09:43
  • @Crostul this only true for naive set theory. Usually the $=$ predicate is just there and isn't defined by formula. – user251257 Mar 19 '16 at 12:53
  • I have never come across a formal system in which $\forall$ is subject to definition. In formal first-order logic, the symbol is just there, and has to satisfy the axioms of first-order logic. There is, however, a definition of the interpretation of $\forall$ in a model in first order logic, and that definition resembles the one you gave. However, note that this definition is not a definition inside the first-order logic, so there is no circularity involved. – Harald Hanche-Olsen Mar 19 '16 at 13:21
  • A similar comment applies to the concept of a propositional function, which is usually considered a meta concept; i.e., it is not a concept within the theory under study, but rather a concept about this theory. – Harald Hanche-Olsen Mar 19 '16 at 13:24

1 Answers1

2

In first-order logic, we define the truth value of of $(\forall x)P(x)$ in a particular structure/model/interpretation $M$ as follows:

$M$ satisfies $(\forall x)P(x)$ if, for all $c$ in the domain of $M$, $M$ satisfies $P(c)$.

Note that the use of sets (as in the question) in entirely superfluous. However, it is the case that $\forall$ is defined in terms of "for all". This is not circular because the "for all" is in the metatheory, which we assume we have already set up, while $\forall$ is just a symbol in the formal language whose semantics are being defined. The reason that we call $\forall$ the "for all symbol" is that it is intended to capture the pre-existing notion of "for all" within the formal language we are defining.

Carl Mummert
  • 81,604