Group: mathematics
Group: meaning and truth
Group: philosophy of mathematics
Group: program proving
Topic: abstraction
Topic: boolean values, binary numbers, and bit strings
Topic: logic programming
Topic: mathematics as a formal system
Topic: object and value equivalence
Topic: reductionism
Topic: sentences, propositions, and truth
Topic: set definition by extension or intension
Topic: symbolic representation
Topic: temporal relationships
 
Summary
Logic is the formalization of reasoning, i.e., rules for deriving consequences from propositions. Aristotle presented the first system of logic. It predominated until the late 19th century when Boole, Frege and others developed symbolic logic.
Boole thought he had found the laws of thought, and Frege argued that his concept writing answered Leibnitz's call for a universal, exact, language. At the least, logic is intrinsic to language.
Boole is now famous for boolean algebra which is a simplification of his system. He observed that arithmetic on 0 and 1 satisfied the same relations as his logic algebra. Boolean algebra is an important tool in the design of computer systems.
Frege introduced logic as we know it today. His system included propositional calculus, functions on arguments, symbolic derivation, and universal and existential quantification.
Kowalski developed a clausal logic as the basis for a programming system. It is closely related to Prolog.
Many logics have been proposed. Modal logic (necessarily, possibly, ...) started with Aristotle. Kripke proposed a 3valued logic for imprecisely known statements. (cbb 4/94)
Subtopic: language as logic
Quote: the principles of logic and mathematics are true because they arise from the rules that govern the use of language; they are analytical [»ayerAJ_1956]
 Quote: mathematics and logic are part of the apparatus of language, not part of its application; allows us to use "900" in our daily life [»wittL_1939]
 Subtopic: meaning as logic
Quote: a theory of meaning should define meaning by a finite number of applications of a finite number of rules on a finite vocabulary [»daviD_1968]
 Subtopic: reasoning as logic
Quote: human reason regards all knowledge as parts of a possible system and hence resists contradiction; but there is no system [»kantI_1781, OK]
 Quote: the faculty of reason has a natural desire to build a selfsubsistent systematic whole by ideas alone [»kantI_1781, OK]
 Quote: Speciosa Generalis reduces truth and reason to a calculus of characters and words; a universal language, easily learned [»leibGW3_1714]
 Quote: a Speciosa Generalis would guide reasoning, avoid errors, and estimate probabilities
 Quote: through mathematical analysis, there is no problem that cannot be solved [»vietF_1591]
 Quote: Leibniz's goal: to conceive all propositions in the form of terms [»leibGW_1686]
 Quote: Hobbeseverything done by our mind is a computation; 'is' and 'is not' corresponds to + and  [»leibGW_1666]
 Quote: all of reasoning may be conducted by symbols, operations, and identity; closely related to algebra [»boolG_1854, OK]
 Quote: there is no inherent limitation to the intelligence of a computer program; e.g., Post's automatic improvement process for deciding if a sentence is a theorem [»mccaJ8_1962]
 Quote: to reason correctly with symbols, translate using a fixed interpretation, formally manipulate the symbols, and translate back the result [»boolG_1854, OK]
 Quote: reducing an argument to symbolic form determines its real premises, detects ambiguities [»boolG_1854, OK]
 Quote: with symbolic logic, the process of inference is precise, almost mechanical
 Quote: by pure thought can derive propositions about sequences that far surpass in generality those derived by intuition or the senses [»fregG_1879]
 Quote: a small number of laws and rules can include the content of all the laws, albeit in an undeveloped state [»fregG_1879]
 Quote: derive complex judgments from simpler ones; clarifies relationships
 Quote: all of psychology is based on the activity of neuron nets, i.e., on twovalued logic [»mccuWS_1943]
 Quote: mathematical logic is seldom used in proofs; it should be a calculational alternative to human reasoning [»dijkEW12_1989]
 Quote: formal reasoning concerns statements that do not mention actual things; e.g., if all alphas are betas and x is an alpha than x is a beta [»russB_1919, OK]
 Subtopic: truth as logic
Quote: absolute and hypothetical truths have the same laws; syllogisms are categorical
 Quote: for every true universal, affirmative, categorical proposition the predicate is contained numerically in the subject [»leibGW4_1679]
 Quote: the true is what can be proved or analyzed; the false is what is contrary [»leibGW_1686]
 Quote: the necessary reduces to an identity; the impossible reduces to a contradiction; the possible is not impossible
 Quote: a false term leads to contradiction; a true term does not
 Quote: necessary truths are those that reduce to identity; impossibles are those that lead to contradiction [»leibGW_1686]
 Quote: to be certain of truth, analyze to the fundamentally true or prove that a contradiction will never occur; the latter can eliminate a long continuation [»leibGW_1686]
 Quote: from truth, falsity never follows, but from an impossibility, anything follows  not used [»ockhW_1310]
 Subtopic: logical reduction
Quote: can reduce any system of logical equations to a single, equivalent equation [»boolG_1854, OK]
 Quote: a proposition is true a priori when it is reducible to identical propositions; its reason always appears [»leibGW_1679]
 Quote: infinite things can be compounded out of the combination of a few; e.g., numbers from digits [»leibGW_1679]
 Subtopic: mathematics as logic
Quote: mathematical analysis uses the art and rules of logic to obtain equations of species (e.g., 'x') instead of numbers [»vietF_1591]
 Subtopic: logic as syntax
Quote: use GAWK for AI because any logic merely defines how strings can be transformed into other strings; GAWK is designed for string transformation [»louiRP8_1996]
 Quote: the stack principle grew out of checking wellformed, propositional formula using Plankalkul [»baueFL_2002]
 Subtopic: sound and effective
Quote: an inference principle needs to be sound (i.e., allow only logical consequences) and effective (i.e., algorithmically decidable)
 Subtopic: qualification
Quote: all uses of the variable 'x' can be transformed into qualification, classes, functions, or combinators; e.g., singular description [»quinWV2_1947]
 Quote: universal qualification by indicating that a function is a fact for any replacement of a sign [»fregG_1879]
 Quote: form existential qualification out of negation and universal qualification [»fregG_1879]
 Quote: in a denoting phrase, 'the' becomes an uniqueness qualification; makes for involved rewordings [»russB_1956]
 Quote: universal qualification needs to specify its scope [»fregG_1879]
 Quote: a logic clause is the same as 'for all x1..xk B1 or ... or x1..xk Bm is implied by A1 and ... and An' [»kowaR11_1973]
 Subtopic: negation
Quote: in paper solutions, negation seldom used; e.g., 'and' appeared 6.1 times per participant while 'not' appeared 0.1 times [»paneJF2_2001]
 Subtopic: contradiction
Quote: those propositions are necessary whose contrary implies a contradiction [»leibGW_1679]
 Subtopic: satisfiability
Quote: implication in firstorder logic can be replaced by unsatisfiability of sentences in clausal form [»kowaR11_1973]
 Quote: survey of propositional satisfiability (SAT) and constraint programming (CP); similarities and differences [»bordL12_2006]
 Quote: a formal framework for discovering inconsistency errors with a boolean SAT solver; e.g., 600 null dereferences in Linux [»dillI6_2007]
 Subtopic: induction
Quote: order the inductive numbers by: m<n if n possesses every hereditary property possessed by the successor of m [»russB_1919, OK]
 Subtopic: firstorder logic
Quote: resolution may be the first complete system of firstorder logic using just one inference principle [»robiJA1_1965]
 Quote: the resolution principle  from any two clauses, one may infer a resolvent; a refutation is a sequence of resolutions leading to the empty clause; unsatisfiable iff refutation [»robiJA1_1965]
 Subtopic: mechanical logic
Quote: analyze and simplify relay networks as equations; equivalent to calculus of propositions; produces minimal, series and parallel networks
 Quote: X' is the negative of X, i.e., the break contacts of a relay; X+X'=1 [»shanCE6_1938]
 Quote: perfect analogy between calculus of switching circuits and Boolean logic; Huntington's postulates and De Morgan's theorem [»shanCE6_1938]
 Quote: simplify seriesparallel circuits by using Shannon's theorems to reduce the number of letters in the expression
 Subtopic: truth table
Quote: use truth tables to prove theorems about hindrances, i.e., open or closed circuits; e.g., associative and distributive laws [»shanCE6_1938]
 Subtopic: Frege's logic
Quote: replace the concepts of subject and predicate with argument and function respectively [»fregG_1879]
 Quote: Frege does not use subject/predicate because it is part of the interaction between speaker and listener [»fregG_1879]
 Quote: Begriffschrift introduced truthfunctional propositional calculus, functions instead of subject/predicate, quantification, derivational forms, and a definition of sequence [»fregG_1879]
 Quote: Frege only uses detachment to infer consequences; other modes of inference are equivalent [»fregG_1879]
 Quote: two of Frege's basic laws are excluded middle and reduction of implication; substitution rules are unstated [»fregG_1879]
 Quote: Frege's rule V allows substitution of equivalents [»fregG_1879]
 Subtopic: Boolean logic
Quote: Boole uses and, or, not, and complement; communtative law and idempotent law [»boolG_1854, OK]
 Quote: only 0 and 1 satisfy x^2=x; algebra of 0 and 1 is the same as the algebra of logic with a new interpretation [»boolG_1854, OK]
 Quote: get the law of contradiction from x^2=x [»boolG_1854, OK]
 Quote: the law of contradiction is the most certain of all principles and the basis of logic
 Quote: Boole used the symbol 'v' instead of the universal qualifier; e.g., y=vx for \forall y x [»boolG_1854, OK]
 Quote: use x=1 for proposition X is true; x=0 for falsehood; xy=1 for proposition X and Y are true together; etc. [»boolG_1854, OK]
 Quote: Boole reduced Aristotle's syllogisms and conversions to symbolic logic; scholastic logic is a collection of truths, not a foundation [»boolG_1854, OK]
 Subtopic: other history of logic
Quote: Leibniz's work in logic remained unpublished and largely unknown until the turn of the century; Boole, Frege, and Peano may have known of his aims in logic [»leibGW_1686]
 Quote: A=A, nonA=nonA, AA=A, nonnonA=A, if A=B then AC=BC for some C, if A=B then nonA=nonB, if A=B then A!=nonB [»leibGW_1686]
 Quote: AnonA is not a thing
 Quote: A and A are the first coincidents [»leibGW_1686]
 Quote: A and nonA are the first disparities; i.e., it is false that some A is B
 Quote: if A is B, it is false that A is nonB
 Subtopic: multivalued logic
Quote: handle a partially defined predicate by specifying its extension (true for these) and antiextension (false for these); e.g., threevalued logic [»kripS_1975]
 Quote: possible truths are those that do not lead to contradiction; contingent truths lack resolution even if continued to infinity [»leibGW_1686]
 Subtopic: temporal logic
Quote: formulas in temporal logic easier to read than firstorder logic and decidable; useful for reactive systems; e.g., P will hold eventually [»thomS4_2000]
 Quote: SPIN represents correctness claims in linear temporal logic (LTL)
 Quote: TRIOa firstorder temporal logic language with a linear notion of time [»ciapE1_1999]
 Quote: the TimeLine graphical editor simplifies the specification of basic temporal properties for SPIN model checkers; linear temporal logic is difficult to use [»holzGJ11_2002]
 Quote: model checking is automated, symbolic testing for properties expressed in temporal logic; can handle 10^100 states [»thomS4_2000]
 Quote: logic model checking is effective for concurrencyrelated errors; based on temporal logic as proposed by Pnueli [»holzGJ11_2002]
 Subtopic: limitations of logic
Quote: logic teaches how to know whether or not reasoning is conclusive but it does not teach how to find conclusive reasonings or demonstrations [»galiG_1638]
 Quote: logic is not flexible enough for thinking because consistency is too strong a requirement [»minsM_1981]

Related Topics
Group: mathematics (23 topics, 560 quotes)
Group: meaning and truth (18 topics, 634 quotes)
Group: philosophy of mathematics (11 topics, 330 quotes)
Group: program proving (10 topics, 311 quotes)
Topic: abstraction (62 items)
Topic: boolean values, binary numbers, and bit strings (44 items)
Topic: logic programming (34 items)
Topic: mathematics as a formal system (30 items)
Topic: object and value equivalence (60 items)
Topic: reductionism (51 items)
Topic: sentences, propositions, and truth (23 items)
Topic: set definition by extension or intension (18 items)
Topic: symbolic representation (26 items)
Topic: temporal relationships (40 items)
