[Logiweb] No .pdf files & "conditioned definitions"

[Klaus Ebbe Grue]

Hi Frederik,

> I have two questions:
>
> #2. In math texts you often encounter "conditioned definitions", i.e. 
> definitions which only make sense if certain requirements are met. For 
> instance, take a look at the following definition:
>
> "Let E be an equivalence relation on a set B, and let b \in B. The 
> equivalence class of b modulo E is the set
> (*) [b]_E = {x \in B | xEb}."
>
> (I hope you can read through my quasi-LaTeX notation). The point is that the 
> defining equation (*) above only makes sense if 1. E is an equivalence 
> relation, 2. b is a member of B.
>
> Is there any way to make such definitions in pyk? I've considered using the 
> "endorse" construction, which implements side conditions in proofs, but I 
> suspect it's not going to work.

The right thing to do is to define [b]_E = {x \in B | xEb} and to tell the 
reader that the definition only makes sense when E is an equivalence
relation and b is a member of B.

As a similar example, consider how Mendelson defines division. We all 
agree that x/y does not make sense when y is zero. But the theorem in 
Mendelson Section 2.9 which allows to define new function letters 
*requires* x/y to be defined for all x and y. So one typically defines 
x/0 to be 0 (c.f. Mendelson Section 3.3, the footnote to the proof of 
Proposition 3.16(o)).

When you prove something about [b]_E, you should assume that E is an
equivalence relation and b is a member of B in the formulation of 
the lemma.

-Klaus