Group: formalism

topic root > Group: philosophy

computer science
data type
meaning and truth
philosophy of mathematics
program proving
relationship between brain and behavior
requirement specification
abstraction by name
analytic truth
empirical truth
logic programming
mathematical proof
mathematics as a formal system
model checker
natural language as a system
people vs. computers
programming as mathematics
temporal relationships
what is a computer

all groups
map of the Thesa web site
topics f-m


Formalism is the use of symbols for logical arguments. It is an important part of the foundation for mathematics. It insures that arguments are rigorous, without gaps in the chain of inferences. For many, formalism appears to solve the problem of knowledge. From a small number of laws and rules, one can develop a boundless number of laws and relationships.

Yet a formal system is just another version of a Turing machine, and a Turing machine is just a number. (cbb 4/94)

Group members up

Group: formal grammar
Topic: classification
Topic: formal methods and languages
Topic: hierarchical structures
Topic: limitations of formalism
Topic: limitations of hierarchical structures
Topic: logic
Topic: reductionism
Topic: state
Topic: taxonomy
Topic: temporal logic
Subtopic: mathematical rigor up

Quote: mathematical logic is the construction of an abstract, strictly formalized, theory that derives a complicated, logical body of knowledge from an assumed, simpler body [currHB7_1929]
Quote: the initial knowledge assumed by mathematical logic should be simple, explicit, and carefully set forth [currHB7_1929]
Quote: mathematical rigor requires that we deduce every new proposition from previously established propositions; we must start with some axioms or unexplained primitives [burgJP_2015]
Quote: proofs can be formalized as a finite sequence of formulas of a formal theory; a part of why proofs are convincing to mathematicians [tymoT2_1979]
Quote: a formal proof does not hinge on the meaning of specific terms; the meaning is carried by the non-specific, arithmetic/logical terms [lakaI_1976]
Quote: in a formalized theory, the tools are completely prescribed by its syntax; in proof-analysis, tools are unconstrained [lakaI_1976]

Subtopic: advantages of formalism up

Quote: use formalization to assure security, exclude tacit pre-assumptions, clarify notations, and resolve universal structures [zemaH3_1966]
Quote: use artificial language for abstract notations, exact syntax, unambiguous words, and shorter expressions [zemaH3_1966]

Subtopic: formalism as knowledge up

Quote: elements are unknowable; while complexes are knowable and explicable via written letters [plat_368]
Quote: Leibniz developed the idea of a formal system as a means to knowledge, and the possibility of transforming a formal system into a real machine [kramS2_1996]
Quote: for Leibniz, formal systems and mechanized symbolic operations establish a norm for how we should think. They do not describe how we think [kramS2_1996]
Quote: Peano's mathematical logic is an example of Leibniz's universal characteristic; all of the ideas of logic are expressed by a small numbers of signs [peanG_1896]

Subtopic: formal as possibility up

Quote: possibility means internally consistent and free from contradiction; proof is a formal matter, attached to the form of sentences, not to their content; Leibniz [hackI_1975]

Subtopic: logic as symbolic system up

Quote: a formal language is a set of symbols with rules for building well-formed expressions; expressions are formulae or terms; formalize logic as models or formal systems [leisAC_1969]
Quote: theorems of a system of symbolic logic consist of expressions derived from formal axioms and rules of procedure as represented by the system; the rules of procedure must be effectively calculable [churA_1936]
Quote: logic is a system of processes that follow laws concerning symbols with a fixed interpretation [boolG_1854 OK]
Quote: Frege developed concept writing to prevent gaps in a chain of inferences; found that language and intuition were inadequate [fregG_1879]
Quote: a proof must be a step-by-step procedure; devised a concept writing to reduce their length; conforms with rules [fregG_1884]
Quote: Frege's ideography will unify the formula languages and extend them to new fields [fregG_1879]
Quote: replace the concepts of subject and predicate with argument and function respectively [fregG_1879]
Quote: concept writing provides symbols for implication and negation [fregG_1879]
Quote: in ontological symbolism, a symbol refers to an independent object or thing; with operative symbolism (Leibniz), the meaning of symbols is irrelevant to their manipulation [kramS2_1996]

Subtopic: formalism as computing up

Quote: algorithms encompass the whole range of concepts dealing with well-defined processes; includes structure of data as well as the structure of the sequence of operations [knutDE9_1979]
Quote: formal systems are equivalent to computing; they can figure things out without having any recourse to meanings [goldR_2005]

Subtopic: formalism as rules, syntactic up

Quote: a formal system is completely identified by the terms, elementary predicates, elementary propositions, axioms, and rules of procedure that yield the elementary theorems [resnMD_1980]
Quote: starting with primitive terms or tokens, operations combine terms into new terms according to the rules of formation [resnMD_1980]
Quote: to distinguish syntactics and semantics we have to separate form and meaning; a problem for information processing [zemaH3_1966]
Quote: formalization is packing as much meaning as possible into defined forms; e.g., the plural in natural language [zemaH3_1966]
Quote: if complexes are knowable then one knows the syllable SO but not the letters S and O; this is absurd [plat_368]
Quote: computer programs are formal (syntactic); they manipulate symbols through precisely stated rules; abstract, manipulated without meaning [searJR1_1990]
Quote: a non-linguistic writing system allows a formal language in which signs are independent of the signified objects; e.g., decimal numbers and Leibniz's characteres [kramS2_1996]
Quote: Leibniz's infinitesimal calculus was independent of what differentials actually are; avoids metaphysical disputes [kramS2_1996]
Quote: elements have only a name; combine names into descriptions of complex things [plat_368]
Quote: use a small vocabulary for formal methods; easier to understand though longer, more abstract, little implementation bias; e.g., Hoare's CSP [boweJP4_1995]
Quote: how to construct a relay switching circuit from equations of the independent and dependent variables [shanCE6_1938]
Quote: to produce an utterance one has to refer back to general rules and forward to specific rules while reconstructing the rules from continuity, context, and exceptions [misrVN_1966]
Quote: God is limitless and perfect; form in limiting matter perfects it; limitlessness in matter is imperfect; the limitlessness of a form undetermined by matter is perfect in character [aquiT_1273]

Subtopic: formalism as existence up

Quote: the most formal thing is existence itself [aquiT_1273]

Subtopic: concise up

Quote: in India, conciseness of composition, especially in scientific matters, was highly prized; more pronounced in earlier works [dattB_1935]
Quote: Panini's mathematical grammar described the language as spoken, concisely defined by enumerations and rules; transmitted orally; transform from syntactic relationship to phonemic realization [misrVN_1966]

Subtopic: universal system up

Quote: logic signs can express any proposition of science, so long as the signs for entities are added [peanG_1889]
Quote: a small number of laws and rules can include the content of all the laws, albeit in an undeveloped state [fregG_1879]
Quote: since the number of laws is boundless, need to find a basic set of laws that generates the rest; not unique [fregG_1879]

Subtopic: formalization of evaluation up

Quote: algorithm for evaluating an applicative expression relative to an environment; first formalization of expression evaluation [landPJ1_1964]
Quote: formal definition of the meaning of a program for proofs of correctness, equivalence, and termination; defines a condition on each command of the program; similar to McCarthy's work on recursive functions [floyRW4_1966]
Quote: a semantic definition is consistent if there are no counterexamples for correct commands; it is complete if there is a counterexample for every erroneous command [floyRW4_1966]

Subtopic: Turing machine up

Quote: formal systems or formalisms are the same as Turing machines [godeK_1931]

Subtopic: formalism without boundaries up

Quote: there is no boundary between 'clearly' and 'not clearly' yet 'clearly' has formal properties [holtAW11_1980]

Related up

Group: computer science
Group: data type
Group: function
Group: hypertext
Group: mathematics
Group: meaning and truth
Group: philosophy
Group: philosophy of mathematics
Group: program proving
Group: relationship between brain and behavior
Group: requirement specification
Group: science
Group: systems
Topic: abstraction
Topic: abstraction by name
Topic: analytic truth
Topic: empirical truth
Topic: logic programming
Topic: mathematical proof
Topic: mathematics as a formal system
Topic: model checker
Topic: natural language as a system
Topic: people vs. computers
Topic: programming as mathematics
Topic: rules
Topic: temporal relationships
Topic: what is a computer

Subtopics up

advantages of formalism
formal as possibility
formalism as computing
formalism as existence
formalism as knowledge
formalism as rules, syntactic
formalism without boundaries
formalization of evaluation
logic as symbolic system
mathematical rigor
Turing machine
universal system

Updated barberCB 1/06
Copyright © 2002-2023 by C.B. Barber
Thesa, Avev, and thid-... are trademarks of C.B. Barber