A Note on Harmony
May. 20th, 2012 03:51 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
purplecat100 Current Papers in Artificial Intelligence, Automated Reasoning and Agent Programming. Number 3
Nissim Francez, Roy Dychkhoff. A Note on Harmony. Journal of Philosophical Logic, 41:613-628.
DOI: http://dx.doi.org/10.1007/s10992-011-9208-0
Open Access?: Computational Logic Publications, St. Andrews University.
Logic is probably not what you think it is and unless you are an academic in the area the idea that there may be many many logics may seem very strange.
However, there are lots of logics out there. A logic, broadly speaking, is a way of saying things (normally involving symbols), a set of axioms (things assumed to be true written in the logic's way of saying things) and a set of rules (for deducing more things from the axioms). People will come up with new logics for a variety of reasons, sometimes there will be something special they want to talk about and they want a logic designed for talking about that thing (like time, or knowledge, or belief). Sometimes they want a logic that is easy to deduce things in either for a human (in which case you want the rules to be "human-like" in some way) or for a machine (in which case you often want to limit the sorts of things you can say).
So suppose you are designing a logic. Suppose in fact you are designing a natural deduction style logic. A natural deduction style logic is supposed to capture a "natural" way of reasoning (an idea, it must be said, I would have hotly contested as an undergraduate). A rule in a natural deduction logic might look a bit like
A B
A & B
Which means if you have deduced that A is true, and you have deduced that B is true then you may deduce that "A and B" is true. The above is referred to as an Introduction Rule. You have introduced the symbol & into what you are saying.
You can also have rules that look like
A & B
A
This means that if you have deduced "A and B" you can deduce that A is true. This is referred to as an Elimination Rule. The rule eliminated the symbol & from the proof.
It should seem fairly intuitive that Introduction and Elimination rules match up in some way. Informally the idea of harmony in the rules of a logic is the idea that the introduction and elimination rules pair up in a "well-behaved" fashion.
The authors of this paper examine two proposals for nailing down "harmony" in a more rigourous fashion and show, in particular, that one version General-Elimination harmony (GE) provides a mechanism by which, if you have an Introduction rule you can "read off" harmonious Elimination rules from it - so if you were designing a logic you could automatically generate the necessary Elimination rules from your Introduction rules. The GE mechanism produces quite general elimination rules - for instance the elimination rule generated for & from our introduction rule above is
which is read as, if I have deduced C using A or B (or both of them) - i.e. if I need to know A or B is true in order to know that C is true - and I have deduced A & B then I can deduce C. The GE mechanism has "read off" [A, B] from the top half of the Introduction Rule for & and filled them into a kind of template for producing elimination rules.
The paper then shows that General Elimination harmony is a special case of the second notion of harmony, Local Intrinsic Harmony. So basically, if you generate your elimination rules from your introduction rules using the GE ideas then you are automatically meet the criteria for both sorts of harmony.
Which is pretty cute.
Nissim Francez, Roy Dychkhoff. A Note on Harmony. Journal of Philosophical Logic, 41:613-628.
DOI: http://dx.doi.org/10.1007/s10992-011-9208-0
Open Access?: Computational Logic Publications, St. Andrews University.
Logic is probably not what you think it is and unless you are an academic in the area the idea that there may be many many logics may seem very strange.
However, there are lots of logics out there. A logic, broadly speaking, is a way of saying things (normally involving symbols), a set of axioms (things assumed to be true written in the logic's way of saying things) and a set of rules (for deducing more things from the axioms). People will come up with new logics for a variety of reasons, sometimes there will be something special they want to talk about and they want a logic designed for talking about that thing (like time, or knowledge, or belief). Sometimes they want a logic that is easy to deduce things in either for a human (in which case you want the rules to be "human-like" in some way) or for a machine (in which case you often want to limit the sorts of things you can say).
So suppose you are designing a logic. Suppose in fact you are designing a natural deduction style logic. A natural deduction style logic is supposed to capture a "natural" way of reasoning (an idea, it must be said, I would have hotly contested as an undergraduate). A rule in a natural deduction logic might look a bit like
A B
A & B
Which means if you have deduced that A is true, and you have deduced that B is true then you may deduce that "A and B" is true. The above is referred to as an Introduction Rule. You have introduced the symbol & into what you are saying.
You can also have rules that look like
A & B
A
This means that if you have deduced "A and B" you can deduce that A is true. This is referred to as an Elimination Rule. The rule eliminated the symbol & from the proof.
It should seem fairly intuitive that Introduction and Elimination rules match up in some way. Informally the idea of harmony in the rules of a logic is the idea that the introduction and elimination rules pair up in a "well-behaved" fashion.
The authors of this paper examine two proposals for nailing down "harmony" in a more rigourous fashion and show, in particular, that one version General-Elimination harmony (GE) provides a mechanism by which, if you have an Introduction rule you can "read off" harmonious Elimination rules from it - so if you were designing a logic you could automatically generate the necessary Elimination rules from your Introduction rules. The GE mechanism produces quite general elimination rules - for instance the elimination rule generated for & from our introduction rule above is
[A, B]
.
.
A & B C
----------
C
which is read as, if I have deduced C using A or B (or both of them) - i.e. if I need to know A or B is true in order to know that C is true - and I have deduced A & B then I can deduce C. The GE mechanism has "read off" [A, B] from the top half of the Introduction Rule for & and filled them into a kind of template for producing elimination rules.
The paper then shows that General Elimination harmony is a special case of the second notion of harmony, Local Intrinsic Harmony. So basically, if you generate your elimination rules from your introduction rules using the GE ideas then you are automatically meet the criteria for both sorts of harmony.
Which is pretty cute.