The Finitary Basis of Formal Systems and a Rigorous Construction of the Propositional Calculus with Its Models

Part I. Syntax

1. Formal system and ordinary reasoning

This note constructs the propositional calculus (PC): Part I covers the language, the axioms, the rule of inference and derivability, and Part II covers its models. The construction is preceded by two questions: how this system is related to ordinary logic (the present section) and where the construction should begin in order to avoid a circle (§ 2). Notation is introduced as needed.

In §§ 3–5 PC is constructed as a family of predicates on words over a finite alphabet. The notions of truth, meaning and consequence play no part in the definitions; the sign \(\to\) is a graphic sign, and its reading as “if …, then” does not enter the definitions. Hence the claim that PC models the logic of ordinary reasoning does not follow from the construction. It cannot be a theorem: one of the two sides being compared, ordinary reasoning, is not a formal object.

The identification of PC with ordinary logic rests on three circumstances: the reading of the signs \(\neg, \land, \lor, \to\) as the connectives “not”, “and”, “or”, “if …, then”; the agreement of PC with the practice of mathematical proofs; and the completeness theorem. The first is a convention about pronunciation. Comparison with ordinary speech reveals the following discrepancies. Each of the formulas below is a theorem of PC in the sense of § 4; the letters \(\mathcal{A}, \mathcal{B}, \mathcal{C}\) denote arbitrary formulas.

1. 1.

   Implication without a connection between premise and conclusion. The formula \((\mathcal{A} \to \mathcal{B}) \lor (\mathcal{B} \to \mathcal{A})\) is a theorem. Under the above reading it asserts that of any two statements one implies the other, whereas the ordinary “if” presupposes a connection between premise and conclusion (the paradoxes of material implication, C. I. Lewis, 1918; the dispute over the truth criterion for conditionals goes back to Philo and Diodorus). The theorem \(\mathcal{A} \to \mathcal{A}\), by contrast, agrees with ordinary logic.

2. 2.

   Order and cause in conjunction. The formula \((\mathcal{A} \land \mathcal{B}) \to (\mathcal{B} \land \mathcal{A})\) is a theorem. The statements “they took the medicine and recovered” and “they recovered and took the medicine” convey different things (P. Strawson, 1952; H. P. Grice assigns this difference to implicatures and excludes it from the truth conditions).

3. 3.

   Bivalence. The formula \(\mathcal{A} \lor \neg\mathcal{A}\) is an axiom. Statements with a vague predicate (“a heap of a hundred grains is large”), statements about contingent future events (Aristotle, De Interpretatione, ch. 9) and statements with a failed presupposition (“the present king of France is bald”; B. Russell, 1905, P. Strawson, 1950) do not obviously fall under this schema. As applied to mathematical statements the law is disputed by the intuitionists (L. E. J. Brouwer).

4. 4.

   Derivation and reasoning. Derivability is monotone (Proposition 5.4): adding a hypothesis does not cancel a derivable formula. Legal reasoning is not subject to monotonicity: a later statute partially repeals an earlier one, the earlier statute not being held false from the outset, and the premises are ordered by a scale of priorities. Nor does the rule modus ponens prescribe accepting the conclusion: someone who has accepted \(\mathcal{A}\) and \(\mathcal{A} \to \mathcal{B}\) and has discovered that \(\mathcal{B}\) is false gives up one of the premises (G. Harman, 1986). Derivability is a relation between formulas; reasoning is a revision of beliefs.

Mathematical practice. In mathematical proofs discrepancies 1–2 play no essential role. Mathematical statements do not depend on time or context, and the basic form of a conditional statement is universal: “for every integer: if it is divisible by \(4\), then it is even”. Such a statement is refuted only by a counterexample in which the premise is true and the conclusion false. The numbers \(8\) (both parts true), \(2\) (premise false, conclusion true) and \(3\) (both parts false) are not counterexamples. If a conditional is treated as a truth function, this requirement determines the table of the implication called material: it is false only when the premise is true and the conclusion false. The calculus of G. Frege (1879) was likewise created for writing down proofs in arithmetic; Frege compared the relation of his notation to ordinary language with the relation of the microscope to the eye.

Explication. The relation of PC to ordinary logic is described by the notion of explication (R. Carnap, 1950): an inexact concept (the explicandum) is replaced by an exact one (the explicatum), which is assessed by similarity to the explicandum, exactness, fruitfulness and simplicity. Coincidence of usage is not required: the biological concept Piscis replaces the everyday “fish” and does not cover the whale. W. Quine (1960, § 53) describes explication as elimination: the functions for the sake of which an unclear expression is used are singled out, a replacement is introduced for these functions, and synonymy is not claimed. The paradigm is the ordered pair in Kuratowski's form: the equality \(\langle X,Y \rangle=\{\{X\},\{X,Y\}\}\) does not express what was meant by a pair and secures the only required property: \(\langle X,Y \rangle=\langle U,V \rangle\) if and only if \(X=U\) and \(Y=V\).

In this sense PC is a replacement for ordinary logic and is not a model of it. Material implication performs those functions of the conditional that are needed in proofs: detachment of the conclusion and the writing of universal statements. It does not perform the other functions of the word “if”. The difference between a model and a replacement shows itself in case of a discrepancy: a model is corrected when it diverges from the phenomenon being modelled, whereas when PC diverges from an ordinary judgement, it is the judgement that is corrected. An implication with a false premise is accepted as true contrary to ordinary judgement, and derivability becomes the criterion of correctness of mathematical reasoning. Thus PC serves mathematics, including computer science; for other fields of knowledge it has no such justification and should not be carried over to them. The choice of replacement is not unique: intuitionistic logic, relevance logics and conditional logics preserve other functions of the ordinary connectives and are assessed by the same criteria.

The completeness theorem. The completeness theorem (§ 9) connects two formal predicates: derivability and truth by the tables. The implication table is itself part of the replacement, so the theorem says nothing about the relation to ordinary logic. The squeezing argument of G. Kreisel (1967, for first-order logic; the scheme is the same) derives from completeness the coincidence of intuitive validity with both formal notions under two conditions: everything derivable is intuitively valid, and everything intuitively valid is true by the tables. The first condition requires accepting formulas of the form \(\neg\mathcal{A} \to (\mathcal{A} \to \mathcal{B})\) as valid. It holds for the notion of correctness accepted in mathematical practice and fails for the ordinary use of the word “if”. The argument concerns a notion that has already been regimented.

The replacement does not eliminate ordinary logic entirely. The definitions of PC are formulated in a contentual metalanguage which itself uses the words “if”, “and”, “not” (item B4 of Convention 2.1). The relation between the object language and the metalanguage is the subject of the next section.

2. The problem of the vicious circle and the choice of a starting point

The construction of formal logic without preliminary conventions runs into the obstacle described in L. Carroll's dialogue What the Tortoise Said to Achilles (1895) and in W. Quine's paper Truth by Convention (1936). The rules for reading and transforming the symbols of the object language are formulated in some metalanguage. Full formalization of the metalanguage requires a meta-metalanguage, which yields an infinite regress; the justification of basic logic by means of that logic itself is a vicious circle (petitio principii).

In textbook presentations this obstacle is bypassed in two ways, each of which raises objections from the standpoint of foundations:

1. 1)

   Set-theoretic definition. A formula is defined as an element of the intersection of all inductive subsets of the free monoid \(\Alf^*\) over the alphabet \(\Alf\) (a construction going back to Frege and Dedekind, with a quantifier over \(\mathcal{P}(\Alf^*)\)) or as the last component of a finite assembly tuple \(\langle \xi_1, \dots, \xi_N \rangle \in (\Alf^*)^N\). Such a definition presupposes axiomatic set theory (with the axioms of infinity and power set) or the arithmetic of the natural numbers \(\mathbb{N}\), which are themselves formulated by means of predicate logic and PC. There is no formal contradiction here, since the system being defined and the metatheory are distinct; the objection concerns the order of justification.

2. 2)

   Conflation of definition and use. The formulation “let \(\mathcal{A}, \mathcal{B}\) be arbitrary formulas; then \((\mathcal{A} \to \mathcal{B})\) is a formula” combines the definition of the predicate “to be a formula” with the use of an already defined predicate. This creates the appearance that the metavariables \(\mathcal{A}, \mathcal{B}\) range over a domain which has not yet been given at the moment the rule is written down.

The circle is broken by explicitly fixing a starting point. In accordance with the finitist programme of D. Hilbert and P. Bernays, the canonical calculi of E. Post, the theory of algorithms of A. A. Markov and the exposition of S. C. Kleene, a stock of primitive notions of the metatheory is set out, accepted without formal definition. This stock does not include the notion of set, actual infinity or a formal theory of arithmetic. The choice of a starting point is not unique; the criterion is the simplicity of the initial notions (see Remark 2.1).

3. Alphabet, words and syntactic predicates

The object alphabet \(\Alf\) is fixed; it consists of exactly eight signs: \[|\qquad \st\qquad (\qquad )\qquad \neg\qquad {\land}\qquad {\lor}\qquad {\to}\] A word over \(\Alf\) is a finite string of its signs; the class of all such words is denoted \(\Alf^*\) (the Kleene star). The Greek letters \(\xi, \eta, \zeta\) are metavariables over words from \(\Alf^*\). Concatenation is written by juxtaposition: \((\xi\to\eta)\) is the word composed of a parenthesis, the word \(\xi\), the sign \(\to\), the word \(\eta\) and a parenthesis. The parentheses attached to predicates belong to the metalanguage and are shown in blue; a compound word in the argument of a predicate is enclosed in single quotes: \(\Form\mo \q{(\xi\to\eta)}\mc \).

The propositional variables are strings composed only of strokes and enclosed on both sides by hash signs: \(\atm{|}\), \(\atm{||}\), \(\atm{|||}\), etc. This notation meets three requirements. The stock of variables must be potentially infinite, so a finite set of letters does not suffice. This stock must be given by the simplest rules over a finite alphabet, so letters with numerical subscripts, which require digits and the notion of a subscript, are not used. Replacing a variable must work without error, so a variable cannot be a subword of another variable: the word \(|||\) is a subword of the word \(||||\), and under replacement a formula would land inside it, whereas the atom \(\atm{|||}\) is not a subword of the atom \(\atm{||||}\). The letters \(a, b, c\) occur below only as metavariables over atoms and do not belong to the alphabet.

Strokes are added only within atoms, so two predicates are introduced, \(\Atom\) and \(\Form\); the first enters the definition of the second only as the premise of rule F1.

The words \(\atm{|}\), \(\atm{||}\), \(\atm{|||}\), etc. have the property \(\Atom\). Instead of such elaborate notations for variables one may mentally picture \(p_1,p_2,p_3\), etc.

The implication in rule F1 goes in one direction: every atom is a formula, while a formula containing a connective or a parenthesis is not an atom.

The capital calligraphic letters \(\mathcal{A}, \mathcal{B}, \mathcal{C}\) denote formulas and the lowercase Latin letters \(a, b, c\) denote atoms; these are metavariables restricted in the sense of B6 (Fig. 1). The notation \(\mathcal{A}(a)\) denotes a formula \(\mathcal{A}\) with a distinguished propositional variable \(a\); neither the occurrence of \(a\) in \(\mathcal{A}\) nor the absence of other variables from \(\mathcal{A}\) is required.

Omission of parentheses. Parentheses are omitted only in notation in the metalanguage; the word itself contains all of them. Outer parentheses are dropped: \(\mathcal{A} \to \mathcal{B}\) denotes the word \((\mathcal{A}\to\mathcal{B})\). When it occurs in a longer formula they are restored: \(\neg(\mathcal{A} \to \mathcal{B})\), \(\mathcal{C} \to (\mathcal{A} \to \mathcal{B})\). Negation introduces no parentheses, so \(\neg\mathcal{A} \to \mathcal{B}\) is read unambiguously as \((\neg\mathcal{A}) \to \mathcal{B}\). The further conventions in common use (the connectives \(\land, \lor\) bind more tightly than \(\to\); a chain of implications associates to the right) are not applied in the present text.

Unfolding the condition. Unfolding the condition from B6 removes the appearance of a circle. The formulation “if \(\mathcal{A}\) and \(\mathcal{B}\) are formulas, then \(\mathcal{A} \to \mathcal{B}\) is a formula” is written as \(\Form\mo \q{\mathcal{A} \to \mathcal{B}}\mc \) and means \[\text{for all words } \xi, \eta:\quad \text{if } \Form\mo \xi\mc \text{ and } \Form\mo \eta\mc , \text{ then } \Form\mo \q{(\xi\to\eta)}\mc ,\] that is, rule F3 for implication. In this notation \(\xi, \eta\) range over words given independently of the notion of formula, and the predicate \(\Form\) enters only the premise and the conclusion of the rule. The totality of formulas is not presupposed. The abbreviated notation is legitimate after Definition 3.2; read as the definition itself, it is what creates the appearance of a circle.

Analysis of words. Words and formulas are analysed by means of recursive arithmetic (T. Skolem, 1923): parentheses, the parenthesis balance and the length of a word are counted, and induction on the length of a word is applied. This use of arithmetic is contentual, in the sense of Remark 2.1.

4. Axioms and theorems of the calculus

The predicate “to be a theorem of PC” is defined purely syntactically: the axioms and the closure under the rule of inference are fixed. Distinct from it is the notion of tautology: a tautology is a formula true by the tables under all assignments of values to its atoms (Definition 7.2). The coincidence of these two predicates is the content of the soundness and completeness theorems (E. Post, 1921; a derivation from a truth table is constructed in the proof of L. Kalmár, 1935), not a definition.

The axioms are given by schemata.

Each instance is obtained by substituting formulas for atoms in a concrete formula and is a formula by Proposition 3.4.

5. Derivability in the context of a list of hypotheses

In a set-theoretic presentation the derivability relation connects an arbitrary, possibly infinite, set of formulas with a single formula. The finitary metatheory has no notion of set, and hypotheses are written as a finite list of formulas. However, forming a list of formulas requires introducing into the alphabet some fresh symbol, a separator of the formulas in the list, so that the list can be parsed unambiguously into formulas. We therefore add the comma to the alphabet as a new symbol and denote the new extended alphabet by \(\Alf'\).

Since the extended alphabet contains the original one, the predicates \(\Atom\), \(\Form\), \(\Thm\) over the new alphabet define exactly the same classes of words, and the meaning of the variables \(\mathcal{A},\mathcal{B},\dots\) and \(a,b,\dots\) remains the same. The comma makes it possible to define a new kind of word: a list of formulas. Since the lowercase Greek letters were earlier reserved for words over the original alphabet only, for words over the new alphabet we use capital Greek letters: \(\Gamma,\Delta\). Their range automatically includes the words over the old alphabet as well.

Formulas contain no comma, so the decomposition of a list into its constituent formulas is unique.

A list of hypotheses is fixed and called a context. Instead of a binary relation between lists and formulas, a predicate on formulas is introduced that depends on the context as a parameter. The empty context, that is, the absence of hypotheses, is also allowed. The empty context is not a word: it is the case in which the parameter is not specified, so no notation for it is required. From now on the letters \(\Gamma, \Delta\) denote contexts. For empty \(\Gamma\) no formula occurs in it, the expression \(\Gamma, \mathcal{A}\) denotes the list consisting of the single formula \(\mathcal{A}\), and the expression \(\Gamma \vdash \mathcal{A}\) takes the form \(\vdash \mathcal{A}\).

Example of a derivation. A derivation in a context is a finite chain of formulas, each of which is an axiom (D1), a hypothesis (D2) or is obtained from two preceding ones by Modus Ponens (D3). For any atoms \(a, b\) one has \(a, \neg a \vdash b\):

The rows of the table contain metavariables and are not words of the language of PC, so what is given is not one derivation but a derivation schema: each instantiation of the metavariables \(a, b\) by concrete atoms gives a separate derivation, and there are infinitely many such derivations.

\(\Gamma[\mathcal{B}/a]\) denotes the context obtained from \(\Gamma\) by substitution in each of its formulas.

Proposition 5.6 imposes no restrictions on the variables of the formula \(\mathcal{B}\): substitution is performed in a single pass, and substituted occurrences are not scanned again. A condition arises only with several successive substitutions when the result has to coincide with a given formula: the next substitution also affects the atoms introduced by the previous one.

Bijectivity is essential: the formula \(a \to a\) is a theorem and is obtained by identifying atoms in the formula \(a \to b\), which is not a theorem (§ 7).

The example continued. The schema \(a, \neg a \vdash b\) carries over from atoms to formulas. For formulas \(\mathcal{A}, \mathcal{B}\) one chooses an atom \(b\) not occurring in \(\mathcal{A}\) and an atom \(a\) different from \(b\). Substituting \(\mathcal{A}\) for \(a\) gives \(\mathcal{A}, \neg\mathcal{A} \vdash b\). Since \(\mathcal{A}\) does not contain the atom \(b\), it does not occur in this context, and substituting \(\mathcal{B}\) for \(b\) gives \(\mathcal{A}, \neg\mathcal{A} \vdash \mathcal{B}\). By monotonicity (Proposition 5.4), any formula is derivable from every context containing a formula and its negation.

Part II. Models of the propositional calculus

6. The purpose of models

Part I defines theorems and derivability as properties of words. The derivability of a formula is confirmed by exhibiting a derivation, whereas its non-derivability cannot be seen directly from the definition: for that one would have to go through all possible derivations (because of Modus Ponens there arises the problem of finding the required premise \(\mathcal A\), which is absent from the consequent). A model solves this problem. Formulas are assigned elements of some algebra (an evaluation of formulas) in such a way that all derivable formulas (theorems) receive one particular value in this algebra; formulas with other values are not derivable. The scheme of such an assignment is shown in Fig. 3: the values of atoms are given arbitrarily, the value of every other formula is determined by its structure, and all theorems receive the value \(1\).

The word “model” is used here in the strict mathematical sense, with a connotation entirely opposite to the one considered in § 1: there the question was whether PC models an external phenomenon, while here mathematical structures serve as models of PC. Truth tables are part of the same replacement and say nothing about ordinary logic.

A mathematical model may be used to interpret or justify a phenomenon or construction both outside mathematics and within mathematics itself. A model of the propositional calculus is precisely the second case: we construct a class of set-theoretic models of a certain formal calculus. The aim of such modelling is to transpose a purely syntactic calculus into the language of algebra (or of other branches of mathematics, for instance topology), in order, on the one hand, to make use of a more familiar set of notions and, on the other, to gain access to the tools of the developed apparatus of algebraic structures (see § 10 for an example). At the same time, the construction of a model (or, more precisely, of a class of models) demands of it a certain exactness: in translating from the language of the calculus into the language of algebra we must reproduce all derivable relations between formulas up to their equivalence (soundness) and take care not to introduce new ones (completeness).

Moreover, this translation must be arranged so that every result about formulas can be interpreted unambiguously in the models and, conversely, every algebraic result (equation) common to the models of the given class can be interpreted unambiguously (modulo a strictly defined equivalence of formulas) in the calculus. This is why the two main requirements on a class of models, soundness and completeness, are decisive in choosing a class of models of a calculus. There may be several (or infinitely many) such classes; such classes may contain just a single model or many (not necessarily isomorphic) models; the way they are constructed may be anything within classical set theory; but soundness and completeness of the classes must be observed unconditionally if we want an exact algebraic picture of the calculus.

Note that it is the class of models, and not one particular model, that accomplishes sound and complete interpretation, because each particular model in the class may have some quite specific algebraic theorems that fail for the class as a whole and fail (after translation back) in the calculus. This both simplifies the situation with interpretation and complicates it. It simplifies it because the set of theorems common to the whole class of models may be considerably narrower than the theory of one particular model; it complicates it because we have to describe many models at once, keeping in mind various “edge cases”.

In this part the metatheory freely uses sets, functions and relations; the finitary restrictions of Part I are lifted for convenience and for full mathematical freedom of reasoning. The notations for the metavariables \(\mathcal{A}, \mathcal{B}, \mathcal{C}\) (for formulas), \(a, b, c\) (the beginning of the Latin alphabet, for propositional variables), \(\Gamma,\Delta\) (for contexts) and \(\vdash\) (derivability) retain the same meaning as before. New: we agree to reserve part of the Latin alphabet (a few letters at the end), that is, letters such as \(x, y, z\), for values of formulas, that is, elements of a model, the Greek \(\varepsilon\) for the valuation function, and \(n,m,k\) for natural numbers. Naturally, we shall also not hesitate to use subscripts and primes to increase the number of available variables.

7. The functional model

On the set \(\mathbb{B}=\{0,1\}\) the following operations are given: \(\neg x = 1-x\), \(x \land y = \min(x,y)\), \(x \lor y = \max(x,y)\), \(x \to y = \max(1-x, y)\). Their truth table is: \[\def\arraystretch{1.15} \begin{array}{cc|cccc} x & y & \neg x & x \land y & x \lor y & x \to y \\ \hline 0 & 0 & 1 & 0 & 0 & 1 \\ 0 & 1 & 1 & 0 & 1 & 1 \\ 1 & 0 & 0 & 0 & 1 & 0 \\ 1 & 1 & 0 & 1 & 1 & 1 \end{array}\]

The value \(\varepsilon(\mathcal{A})\) depends only on the values of \(\varepsilon\) on the atoms occurring in \(\mathcal{A}\). Therefore a formula all of whose atoms are among \(a_1, \dots, a_n\) defines a function \(f_{\mathcal{A}} \colon \mathbb{B}^n \to \mathbb{B}\). The set \(B_n\) of all such functions with pointwise operations is called the functional model in \(n\) variables; here \(f_{\neg\mathcal{A}} = \neg f_{\mathcal{A}}\) and \(f_{\mathcal{A} \circ \mathcal{B}} = f_{\mathcal{A}} \circ f_{\mathcal{B}}\), where \(\circ\) on the right-hand side is understood pointwise. The model \(B_n\) has exactly \(2^{2^n}\) elements.

Substitution of a formula into a formula corresponds to a shift of the valuation: \(\varepsilon(\mathcal{A}[\mathcal{B}/a]) = \varepsilon'(\mathcal{A})\), where the valuation \(\varepsilon'\) coincides with \(\varepsilon\) everywhere except that \(\varepsilon'(a) = \varepsilon(\mathcal{B})\). This is checked by structural induction on \(\mathcal{A}\).

Hence an atom is not a theorem (take \(\varepsilon(a)=0\)), \(a \nvdash a \land \neg a\), and the pair \(\vdash \mathcal{A}\), \(\vdash \neg\mathcal{A}\) is impossible (consistency of PC).

A tuple of values \(\langle x_1, \dots, x_n \rangle \in \mathbb{B}^n\) is abbreviated \(\vec{x}\), so that \(f(\vec{x})\) means \(f(x_1, \dots, x_n)\).

Functional completeness means that every function is expressible by a formula and differs from logical completeness. The converse of Proposition 7.3 (everything true in the model is derivable) follows from the general construction for Boolean algebras and is proved in Theorem 9.3.

8. Boolean algebras as models

A Boolean algebra is a distributive lattice \(\langle B, \land, \lor, 0, 1 \rangle\) with complement: \(x \land \neg x = 0\), \(x \lor \neg x = 1\). In it one sets \(x \to y = \neg x \lor y\), and \(x \leqslant y\) means \(x \land y = x\). Examples: \(\mathbb{B}\); the functional model \(B_n\); the set of all subsets of a set \(X\) with the set-theoretic operations. The one-element algebra, in which \(0=1\), is not excluded.

A valuation with values in a Boolean algebra \(B\) is given and extended as in Definition 7.1. The notation \(\Gamma \models_{\mathsf{BA}} \mathcal{A}\) means: in every Boolean algebra \(B\), every valuation \(\varepsilon\) such that \(\varepsilon(\mathcal{C})=1\) for all \(\mathcal{C} \trianglelefteq \Gamma\) satisfies \(\varepsilon(\mathcal{A})=1\). The relation \(\models_{\mathbb{B}}\) is the special case with the single model \(\mathbb{B}\).

9. Completeness

9.1. Completeness with respect to the class of Boolean algebras

A model refuting a non-derivable formula is constructed from the syntax itself. A context \(\Gamma\) is fixed. The notation \(\mathcal{A} \preceq \mathcal{B}\) means \(\Gamma \vdash \mathcal{A} \to \mathcal{B}\); formulas are equivalent, \(\mathcal{A} \sim \mathcal{B}\), if \(\mathcal{A} \preceq \mathcal{B}\) and \(\mathcal{B} \preceq \mathcal{A}\).

By the lemma, \(\sim\) is a congruence, and the classes \([\mathcal{A}]\) with the operations \([\mathcal{A}] \land [\mathcal{B}] = [\mathcal{A} \land \mathcal{B}]\), \([\mathcal{A}] \lor [\mathcal{B}] = [\mathcal{A} \lor \mathcal{B}]\), \(\neg[\mathcal{A}] = [\neg\mathcal{A}]\) form a Boolean algebra \(\mathsf{LT}_\Gamma\), the Lindenbaum–Tarski algebra of the context \(\Gamma\); for the empty context it is denoted \(\mathsf{LT}\). By item (7), its unit is the class of formulas derivable in the context. By item (6), \([\mathcal{A} \to \mathcal{B}] = [\mathcal{A}] \to [\mathcal{B}]\).

Translation dictionary. The construction \(\mathsf{LT}_\Gamma\) translates the calculus into the language of algebra. The order of the Boolean algebra is the relation \(\preceq\): the inequality \([\mathcal{A}] \leqslant [\mathcal{B}]\) means \(\Gamma \vdash \mathcal{A} \to \mathcal{B}\), that is, by the deduction theorem, \(\Gamma, \mathcal{A} \vdash \mathcal{B}\). Therefore, for a context consisting of one formula, the derivability sign translates into the inequality sign. For the algebra \(\mathsf{LT}\) the translation is as follows:

9.2. Reduction to a single model

10. Computation in the model: Zhegalkin polynomials

The translation into the language of algebra yields not only a check of derivability by going through the rows of a truth table, but also computation by the rules of arithmetic. For this purpose the Boolean algebra is rebuilt into a ring.

In a Boolean algebra one sets \(xy = x \land y\) and \(x + y = (x \land \neg y) \lor (\neg x \land y)\). On \(\mathbb{B}\) these are multiplication and addition modulo \(2\). Therefore \(\mathbb{B}\) satisfies the laws of a commutative ring with unit, the identities \(x^2 = x\) and \(x + x = 0\), and also the equalities \[\neg x = 1 + x, \qquad x \lor y = x + y + xy, \qquad x \to y = 1 + x + xy.\] By Lemma 8.1 (b) all this holds in every Boolean algebra: it is a commutative ring with unit in which \(x^2 = x\) (a Boolean ring; M. Stone, 1936), and the connectives are expressed through the ring operations.

Example. Peirce's law \(((a \to b) \to a) \to a\) is checked in two lines. We have \(p_{a \to b} = 1 + a + ab\), whence \[p_{(a \to b) \to a} = 1 + (1 + a + ab) + (1 + a + ab)a = a + ab + ab = a,\] that is, the formula \((a \to b) \to a\) is equivalent to the atom \(a\). Therefore \(p_{((a \to b) \to a) \to a} = 1 + a + a \cdot a = 1\), and the formula is derivable; the derivation from the axioms itself is not required for this.

General statements. A truth table checks each formula separately, whereas computation in the ring yields statements about infinite families of formulas. The expression \(\mathcal{A} \leftrightarrow \mathcal{B}\) abbreviates \((\mathcal{A} \to \mathcal{B}) \land (\mathcal{B} \to \mathcal{A})\). Its polynomial is linear: \(p_{\mathcal{A} \leftrightarrow \mathcal{B}} = 1 + p_{\mathcal{A}} + p_{\mathcal{B}}\).

Context and ideal. In the ring a context translates into an ideal: \(\mathcal{C}_1, \dots, \mathcal{C}_k \vdash \mathcal{B}\) if and only if \(1 + p_{\mathcal{B}}\) lies in the ideal generated by the polynomials \(1 + p_{\mathcal{C}_i}\). If \(1 + p_{\mathcal{B}}\) lies in this ideal, then wherever all \(p_{\mathcal{C}_i}\) equal \(1\), the polynomial \(p_{\mathcal{B}}\) also equals \(1\), and Theorem 9.3 applies. Conversely, for \(q = p_{\mathcal{C}_1} \cdots p_{\mathcal{C}_k}\), derivability means \(q(1 + p_{\mathcal{B}}) = 0\), whence \(1 + p_{\mathcal{B}} = (1 + q)(1 + p_{\mathcal{B}})\), and \(1 + q\) lies in the ideal. The homomorphism \(h\) from the proof of Theorem 9.3 is an epimorphism onto \(\mathbb{F}_2\), and the complement of the ultrafilter \(U\) is its kernel, a maximal ideal of the ring \(\mathsf{LT}_\Gamma\).

11. Duality, uniqueness of the two-valued model and Post completeness

The truth table of § 7 is not selected from among others: the axioms and Modus Ponens determine it uniquely up to the permutation of the values \(0\) and \(1\), and this permutation corresponds to passing to dual formulas. Nor can the calculus be extended while preserving consistency and closure under substitution.

In terms of the dictionary, duality reverses the order: the map \(y \mapsto \neg y\) is an isomorphism of a Boolean algebra onto the algebra in which \(\land\) and \(\lor\), \(0\) and \(1\) exchange roles. Therefore together with every identity its dual holds; thus distributivity \(x \land (y \lor z) = (x \land y) \lor (x \land z)\) implies \(x \lor (y \land z) = (x \lor y) \land (x \lor z)\), and to the theorem \(a \lor \neg a\) there corresponds the theorem \(\neg(a \land \neg a)\).

The number of tuples of operations on \(\{0,1\}\) equals \(4 \cdot 16^3 = 16384\), and for each of the two distinguished values exactly one tuple is a model of PC. For the distinguished value \(1\) this is \(\mathbb{B}\). For the distinguished value \(0\) this is the flipped model: \(\neg x = 1 - x\), \(x \land y = \max(x,y)\), \(x \lor y = \min(x,y)\), \(x \to y = \min(1-x, y)\). The permutation of values is an isomorphism between these two models. The value of a formula \(\mathcal{A}\) in the flipped model equals the value of \(\mathcal{A}^*\) in \(\mathbb{B}\) under the same valuation, so computation in the flipped model is computation of the dual formula: a formula \(\mathcal{A}\) is a theorem if and only if \(f_{\mathcal{A}^*}\) is identically equal to \(0\).

By Theorem 9.3 the theorems are exactly the tautologies, so every calculus in the same language that is sound with respect to \(\mathbb{B}\) is contained in PC. With closure under substitution preserved, PC can be extended only to an inconsistent calculus.

This result was obtained by D. Hilbert and P. Bernays (1918; see Zach, 1999) and by E. Post (1921). Consequently, every consistent calculus in the same language that is closed under substitution and Modus Ponens and differs from PC fails to contain some of its theorems. Such is the position of intuitionistic logic, relevance logics and many-valued logics lying between intuitionistic and classical logic: their theorems form a part of the theorems of PC.

Summary

The construction of Part I consists of the following stages.

1. 1.

   PC is introduced as an explicatum: a formal system replacing ordinary reasoning in the functions required by mathematical proof. Its correspondence with ordinary logic is not a theorem and is not established by the completeness theorem; its domain of application is mathematics, including computer science.

2. 2.

   The finitary base of the metalanguage is fixed: a finite list of signs, words and concatenation, graphic identity \(\equiv\), predicates, ordinary logic in simple formulations, recursive construction of classes of words, and metavariables.

3. 3.

   The alphabet \(\Alf\) and the words \(\Alf^*\) with metavariables \(\xi, \eta, \zeta\) are given; the predicates \(\Atom\) and \(\Form\) with metavariables \(a, b, c\) and \(\mathcal{A}, \mathcal{B}, \mathcal{C}\) are constructed; the substitution \(\mathcal{A}[\mathcal{B}/a]\), which preserves formulas, is introduced; unique parsing is proved.

4. 4.

   The axioms are given by schemata, and the theorem predicate \(\Thm\) by closure under Modus Ponens.

5. 5.

   Finite lists of formulas are defined as words over the extended alphabet \(\Alf'\); derivability \(\Gamma \vdash \mathcal{A}\) is given as a predicate on formulas in a context \(\Gamma\), which may be empty; it is preserved under substitution carried out consistently in the context and in the conclusion.

6. 6.

   The notion of finite iteration and contentual arithmetic are retained (Remark 2.1); statements about arbitrary infinite totalities of hypotheses are not formulated in the base.

Part II translates the calculus into the language of algebra: formulas are assigned values, and the main requirements on a class of models are soundness and completeness. The functional model \(B_n\) reduces a formula with \(n\) atoms to a Boolean function, and every such function is given by a formula. Boolean algebras form a class of models with respect to which PC is complete by virtue of the construction \(\mathsf{LT}_\Gamma\); this construction yields a translation dictionary in which derivability corresponds to the order of the algebra. Post's theorem reduces the class to the single model \(\mathbb{B}\), and Corollary 9.4 identifies \(B_n\) with a fragment of the Lindenbaum–Tarski algebra. In the Boolean ring formulas are written by Zhegalkin polynomials, and logical computations reduce to arithmetic modulo \(2\). The two-valued model is unique up to the permutation of values, and this permutation corresponds to passing to dual formulas. PC cannot be extended while preserving consistency and closure under substitution.

References

• Carnap R. Logical Foundations of Probability. Chicago: University of Chicago Press, 1950.
• Carroll L. What the Tortoise said to Achilles // Mind. 1895. Vol. 4.
• Hilbert D., Bernays P. Grundlagen der Mathematik. Vol. 1. Berlin: Springer, 1934.
• Kazimirov N. I. The Architecture of Mathematical Models: course notes, subsection “The Lindenbaum–Tarski algebra”.
• Kazimirov N. I. Mathematics as a Foreign Language. mathem.at/Materials/maglish_index_en.html
• Kleene S. C. Introduction to Metamathematics. Amsterdam: North-Holland, 1952.
• Kreisel G. Informal rigour and completeness proofs // Problems in the Philosophy of Mathematics / ed. I. Lakatos. Amsterdam: North-Holland, 1967.
• Markov A. A. Theory of algorithms // Trudy Mat. Inst. Steklov. 1954. Vol. 42 (in Russian).
• Post E. Introduction to a general theory of elementary propositions // American Journal of Mathematics. 1921. Vol. 43.
• Quine W. V. O. Word and Object. Cambridge, MA: MIT Press, 1960.
• Rasiowa H., Sikorski R. The Mathematics of Metamathematics. Warsaw: PWN, 1963.
• Zach R. Completeness before Post: Bernays, Hilbert, and the development of propositional logic // Bulletin of Symbolic Logic. 1999. Vol. 5.
• Zhegalkin I. I. On the technique of calculating propositions in symbolic logic // Matematicheskii Sbornik. 1927. Vol. 34, no. 1 (in Russian).