Individual km#abstract_algebra
>part: mathematical_logic__symbolic_logic__metamathematics__metamathematic
>part: application_of_techniques_of_formal_logic_to_mathematics
>part: 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
>part: application_of_mathematical_techniques_to_formal_logic
>part: sentential_logic__propositional_logic__propositional_calculus proof theory for reasoning with propositional formulas as symbolic logic; it is extensional
>part: predicate_logic__predicatelogic__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: FOL__first-order_logic__firstorderlogic__first-order_predicate_calculus__predicate_logic__predicatelogic 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: PCEF_logic__logic_of_positive_conjunctive_existential_formulas
>part: HOL__higher-order_logic based on a hierarchy of types
>part: logic_for_reasoning_about_computer_programs
>part: Hoare_logic
>part: logic_for_reasoning_about_concurrent_processes_or_mobile_processes
>part: CSP
>part: CCS
>part: pi-calculus
>part: logic_for_capturing_computability__logicforcapturingcomputability
>part: computability_logic__computabilitylogic
No statement uses or specializes abstract_algebra; click here to add one.