linlog: linear logic, proved in the browser
linlog proves sequents of linear logic in the browser; the page needs JavaScript and WebAssembly.
linlog proves sequents of linear logic in the browser; the page needs JavaScript and WebAssembly.
⅋ puts its two formulas side by side in one goal, and the axiom closes a goal that holds an atom and its dual alone.
The axiom pairs an atom with its dual, A with A⊥: two copies of A are no pair, and no other rule acts on an atom.
A hypothesis left of ⊢ is its dual on the right: ⊢ A⊥, A, which the axiom closes.
A⊥ and B are no dual pair: every atom must meet its own dual.
The dual of A⊥ is A again, so the goal is an axiom in disguise.
⅋ first, since it never loses a proof; then ⊗, whose split must send each atom to the premise that holds its dual.
B and C have no duals to meet: atoms are resources, each used exactly once.
Two splits, each sending every atom to the premise where its dual is.
However A⊥ and B⊥ are sent to the premises of ⊗, a premise is left whose formulas do not pair; linlog sees it from the counts of the connectives alone.
One-sided, each implication is a ⅋: two splits pass every atom to its dual.
It would need a goal of two pairs split with nothing between them, which is the Mix rule. Without Mix there is no proof; with it there is one (lesson 8).
A & B on the left is A⊥ ⊕ B⊥ on the right: choose the side whose dual is in the goal.
⊕ chooses the side the goal can prove.
& asks for both A and B from the same context, and A ⊕ B gives one of them. Read classically the sequent is false when A is true and B false.
& gives both premises the whole context; in each, ⊕ chooses the side that premise can prove.
A & B is one resource, A or B as you choose, not both: the search tries every way and finds none.
& copies the context into both premises: in each, the hypothesis A & B gives the side that premise needs.
1 closes a goal in which it is alone.
⊥ disappears and leaves the empty goal, which no rule closes.
1 is the unit of ⊗: the split sends nothing to its side.
1 needs an empty context, and nothing takes A and A⊥ away from it.
⊤ closes any goal it is in, whatever else is there.
0 has no rule, and the axiom needs A and A⊥ alone.
0 on the left is ⊤ on the right, which closes the goal.
!A on the left is ?A⊥ on the right: ?d takes one copy out.
A plain atom is used once; only a formula under ! may be copied.
?c makes two copies of ?A⊥, and ?d opens each.
! needs every other formula of its goal under ?, and A⊥ is not.
?w drops ?A⊥, and then 1 is alone.
?A on the left is !A⊥ on the right, which needs everything else under ?, and A is not.
!A may be copied (?c on its dual), one copy derelicted to A (?d), the other kept behind !, whose promotion needs every other formula of its goal under ?.
Promotion is allowed once the context is ?A⊥ and ?B⊥ alone; then each is derelicted into its premise.
Two sides: ⊸L uses the hypothesis A ⊸ B, sending A to prove its argument and keeping B for the rest.
An implication does not run backward: A is wanted and never given, and linlog’s count of the atoms says so.
⊸R moves A to the left; then each implication is used once, in a chain from A to C.
The implication wants A twice, and there is one A: a hypothesis is used once.
⊸R twice puts A and B on the left; ⊸L then proves A ⊗ B from them.
Each implication needs an A of its own, and there is one.
!A gives as many A as needed: promoted for the argument of !A ⊸ B, derelicted for the A on the right.
!A ⊸ B wants !A, and a single A cannot be promoted: promotion needs every hypothesis under !.
B has no dual to meet, and linear logic throws nothing away; linlog’s refutation counts the atoms.
It looks lossy, but both sides choose: & gives A, and ⊕ takes it.
Read classically it is false when A is false and B true, and a sequent false so has no proof in linear logic.
The rule a ⊸ a ⊗ a, used three times, turns one a into four: a Petri net, which the Horn engine searches.
The atoms balance and the classical reading is true, so only the search’s exhaustion says no, and there is no certificate to check.
Each use of a ⊸ a ⊗ a ⊗ a takes one a and gives three, two more, so the number of a stays odd and never reaches two. linlog’s search tries every way and finds none.
A net of two axiom links: once it is proved, the Net tab draws it.
Its only linking closes a cycle through the ⅋, which the switching criterion refuses; linlog’s count equation refutes it before any linking.
Three axiom links, and every switching of the net’s ⅋ leaves it connected and without a cycle.
With no ⊗ to join them, the two pairs make a net in two pieces, which the criterion refuses without Mix.
An intuitionistic proof’s net is its essential net, directed from the hypotheses toward the goal.
With Mix, two nets side by side make one: the net of this proof is in two pieces, which Mix allows.
The axiom needs A⊥ and A alone: B would be left over, and only ⊤ (which closes a goal it is in) or ?w (which drops a formula under ?) disposes of a formula; the goal has neither.
Three splits, each sending every atom to the premise where its dual is: the order of the factors does not matter, only that each atom meets its own dual.
⅋ first, on the implications and the conclusion; then each ⊗ is split so that A goes where A ⊸ B is, and C where C ⊸ D is.
A feeds A ⊸ B, but D is offered where C is wanted: C and D find no duals to meet, as linlog’s count of the atoms says.
& on the right is proved twice from the same hypothesis, once for A and once for B (or C); the hypothesis gives B ⊕ C for the second, whose two cases cannot both give B, and the choice between A & B and A & C must be made before the case is known.
The hypothesis is one of two cases, and the proof answers each: in the case A & B it gives A, and B for B ⊕ C; in the case A & C, A and C.
& gives both its premises the whole context, so the one A serves B in one premise and C in the other, each premise choosing the implication it needs.
⊤ on the left is 0 on the right, which has no rule, and the first premise of & asks for 1 with that 0 beside it, where 1 must be alone.
Its dual on the right is ⊤ ⅋ A⊥: ⅋ takes it apart, and ⊤ closes the goal whatever A and B are.
Either side of the hypothesis gives A and a 1, which is a ⊥ on the right and goes away; the split sends A⊥ to A and nothing to 1 ⊕ 0, where ⊕ takes 1, since 0 has no rule.
B ⊸ ⊥ is B⊥ ⅋ ⊥: once ⊥ disappears, the implications chain as in lesson 2, each split sending every atom to its dual.
(A ⊗ B) ⊸ ⊥ says that A and B together give nothing: it is A⊥ ⅋ B⊥ ⅋ ⊥, and ⊥ simply disappears.
!A & !B is one of the two, as the proof chooses, not both, and it is no ! formula itself: on the right it is ?A⊥ ⊕ ?B⊥, not under ?, so ! cannot be promoted beside it.
The hypothesis may be copied (?c): one copy chooses A, the other B, and each ! is promoted, since the copy beside it is under ?.
Promotion first, since both hypotheses are ? formulas on the right; then & gives each premise both, and each drops the one it does not need (?w).
B⊥ is under no ?: on the side of !B it stops the promotion of !B, on the side of !A that of !A, and !B promoted alone leaves B with no dual.
?w drops the unused ?B⊥, ?c copies ?A⊥, and the split sends one copy to each side of ⊗; !A is promoted beside its copy, which is under ?, and ?d opens each copy for its axiom.
⊸R twice puts B and A on the left; ⊸L feeds A to the hypothesis, and its B ⊸ C takes B.
⊸R puts !A on the left; now every hypothesis is under !, so !C may be promoted, and A, A ⊸ B and B ⊸ C, each taken out of its ! once, give C.
The hypothesis wants A ⊸ B as its argument, and nothing gives that B; the atoms do not balance, as linlog’s count says.
The Handbook gives it as a formula of intuitionistic linear logic with no proof there, although its classical reading has one. With one formula on the right, linlog’s search tries every way and finds none.
One-sided, the formula is ((((⊤ ⅋ 1) ⊗ ⊥) ⅋ 0) ⊗ ⊤) ⅋ 1, and its proof keeps 1 beside ⊤ and 0 in one goal: ⊤ closes it. Intuitionistic mode has no goal with two formulas on the right, so the same text has no proof there.
⊸L on A ⊸ B sends the hypothesis A alone to its left premise, A ⊢ A, and goes on with B, C ⊢ B ⊗ C, which ⊗R splits. The A is used up by the implication.
Doubling three times turns one a into four, and the second rule makes two b of them: a Petri net, whose firings the Horn engine searches.
The first rule turns a into two b, the second two b into c: each used once, though ! would allow more, and the search finds that once is enough.
Every rule turns one token into one, so one a gives one c at most, and the goal wants two; the Horn engine’s search tries every firing and finds none that reaches it.
Take B from A & B, the B that B ⊕ D needs: one-sided, ⊕₂ chooses B⊥ from A⊥ ⊕ B⊥. Choosing A⊥ loses the proof at once: A⊥ then has no A to meet.
The converse of weak distributivity: read classically it is false where A is true and the rest false, so it has no proof and no net.
Three axiom links, and every switching of the net’s ⅋ nodes leaves it connected and without a cycle.
Each implication takes its own argument from the pair A ⊗ C: the essential net runs from A to B and from C to D, side by side.
The goal wants C ⊗ A, and the one A given goes to make C: linlog’s count of the atoms says no net links them all.
⊸R first, then ⊸L, whose argument A ⊗ B is proved from the swapped pair: its essential net leads from the hypotheses to C ⊗ A.
The goal’s implications unfold by ⅋; then the splits, each led by where an atom’s dual is, give the net its axiom links.
!B needs a box, and a box’s other doors must all be under ?. One-sided they are ?(A ⊗ B⊥) and A⊥, and A⊥ is not: whatever is copied from !(A ⊸ B), the one A cannot go into the box.
One-sided the hypothesis is ?A⊥, under ?, so ! may promote twice: !!A, then !A, then ?d and the axiom. In the net each promotion is a box, one inside the other.
⊗L puts !A and !B side by side; every hypothesis is under !, so !R may close the box around B ⊗ A, and inside it each is used once.
!L uses the translated implication once, and ⊸L applies it: its argument is !A, which !R proves from the hypothesis !A alone, and B is the goal.
!B is never used: a hypothesis under ! may be dropped (!w), which the K combinator needs.
The image of Peirce’s law, ((A → B) → A) → A, under Girard’s call-by-name translation, as linlog seq print --logic intuitionistic prints it. The law does not hold intuitionistically, and its image has no proof: to use the hypothesis one must prove !A ⊸ B, and nothing gives B.
The image of Peirce’s law, ((A → B) → A) → A, under the translation of classical logic into affine MALL, as linlog seq print --logic classical prints it. & gives two goals; in the first, B is left over and weakening drops it. Without weakening, in classical mode, the image has no proof.
The argument !A is used twice: !c copies it, and each copy goes into one application by !R.
The image of ¬¬A → A under Girard’s call-by-name translation, ¬A written A → ⊥ and ⊥ as 0. Intuitionistically the law fails, and the image has no proof: using the hypothesis needs a proof of !A ⊸ 0, which asks for 0 from !A, and only the hypothesis itself gives 0, which asks for the same again.
Both translated hypotheses need the argument !A: !c copies it, and each copy goes into its application by !R.
A cut on C proves the lemma A, A ⊸ B, B ⊸ C ⊢ C and uses it in C ⊸ D, C ⊢ D: nine inferences. The cut-free proof, three ⊸L and four axioms, has seven. The lemma is used once, so the cut only adds its own inference and an axiom on C.
No proof: the goal asks for two B and the hypotheses give one. A cut on B proves B once, and the premise that uses it, B ⊢ B ⊗ B, has a B too few; linlog counts the atoms and says so. A lemma can be used twice only under !.
Prove the lemma !C once from the three hypotheses, by !R since all three are under !, then cut on it: !c copies !C, and each copy gives a C. Sixteen inferences with the cut; the cut-free proof derives C twice, twenty inferences.
No proof. The lemma !B would need !R, which takes only hypotheses under !, and A ⊸ B is not; without it, A ⊸ B gives one B and the goal needs two, which linlog’s count of B shows.
Cut on !B: its proof, !R over ⊸L, is written once, and two !c make three copies of it for the three B. Seventeen inferences with the cut, twenty-one without.
The lemma !C, proved once from the three hypotheses, then copied twice by !c: twenty inferences. The cut-free proof derives C three times over, thirty-two inferences: each use costs the whole chain again.
The witness is the constant a both times: ∃R with a asks for q(a), and ∀L with a takes the instance p(a) ⊸ q(a), which ⊸L applies to the hypothesis p(a).
No proof: ∃L opens ∃x. p(x) with a fresh eigenvariable, p(b), never with the constant a the goal names, and p(b) ⊢ p(a) is no axiom. Knowing that something has p says nothing of a.
Make the eigenvariables first: ∀R gives a, ∃L gives b. Then the witnesses can name them: ∃R takes b, ∀L takes a, and r(a, b) ⊢ r(a, b) is the axiom.
⊸R takes ∀x. p(x) as a hypothesis, ∀R makes the eigenvariable a for the goal q(a), and both ∀ hypotheses take a as their witness: p(a) ⊸ q(a) and p(a), joined by ⊸L.
No proof: ∀L takes one instance, p(a) or p(b), and uses the hypothesis up. The goal needs two, so p occurs once too often on the right, as linlog’s count says. Under ! the hypothesis could be copied first.
∃L names the something a, ⊗L gives p(a) and q(a), ⊗R sends each to its side, and each ∃R takes the witness a.
No proof: the y of the hypothesis depends on x, the y of the goal may not. In every order, the witness of ∃R would have to be the eigenvariable ∃L makes later, which the eigenvariable condition refuses; linlog’s search is exhaustive.
!c copies the hypothesis, !L opens each copy, and the two ∀L take the witnesses a and b; ⊗R sends one instance to each side.
No proof: the two ∃L make two eigenvariables, p(a) and q(b), and the one witness of ∃R cannot be both. Something has p and something has q, perhaps not the same.
The rule is needed twice, so !c copies it; the witnesses are terms: a for the step from p(a) to p(f(a)), and f(a) for the step on to p(f(f(a))).
A proof starts from a sequent typed in the tab’s field, in ASCII or in the
signs. The tour has typed A * B |- B * A and pressed Enter.
The derivation grows upwards on the stage. Drag or scroll to move it, and zoom with the buttons at the bottom right. The goal you work on is lit; the others are dimmed.
Every formula of an open goal is a button. Clicking it lists the rules linlog gives for it, and nothing else; a rule is applied only when you pick it.
The tour applied ⅋ to the first formula. A rule that does not apply is
refused at the goal, with linlog’s reason.
⊗ splits its goal’s other formulas between two premises. The tour sent B⊥
to the left one, with B; the split chooser says before you apply a split
whether it can still close.
Close all lets linlog’s search finish every open goal within the budget set in Settings. Its inferences are drawn apart from yours, and Hint gives the next step one rung at a time.
The dot on the tab is the verdict: green for a proof that linlog checked, red for no proof, amber when the search gave up. Its details are a click away.
Undo works on the branch you are on, Steps goes back to any step, Export writes the proof in every format, Import reads one back. Practice has problems to prove, Learn the tutorial and the reference.
This page is linlog’s prover for linear logic, running in your browser: you type a sequent and prove it step by step, or let linlog’s search close a goal. linlog’s library is compiled to WebAssembly and runs in the page; nothing you type is sent anywhere, and your proofs stay in this browser’s storage.
linlog’s manual describes the command line prover and its benchmarks, the library’s documentation is at /linlog/, and their source is on GitHub. For AI models, llms.txt says what this page is and where linlog’s guide for them is. Questions, mistakes and wishes are welcome as issues.
Every problem here has a proof. Choose the kinds and the difficulty you want, or let chance choose; a problem opens as a proof on a new tab, and Hint helps when you are stuck. The difficulty counts what a proof by hand takes: its steps, and the choices on the way that a count of the atoms does not settle.
The connectives, as you type them and as linlog prints them. One-sided, every
formula is on the right of ⊢ and A⊥ is the dual of A; two-sided
(intuitionistic, or classical with the Two-sided switch), the hypotheses are on the left.
| sign | typed | name | reading |
|---|---|---|---|
A ⊗ B |
A * B |
tensor | both, side by side |
A ⅋ B |
A | B, A par B |
par | the dual of tensor |
A ⊸ B |
A -o B |
linear implication | consumes A, gives B; A⊥ ⅋ B |
A & B |
A & B |
with | either one, the other’s choice |
A ⊕ B |
A + B |
plus | one of them, the prover’s choice |
!A |
!A |
of course | as many A as needed |
?A |
?A |
why not | the dual of of course |
A⊥ |
~A, A^ |
negation | the dual |
1, ⊥ |
1, bot |
the units of ⊗ and ⅋ |
|
⊤, 0 |
top, 0 |
the units of & and ⊕ |
|
∀x. A |
forall x. A |
for all | A for every x; the dual of exists |
∃x. A |
exists x. A |
exists | A for some x, a witness chosen |
⊢ is typed |-. With quantifiers, atoms take arguments: p(x, f(a)) is the
predicate p of the variable x and the term f(a). A name a quantifier binds is
its variable; any other name in an argument is a constant or, with arguments, a function
symbol; a name has one arity throughout. A quantifier reaches as far right as it can, so
forall x. p(x) * q(x) is ∀x. (p(x) ⊗ q(x)), and forall x y. A binds both.
Proving, ∀R and ∃L make an eigenvariable, a fresh constant written a, b, …;
∃R and ∀L take a witness, a term of the sequent’s constants and function symbols
and of the eigenvariables made below the goal, or leave it open as $1 for an axiom or
the search to fill. An open witness never takes an eigenvariable made after it: the
eigenvariable condition.
The rules
Each rule as a schema: its premises above the bar, its conclusion below, its name
beside it, as the stage writes it. Γ and Δ stand for any formulas, ?Γ for
formulas each under ?. No rule acts on 0. With Learn on, a rule in the stage’s
popover shows its schema on hover, and a formula its connective’s reading.
These are the rules of the one-sided calculus as the LLHandbook project’s Handbook
of linear logic states them (draft of 6 March 2026, section 1.3.5, Table 1.4,
p. 22), with its cut and its first-order quantifiers, there (∀₁) and (∃₁). There the
axiom takes any formula; section 1.3.2 (p. 14) shows that atoms suffice, and linlog’s
axiom takes an atom. A[t/x] is A with the term t in place of x. The two-sided names are linlog’s names for
the same rule in a two-sided derivation: the principal formula on the right, or its
dual on the left.
The two-sided rules
In intuitionistic mode a sequent has its hypotheses on the left of ⊢ and exactly
one formula on the right, and the stage names each rule two-sided: a left rule uses
a hypothesis, a right rule proves the goal. Each is a one-sided rule above read from
the other side: ⊸L is ⊗ on the hypothesis A ⊸ B, whose dual is A ⊗ B⊥. With
Learn on, a rule in an intuitionistic proof’s popover shows its two-sided schema.
These are the rules of intuitionistic linear logic as the Handbook
of linear logic states them (section 1.7.2.1, Table 1.5, p. 48), with the cut and
the first-order quantifiers and without the exchange, in linlog’s names: there (wL),
(cL), (∀₁L) and the like, here !w, !c, ∀L. As above, linlog’s axiom takes an
atom.
The engines
Every search on this page is linlog’s: it picks an engine by the sequent’s fragment and mode (Settings can force one), and the page names the engine beside what it did. Each engine and where it comes from:
- Focused search
- Searches backward from the goal: the invertible rules first, then one formula in focus at a time. Classical mode; the two-sided focused search is the same on intuitionistic sequents. Jean-Marc Andreoli, Logic programming with focusing proofs in linear logic, Journal of Logic and Computation 2(3), 297–347, 1992.
- Two-sided focused search
- The focused search on an intuitionistic sequent, one formula right of
⊢. Andreoli 1992, as above. - Proof-net search
- For MLL without units: links each atom with a dual until the net passes Danos and Regnier's switching criterion (every switching leaves the graph a tree). Proof nets: Jean-Yves Girard, Linear logic, Theoretical Computer Science 50(1), 1–102, 1987. The criterion, stated and proved: Jean Gallier, Constructive logics. Part II: linear logic and proof nets, University of Pennsylvania, section 7 (Definition 7.6, Theorem 7.9).
- Essential-net search
- For intuitionistic MLL without units: Lamarche's essential net, directed from the hypotheses toward the goal, correct when it has no cycle and its paths pass where the criterion says. Stated, with Lamarche's theorem that a sequent is provable exactly when its essential net is correct: Richard Moot, Graph algorithms for improving type-logical proof search, arXiv:0805.2303, 2008, section 2.3.
- Planar nets of the ordered modes
- linlog's cyclic mode and Lambek calculus keep the order of the formulas, and their nets are linked without crossings. François Lamarche and Christian Retoré, Proof nets for the Lambek calculus: an overview, Proofs and Linguistic Categories (3rd Roma Workshop), 1996; the planar linkings: Moot 2008, as above. This page offers neither mode yet.
- Horn engine
- A goal of atoms, implications and implications under
!is a Petri net with a marking to reach: the engine searches its markings, and in affine mode, where tokens may be left over, whether a marking covering the goal is reachable, backward from the goal. Petri nets and linear logic: Uffe Engberg and Glynn Winskel, Petri nets as models of linear logic, DAIMI Report PB-301, Aarhus University, 1990; the backward search: Parosh Aziz Abdulla, Kārlis Čerāns, Bengt Jonsson and Yih-Kuen Tsay, General decidability theorems for infinite-state systems, LICS 1996, 313–321. - Inverse method
- Searches forward: derives sequents from the axioms upward, whole focused phases at a time, until it reaches the goal or nothing new comes; then the set it derived, which linlog checks, is the refutation. Kaustuv Chaudhuri and Frank Pfenning, Focusing the inverse method for linear logic, CSL 2005, LNCS 3634, 200–215.
- Additive path
- For two formulas built of
&,⊕, their units and atoms: decides each pair of their subformulas by linear logic's additive rules,&,⊕and⊤, with the axiom, remembering each answer. The rules: the LLHandbook project, Handbook of linear logic, section 1.3.5, Table 1.4. Related: the word problem for lattices, which Whitman solved; Alan Day, A simple solution to the word problem for lattices, Canadian Mathematical Bulletin 13(2), 253–254, 1970. - Classical refuter
- Reads the sequent as ordinary logic (
⊗and&as and,⅋and⊕as or,!and?erased) and looks for an assignment that makes it false: read so, every rule of linear logic is a rule of ordinary logic, so a sequent false under one assignment has no proof. "Mapping ⊗ and & to ∧ and ⅋ and ⊕ to ∨ turns linear provable formulas into valid classical formulas": the LLHandbook project, Handbook of linear logic, section 1.1, proved in section 1.8 (Theorem 1.8.1, the skeleton). The refuter's ground is that statement read backward: a formula false under one assignment is no valid classical formula, so no provable linear one.
Lessons that perform real steps on the stage and teach the logic, from reading a sequent to proof nets, cut, the quantifiers and ordinary logic. Each plays a worked proof one inference at a time, asking you to predict each rule before it shows the step and its reason; then it leaves the same proof’s last steps to you, gives practice, and ends with a check. The tour shows the page itself.
A sequent ⊢ Γ asks for a proof of the formulas Γ together, separated by commas.
A⊥ is the dual of A, its negation. Typed in classical mode, Γ |- Δ moves each
hypothesis to the right as its dual: A |- A is ⊢ A⊥, A. The dual of a compound
formula follows De Morgan’s laws, (A ⊗ B)⊥ = A⊥ ⅋ B⊥, and A⊥⊥ is A again.
The axiom closes a goal that holds an atom and its dual, and nothing else.
⅋ puts its two parts side by side in the same goal, and never loses a proof: apply it
first. ⊗ splits the goal into two premises, its left part with some of the other
formulas and its right part with the rest, each formula in exactly one premise. The
split is where a proof is won or lost. A -o B is typed for A⊥ ⅋ B.
& gives both premises the whole context, the same formulas copied rather than split,
and never loses a proof. ⊕ chooses one side, ⊕₁ the left and ⊕₂ the right, and
the choice can be the wrong one. Read as a hypothesis, A & B is one resource you take
either part of, and A ⊕ B is two cases you must answer.
1 closes a goal that holds 1 alone. ⊥ disappears and leaves the rest of the goal.
⊤ closes any goal it is in, whatever else is there. Nothing acts on 0. They are
each other’s duals: 1⊥ = ⊥ and ⊤⊥ = 0, so a hypothesis 1 reads ⊥ on the right.
A hypothesis !A is ?A⊥ on the right, and may be used any number of times: ?d takes
one A⊥ out of it, ?c copies it, ?w drops it. ! (promotion) acts on !A only when
every other formula of the goal is under ?: what !A is built from must be reusable.
In intuitionistic mode, chosen with the calculus’s switch on the tab, a sequent has its
hypotheses on the left of ⊢ and exactly one formula on the right: A ⊸ B, B ⊸ C ⊢ A ⊸ C reads “from A ⊸ B and B ⊸ C, A ⊸ C”. It is typed with -o for ⊸ and
has no ⊥, ⅋ or ?.
The rules come in pairs: a right rule proves the goal, a left rule uses a hypothesis,
and the stage names them so (⊸R, ⊸L, ⊗L, ⊗R, …). Each is a one-sided rule read
from the other side, so nothing new is allowed, but something is forbidden: a rule that
would leave two formulas on the right does not exist. ⊸L splits the hypotheses as
⊗ splits a goal, and the split is again where a proof is won or lost.
linlog gives one of three answers. Provable: it found a proof, and its checker accepted it. Unprovable: no proof exists, and linlog says why. Unknown: the search stopped at a bound, its budget of work or of copies, before it decided, which says nothing either way.
An attempt that gets stuck proves nothing about the sequent: a wrong step loses one
attempt, and another may succeed. “No proof” is a claim about every attempt, so it needs
a reason that holds for all of them. linlog’s reasons: an atom whose duals do not pair
off (where no ⊤ and no ? can drop a formula, every proof ends in axioms, each
pairing an atom with its dual); a classical
countermodel (read as ordinary logic the sequent is false, and every provable sequent
reads as true); and an exhausted search, which tried every way and found none.
A proof net draws a proof without the order of its rules. Each formula is the tree of its connectives, a link per connective, and each axiom becomes a link between an atom and its dual. Two derivations that differ only in the order of independent rules have one net.
Not every way of linking the atoms is a proof. Danos and Regnier’s switching condition
says which are: at each ⅋, keep one of its two premises and drop the other edge; for
every such choice the graph must be connected and without a cycle. A finished MLL or
MELL proof has its net in the stage’s Net tab, where each promotion ! draws a box; in
intuitionistic mode the net is Lamarche’s essential net, directed from the hypotheses
to the goal. The page draws nets of finished proofs; it does not edit them.
A cut proves a lemma once and uses it. Of a goal Γ, Δ ⊢ C it leaves two premises:
Γ ⊢ A proves the lemma A from some of the hypotheses, and Δ, A ⊢ C uses it
beside the rest. One-sided, the lemma is A in one premise and its dual A⊥ in the
other. On the stage, a goal’s Cut asks for the lemma and for the hypotheses that prove
it.
linlog’s search never cuts, and needs none: every proof with cuts has one without
(cut elimination), so a cut never proves what has no proof. It can make a proof
shorter, though rarely without !, since each formula is used once. A lemma under !
is proved once and copied for each use, where the cut-free proof derives it again
every time. Eliminating the cut shows that price: the lemma’s proof is copied once per
use.
With quantifiers, atoms take arguments: p(a), r(x, y), p(f(a)). ∀x. A is typed
forall x. A and ∃x. A exists x. A; a quantifier reaches as far right as it can.
The four rules come in two kinds. ∀R and ∃L open the formula with an
eigenvariable, a fresh name a, b, … about which nothing is known, so proving A
for it proves it for every x. ∃R and ∀L take a witness, a term you choose in the
witness chooser, or leave open as $1 for an axiom to fill. A witness names only
eigenvariables made below it, and an open witness never takes one made after it: the
eigenvariable condition. So make the eigenvariables first; those steps never lose a
proof.
∀ is like & over every term, ∃ like ⊕ choosing one. And as everywhere in linear
logic, a hypothesis ∀x. A gives one instance, once; under ! it gives as many as
needed.
Ordinary propositional logic, with →, ∧, ∨ and ¬, is decided by translating it
into linear logic and proving the image. Girard’s call-by-name translation takes
intuitionistic logic into intuitionistic linear logic: A → B becomes !A ⊸ B, and
every hypothesis goes under !, because an ordinary hypothesis may be used any number
of times or not at all. Classical logic goes into affine linear logic, ∧ as & and
∨ as ⅋, where weakening drops what is not needed.
The page has no ordinary mode yet, so this lesson proves the images, as linlog seq print --logic intuitionistic and --logic classical print them: modus ponens, A → B, A ⊢ B, becomes !(!A ⊸ B), !A ⊢ B.
The text of this page is © Fabian Lukas Grubmüller 2026, licensed underCC BY 4.0.
