commit 845b20470e3c57466088262629ee6aee5f86e243
parent 3681e3c715632cdcecae9099a00af900e36e1e13
Author: Alex Balgavy <alex@balgavy.eu>
Date: Tue, 29 Mar 2022 18:11:23 +0200
Finalize advanced logic notes
Diffstat:
3 files changed, 7 insertions(+), 1 deletion(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -25,6 +25,8 @@ Worked exercises:
- [Homework 1](homework-1/): misc topics
- [Some midterm solutions](some-midterm-solutions/): validity, bisimulation, definability in BML
+[Here's my Anki deck](advanced-logic.apkg)
+
I drew the graphs on these pages with [Graphviz](https://graphviz.org/), I used [vim-literate-markdown](https://github.com/thezeroalpha/vim-literate-markdown)'s tangling functionality to quickly extract graph code to separate files.
You can install Graphviz and run e.g. `dot < graph.dot -Tsvg > graph.svg` (also accepts input files as parameters).
Or you can install [PlantUML](https://plantuml.com/), surround the code with `@startdot...@enddot`, and run `plantuml -p -Tsvg < graph.puml > graph.svg`.
diff --git a/content/advanced-logic-notes/advanced-logic.apkg b/content/advanced-logic-notes/advanced-logic.apkg
Binary files differ.
diff --git a/content/advanced-logic-notes/formula-validity-using-sequents-and-tableaux/index.md b/content/advanced-logic-notes/formula-validity-using-sequents-and-tableaux/index.md
@@ -22,6 +22,10 @@ For modal logic:
- If we get a sequent of the form p₁...n, ◇φ₁..◇φm ⇒ q₁..qk, ◇ψ₁...◇ψl
- Such a sequent only valid iff either pᵢ = qj for some i and j, or φᵢ ⇒ ψ₁...ψl is valid for some i ∈ {1...m}
+A sequent _closes_ if the conjunction of the left side implies a disjunction of the right side.
+That is, φ₁ ∧ ... ∧ φᵤ ⇒ ψ₁ ∨ ... ∨ ψᵥ.
+So if _any_ of the formulas on the left appear on the right.
+
Start with intended conclusion, try to build a proof while moving upwards.
Formula is valid iff it is derivable in sequent calculus.
Validity using sequents:
@@ -41,7 +45,7 @@ If all solid branches close, yields validity of initial sequent.
If at least one branch does not close, yields a counterexample.
The dot separates assumptions on the left from what's true on the right.
-A branch closes if what's assumed also holds in the state.
+"Closing" is the same as for sequents.
