The history of logic contains several different questions about the rules of inference. Must every statement receive exactly one of two truth values? Must a premise contribute to its conclusion? Can inconsistent information be used without making every conclusion follow? Can an assumption be copied or discarded freely?
Each question motivates a different mathematical investigation. The answers should not be grouped into an undifferentiated alternative to classical logic.
The intuitionism note examined constructive evidence. The modal-logic note examined operators interpreted through related situations. This note develops four further changes, identifying the exact feature at issue in each case.
Many-valued logic: changing the semantic values
Jan Łukasiewicz introduced a three-valued calculus in 1920, initially connected with philosophical questions about future contingents. Emil Post independently investigated general finite-valued propositional systems in his 1921 dissertation work.
Their contributions opened a mathematical study of logical matrices: a set of values, operations interpreting connectives, and designated values that count as acceptable conclusions.
In Łukasiewicz's three-valued system, use values and designate only . Negation is , and implication is
The implication table is therefore:
| Antecedent / consequent | |||
|---|---|---|---|
With disjunction interpreted as the maximum, receives when does. It is consequently not valid in this matrix.
Modus ponens nevertheless preserves designation. If and , the last row forces .
The calculation matters more than calling the middle value “unknown.” Different systems can use three values with different operations and different designated sets. Kleene's treatments of partial computation, for example, have another motivation. A value is not a probability merely because it is written as a number.
This tradition eventually connects with algebraic logic and fuzzy logics, including later work by Zadeh and Hájek. Those connections require additional semantics; they do not follow just from adding a third value. The historical account of many-valued logic distinguishes these developments.
Sources and credit for Emil Leon Post
Creator not identified in the source record. Via Wikimedia Commons. Image source · Public domain · Biographical dates
Sources and credit for Jan Łukasiewicz
National Digital Archives of Poland; photographer not identified in the source record. Via Wikimedia Commons. Image source · Public domain · Biographical dates
Sources and credit for Lotfi A. Zadeh
BBR100. Via Wikimedia Commons. Image source · CC BY-SA 4.0 · Biographical dates
Sources and credit for Petr Hájek
M. H.. Via Wikimedia Commons. Image source · CC0 · Biographical dates
Relevance: requiring a connection
Classical propositional logic validates
Under the truth-functional interpretation, this is straightforward: once is true, the truth of cannot make false.
As a statement of relevant implication, however, seems to assert a connection that the premises have not supplied. The unrelated assumption does no work.
Alan Anderson and Nuel Belnap developed influential systems of relevance and entailment, brought together in Entailment in 1975, with later volumes and contributions by collaborators. Their work has predecessors in concerns about implication, including Ackermann's investigations.
One useful diagnostic is the variable-sharing property of standard relevant systems such as R: a theorem of the form must have a propositional variable shared between and . This rules out arbitrary theorems with disjoint variables.
Variable sharing is a necessary test in that setting, not a complete definition of relevant validity. The nested formula above requires a more careful analysis than inspecting its outermost variables.
Proof systems can track which assumptions a conclusion uses. Semantics developed by Routley, Meyer, and others supply mathematical interpretations of relevant connectives, often with structures more elaborate than ordinary two-valued truth tables.
The point is not that classical logic made an arithmetical mistake. Different systems formalize different intended relations between premises and conclusions.
Paraconsistency: separating inconsistency from triviality
Classical consequence validates explosion:
A familiar derivation first infers from and then uses to eliminate the first disjunct. If all those rules remain unrestricted, a contradiction supports any conclusion.
A paraconsistent consequence relation blocks explosion in at least some cases. This permits a distinction between a theory containing a contradiction and a theory in which every sentence is derivable.
Stanisław Jaśkowski's discussive logic of 1948 and Newton da Costa's systems developed from the 1950s and 1960s supplied different approaches. Later work includes Graham Priest's Logic of Paradox and the information-oriented semantics associated with Nuel Belnap and J. Michael Dunn.
Sources and credit for Newton da Costa
George Bergman. Via Wikimedia Commons. Image source · GFDL 1.2 · Biographical dates
Sources and credit for Graham Priest
Philosophy at the University of Edinburgh. Via Wikimedia Commons. Image source · CC BY 4.0 · Biographical dates
A simple semantic illustration uses the values true only, false only, and both true and false. Designate true only and both. In the familiar three-valued LP interpretation, negation exchanges true only and false only while preserving both.
Assign the value both and the value false only. Then and are designated, but is not. Designation-preserving consequence therefore does not validate explosion.
This example concerns LP's consequence relation. It is not a definition of every paraconsistent logic, and its implication behavior should not be silently identified with ordinary classical implication.
Paraconsistency also does not require the philosophical belief that some contradictions are true. A researcher may use it to reason cautiously with conflicting records while regarding the underlying conflict as an error to investigate.
Conversely, many-valuedness alone does not imply paraconsistency. The Łukasiewicz matrix above designates only ; no value makes both and designated. Its treatment of contradiction is therefore different.
Structural rules: how assumptions may be used
The Gentzen note introduced sequents. Some rules manipulate the surrounding collection of assumptions rather than the internal form of a connective.
Weakening permits an unused assumption:
Contraction permits two uses to be supplied by one assumption:
Exchange permits assumptions to be reordered. These rules are natural when an assumption represents an indefinitely reusable truth. Other interpretations give them substantive consequences.
Joachim Lambek's 1958 calculus, developed in connection with the mathematics of sentence structure, restricted structural behavior. Order matters when expressions occupy positions in a sentence.
Jean-Yves Girard's 1987 linear logic made the use of assumptions a central object of proof-theoretic analysis. Its distinctions support applications to computation, semantics, and resource-sensitive reasoning.
Sources and credit for Joachim Lambek
Andrej Bauer.. Via Wikimedia Commons. Image source · CC BY-SA 2.5 si · Biographical dates
Sources and credit for Jean-Yves Girard
UTLS. Via Wikimedia Commons. Image source · CC BY-SA 4.0 · Biographical dates
A linear example
Write for a linear implication and for multiplicative conjunction.
If a process consumes an to produce a , the sequent
expresses an appropriate use of the supplied input and process.
By contrast,
is not generally derivable in the corresponding linear fragment. Tensor introduction must divide the available assumptions between two branches. A single unrestrictedly uncopyable occurrence of cannot supply both.
This is a statement about the formal use of assumptions. Reading as one ticket or one unit of fuel can help, but logical resources need not be physical consumables.
Linear logic also distinguishes multiplicative and additive connectives. Their introduction rules allocate or share contexts in different ways. That distinction would disappear if one simply replaced every conjunction symbol with the same connective.
The exponential marks a controlled way to recover weakening and contraction. A reusable assumption can then be duplicated or omitted according to the relevant rules. Linear logic therefore explains where unrestricted reuse is permitted instead of merely banning reuse everywhere.
Four changes, four standards of explanation
| Tradition | Central issue | What an adequate example must identify |
|---|---|---|
| Many-valued logic | Semantic values and designated values | The operations and the criterion for consequence |
| Relevant logic | Connection between premises and conclusion | The intended implication and its proof or semantic restrictions |
| Paraconsistent logic | Inconsistency without explosion | A contradictory set of premises that does not entail everything |
| Linear logic | Use of assumptions | The structural rules available for each kind of assumption |
These investigations can overlap. A system may be both relevant and paraconsistent, or admit a many-valued semantics. Their overlap does not erase the differences in motivation or formal definition.
The history also changes how we read the phrase “the rules of logic.” A rule can be assessed against a specified interpretation, a proof-theoretic discipline, or an intended application. The resulting mathematics makes the choice explicit.
From assumptions to computation
Once a derivation records how assumptions are introduced, combined, and discharged, it begins to resemble a structured computation. This resemblance becomes exact for suitable calculi.
The next note constructs a proof and a typed program together, showing why normalization of a proof can correspond to evaluation of a program.
Sources and further reading
- Jan Łukasiewicz, writings on three-valued logic from 1920; Emil L. Post, “Introduction to a General Theory of Elementary Propositions” (1921).
- Alan R. Anderson and Nuel D. Belnap Jr., Entailment, volume I (1975).
- Stanisław Jaśkowski, “A Propositional Calculus for Inconsistent Deductive Systems” (1948); Newton C. A. da Costa, papers on inconsistent formal systems.
- Graham Priest, “The Logic of Paradox” (1979).
- Joachim Lambek, “The Mathematics of Sentence Structure” (1958).
- Jean-Yves Girard, “Linear Logic” (1987), Theoretical Computer Science 50, 1–102.
- Many-Valued Logic, Stanford Encyclopedia of Philosophy, for historical orientation and distinctions among semantic traditions.