*(This post has been modified to correct some errors and add some clarifications in response to comments from alert readers. Thanks for the corrections!)*
\nToday, we’re going to take a brief diversion from category theory to play with
\nsome logic. There are some really neat connections between variant logics and category theory. I’m planning on showing a bit about the connections between category theory and one of those, called *linear logic* . But the easiest way to present things like linear logic is using a mechanism based on sequent calculus<\/b>.
\nSequent calculus is a deduction system for performing reasoning in first order propositional logic. But it’s notation and general principles are useful for all sorts of reasoning systems, including many different logics, all sorts of type theories, etc. The specific sequent calculus that I’m to talk about is sometimes called system-LK; the general category of things that use this basic kind of rules is called Gentzen systems.
\nThe sequent calculus consists of a set of rules called *sequents*, each of which is normally written like a fraction: the top of the fraction is what you know before applying the sequent; the bottom is what you can conclude. The statements in the sequents are always of the form:<\/p>\n
CONTEXTS, Predicates :- CONTEXTS, Predicates<\/p>\n
\nThe “CONTEXTS” are sets of predicates that you already know are true. The “:-” is read “entails”; it means that the *conjuction* of the statements and contexts to the left of it can prove the *disjunction* of the statements to the right of it. In predicate logic, the conjuction is logical and, and disjunction is logical or, so you can read the statements as if “,” is “∧” on the left of the “:-“, and “∨” on the right. *(Note: this paragraph was modified to correct a dumb error that I made that was pointed out by commenter Canuckistani.)*
\nContexts are generally written using capital greek letters; predicates are generally written using uppercase english letters. We often put a name for an inference rule to the right of the separator line for the sequent.
\nFor example, look at the following sequent:
\nΓ :- Δ
\n————— Weakening-Left
\nΓ,A :- Δ
\nThis sequent is named Weakening-left; the top says that “Given Γ everything in Δ can be proved.”; and
\nthe bottom says “Using Γ plus the fact that A is true, everything in Δ can be proved”. The full sequent basically says: if Δ is provable given Γ, then it will still be provable when A is added to Γ;in other words, adding a true fact won’t invalidate any proofs that were valid before the addition of A. *(Note: this paragraph was modified to correct an error pointed out by a commenter.)*
\nThe sequent calculus is nothing but a complete set of rules that you can use to perform any inference in predicate calculus. A few quick syntactic notes, and I’ll show you the full set of rules.
\n1. Uppercase greek letters are contexts.
\n2. Uppercase english letters are *statements*.
\n3. Lowercase english letters are *terms*; that is, the objects that predicates
\ncan reason about, or variables representing objects.
\n4. A[b] is a statement A that contains the term b in some way.
\n5. A[b\/c] means A with the term “b” replaced by the term “c”.
\n——-
\nFirst, two very basic rules:
\n1.
\n———— (Identity)
\nA :- A
\n2. Γ :- A, Δ Σ, A :- Π
\n—————————————— (Cut)
\nΓ,Σ :- Δ, Π
\nNow, there’s a bunch of rules that have right and left counterparts. They’re duals of each other – move terms across the “:-” and switch from ∧ to ∨ or vice-versa.
\n3. Γ, A :- Δ
\n————————— (Left And 1)
\nΓ, A ∧ B :- Δ
\n4. Γ :- A, Δ
\n——————— ——— (Right Or 1)
\nΓ, :- A ∨ B, Δ
\n5. Γ, B :- Δ
\n——————— ——(Left And 2)
\nΓ,A ∧ B :- Δ
\n6. Γ :- B, Δ
\n——————— ——— (Right Or 2)
\nΓ :- A ∧ B, Δ
\n7. Γ, A :- Δ Σ,B :- Π
\n————————————— (Left Or)
\nΓ,Σ, A ∨ B :- Δ,Π
\n8. Γ :- A,Δ Σ :- B,Π
\n—————————— ——(Right And)
\nΓ,Σ :- A ∧ B, Δ,Π
\n9. Γ :- A,Δ
\n————— —— (Left Not)
\nΓ, ¬A :- Δ
\n10. Γ,A :- Δ
\n——————— (Right Not)
\nΓ :- ¬A, Δ
\n11. Γ :- A,Δ Σ,B :- Π
\n————————————— (Left Implies)
\nΓ, Σ, A → B :- Δ,Π
\n12. Γ,A[y] :- Δ *(y bound)*
\n————————————— (Left Forall)
\nΓ,∀x A[x\/y] :- Δ
\n13. Γ :- A[y],Δ *(y free)*
\n————————————— (Right Forall)
\nΓ :- ∀x A[x\/y],Δ
\n14. Γ, A[y] :- Δ *(y bound)*
\n———————————— (Left Exists)
\nΓ,∃x A[x\/y] :- Δ
\n15. Γ, :- A[y], Δ *(y free)*
\n————————————(Right Exists)
\nΓ :- ∃x A[x\/y], Δ
\n16. Γ :- Δ
\n—————— (Left Weakening)
\nΓ, A :- Δ
\n17. Γ :- Δ
\n—————— (Right Weakening)
\nΓ :- A, Δ
\n18. Γ, A, A :- Δ
\n——————— (Left Contraction)
\nΓ,A :- Δ
\n19. Γ :- A, A, Δ
\n——————— (Right Contraction)
\nΓ :- A, Δ
\n20. Γ, A, B, Δ :- Σ
\n————————— (Left Permutation)
\nΓ,B, A, Δ :- Σ
\n21. Γ :- Δ, A, B, Σ
\n————————— (Right Permutation)
\nΓ :- Δ B, A, Σ
\nHere’s an example of how we can use sequents to derive A ∨ ¬ A:
\n1. Context empty. Apply Identity.
\n2. A :- A. Apply Right Not.
\n3. empty :- ¬ A, A. Apply Right And 2.
\n4. empty : A ∨ ¬A, A. Apply Permute Right.
\n5. empty :- A, A ∨ ¬ A. Apply Right And 1.
\n6. empty :- A ∨ ¬ A, A ∨ ¬ A. Right Contraction.
\n7. empty :- A ∨ ¬ A
\nIf you look *carefully* at the rules, they actually make a lot of sense. The only ones that look a bit strange are the “forall” rules; and for those, you need to remember that the variable is *free* on the top of the sequent.
\nA lot of logics can be described using Gentzen systems; from type theory, to temporal logics, to all manner of other systems. They’re a very powerful tool for describing all manner of inference systems.<\/p>\n","protected":false},"excerpt":{"rendered":"
*(This post has been modified to correct some errors and add some clarifications in response to comments from alert readers. Thanks for the corrections!)* Today, we’re going to take a brief diversion from category theory to play with some logic. There are some really neat connections between variant logics and category theory. I’m planning on […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[76,24],"tags":[],"class_list":["post-77","post","type-post","status-publish","format-standard","hentry","category-category-theory","category-goodmath"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-1f","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/77","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=77"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/77\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=77"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=77"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=77"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}