Semantic Classification of Resources about Logic


This document complements the other "kowledge management" related files, e.g. the general 'Semantic Classification of Knowledge Management Resources', the 'Semantic Classification of Formal Concept Analysis Resources' and the 'Semantic Classification of Conceptual Graph Resources'. However, for now, this file only has the first section ("Domains and Theorie"). It also only use the ">part" and "url" links. Other links will be used later. (This is just a beginning).

The generic user "km" is used below. Since this is a "generic user", no password is (and can be) associated to it in WebKB-2, and anyone may add categories in this name.

Reminder: (i) the link "object" has different (more specialized) meanings depending on the connected categories, (ii) so does the link "part": between physical objects it refers to the link "physical part", between tasks it refers to the link "subtask".

Domains and Theories

WordNet has two categories for "logic": #logic.philosophy refers to a "field of study" and #system_of_logic refers to a particular kind of system (and hence of collection). In our ontology, #system_of_logic is a concept type while fields of study are individuals organised by links ">part" (subdomain) and, like theories, are interpreted as "one or several propositions" (one proposition may be composed of sub_propositions). Below, we develop the hierarchy of fields of study below #logic.philosophy. In the low-level of these hierarchies are particular theories which could be represented as instances of #system_of_logic (in these cases, with this representation, the field of study can be nothing more that the theory itself). WordNet gives a few specializations to #system_of_logic which may be interpreted both as theories and fields of study (e.g. #Aristotlean_logic and #propositional_logic); hence, in our integration of WordNet, we have represented these specializations as instances (not subtypes; WordNet does not make the difference) and re-used their identifiers in the classification of fields of study below.

Similarly, an individual km#semantics_of_logic is introduced to represent the field of study "semantics of logic". A type km#semantic_of_logic could be introduced to

What is represented below is my interpretation of the documents accessible from Some parts are probably incorrect (e.g. I commented the part about "application_of_mathematical_techniques_to_formal_logic" because I am unsure about it). In a short while, the interface of WebKB-2 will include a knowledge-oriented wiki system to permit users to update pages such as this one but for now, if you have corrections or additional representations, thanks for mailing them to me (e.g. by sending a corrected file).

km#semantics_of_logic (^approaches that logicians have introduced to understand and determine that part of meaning in which they are interested; the logician traditionally is not interested in the sentence as uttered but in the proposition, an idealised sentence suitable for logical manipulation^)
  >part of: #semantics,
  >part: km#model-theoretic_semantics  km#proof-theoretic_semantics,

    km#model-theoretic_semantics (^the most widepsread approach, and is based on the idea that the meaning of the various parts of the propositions are given by the possible ways we can give a recursively specified group of interpretation functions from them to some predefined mathematical domains: an interpretation of first-order predicate logic is given by a mapping from terms to a universe of individuals, and a mapping from propositions to the truth values "true" and "false"^);

    km#proof-theoretic_semantics (^approach associating the meaning of propositions with the roles that they can play in inferences^)

  //a field of study; the purpose of a logic is to characterize the difference between valid and invalid arguments
  >part: km#inductive_reasoning_system km#deductive_reasoning_system
         km#binary_logic  km#multi-valued_logic
         km#informal_logic km#formal_logic,

    km#inductive_reasoning_system (^study of deriving a "reliable" ("inductively valid") generalization from observations^);

    km#deductive_reasoning_system (^an inference is "deductively valid" if and only if there is no possible situation in which all the premises are true and the conclusion false^);

    km#binary_logic__boolean_logic (^logic where the principle of bivalence is respected; this principle states that for any proposition P, either P is true or P is false^)

    km#multi-valued_logic__many-valued_logic (^logic in which there are more than two possible truth values^)
     >part: km#fuzzy_logic  km#probability_logic,

    km#informal_logic (^study of logic as used in natural language arguments^);

     >part: km#philosophical_logic  km#mathematical_logic
            km#non-modal_logic  km#modal_logic
            km#classical_logic km#non_classical_logic
            km#type_theory  km#term_logic  km#dialectical_logic,

       km#philosophical_logic (^deals with formal descriptions of natural language and hence philosophical logicians have contributed a great deal to the development of non-standard logics^)
        //shares much of the ">part" of km#mathematical_logic; left implicit here

       km#mathematical_logic__symbolic_logic__metamathematics //(last name is obsolete)
        >part of: km#abstract_algebra,
        >part: km#application_of_techniques_of_formal_logic_to_mathematics
               km#sentential_logic  km#predicate_logic

           >part: km#logicism;

             km#logicism (^pioneered by philosopher-logicians such as Gottlob Frege and Bertrand Russell: the idea was that mathematical theories were logical tautologies, and the programme was to show this by means to a reduction of mathematics to logic. The various attempts to carry this out met with a series of failures, from the crippling of Frege's project in his Grundgesetze by Russell's Paradox, to the defeat of Hilbert's Program by Gödel's incompleteness theorems; however, every rigorously defined mathematical theory can be exactly captured by a first-order logical theory; Frege's proof calculus is enough to describe the whole of mathematics, though not equivalent to it^);

/*        km#application_of_mathematical_techniques_to_formal_logic
           >part of: km#proof_theory  km#model_theory  km#axiomatic_set_theory  km#recursion_theory;

             km#proof_theory__calculus (^study of the part of a logical system which determines how to construct arguments: to derive conclusions from premises; it is a set of axioms (which may be an empty set), and a set of inference rules for deriving new well-formed formulas (wffs) from a given set of wffs; it must thus include or be defined in terms of a formal grammar, which will state all of the allowable expressions, the wffs, in the language; any grammar will in general also be given a semantics, which explains those features (truth, implication) that are, presumably, of interest; ideally the axioms and inference rules of a calculus are chosen such that if the formulas in a set are semantically true then any formulas derivable from them are also true; hence a calculus is formulated independently of a semantics, but with the aim of agreeing with it^);

             km#model_theory (^study of the representation of mathematical concepts in terms of set theory, or the study of the models which underlie mathematical systems^)
               object: km#model-theoretic_semantics;

             km#axiomatic_set_theory (^mathematical theory of sets^);

             km#recursion_theory__computability_theory (^part of the theory of computation dealing with which problems are solvable by algorithms (equivalently, by Turing machines), with various restrictions and extensions^)

          km#sentential_logic__propositional_logic__propositional_calculus (^proof theory for reasoning with propositional formulas as symbolic logic; it is extensional^);

          km#predicate_logic__predicate_calculus (^permits the formulation of quantified statements such as "there is at least one X such that..." or "for any X, it is the case that...", where X is an element of a set called the domain of discourse^)
           >part:  km#FOL  km#HOL,

             km#FOL__first-order_logic__first-order_predicate_calculus__predicate_logic (^FOL is distinguished from HOL in that it does not allow statements such as "for every property, it is the case that..." or "there exists a set of objects such that..."; it is a stronger theory than sentential logic, but a weaker theory than arithmetic, set theory, or second-order logic; it is strong enough to formalize all of set theory and thereby virtually all of mathematics^)
              >part: km#PCEF_logic; //+ km#first-order_theory;


//               km#first-order_theory (^theory that can be axiomatised as an extension of FOL by adding a recursive set of first-order sentences as axioms^)

             km#HOL__higher-order_logic (^based on a hierarchy of types^);

           >part: km#Hoare_logic 

              >part: km#CSP  km#CCS  km#pi-calculus;

              >part: km#computability_logic;

       km#non-modal_logic__extensional_logic (^as opposed to intensional logics, the truth value of a complex sentence is determined by the truth values of its sub-sentences^);

       km#modal_logic__intensional_logic (^sentences are qualified by modalities such as possibly and necessarily; both "Bush is president" and "2+2=4" are true, yet "Necessarily, Bush is president" is false, while "Necessarily, 2+2=4" is true^)
        >part: km#deontic_logic  km#epistemic_logic  km#temporal_logic  km#conditional_logic,
          km#temporal_logic (^system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time^)
           >part: km#tense_logic  km#computational_tree_logic__CTL  km#linear_temporal_logic,
/* Linear Temporal Togic is a "subset of" Computational Tree Logic,
   like FOL is a "subset of" HOL, but there does not seem to be a subdomain relation
   between these fields of study. May be this form of "subset of" could be
   represented by a "part of" relation, provided this is the sole/main kind of
   "part of" relation between theories.

        >part: km#substructural_logic  km#paraconsistent_logic  km#natural_deduction

          km#substructural_logic (^system of propositional calculus that are weaker than the conventional one^)
           >part: km#relevance_logic  km#linear_logic,

             km#relevance_logic__relevant_logics (^systems developed as attempts to avoid the paradoxes of material and strict implication^)

           >part: km#relevance_logic  km#many-valued_logic  km#non-adjunctive_logic;


          km#intuitionistic_logic__constructivist_logic (^logic used in mathematical intuitionism and other forms of mathematical constructivism^)

       km#type_theory (^branch of mathematics and logic that concerns itself with classifying entities into sets called types^)

        >part: #Aristotelian_logic;