User helmut brandl - MathOverflowmost recent 30 from http://mathoverflow.net2013-05-26T04:08:17Zhttp://mathoverflow.net/feeds/user/27009http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/117987/theorems-about-endofunctions-and-closuresTheorems about endofunctions and closuresHelmut Brandl2013-01-03T20:00:44Z2013-01-06T02:22:19Z
<p>Background: I want to use partial functions $f:A\to A$ (i.e. endofunctions) to prove assertions about linked structures.</p>
<p>Definitions: </p>
<p>Lets call a set $p$ closed under $f$ iff $\forall x. x \in p \land x\in f.domain \Rightarrow f(x)\in p$. All sets closed under $f$ form a closure system. I.e. we can close each set $p$ under the function $f$ with the expression $p.closed(f)$, i.e. $p.closed(f)$ is the least set which contains $p$ and is closed under $f$.</p>
<p>Important are the one element sets $p = \{ a\}$. I.e. we can define $a.closed(f)$ as $\{a\}.closed(f)$.</p>
<p>Furthermore we can define predicates on sets
$p.iscycle(f) = (\exists a: p=a.closed(f)
\land a\in f.domain
\land a \in f(a).closed(f))$,
$p.hascycle(f) = (\exists a: a\in p \land a.closed(f).iscycle)$,
$p.islinear(f) = (p\ne \emptyset \Rightarrow \exists a:p=a.closed(f))
\land \lnot p.hascycle(f) )$.</p>
<p>Theorems:</p>
<p>With these definitions I want to prove theorems like the following:</p>
<ul>
<li><p>$p.iscycle(f) \Rightarrow f'.isinjective$ where $f'$ is $f$ restricted to the elements of $p$.</p></li>
<li><p>$p.islinear(f) \Rightarrow f'.isinjective$, $f'$ as above</p></li>
</ul>
<p>Can anybody give me hints on how to prove such theorems or give me some links to find papers about these type of structures?</p>
http://mathoverflow.net/questions/109915/the-used-symbols-for-equality-and-equivalenceThe used symbols for equality and equivalenceHelmut Brandl2012-10-17T14:52:52Z2012-10-17T15:00:07Z
<p>Background: I am currently developing a general purpose programming language which allows formal verification (i.e. correctness proofs) of programs. During the development it came out that a lot of mathematics (order theory, lattice theory, cpos, etc.) is necessary to reach a sound definition.</p>
<p>For objects it is necessary to distinguish between identity and equality. Two objects are identical if they are indistinguishable. For this notion I have used the symbol $\sim$ (i.e. $a\sim b$ means the object $a$ is indistinguishable from the object $b$. Furthermore I allow user specific definitions of equality using the $=$ sign. I.e. $a=b$ means that $a$ and $b$ are equivalent with respect to some equivalence relation.</p>
<p>During my study of the needed mathematical theories I get more and more convinced that it would be better to take $=$ for identity or indistinguishability and $\sim$ for equalitiy or equivalence.</p>
<p>Is there a commonly accepted usage of symbols in mathematics expressing the notion of identy and equality?</p>
<p>P.S. For those who are interested in the definition of the programming language <a href="http://softwareverificaton.wordpress.com" rel="nofollow">here is a link to my blog</a></p>
http://mathoverflow.net/questions/109640/definition-of-continuous-functions-in-order-theoryDefinition of continuous functions in order theoryHelmut Brandl2012-10-14T19:08:31Z2012-10-15T02:53:58Z
<p>If we have a complete partial order (i.e. directed complete) I find frequently the following definition of a continuous function. A function $f:A\to B$ where $A$ and $B$ are cpos is called continuous if it maps the suprema of directed subsets of $A$ (if exist) to the corresponding suprema of directed subsets of $B$.</p>
<p>In complete lattices I would define continuous functions as functions which preserve suprema and infima (since both exist in a complete lattice for any subset).</p>
<p>Since complete lattices are cpos the following question arises: Are both definitions consistent? The requirement that all suprema and infima are preserved is stronger than the requirement that only suprema of directed sets are preserved. Therefore it might be possible that both definitions are different. Or are they equivalent?</p>
http://mathoverflow.net/questions/109066/transitive-closures-and-inductive-reasoning-solvedTransitive closures and inductive reasoning [solved]Helmut Brandl2012-10-07T14:28:20Z2012-10-07T22:53:23Z
<p>Let's say that r is an endorelation over A (i.e. $r$ is a subset of $A \times A$), $\bar{r}$ is the transitive closure of r (i.e. the least set containing r and being transitive).</p>
<p>Furthermore $r$ has the property that for all $x,y$ such that $(x,y) \in r$ and $x$ has a certain property $p(x)$ implies that $y$ has the property as well ($p(y)$ is valid).</p>
<p>I am trying to proof that the transitive closure $\bar{r}$ of r has this property as well.</p>
<p>I.e. I am trying to proof</p>
<p>\begin{equation}
(\forall x,y: (x,y) \in r \land p(x) \Rightarrow p(y)) \Rightarrow (\forall x,y: (x,y) \in \bar{r} \land p(x) \Rightarrow p(y))
\end{equation}</p>
<p>But I cannot find a proof of this assertion.</p>
<p>For me the above claimed assertion is obvious so it should have a proof. Can anybody help me to find some or to find counterexample which demonstrates that the above assertion is not valid in general.</p>
<p>It is easy to prove that $r$ and its transitive closure have the same domain and the same range. Furthermore I can prove that any domain/range restriction of $r$ results in the same domain/range restriction of its transtitive closure.</p>
http://mathoverflow.net/questions/108844/wellfounded-sets-and-predecessorswellfounded sets and predecessorsHelmut Brandl2012-10-04T18:48:45Z2012-10-04T18:57:46Z
<p>Following question: Let's assume that W is a wellfounded set, i.e. it has a partial order and every nonempty subset of W has minimal elements with respect to the order.</p>
<p>Now we can easily define a binary relation 'preceeds' with the definition</p>
<p>a.preceeds(b) = b.is_minimal({x: a < x})</p>
<p>I am not able to prove that the fact that an element b has no predecessor (with respect to the preceeds relation) implies that b is minimal in W.</p>
<p>Is it possible in a wellfounded set that an element b has no predecessor but there are elements a below it (i.e. a < b)? If this is possible are there examples?</p>
<p>Thanks for any help.</p>
http://mathoverflow.net/questions/117987/theorems-about-endofunctions-and-closuresComment by Helmut BrandlHelmut Brandl2013-01-05T00:18:13Z2013-01-05T00:18:13Z@Joel: I think you are right with your comment on "islinear". My definition seems to be too restrictive. Maybe it is better to use $p.islinear(f) = (\forall x,y. x \in p \land y \in p \Rightarrow x \in y.closed(f) \lor y \in x.closed(f)) \land \lnot p.hascycle(f)$http://mathoverflow.net/questions/117987/theorems-about-endofunctions-and-closuresComment by Helmut BrandlHelmut Brandl2013-01-04T14:23:59Z2013-01-04T14:23:59ZIf both of these implications are easy to prove, why don't you provide a proof. My problems is that I have not yet been able to prove these implications. They are evident, but I need a proof.http://mathoverflow.net/questions/117987/theorems-about-endofunctions-and-closuresComment by Helmut BrandlHelmut Brandl2013-01-04T00:22:23Z2013-01-04T00:22:23Z@Joel
Notation: How would you write these predicates? $cyc(p,f)$ and $lin(p,f)$?
Integers: I am looking only at closures here(my intention is to prove assertions of linked structures). The predicate $p.islinear(f)$ expresses the fact that $p$ is a closure starting from a one element set and does not have cycles. The fact that the set of integers is not linear according to this definition is implied by the fact that the integers are not a closure under a function starting from a one element set.http://mathoverflow.net/questions/117987/theorems-about-endofunctions-and-closuresComment by Helmut BrandlHelmut Brandl2013-01-03T21:51:12Z2013-01-03T21:51:12ZYou are right again. I have transcribed it wrongly into latex. The clause $p=a.closed(f)$ substitutes the clause $a \in p$ because the former implies the latter.http://mathoverflow.net/questions/117987/theorems-about-endofunctions-and-closuresComment by Helmut BrandlHelmut Brandl2013-01-03T21:31:23Z2013-01-03T21:31:23ZJust the opposite. Starting from $f(a)$ and repeatedly applying $f$ it cycles back to $a$. This was a typo which I have corrected now. Sorry and thanks for the hint.http://mathoverflow.net/questions/109915/the-used-symbols-for-equality-and-equivalenceComment by Helmut BrandlHelmut Brandl2012-10-17T19:32:56Z2012-10-17T19:32:56Z@Per: The different types of operator symbols to use are quite clear. The most naturals are =,==,=== as you proposed or ~ which is quite accessible form the keyboard as well. But my question is what symbol should represent which equivalence relation? And which choices are inline with the use in mathematics. From my perception = and ~ are used in mathematics with the meaning of identity (=) and equivalence (~). And if this is the case I tend to stick to this definition.http://mathoverflow.net/questions/109915/the-used-symbols-for-equality-and-equivalenceComment by Helmut BrandlHelmut Brandl2012-10-17T17:00:30Z2012-10-17T17:00:30Z@Andreas: You confirm my suspicion that in mathematics "equal" and "identical" are used as synonyms, i.e. $=$ is the strongest equivalence relation. This implies that I have to reconsider my decision to use = for equality in the sense of equivalence with respect to some equivalence relation (which might not be the strongest possible) and ~ for identity (i.e. the strongest equivalence relation.http://mathoverflow.net/questions/109915/the-used-symbols-for-equality-and-equivalenceComment by Helmut BrandlHelmut Brandl2012-10-17T16:14:56Z2012-10-17T16:14:56ZI see $=$ is used in mathematics for equality in the sense of identity. $a=b$ usually means I can substitute $a$ by $b$ and vice versa in any formula. I think this is called Leibnitz equality. http://mathoverflow.net/questions/109640/definition-of-continuous-functions-in-order-theory/109644#109644Comment by Helmut BrandlHelmut Brandl2012-10-15T01:30:06Z2012-10-15T01:30:06ZSo we have continuous maps in cpos which preserve joins of directed sets. The we have maps in complete lattices which preserve joins and we have maps in complete lattices which preserve meets. From your answer I understand that all three definitions describe different concepts. Right?
If this is correct, is there clear definition of continuity in complete lattices?http://mathoverflow.net/questions/109066/transitive-closures-and-inductive-reasoning-solvedComment by Helmut BrandlHelmut Brandl2012-10-07T15:35:37Z2012-10-07T15:35:37ZThanks! It so simple. That's the answer to my question.http://mathoverflow.net/questions/109066/transitive-closures-and-inductive-reasoning-solvedComment by Helmut BrandlHelmut Brandl2012-10-07T14:49:57Z2012-10-07T14:49:57ZYes, I thought the convention that $\land$ binds tighter than $\Rightarrow$ is quite common. Thanks for the hint.http://mathoverflow.net/questions/108844/wellfounded-sets-and-predecessors/108845#108845Comment by Helmut BrandlHelmut Brandl2012-10-04T19:03:34Z2012-10-04T19:03:34ZThanks. This explains why I am not able to prove this wrong assertion.