Editing Non-monotonic logic (section)

==Proof-theoretic versus model-theoretic formalizations of non-monotonic logics==

[[proof theory|Proof-theoretic]] formalization of a non-monotonic logic begins with adoption of certain non-monotonic [[rules of inference]], and then prescribes contexts in which these non-monotonic rules may be applied in admissible deductions. This typically is accomplished by means of fixed-point equations that relate the sets of premises and the sets of their non-monotonic conclusions. [[Default logic]] and [[autoepistemic logic]] are the most common examples of non-monotonic logics that have been formalized that way.<ref name="Suchenek">{{citation
 | last1 = Suchenek | first1 = Marek A.
 | title = Notes on Nonmonotonic Autoepistemic Propositional Logic
 | pages = 74–93
 | publisher = Warsaw School of Computer Science
 | journal = Zeszyty Naukowe
 | issue = 6
 | year = 2011
 | url = http://zeszyty-naukowe.wwsi.edu.pl/zeszyty/zeszyt6/NotesonNonmonotonicAutoepistemicPropositionalLogic.pdf}}.</ref>

[[model theory|Model-theoretic]] formalization of a non-monotonic logic begins with restriction of the [[semantics]] of a suitable monotonic logic to some special models, for instance, to minimal models,<ref>{{citation |first1=Marek A. |last1=Suchenek |title=Applications of Lyndon Homomorphism Theorems to the theory of minimal models. |journal=International Journal of Foundations of Computer Science |issue= 1|pages=49–59 |date=1990 |volume=01 |doi=10.1142/S0129054190000059 |publisher=World Scientific}}</ref><ref>{{citation |first1=Michael |last1=Gelfond |first2=Halina |last2=Przymusinska |first3=Teodor |last3=Przymusinski |title=On the relationship between CWA, minimal model, and minimal herbrand model semantics |journal=International Journal of Intelligent Systems  |publisher=Wiley |volume= 5 |issue= 5|pages=549–564 |date=1990 |doi=10.1002/int.4550050507  |doi-access=free }}</ref> and then derives a set of non-monotonic [[rules of inference]], possibly with some restrictions on which contexts these rules may be applied in, so that the resulting deductive system is [[Soundness|sound]] and [[Completeness (logic)|complete]] with respect to the restricted [[semantics]].<ref name="Suchenek2">{{citation
 | last1 = Suchenek | first1 = Marek A.
 | title = First-order syntactic characterizations of minimal entailment, domain-minimal entailment, and Herbrand entailment
 | pages = 237–263
 | publisher = Kluwer Academic Publishers / Springer
 | journal =  [[Journal of Automated Reasoning]]
 | issue = 2
 | year = 1993
 | volume = 10
 | doi = 10.1007/BF00881837
 | url = https://www.deepdyve.com/lp/springer-journals/first-order-syntactic-characterizations-of-minimal-entailment-domain-f1OOm5TaaM| url-access = subscription
 }}.</ref> Unlike some proof-theoretic formalizations that suffered from well-known paradoxes and were often hard to evaluate with respect of their consistency with the intuitions they were supposed to capture, model-theoretic formalizations were paradox-free and left little, if any, room for confusion about what non-monotonic patterns of reasoning they covered. Examples of proof-theoretic formalizations of non-monotonic reasoning, which revealed some undesirable or paradoxical properties or did not capture the desired intuitive comprehensions, that have been successfully (consistent with respective intuitive comprehensions and with no paradoxical properties, that is) formalized by model-theoretic means include [[Circumscription (logic)|first-order circumscription]], [[closed-world assumption]],<ref name="Suchenek2" /> and [[autoepistemic logic]].<ref name="Suchenek" />