Linear logic
Encyclopedia
Linear logic is a substructural logic
proposed by Jean-Yves Girard
as a refinement of classical
and intuitionistic logic
, joining the dualities
of the former with many of the constructive
properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics
, and quantum physics, and to a lesser extent in linguistics
(see Glue Semantics
) particularly because of its emphasis on resource-boundedness, duality, and interaction.
Linear logic lends itself to many different presentations, explanations and intuitions.
Proof-theoretically, it derives from an analysis of classical sequent calculus
in which uses of (the structural rule
s) contraction
and weakening
are carefully controlled. Operationally, this means that logical deduction is no longer merely about an ever-expanding collection of persistent "truths", but also a way of manipulating resources that can not always be duplicated or thrown away at will. In terms of simple denotational models, linear logic may be seen as refining the interpretation of intuitionistic logic by replacing cartesian closed categories by symmetric monoidal categories, or the interpretation of classical logic by replacing boolean algebras by C*-algebras.
Here and range
over logical atoms
. For reasons to be explained
below, the connectives , , 1, and
are called multiplicatives, the connectives &,
, , and 0 are called additives, and the
connectives ! and ? are called exponentials. We can further
employ the following terminology:
is called "multiplicative conjunction" or "times" (or sometimes "tensor") is called "additive disjunction" or "plus"
Every proposition in CLL has a dual , defined as follows:
Observe that is an involution, i.e., for all propositions. is also called the linear negation of .
The columns of the table suggest another way of classifying the connectives of linear logic, termed polarity: the connectives negated in the left column are called positive, while their duals on the right are called negative.
Linear implication is not included in the grammar of connectives, but is definable in CLL using linear negation and multiplicative disjunction, by . The connective is sometimes pronounced "lollipop
", owing to its shape.
. We use the letters and to range over list of propositions , also called contexts. A sequent places a context to the left and the right of the turnstile
, written . Intuitively, the sequent asserts that the conjunction of entails the disjunction of (though we mean the "multiplicative" conjunction and disjunction, as explained below). Girard describes classical linear logic using only one-sided sequents (where the left-hand context is empty), and we follow here that more economical presentation.
We now give inference rules describing how to build proofs of sequents.
First, to formalize the fact that we do not care about the order of propositions inside a context, we add the structural rule of
exchange:
(Alternatively we could accomplish the same thing by defining contexts to be multisets rather than lists.)
Note that we do not add the structural rules of weakening and contraction, because we do care about the
absence of propositions in a sequent, and the number of copies present.
Next we add initial sequents and cuts:
The cut rule can be seen as a way of composing proofs, and initial sequents serve as the units
for composition. In a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof. Ultimately, this canonical form
property (which can be divided into the completeness of atomic initial sequents
and the cut-elimination theorem
, inducing a notion of analytic proof
) lies behind the applications of linear logic in computer science, since it allows the logic to be used in proof search and as a resource-aware lambda-calculus.
Now, we explain the connectives by giving logical rules. Typically in sequent calculus
one gives both "right-rules" and "left-rules" for each connective, essentially describing two modes of reasoning
about propositions involving that connective (e.g., verification and falsification). In a one-sided presentation, one instead makes use of negation: the right-rules for a connective
(say ) effectively play the role of left-rules for its dual . So, we should expect a certain "harmony"
between the rule(s) for a connective and the rule(s) for its dual.
and for their units:
Observe that the rules for multiplicative conjunction and disjunction are admissible
for
plain conjunction and disjunction under a classical interpretation
(i.e., they are admissible rules in LK).
and for their units:
Observe that the rules for additive conjunction and disjunction are again admissible
under a classical interpretation. But now we can explain the basis for the multiplicative/additive distinction
in the rules for the two different versions of conjunction: for the multiplicative connective ,
the context of the conclusion is split up between the premises, whereas
for the additive case connective (&) the context of the conclusion is carried whole into both
premises.
structural rules of weakening and contraction for ?'d propositions:
and use the following logical rules:
One might observe that the rules for the exponentials follow a different pattern from the rules for the other connectives,
and that there is no longer such a clear symmetry between the duals ! and ?. This situation is remedied in alternative
presentations of CLL (e.g., the LU presentation).
Distributivity :
Exponential isomorphism :
(Here
.)
The following is not in general an equivalence, only an implication:
Semi-distributivity :
Formally, there exists a translation of formulae of intuitionistic logic to formulae of linear logic in a way which guarantees that the original formula is provable in intuitionistic logic if and only if the translated formula in provable in linear logic. Using the Gödel–Gentzen negative translation
, we can thus embed classical first-order logic into linear first-order logic.
Suppose we represent a candy bar by the atomic proposition , and a dollar by . To state the fact that a dollar will buy you one candy bar, we might write the implication . But in ordinary (classical or intuitionistic) logic, from and one can conclude . So, ordinary logic leads us to believe that we can buy the candy bar and keep our dollar! Of course,
we can avoid this problem by using more sophisticated encodings, although typically such encodings suffer from the frame problem
. However, the rejection of weakening and contraction allows linear logic to avoid this kind of spurious reasoning even with the "naive" rule. Rather than , we express the property of the vending machine as a linear implication . From and this fact, we can conclude , but not . In general, we can use the linear logic proposition to express the validity of transforming resource into resource .
Running with the example of the vending machine, let us consider the "resource interpretations" of the other multiplicative and additive connectives. (The exponentials provide the means to combine this resource interpretation with the usual notion of persistent logical truth
.)
Multiplicative conjunction denotes simultaneous occurrence of resources, to be used as the consumer directs. For example, if you buy a stick of gum and a bottle of soft drink, then you are requesting . The constant 1 denotes the absence of any resource, and so functions as the unit of .
Additive conjunction represents alternative occurrence of resources, the choice of which the consumer controls. If in the vending machine there is a packet of chips, a candy bar, and a can of soft drink, each costing one dollar, then for that price you can buy exactly one of these products. Thus we write . We do not write , which would imply that one dollar suffices for buying all three products together. However, from , we can correctly deduce , where . The unit of additive conjunction can be seen as a wastebasket or garbage collector
for irrelevant alternatives. For example, we can write to express that three dollars will buy you a candy bar and something else (we don't care what).
Additive disjunction represents alternative occurrence of resources, the choice of which the machine controls. For example, suppose the vending machine permits gambling: insert a dollar and the machine may dispense a candy bar, a packet of chips, or a soft drink. We can express this situation as . The constant 0 represents a product that cannot be made, and thus serves as the unit of (a machine that might produce or is as good as a machine that always produces because it will never succeed in producing a 0).
Multiplicative disjunction is more difficult to gloss in terms of the resource interpretation, although we can encode back into linear implication, either as or .
, proof net have been created to avoid the bureaucracy, that is all the things that make two derivation different in the logical point of view, but not in a “moral” point of view.
For instance, these two proofs are “morally” identical:
The goal of proof net is to make them identical by creating a graphical representation of them.
relation in full CLL is undecidable
. Fragments of
CLL are often considered, for which the decision problem is more subtle:
Different intuitionistic variants of linear logic have been considered. When based on a single-conclusion sequent calculus presentation, like in ILL (Intuitionistic Linear Logic), the connectives , ⊥, and ? are absent, and linear implication is treated as a primitive connective. In FILL (Full Intuitionistic Linear Logic) the connectives , ⊥, and ? are present, linear implication is a primitive connective and, similarly to what happens in intuitionistic logic, all connectives (except linear negation) are independent.
There are also first- and higher-order extensions of linear logic, whose formal development is somewhat standard (see first-order logic
and higher-order logic
).
Substructural logic
In logic, a substructural logic is a logic lacking one of the usual structural rules , such as weakening, contraction or associativity...
proposed by Jean-Yves Girard
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
as a refinement of classical
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
and intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
, joining the dualities
Duality (mathematics)
In mathematics, a duality, generally speaking, translates concepts, theorems or mathematical structures into other concepts, theorems or structures, in a one-to-one fashion, often by means of an involution operation: if the dual of A is B, then the dual of B is A. As involutions sometimes have...
of the former with many of the constructive
Constructivism (mathematics)
In the philosophy of mathematics, constructivism asserts that it is necessary to find a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption, one still has not found the object and therefore not proved its...
properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics
Game semantics
Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes. In the late 1950s Paul Lorenzen was the...
, and quantum physics, and to a lesser extent in linguistics
Linguistics
Linguistics is the scientific study of human language. Linguistics can be broadly broken into three categories or subfields of study: language form, language meaning, and language in context....
(see Glue Semantics
Glue Semantics
Glue semantics, or simply Glue is a linguistic theory of semantic composition and the syntax-semantics interface which assumes that meaning composition is constrained by a set of instructions stated within a formal logic, Linear logic...
) particularly because of its emphasis on resource-boundedness, duality, and interaction.
Linear logic lends itself to many different presentations, explanations and intuitions.
Proof-theoretically, it derives from an analysis of classical sequent calculus
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
in which uses of (the structural rule
Structural rule
In proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgements or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic...
s) contraction
Idempotency of entailment
Idempotency of entailment is a property of logical systems that states that one may derive the same consequences from many instances of a hypothesis as from just one...
and weakening
Monotonicity of entailment
Monotonicity of entailment is a property of many logical systems that states that the hypotheses of any derived fact may be freely extended with additional assumptions. In sequent calculi this property can be captured by an inference rule called weakening, or sometimes thinning, and in such...
are carefully controlled. Operationally, this means that logical deduction is no longer merely about an ever-expanding collection of persistent "truths", but also a way of manipulating resources that can not always be duplicated or thrown away at will. In terms of simple denotational models, linear logic may be seen as refining the interpretation of intuitionistic logic by replacing cartesian closed categories by symmetric monoidal categories, or the interpretation of classical logic by replacing boolean algebras by C*-algebras.
Syntax
The language of classical linear logic (CLL) is defined inductively by the BNF notation| ::= | ||
Here and range
over logical atoms
Atomic formula
In mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic...
. For reasons to be explained
below, the connectives , , 1, and
are called multiplicatives, the connectives &,
, , and 0 are called additives, and the
connectives ! and ? are called exponentials. We can further
employ the following terminology:
is called "multiplicative conjunction" or "times" (or sometimes "tensor") is called "additive disjunction" or "plus"
- & is called "additive conjunction" or "with" is called "multiplicative disjunction" or "par"
- ! is pronounced "of course" (or sometimes "bang")
- ? is pronounced "why not"
Every proposition in CLL has a dual , defined as follows:
Observe that is an involution, i.e., for all propositions. is also called the linear negation of .
The columns of the table suggest another way of classifying the connectives of linear logic, termed polarity: the connectives negated in the left column are called positive, while their duals on the right are called negative.
Linear implication is not included in the grammar of connectives, but is definable in CLL using linear negation and multiplicative disjunction, by . The connective is sometimes pronounced "lollipop
Lollipop
A lollipop, pop, lolly, sucker, or sticky-pop is a type of confectionery consisting mainly of hardened, flavored sucrose with corn syrup mounted on a stick and intended for sucking or licking. They are available in many flavors and shapes.- Types :Lollipops are available in a number of colors and...
", owing to its shape.
Sequent calculus presentation
One way of defining linear logic is as a sequent calculusSequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
. We use the letters and to range over list of propositions , also called contexts. A sequent places a context to the left and the right of the turnstile
Turnstile (symbol)
In mathematical logic and computer science the symbol \vdash has taken the name turnstile because of its resemblance to a typical turnstile if viewed from above. It is also referred to as tee and is often read as "yields", "proves", "satisfies" or "entails"...
, written . Intuitively, the sequent asserts that the conjunction of entails the disjunction of (though we mean the "multiplicative" conjunction and disjunction, as explained below). Girard describes classical linear logic using only one-sided sequents (where the left-hand context is empty), and we follow here that more economical presentation.
We now give inference rules describing how to build proofs of sequents.
First, to formalize the fact that we do not care about the order of propositions inside a context, we add the structural rule of
exchange:
|
|
(Alternatively we could accomplish the same thing by defining contexts to be multisets rather than lists.)
Note that we do not add the structural rules of weakening and contraction, because we do care about the
absence of propositions in a sequent, and the number of copies present.
Next we add initial sequents and cuts:
|
|
| ||||||||||||||||
The cut rule can be seen as a way of composing proofs, and initial sequents serve as the units
Identity element
In mathematics, an identity element is a special type of element of a set with respect to a binary operation on that set. It leaves other elements unchanged when combined with them...
for composition. In a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof. Ultimately, this canonical form
Canonical form
Generally, in mathematics, a canonical form of an object is a standard way of presenting that object....
property (which can be divided into the completeness of atomic initial sequents
Completeness of atomic initial sequents
In sequent calculus, the completeness of atomic initial sequents states that initial sequents can be derived from only atomic initial sequents . This theorem plays a role analogous to eta expansion in lambda calculus, and dual to cut-elimination and beta reduction...
and the cut-elimination theorem
Cut-elimination theorem
The cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively...
, inducing a notion of analytic proof
Analytic proof
In mathematical analysis, an analytical proof is a proof of a theorem in analysis that only makes use of methods from analysis, and which does not make use of results from geometry...
) lies behind the applications of linear logic in computer science, since it allows the logic to be used in proof search and as a resource-aware lambda-calculus.
Now, we explain the connectives by giving logical rules. Typically in sequent calculus
one gives both "right-rules" and "left-rules" for each connective, essentially describing two modes of reasoning
about propositions involving that connective (e.g., verification and falsification). In a one-sided presentation, one instead makes use of negation: the right-rules for a connective
(say ) effectively play the role of left-rules for its dual . So, we should expect a certain "harmony"
Logical harmony
Logical harmony, a name coined by Sir Michael Dummett, is a supposed constraint on the rules of inference that can be used in a given logical system....
between the rule(s) for a connective and the rule(s) for its dual.
Multiplicatives
The rules for multiplicative conjunction and disjunction :|
|
| ||||||||||||||||
and for their units:
|
|
| |||||||||||||
Observe that the rules for multiplicative conjunction and disjunction are admissible
Admissible rule
In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense,...
for
plain conjunction and disjunction under a classical interpretation
(i.e., they are admissible rules in LK).
Additives
The rules for additive conjunction (&) and disjunction :|
|
|
| ||||||||||||||||||||
and for their units:
|
| (no rule for ) | ||||||||||
Observe that the rules for additive conjunction and disjunction are again admissible
under a classical interpretation. But now we can explain the basis for the multiplicative/additive distinction
in the rules for the two different versions of conjunction: for the multiplicative connective ,
the context of the conclusion is split up between the premises, whereas
for the additive case connective (&) the context of the conclusion is carried whole into both
premises.
Exponentials
The exponentials are used to give controlled access to weakening and contraction. Specifically, we addstructural rules of weakening and contraction for ?'d propositions:
|
|
|
and use the following logical rules:
|
|
|
One might observe that the rules for the exponentials follow a different pattern from the rules for the other connectives,
and that there is no longer such a clear symmetry between the duals ! and ?. This situation is remedied in alternative
presentations of CLL (e.g., the LU presentation).
Remarkable formulae
In addition to the De Morgan dualities described above, some important equivalences in linear logic include:Distributivity :
Exponential isomorphism :
(Here
.)The following is not in general an equivalence, only an implication:
Semi-distributivity :
Encoding classical/intuitionistic logic in linear logic
Both intuitionistic and classical implication can be recovered from linear implication by inserting exponentials: intuitionistic implication is encoded as , and classical implication as .. The idea is that exponentials allow us to use a formula as many times as we need, which is always possible in classical and intuitionistic logic.Formally, there exists a translation of formulae of intuitionistic logic to formulae of linear logic in a way which guarantees that the original formula is provable in intuitionistic logic if and only if the translated formula in provable in linear logic. Using the Gödel–Gentzen negative translation
Gödel–Gentzen negative translation
In proof theory, the Gödel–Gentzen negative translation is a method for embedding classical first-order logic into intuitionistic first-order logic. It is one of a number of double-negation translations that are of importance to the metatheory of intuitionistic logic...
, we can thus embed classical first-order logic into linear first-order logic.
The resource interpretation
Lafont (1993) first showed how intuitionistic linear logic can be explained as a logic of resources, so providing the logical language with access to formalisms that can be used for reasoning about resources within the logic itself, rather than, as in classical logic, by means of non-logical predicates and relations. Antony Hoare (1985)'s classical example of the vending machine can be used to illustrate this idea.Suppose we represent a candy bar by the atomic proposition , and a dollar by . To state the fact that a dollar will buy you one candy bar, we might write the implication . But in ordinary (classical or intuitionistic) logic, from and one can conclude . So, ordinary logic leads us to believe that we can buy the candy bar and keep our dollar! Of course,
we can avoid this problem by using more sophisticated encodings, although typically such encodings suffer from the frame problem
Frame problem
In artificial intelligence, the frame problem was initially formulated as the problem of expressing a dynamical domain in logic without explicitly specifying which conditions are not affected by an action. John McCarthy and Patrick J. Hayes defined this problem in their 1969 article, Some...
. However, the rejection of weakening and contraction allows linear logic to avoid this kind of spurious reasoning even with the "naive" rule. Rather than , we express the property of the vending machine as a linear implication . From and this fact, we can conclude , but not . In general, we can use the linear logic proposition to express the validity of transforming resource into resource .
Running with the example of the vending machine, let us consider the "resource interpretations" of the other multiplicative and additive connectives. (The exponentials provide the means to combine this resource interpretation with the usual notion of persistent logical truth
Logical truth
Logical truth is one of the most fundamental concepts in logic, and there are different theories on its nature. A logical truth is a statement which is true and remains true under all reinterpretations of its components other than its logical constants. It is a type of analytic statement.Logical...
.)
Multiplicative conjunction denotes simultaneous occurrence of resources, to be used as the consumer directs. For example, if you buy a stick of gum and a bottle of soft drink, then you are requesting . The constant 1 denotes the absence of any resource, and so functions as the unit of .
Additive conjunction represents alternative occurrence of resources, the choice of which the consumer controls. If in the vending machine there is a packet of chips, a candy bar, and a can of soft drink, each costing one dollar, then for that price you can buy exactly one of these products. Thus we write . We do not write , which would imply that one dollar suffices for buying all three products together. However, from , we can correctly deduce , where . The unit of additive conjunction can be seen as a wastebasket or garbage collector
Garbage collection (computer science)
In computer science, garbage collection is a form of automatic memory management. The garbage collector, or just collector, attempts to reclaim garbage, or memory occupied by objects that are no longer in use by the program...
for irrelevant alternatives. For example, we can write to express that three dollars will buy you a candy bar and something else (we don't care what).
Additive disjunction represents alternative occurrence of resources, the choice of which the machine controls. For example, suppose the vending machine permits gambling: insert a dollar and the machine may dispense a candy bar, a packet of chips, or a soft drink. We can express this situation as . The constant 0 represents a product that cannot be made, and thus serves as the unit of (a machine that might produce or is as good as a machine that always produces because it will never succeed in producing a 0).
Multiplicative disjunction is more difficult to gloss in terms of the resource interpretation, although we can encode back into linear implication, either as or .
Proof nets
Introduced by Jean-Yves GirardJean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
, proof net have been created to avoid the bureaucracy, that is all the things that make two derivation different in the logical point of view, but not in a “moral” point of view.
For instance, these two proofs are “morally” identical:
|
|
|
The goal of proof net is to make them identical by creating a graphical representation of them.
Decidability/complexity of entailment
The entailmentEntailment
In logic, entailment is a relation between a set of sentences and a sentence. Let Γ be a set of one or more sentences; let S1 be the conjunction of the elements of Γ, and let S2 be a sentence: then, Γ entails S2 if and only if S1 and not-S2 are logically inconsistent...
relation in full CLL is undecidable
Undecidable problem
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is impossible to construct a single algorithm that always leads to a correct yes-or-no answer....
. Fragments of
CLL are often considered, for which the decision problem is more subtle:
- Multiplicative linear logic (MLL): only the multiplicative connectives. MLL entailment is NP-completeNP-completeIn computational complexity theory, the complexity class NP-complete is a class of decision problems. A decision problem L is NP-complete if it is in the set of NP problems so that any given solution to the decision problem can be verified in polynomial time, and also in the set of NP-hard...
. - Multiplicative-additive linear logic (MALL): only multiplicatives and additives (i.e., exponential-free). MALL entailment is PSPACE-completePSPACE-completeIn complexity theory, a decision problem is PSPACE-complete if it is in the complexity class PSPACE, and every problem in PSPACE can be reduced to it in polynomial time...
. - Multiplicative-exponential linear logic (MELL): only multiplicatives and exponentials. The decidability of MELL entailment is currently open.
Variants of linear logic
Many variations of linear logic arise by further tinkering with the structural rules:- Affine logicAffine logicAffine logic is a substructural logic whose proof theory rejects the structural rule of contraction. It can also be characterized as linear logic with weakening....
, which forbids contraction but allows global weakening. - Strict logicStrict logicStrict logic is essentially synonymous with relevant logic, though it can be characterized proof-theoretically as* ordinary logic without weakening, or* linear logic with contraction....
or relevant logic, which forbids weakening but allows global contraction. - Non-commutative logic or ordered logic, which removes the rule of exchange, in addition to barring weakening and contraction. In ordered logic, linear implication divides further into left-implication and right-implication.
Different intuitionistic variants of linear logic have been considered. When based on a single-conclusion sequent calculus presentation, like in ILL (Intuitionistic Linear Logic), the connectives , ⊥, and ? are absent, and linear implication is treated as a primitive connective. In FILL (Full Intuitionistic Linear Logic) the connectives , ⊥, and ? are present, linear implication is a primitive connective and, similarly to what happens in intuitionistic logic, all connectives (except linear negation) are independent.
There are also first- and higher-order extensions of linear logic, whose formal development is somewhat standard (see first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
and higher-order logic
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
).
See also
- Linear types
- Logic of unity (LU)
- Proof netProof netIn proof theory, proof nets are a geometrical method of representing proofs thateliminates two forms of bureaucracy that differentiates proofs: irrelevant syntactical features of regular proof calculi such as the natural deduction calculus and the sequent calculus, and the order of rules applied...
s - Geometry of interactionGeometry of interactionThe geometry of interaction was introduced by Jean-Yves Girard shortly after his work on Linear Logic. In linear logic, proofs can be seen as some kind of networks instead of the flat tree structure of sequent calculus. To distinguish the real proof nets from all the possible networks, Girard...
- Game semanticsGame semanticsGame semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes. In the late 1950s Paul Lorenzen was the...
- Intuitionistic logicIntuitionistic logicIntuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
- Computability logicComputability logicIntroduced by Giorgi Japaridze in 2003, computability logic is a research programme and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic which is a formal theory of truth...
- LudicsLudicsIn proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics are its notion of compound connectives using a technique known as focusing or focalisation , and its use of locations or loci over a base instead of propositions.More...
- Chu spaceChu spaceChu spaces generalize the notion of topological space by dropping the requirements that the set of open sets be closed under union and finite intersection, that the open sets be extensional, and that the membership predicate be two-valued...
s - Uniqueness typeUniqueness typeIn computing, a unique type guarantees that an object is used in a single-threaded way, with at most a single reference to it. If a value has a unique type, a function applied to it can be optimized to update the value in-place in the object code. In-place updates improve the efficiency of...
External links
- Patrick Lincoln Introduction to Linear Logic (Postscript)
- Introduction to Linear Logic by Torben Brauner http://www.brics.dk/LS/96/6/BRICS-LS-96-6/BRICS-LS-96-6.html
- A taste of linear logic by Philip Wadler http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html
- Linear Logic by Roberto Di Cosmo and Dale Miller. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).
- Overview of linear logic programming by Dale Miller. In Linear Logic in Computer Science, edited by Ehrhard, Girard, Ruet, and Scott. Cambridge University Press. London Mathematical Society Lecture Notes, Volume 316, 2004.