Revision theory is a subfield of philosophical logic. It consists of a general theory of definitions, including (but not limited to) circular and interdependent concepts. A circular definition is one in which the concept being defined occurs in the statement defining it—for example, defining a G as being blue and to the left of a G. Revision theory provides formal semantics for defined expressions, and formal proof systems study the logic of circular expressions.
Definitions are important in philosophy and logic. Although circular definitions have been regarded as logically incorrect or incoherent, revision theory demonstrates that they are meaningful and can be studied with mathematical and philosophical logic. It has been used to provide circular analyses of philosophical and logical concepts.
History Revision theory is a generalization of the revision theories of truth developed by Anil Gupta, Hans Herzberger, and Nuel Belnap.See, respectively, Gupta (1982), Herzberger (1982), and Belnap (1982). In the revision theories of Gupta and Herzberger, revision is supposed to reflect intuitive evaluations of sentences that use the truth predicate. Some sentences are stable in their evaluations, such as the truth-teller sentence, The truth-teller is true. Assuming the truth-teller is true, it is true, and assuming that it is false, it is false. Neither status will change. On the other hand, some sentences oscillate, such as the liar, The liar sentence is not true. On the assumption that the liar is true, one can show that it is false, and on the assumption that it is false, one can show that it is true. This instability is reflected in revision sequences for the liar.
The generalization to circular definitions was developed by Gupta, in collaboration with Belnap. Their book, The Revision Theory of Truth, presents an in-depth development of the theory of circular definitions, as well as an overview and critical discussion of philosophical views on truth and the relation between truth and definition.
Philosophical background The philosophical background of revision theory is developed by Gupta and Belnap.Gupta and Belnap (1993) Other philosophers, such as Aladdin Yaqūb, have developed philosophical interpretations of revision theory in the context of theories of truth, but not in the general context of circular definitions.Yaqūb (1993)
Gupta and Belnap maintain that circular concepts are meaningful and logically acceptable. Circular definitions are formally tractable, as demonstrated by the formal semantics of revision theory. As Gupta and Belnap put it, "the moral we draw from the paradoxes is that the domain of the meaningful is more extensive than it appears to be, that certain seemingly meaningless concepts are in fact meaningful."Gupta and Belnap (1993, 278)
The meaning of a circular predicate is not an extension, as is often assigned to non-circular predicates. Its meaning, rather, is a rule of revision that determines how to generate a new hypothetical extension given an initial one. These new extensions are at least as good as the originals, in the sense that, given one extension, the new extension contains exactly the things that satisfy the definiens for a particular circular predicate. In general, there is no unique extension on which revision will settle.This point is discussed further by Gupta and Belnap (1993, 121), Shapiro (2006), and Gupta (2011, 160-161).
Revision theory offers an alternative to the standard theory of definitions. The standard theory maintains that good definitions have two features. First, defined symbols can always be eliminated, replaced by what defines them. Second, definitions should be conservative in the sense that adding a definition should not result in new consequences in the original language. Revision theory rejects the first but maintains the second, as demonstrated for both of the strong senses of validity presented below.
The logician Alfred Tarski presented two criteria for evaluating definitions as analyses of concepts: formal correctness and material adequacy. The criterion of formal correctness states that in a definition, the definiendum must not occur in the definiens. The criterion of material adequacy says that the definition must be faithful to the concept being analyzed. Gupta and Belnap recommend siding with material adequacy in cases in which the two criteria conflict.Gupta and Belnap (1993, 277) To determine whether a circular definition provides a good analysis of a concept requires evaluating the material adequacy of the definition. Some circular definitions will be good analyses, while some will not. Either way, formal correctness, in Tarski's sense, will be violated.
Semantics for circular predicates The central semantic idea of revision theory is that a definition, such as that of being a , provides a rule of revision that tells one what the new extension for the definiendum should be, given a hypothetical extension of the definiendum and information concerning the undefined expressions. Repeated application of a rule of revision generates sequences of hypotheses, which can be used to define logics of circular concepts. In work on revision theory, it is common to use the symbol, , to indicate a definition, with the left-hand side being the definiendum and the right-hand side the definiens. The example
Being a is defined as being both blue and to the left of a
can then be written as
Being a being both blue and to the left of a .
Given a hypothesis about the extension of , one can obtain a new extension for appealing to the meaning of the undefined expressions in the definition, namely blue and to the left of.
We begin with a ground language, , that is interpreted via a classical ground model , which is a pair of a domain and an interpretation function .This section is based on Gupta and Belnap (1993). Suppose that the set of definitions is the following,
where each is a formula that may contain any of the definienda , including itself. It is required that in the definitions, only the displayed variables, , are free in the definientia, the formulas . The language is expanded with these new predicates, , to form +. When the set contains few defined predicates, it is common to use the notation, to emphasize that may contain .
A hypothesis is a function from the definienda of to tuples of . The model is just like the model except that interprets each definiendum according to the following biconditional, the left-hand side of which is read as “ is true in .”
The set of definitions yields a rule of revision, or revision operator, . Revision operators obey the following equivalence for each definiendum, , in .
A tuple will satisfy a definiendum after revision just in case it satisfies the definiens for , namely , prior to revision. This is to say that the tuples that satisfy according to a hypothesis will be exactly those that satisfy according to the revision of that hypothesis.
The classical connectives are evaluated in the usual, recursive way in . Only the evaluation of a defined predicate appeals to the hypotheses.
Sequences Revision sequences are sequences of hypotheses satisfying extra conditions.This section is based on Gupta and Belnap (1993) and Kremer (2014). We will focus here on sequences that are -long, since transfinite revision sequences require the additional specification of what to do at limit stages.
Let be a sequence of hypotheses, and let be the -th hypothesis in . An -long sequence of hypotheses is a revision sequence just in case for all ,
Recursively define iteration as
and
The -long revision sequence starting from can be written as follows.
One sense of validity, validity, can be defined as follows. A sentence is valid in in on iff there exists an such that for all and for all , . A sentence is valid on just in case it is valid in all .
Validity in can be recast in terms of stability in -long sequences. A sentence is stably true in a revision sequence just in case there is an such that for all , . A sentence is stably false in a revision sequence just in case there is an such that for all , . In these terms, a sentence is valid in in on just in case is stably true in all -long revision sequences on .
Examples For the first example, let be Let the domain of the ground model be , and let and . There are then four possible hypotheses for : , , , . The first few steps of the revision sequences starting from those hypotheses are illustrated by the following table.
+ Sample revision for stage 0stage 1stage 2stage 3
As can be seen in the table, goes in and out of the extension of . It never stabilizes. On the other hand, either stays in or stays out. It is stable, but whether it is stably true or stably false depends on the initial hypothesis.
Next, let be As shown in the following table, all hypotheses for the ground model of the previous example are revised to the set .
+ Sample revision for stage 0stage 1stage 2stage 3
For a slightly more complex revision pattern, let contain and all the numerals, , and let the ground model be , whose domain is the natural numbers, , with interpretation such that for all numerals and is the usual ordering on natural numbers. Let be Let the initial hypothesis be . In this case, the sequence of extensions builds up stage by stage.
Although for every , is valid in , is not valid in .
Suppose the initial hypothesis contains 0, 2, and all the odd numbers. After one revision, the extension of will be . Subsequent revisions will build up the extension as with the previous example. More generally, if the extension of is not all of , then one revision will cut the extension of down to a possibly empty initial segment of the natural numbers and subsequent revisions will build it back up.
Proof system There is a Fitch-style natural deduction proof system, , for circular definitions.A presentation of can be found in chapter 5 of Gupta and Belnap (1993). The system uses indexed formulas, , where can be any integer. One can think of the indices as representing relative position in a revision sequence. The premises and conclusions of the rules for the classical connectives all have the same index. For example, here are the conjunction and negation introduction rules.
| In
| |__
| In
For each definition, , in , there is a pair of rules.
| DfIn
| DfElim In these rules, it is assumed that are free for in .
Finally, for formulas of , there is one more rule, the index shift rule.
| IS In this rule, and can be any distinct indices. This rule reflects the fact that formulas from the ground language do not change their interpretation throughout the revision process.
The system is sound and complete with respect to validity, meaning a sentence is valid in just in case it is derivable in .
Recently Riccardo Bruni has developed a Hilbert-style axiom system and a sequent system that are both sound and complete with respect to .Bruni (2013)
Transfinite revision For some definitions, validity is not strong enough.The definitions of this section are taken from Gupta and Belnap (1993). For example, in definition , even though every number is eventually stably in the extension of , the universally quantified sentence is not valid. The reason is that for any given sentence to be valid, it must stabilize to true after finitely many revisions. On the other hand, needs infinitely many revisions, unless the initial hypothesis already assigns all the natural numbers as the extension of .
Natural strengthenings of validity, and alternatives to it, use transfinitely long revision sequences. Let be the class of all ordinals. The definitions will focus on sequences of hypotheses that are -long.