# Why PROP (Set of all propositions) is a set by ZF axioms?

In Propositional Logic when we define the set of all propositions inductively how we can prove such a set(smallest with such properties) does exists? means that the set (of all sets with these properties) under intersection operation is not empty?

Definition 1.1.2 from Van Dalen book:

The Set $PROP$ of propositions is the smallest set $X$ with the properties:

(i) $p_{i}\in X (i\in \mathbb{N})$, $\bot \in X$

(ii) $A,B \in X$ then $(A\wedge B), (A\vee B), (A\rightarrow B), (\neg A) \in X$

I know in propositional logic we model it mathematically based on ZF(C) as a common accepted foundation for mathematics and I know there is another definition by formation sequences, I think it shows at least one such set exists but I want to know without it, how we can show that $PROP$ is a set in ZFC?

-
In the definition you gave, without loss of generality we can let the proposition letters be the even natural numbers, and we can use (some of) the odd ones to code the logical and punctuation symbols. Then the set of propositions can be thought of, via this encoding, as a subset of the set of finite sequences of natural numbers, obtainable via the Cut Axiom, or Replacement. But (probably) no one really thinks of the set of propositions in this way. It is just a convenient indexing. –  André Nicolas Sep 20 '12 at 5:57
@Nicolas. I mean that isn't it possible that properties (i) and (ii) together be somehow contradictory such that there isn't any set with these properties? for example in set theory for defining natural numbers (as intersection of all inductive set) we postulate the Axiom of Infinity (or existence of at least one inductive set) but how we without mentioning obviously any axiom know that at least one inductive subset of expressions (finite sequences of signs of our alphabets and connectives) with these properties exist? –  user32349 Sep 20 '12 at 7:24
I just sketched a proof that we can do it in ZF. I did not mention several odf the axioms, including Infinity, which we need to construct the set of integers, Pairing, Powerset, and so on, because they are all part of standard construction processes in ZF. We don't need Choice. –  André Nicolas Sep 20 '12 at 8:30
How we know corresponding (via such encoding) subset of finite sequence of natural numbers which satisfy such conditions exists? don't you think that the problem is translated to that situation again? why such definition is not self-contradictory? I think we should show at least one set with properties (i) and (ii) together exists because the problem is about "the smallest set X ...". Can we say the set of all finite sequence of natural numbers is such a inductive set according to the encoding and then by Replacement Axiom we have at least one set satisfy the main definition? –  user32349 Sep 20 '12 at 9:01
Symbols such as $\land$ and $($ are not sets. So if we want to construct PROP in ZF encoding is necessary. The rest (construction of the set natural numbers, construction of the set of finite sequences from a set, and so on are standard ZF constructions that you will see in any detailed development of ZF. It takes about one chapter. –  André Nicolas Sep 20 '12 at 13:55

It is easy to show that for any nonempty set of solutions to (i)+(ii), their intersection is still a solution. Then, under the assumption that some set $A$ is a solution, we can set $\mathit{PROP}$ to be the intersection of all subsets of $A$ that satisfy (i)+(ii), and that is clearly minimal among all solutions that are subsets of $A$. However, this is also a global minimum, because for any solution $B$, it holds that $\mathit{PROP}\subseteq B\cap A \subseteq B$.
Now for the main part. We suppose we have decided on a fixed set $L$ of proposition letters and and some arbitrary mathematical objects not in $L$ to represent the logical symbols. Then $\Sigma = L\cup\{{\land},{\lor},{\to},{\neg},{\bot},{(},{)}\}$ is a set, and then the collection $\Sigma^*$ of all finite sequences of elements of $\Sigma$ is a set. Now $\Sigma^*$ satisfies both of your conditions (i) and (ii), so we can use it as $A$ in the reasoning above. Therefore $\mathit{PROP}$ exists.
(Why is $\Sigma^*$ a set? Each of its elements is a function from some subset of $\mathbb N$ to $\Sigma$, so in particular it is a relation between $\mathbb N$ and $\Sigma$. So every element of $\Sigma^*$ is a subset of $\mathbb N\times \Sigma$, and therefore $\Sigma^*$ itself is a subset of $\mathcal P(\mathbb N \times \Sigma)$ and so $\Sigma^*$ is a set).
Great, then the set $L$ of preposition letters (atomic formulas) should always be given as a (countable or non-countable) set? mean that should we show first that L is also a set or we suppose we have one in hand in our prepositional language as alphabets. –  user32349 Sep 21 '12 at 3:42
I cannot imagine any situation where one would want to choose as $L$ something that is not plainly and obviously a set. –  Henning Makholm Sep 21 '12 at 9:39