John, (01)
what are the AGM operations ? Do I know them by another name? (02)
On Wed, Dec 31, 2014 at 9:32 AM, John F Sowa <sowa@xxxxxxxxxxx> wrote:
> I have often mentioned and recommended the Lindenbaum lattice
> of theories. For any classical logic L, it's possible to organize
> all theories expressible in L in a Lindenbaum lattice.
>
> Since there are infinitely many theories in L, each of which has
> infinitely many statements, it's not possible to store them. But
> it is possible to use the lattice as a framework for relating
> the axioms for a collection of theories and microtheories of any
> ontology or collection of ontologies expressible in L.
>
> The top of the lattice is the theory that contains no axioms
> and all possible theorems provable from zero assumptions.
> These include all the Boolean tautologies, and theorems such as
> "If x likes y, then x likes y, and every unicorn is a unicorn."
>
> The bottom of the lattice is the inconsistent theory that
> contains every statement expressible in the logic (which
> includes all their negations).
>
> An important application of the Lindenbaum lattice is its use for
> relating proofs in a nonmonotonic logic N to proofs in the classical
> logic L on which N is based:
>
> * For a nonmonotonic theory T in N, and a proof P of a statement S
> in T, there exist two theories T1 and T2 in L:
>
> * T1 contains the subset of all classical axioms for T
> (but T may contain zero or more nonmonotonic axioms).
>
> * The proof P of S in T can be mapped to a walk W through the
> lattice of classical theories from T1 to T2.
>
> * Each step of P that uses a classical axiom remains at the
> current classical theory in the walk W.
>
> * But each step of P that uses a nonmonotonic axiom in T,
> takes one step on the path W to a theory that modifies the
> previous classical theory by one of the AGM operations for
> theory revision.
>
> * The final step of the proof ends at the classical theory T2,
> which is a modification of T1 by one AGM operation for each
> nonmonotonic step of P. Then a purely classical proof can
> derive S from the axioms of the revised theory T2.
>
> * Comment: For negation as failure and for Reiter's default logic,
> the walk W always adds axioms. The theory T2 is therefore a
> specialization (more axioms) of T1. But defeasible logics may
> use the AGM operation of *contraction*, which moves to a theory
> that is higher in the lattice (fewer implications) than the
> previous theory. This makes the walk more complicated, since
> you have to make sure that you don't use an axiom at one step
> that is deleted at a later step.
>
> The following note links to the December issue of Logica Universalis,
> which begins with two freely downloadable articles.
>
> John
>
> -------- Forwarded Message --------
> Subject: Adolf Lindenbaum: Notes on his Life, with Bibliography
> Date: Wed, 31 Dec 2014
> From: UNILOG 2015
>
> Adolf Lindenbaum: Notes on his Life, with Bibliography
> Logica Universalis, 8, Dec 2014 (Open Access)
> Jan Zygmunt and Robert Purdy
>
> This paper is dedicated to Adolf Lindenbaum (1904–1941) — Polish Jewish
> mathematician and logician; a member of the Warsaw school of mathematics
> under Waclaw Sierpinski and Stefan Mazurkiewicz and school of
> mathematical logic under Jan Lukasiewicz and Stanislaw Lesniewski;
> and Alfred Tarski’s closest collaborator of the inter-war period.
>
> Our paper is divided into three main parts. The first part is
> biographical and narrative in character. It gathers together what
> little is known of Lindenbaum’s short life. The second part is a
> bibliography of Lindenbaum’s published output, including his public
> lectures. Our aim there is to be complete and definitive. The third
> part is a list of selected references in the literature attesting
> to his unpublished results and delineating their extent.
>
> Logica Universalis
> Volume 8, Issue 3-4, December 2014
> http://link.springer.com/journal/11787/8/3/page/1
>
> _________________________________________________________________
> Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
> Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
> Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> Shared Files: http://ontolog.cim3.net/file/
> Community Wiki: http://ontolog.cim3.net/wiki/
> To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
> (03)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (04)
|