User helmut brandl - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-26T04:08:17Z http://mathoverflow.net/feeds/user/27009 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/117987/theorems-about-endofunctions-and-closures Theorems about endofunctions and closures Helmut Brandl 2013-01-03T20:00:44Z 2013-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-equivalence The used symbols for equality and equivalence Helmut Brandl 2012-10-17T14:52:52Z 2012-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-theory Definition of continuous functions in order theory Helmut Brandl 2012-10-14T19:08:31Z 2012-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-solved Transitive closures and inductive reasoning [solved] Helmut Brandl 2012-10-07T14:28:20Z 2012-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>$$(\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))$$</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-predecessors wellfounded sets and predecessors Helmut Brandl 2012-10-04T18:48:45Z 2012-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 &lt; 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 &lt; b)? If this is possible are there examples?</p> <p>Thanks for any help.</p> http://mathoverflow.net/questions/117987/theorems-about-endofunctions-and-closures Comment by Helmut Brandl Helmut Brandl 2013-01-05T00:18:13Z 2013-01-05T00:18:13Z @Joel: I think you are right with your comment on &quot;islinear&quot;. 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-closures Comment by Helmut Brandl Helmut Brandl 2013-01-04T14:23:59Z 2013-01-04T14:23:59Z If 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-closures Comment by Helmut Brandl Helmut Brandl 2013-01-04T00:22:23Z 2013-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-closures Comment by Helmut Brandl Helmut Brandl 2013-01-03T21:51:12Z 2013-01-03T21:51:12Z You 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-closures Comment by Helmut Brandl Helmut Brandl 2013-01-03T21:31:23Z 2013-01-03T21:31:23Z Just 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-equivalence Comment by Helmut Brandl Helmut Brandl 2012-10-17T19:32:56Z 2012-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-equivalence Comment by Helmut Brandl Helmut Brandl 2012-10-17T17:00:30Z 2012-10-17T17:00:30Z @Andreas: You confirm my suspicion that in mathematics &quot;equal&quot; and &quot;identical&quot; 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-equivalence Comment by Helmut Brandl Helmut Brandl 2012-10-17T16:14:56Z 2012-10-17T16:14:56Z I 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#109644 Comment by Helmut Brandl Helmut Brandl 2012-10-15T01:30:06Z 2012-10-15T01:30:06Z So 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-solved Comment by Helmut Brandl Helmut Brandl 2012-10-07T15:35:37Z 2012-10-07T15:35:37Z Thanks! It so simple. That's the answer to my question. http://mathoverflow.net/questions/109066/transitive-closures-and-inductive-reasoning-solved Comment by Helmut Brandl Helmut Brandl 2012-10-07T14:49:57Z 2012-10-07T14:49:57Z Yes, 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#108845 Comment by Helmut Brandl Helmut Brandl 2012-10-04T19:03:34Z 2012-10-04T19:03:34Z Thanks. This explains why I am not able to prove this wrong assertion.