--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/cb10d0f6-a02d-93dc-9449-c95701dea79a%40att.net.
!0!
"p2 симметричен/коммутативен на TV означает что для каждых x,y из TV: (x p2 y) тождественно (y p2 x)."
Declaration COMM_TV func(TV func(TV TV TV)) definition (p2):(∀x:TV(∀y:TV ((x p2 y)=(y p2 x)) )).
"Declaration EQTV_trans :TV definition ():TRANS_TV(=)."
Declaration EQTV_trans func(TV) definition ():(∀x:TV (∀y:TV (∀z:TV (((x=y) and (y=z)) → (x=z))))).
Dear Jon,
The animation is mesmerizing: I would watch and watch. But without the pause, next frame, and playback speed settings, it's just a work of art that calls to see it step by step.
And on page [1] you start with the double negation theorem.
Have a look at a few of my comments as a reader, and only on the graph topic taken separately.
Let me point out that graph manipulation is best described in terms of graph technique to which any other interpretation (En, Ex) is external.
(J12) It would be nice to explicitly say what do "a", "b", "c" mean, for example, like this: Let "a", "b", "c" be some graphs.
(Ax) Axioms do not say that graph operations have a parameter or two. This is clear only from the diagram of the proof. And the parameter is most likely an arbitrary graph?
(Insert) Let us consider the application of the Insert operation of axiom J1 in the proof of Double negation.
What is this parameter "(a)"? From [2] we see that this is
i.e. some graph with a true-node?
My Insert command algorithm turned out like this.
operation Insert
input:
-Let CG0 is a graph under transformation.
--precondition: CG0 has at least one arc.
-Let the arc e1 and the nodes v1, v2 adjacent to it are selected in CG0.
- Let CG1 be a graph to be inserted.
--precondition: CG1 has one true-node.
algorithm:
-create a copy of the graph CG1, designating it CG2.
-put the true-node of CG1 under v1.
-put the true-node of CG2 under v2.
END
“put node v3 under the node v4.” means put it together but take attributes from v4.
So v1, v2 are not true-nodes after Insert.
Later we meet Insert
It is not clear here whether "a" has a single true-node?
Anyway, I can’t get the algorithm from the picture for J1, so I don’t know if my version is correct.
It would be better to describe each operation separately and algorithmically, including specifying all parameters. As algorithms need the most accuracy in math ;-)
I understand that for your amazing project, these are small things. But they will help the programmer to readJ
At the end let me point out the opinion about a proof I like very much: proof itself is a kind of expression where sentences are arguments of derivation rules. To keep it condensed, proof becomes a lattice…
Best wishes,
Alex Shkotin
[1] https://oeis.org/wiki/Propositional_Equation_Reasoning_Systems
[2] https://oeis.org/wiki/Theme_One_Program_%E2%80%A2_Logical_Cacti
--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/6def8460-3286-06db-a77b-87f7d02f792e%40att.net.
[3] https://docs.google.com/drawings/d/1Zrjdj7KzqtNQTeOxYT38qBNblKdFpvBgJDCBZwzeAqU/edit?usp=sharing
--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/d6c18510-cc23-2556-bad5-4677d087649f%40att.net.
Dear John, happy 4th of July!
The topic of graph processing is my favorite. And I only in the traditions of the ancient Greeks wanted to show instead of animation that the proof is some structure that you can look at and enjoy.
The theme of the sign is utilitarian for me: the sign is the role of a suitable entity in the process of exchanging information and knowledge. It is certainly possible to delve into the types of signs (icons, symbols ...) or expand the idea of a sign to biological processes (as with a sunflower), but this is not mine.
I'll give you an example. Years ago, a friend of mine picked up his home phone only after the second call, when the first ended after three beeps. For him, it was a sign that his friend was calling.
Best holiday wishes,
Alex
--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to a topic in the Google Groups "ontolog-forum" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/ontolog-forum/vlsQqvEiIkY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/30309b75-39d8-0990-009e-657df5813955%40att.net.