Topic: logic

topics > philosophy > Group: formalism

meaning and truth
philosophy of mathematics
program proving

boolean values, binary numbers, and bit strings
logic programming
mathematics as a formal system
object and value equivalence
sentences, propositions, and truth
set definition by extension or intension
symbolic representation
temporal relationships


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 3-valued logic for imprecisely known statements. (cbb 4/94)

Subtopic: language as logic up

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 up

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 up

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 self-subsistent 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: Hobbes--everything 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 two-valued 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 up

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 up

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 up

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 up

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 well-formed, propositional formula using Plankalkul [»baueFL_2002]

Subtopic: sound and effective up

Quote: an inference principle needs to be sound (i.e., allow only logical consequences) and effective (i.e., algorithmically decidable)

Subtopic: qualification up

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 up

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 up

Quote: those propositions are necessary whose contrary implies a contradiction [»leibGW_1679]

Subtopic: satisfiability up

Quote: implication in first-order 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 up

Quote: order the inductive numbers by: m<n if n possesses every hereditary property possessed by the successor of m [»russB_1919, OK]

Subtopic: first-order logic up

Quote: resolution may be the first complete system of first-order 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 up

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 series-parallel circuits by using Shannon's theorems to reduce the number of letters in the expression

Subtopic: truth table up

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 up

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 truth-functional 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 up

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 up

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, non-A=non-A, AA=A, non-non-A=A, if A=B then AC=BC for some C, if A=B then non-A=non-B, if A=B then A!=non-B [»leibGW_1686]
Quote: A-non-A is not a thing
Quote: A and A are the first coincidents [»leibGW_1686]
Quote: A and non-A 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 non-B

Subtopic: multi-valued logic up

Quote: handle a partially defined predicate by specifying its extension (true for these) and anti-extension (false for these); e.g., three-valued 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 up

Quote: formulas in temporal logic easier to read than first-order 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: TRIO--a first-order 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 concurrency-related errors; based on temporal logic as proposed by Pnueli [»holzGJ11_2002]

Subtopic: limitations of logic up

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

Related Topics up

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)

Updated barberCB 5/05
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.