Collaborative articulation of how abstraction and language is employed in the computational manifestation of numbers -- including analysis of the role of syntax, semantics, and meaning in the specification and use of software interfaces.

In the narrow sense, logic is the theory of valid arguments or the theory of deductive inference. A slightly broader sense includes the theory of definition. ... -- Patrick Suppes, preface to Introduction to Logic [5:p.xiv]

Miser demonstrates a model of computation. The specification of Miser establishes the functional requirements for a computing machine (the mechanism). The machines are typically implemented by software programs operated on conventional digital computers. That this can be done at all is a demonstration of how well digital computers are useful for manifestation of abstractions.

While it is appropriate to think of a Miser as a machine with a variety of physical realizations, there is a mathematical theory that dictates the essential characteristics that each realization is expected to manifest. This is by design. We want Miser to be amenable to mathematical reasoning and analysis. The mathematical theory determines the correct behavior of Miser implementations. Even so, no result in the mathematical theory can ever be a proof about a Miser implementation. We want to develop an appreciation for how this is so and how there remains an useful connection between theories and concrete realizations even though the connection is a bridge that the theory can never cross.

The mathematical theory is essentially pure logic applied to a simple subject matter: the Miser Obs and functions over them. It is also the case that Miser procedures perform in logic-resembling ways and can achieve what is known as a computational logic. Both of these conditions require that we be careful about our demands on logic and how they will be expressed. We need to look at how the theory for Miser is expressed as a logical theory as well as how logic is expressed in Miser procedures (that is, by computational means).

This reliance on a logical theory will assist our differentiation among computation, logic, and mathematics. This will, in turn, help us clarify the relationship between procedures and functions and algorithms for functions as we look more closely at the Miser computational model.

The logical theory for oMiser, the foundation system, is symbolized Ot, short for Ob theory. It is an application of First-Order Logic.

1. First-Order Logic

The logical theory for Miser is mostly expressed in an informal style. Most of the assertions under the theory are in the form of equations or identities: equalities and inequalities.

Although there is not much need for a full-up expression in a formal logic, there is always an equivalent formal expression using First-Order Logic with equality (FOL=). The FOL= logical symbolism employs the following forms:

x = y equality: read as "x equals y"

x ≠ y inequality: read as "x not-equal-to y"

∀u(p) universal quantification, read as "for all u, p"

∃u(p) existential quantification, read as "there exists u such that p"

¬p negation: read as "not p", also seen as "~p" and "-p"

p ∧ q conjunction: read as "p and q", also seen as "p&q"

p ∨q disjunction: read as "p or q"

p → q conditional: read as "if p then q" or "p implies q", also seen as "p⇒q" or "p⊃q"

p ↔ q biconditional: read as "p if and only if q" or "p equivalent q", also seen as "x⇔y" or "x≡y"

A common order of precedence of the operations is indicated in the progression. The components of the equality and inequalities can be constants, variables, and expressions involving functions of operands that are the same kind of components. These are not applicative expressions and should not be read as Frugalese applicative operations (just yet, if ever).

A basic introduction to FOL notation is available on-line in the MIT Open Courseware [2]. There are other on-line descriptions [4, 6]. These should provide enough background to be able to read the formalisms of Ot.

The specific form used here is that described in the Handbook of Mathematical Logic [1]. Leisurely expositions with many examples and exercises are available in the books by Lemmon [3] and Suppes [5].

2. Informal Expression

The informal expression allows us to avoid heavy use of special symbols. For example, an axiom of equality,

∀x∀y∀z (x = y ∧ y = z → x = z)

could be expressed informally for Ot as

"For Obs x, y, z, if x = y and y = z, then x = z."

There are further examples to be found among the posts on Numbering Peano and in other Miser Project materials.

3. Ot as a Logical Theory

For Ot, there are additional constants to be introduced (e.g., ob_A, ob_B). We also presume a variety of functions (e.g., ob.a, ob.b, ob.ap). These and other additions to FOL= constitute Ot.

In particular, we assume that the variables of quantifiers (x and y in ∀x, ∃y) refer to Obs.

Because the domain of discourse, as it is known, is the Obs and only the Obs, how functions are represented in Ot becomes an interesting topic. The same is true for additional predicates (i.e., beyond the predicate implicitly associated with "="). We will explore these matters in further posts and articles of the Miser Project.

For now it is useful to point out that there is no direct way to express something about all/any functions or all/any predicates using FOL= (a consequence of being first-order). When we speak in such a way, it will have to be informally and outside of Ot. That situation is also to be explored further.

[update 2008-05-07T17:29Z: I couldn't resist changing the title from "The Logic of It" to "The Logic of Ot," a bad-pun opportunity which I hadn't noticed until making a diary entry about having completed the post. It is an apt phrasing, besides. As long as I am here, I also append a little more content to section 3.]

[1] Jon Barwise: An Introduction to First-Order Logic. Chapter A.1 (pp. 5-46) in Handbook of Mathematical Logic, Jon Barwise (ed). Studies in Logic and the Foundations of Mathematics, volume 90, Elsevier (Amsterdam: 1977). ISBN 0-444-86388-5 pbk.

The concerns I have expressed over Handbook do not apply to this chapter (although I just found a typo in the first example in section 3), which is tidy and makes useful connection to model-theoretic considerations. Our notational symbols are those used here.

These notes provide a leisurely and elementary introduction to FOL= notation with understandable applications to every-day logical situations.

[3] E. J. Lemmon: Beginning Logic. Van Nostrand Reinhold (Great Britain: 1965), modest revision edited by George W. D. Berry, Hackett Publishing (Indianapolis: 1978). ISBN 0-915144-50-6 pbk.

One advantage of this text, considered by its author to be more elementary than Suppes[5], with which it matches its notation, is that it is still used as a textbook and the author's insider remarks are entertaining. The Bibliography notes are recommended.

This is a good place to find a summary of the notation without all of the subtleties and accompanying discourse. For a deeper look into how formal logic and logical theories work, Lemmon and Suppes will be rewarding [3, 5].

[5] Patrick Suppes: Introduction to Logic. Van Nostrand Reinhold (New York: 1957), Dover unabridged republication (New York: 1999). ISBN 0-486-40687-3 pbk.

Recommended for its gradual progression and build-up of first-order logic with useful examples and exercises. Chapter 11, on Functions, is a valuable bonus (as well as slightly contrary to what we have to say about functions in the context of the Miser Project).