[Logiweb] Re: Larger examples?

[Robert Lamar]

Frederik,

Frederik Eriksen wrote:
> Robert Lamar wrote:
>> Having worked through the tutorials (which are well-written, in my 
>> opinion), I am now looking for other sources of information, guidance, 
>> and inspiration as I attempt to improve my working knowledge of 
>> Logiweb.  I have found the Peano example, but it is very 
>> foundational.  Are there any examples from other parts of 
>> mathematics?  Perhaps pages which define things such as groups, 
>> polynomials, or graphs?
>>
>>  [...]
> 
> Well, there is my M.Sc. thesis "Constructing the real numbers in 
> Logiweb" (URL: www.topps.diku.dk/eriksen/realNumbers). In the thesis, I 
> develop some of Cantor's theory of the real numbers, using ZF set theory 
> (and propositional logic and predicate logic). A word of caution: Most 
> of the thesis is in Danish. However, since the formal theorems of the 
> thesis are in English, it may still be of some use to you.

Thank you, belatedly, for pointing me towards this document.  I am still 
familiarizing myself with it, but it looks like it may be quite helpful. 
  From my initial observations, it seems like there are plenty of 
cognates between Danish and English, so I should do well enough on that 
score.

Thanks,
Robert