Re: ZFC in 4 Axioms.


hagman wrote:
zuhair schrieb:

Hi all,

I just occured to my mind, that ZFC can be reduced to four axioms as
below:

1)Extensionality 2) Comprehension 3)Infinity 4)AC.

1),2),3) are as in the traditional presentation of ZFC.

Axiom 2) (ExAy yex<->P(y))<->x=/=y

I am not sure of the above.

Zuhair

You should first make yourself comfortable with what you mean by the
above, what is a well-formed formula, etc..
I assume you want to start with a sufficiently large set of otherwise
unused symbols standing for variables (which shall refer to sets),
then "atoms" (suing some BNF notation),
<atom> ::= <var>e<var> | <var>=<var>
meaning the set denoted by the first var is an element of the one
denoted by the second var or the two sets are equal, respectively;
for future reference, we say that both vars are "free" in this atom and
no variable is "bound".
Next we have
<formula> ::= <atom> | ~<formula> | (<formula>v<formula>) |
(<formula>&<formula>) | (<formula> -> <formula>) | (<formula> <->
<formula>) | E<var><formula> | A<var><formula>
In the first six variants, the free variables of the resulting formula
are precisely the union of free variables in the constituent(s) and
similarly for the bound variables. To simplify matters (even though
it's not necessary that strict), let us allow the construction only if
the resulting set of free variables is disjoint to the set of bound
variables.
In the latter two variants, we shall allow the construction only if
<var> is not a bound variable of <formula>, we say that the resulting
set of bound variables is bound variables of the formula with <var>
added and the resulting set of free variables is the set of free
variables of <formula> with <var> removed (if it was free).
Now given a sequence of symbols, we can mechanically decide
- is it well-formed?
- which variables are free?
- which variables are bound?

One might get rid of a few constructions (e.g. replace (P<->Q) by
((P->Q)&(Q->P))) if one wants.
In the axiom scheme, you probably want P(y) to stand for "any <formula>
where y is a free variable".
Then
(ExAy yex<->P(y))<->~x=y
should rather be written as either
(ExAy (yex<->P(y)) <-> ~u=v)
with free variables u and v (and whatever is free in P(y) besides x and
y)
or
Ex (Ay (yex<->P(y)) <-> ~x=v)
with free variables u and whatever is free in P(y) besides x and y
or
ExAy ((yex<->P(y)) <-> ~x=y)

Yes, this is the one.
with no free variables, except what is free in P(y) apart from x and y.
Of course, all these variants have different meaning.

Especially note that I may take P(y):= yex<->Q(y) and this would allow
me to replace
yex<->P(y) with Q(y) in all variants, so the axiom scheme is equivalent
to
(ExAy Q(y) <-> ~u=v)
or
Ex (Ay Q(y) <-> ~x=v)
or
Ex Ay (Q(y) <-> ~x=y)

Yes , I think this last one is what I meant.

Zuhair

.

Relevant Pages

  • Re: completeness what is it exactly
    ... that has no occurrences of free variables. ... If 'p' is a sentential letter (a 0-place predicate symbol), ... Axiom A has sentence letters, ... Sentences are formula's without sentence letters (Or propositional ...
    (sci.logic)
  • Re: Request for Peer Review - Refutation of Cantor Theorem Conclusion
    ... A mapping function is a function that maps one set to another; ... y subset S and x notin y} exist by the Axiom Schema of Separation ... Your formula has two free variables; ...
    (sci.logic)
  • Re: ZFC in 4 Axioms.
    ... In the first six variants, the free variables of the resulting formula ... set of bound variables is bound variables of the formula with ... In the axiom scheme, you probably want Pto stand for "any ...
    (sci.math)
  • Re: A brick in Cantors argument.
    ... The actual axiom doesn't need strengthening - all that needs ... Note that phi is allowed to contain free variables, ... With parameters, free variables, the comprehension schema suffices. ...
    (sci.logic)
  • Re: Request for Peer Review - Refutation of Cantor Theorem Conclusion
    ... It is not a unique digit ... That is simply not what the axiom of separation says, ... us just refer to it as C. Have I made any mistakes so far? ... has TWO free variables: x and D. You have not defined D yet, ...
    (sci.logic)