# Re: Sixth normal form

Date: Fri, 10 Aug 2007 11:55:03 -0000

Message-ID: <1186746903.126913.321140_at_z24g2000prh.googlegroups.com>

On 10 aug, 13:08, Jan Hidders <hidd..._at_gmail.com> wrote:

> On 9 aug, 20:53, vldm10 <vld..._at_yahoo.com> wrote:

*>
**>
**>
**> > Although your comments in this thread are knowledgeable and useful I
**> > have a few remarks here.
**>
**> > On Aug 7, 3:30 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
**>
**> > > On 7 aug, 20:36, vldm10 <vld..._at_yahoo.com> wrote:
**>
**> > > > On Aug 1, 7:36 am, Jan Hidders <hidd..._at_gmail.com> wrote:
**>
**> > > > > Any attempt to reformulate it to something easier or more intuitive in
**> > > > > my experience almost always ends up with something that is either
**> > > > > wrong or actually harder to understand.
**>
**> > > > > The only somewhat mysterious part may be the "JD is implied by the
**> > > > > CKs" but this can be tested by the following simple procedure:
**>
**> > > > > 1. Let jd be the join dependency we want to test
**> > > > > 2. While jd has two elements (being sets of attributes) Si and Sj such
**> > > > > that the intersection of Si and Sj contains a candidate key do:
**> > > > > 2.1 replace Si and Sj with the union of Si and Sj
**> > > > > 3. If jd contains the header of the relation (which is also a set of
**> > > > > attributes) then return "yes" else "false"
**> > > > > -- Jan Hidders
**>
**> > > > You gave here the procedure which is more on intuitive level than
**> > > > based on some formal system.
**>
**> > > Although somewhat informally described by me, it is a proper algorithm
**> > > and as such *is* a formal system that has been proven both sound and
**> > > complete.
**>
**> > I have a feeling that you didn't pay enough attention to make a
**> > distinction between a constructioun (construct) and a formal axiomatic
**> > system (FAS). I mean here on construction for 5NF and 6NF, that put
**> > "things" in 5NF, 6NF.
**>
**> Indeed, the algorithm is not a formal axiomatic system, but it is a
**> formal system in the broader sense of the word. And if you look
**> closely you will see that it is in fact based on a very simple
**> axiomatic system whose propositions are JDs and CKs and has one
**> inference rule that allows you to derive JDs.
*

In case anyone's interested:

For a relation with header H (a set of attrbiutes) this formal system
starts with the following axioms:

- JD{H}

- any CKs that hold

Next to the trivial inference rule that says that all axioms are derived there is the following inference rule : (+ denotes set union, * denotes set intersection, <= denotes set inclusion)

IF

1. we derive JD{C_1, ..., C_i, ..., C_m} 2. C_i = D_1 + D_2 3. we derive CK(E) 4. D_1 * D_2 <= E

**THEN**

we derive JD{C_1, ..., D_1, D_2, ..., C_m}

- Jan Hidders