commit e34c8bd4a764cdeac2426de3e31d38c17087f5b4
parent 505e978e83b5e86bf7ac00a602c1be85cf691f33
Author: Alex Balgavy <alex@balgavy.eu>
Date: Tue, 8 Feb 2022 18:39:02 +0100
Advanced logic: lecture 1
Diffstat:
5 files changed, 109 insertions(+), 0 deletions(-)
diff --git a/content/_index.md b/content/_index.md
@@ -11,6 +11,7 @@ title = "Alex's university course notes"
* [Hardware Security](hwsec-notes/)
* [Advanced Computer Networks](acn-notes/)
* [Software Containerisation](softcont-notes/)
+* [Advanced Logic](advanced-logic-notes/)
## Subject notes: Year 1
* [Computer & Network Security](computer-network-security/)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -0,0 +1,5 @@
++++
+title = 'Advanced Logic'
++++
+# Advanced Logic
+1. [Lecture 1](lecture-1)
diff --git a/content/advanced-logic-notes/lecture-1.md b/content/advanced-logic-notes/lecture-1.md
@@ -0,0 +1,33 @@
++++
+title = 'Lecture 1'
++++
+
+# Intro
+
+Basic model logic operators:
+- □: necessary, known, provable
+- ◇: possible, considered possible
+
+- ◇ φ ⇔ ¬□ ¬φ
+- □ φ ⇔ ¬◇ ¬φ
+
+# First-order propositional logic
+Includes variables, T, ⊥, not, and, or, implication.
+Proofs are given by structural induction.
+Precedence is ¬, then ∧∨, then →.
+
+a valuation v : Var → {0,1} maps propositional variables to truth values.
+
+the semantics of a formula under a valuation is defined with ⟦p⟧ᵥ = v(p), with p ∈ Var
+
+if ⟦φ⟧ᵥ = 1, we write v ⊨ φ (read "v models φ")
+- then, φ has a model, so φ is satisfiable
+
+If every model of all φᵢ is a model of ψ, we write φ₁,...,φn ⊨ ψ
+- then ψ is a semantic consequence of φ₁,...,φn
+
+If v ⊨ φ for all valuations of v, then ⊨ φ (φ is a tautology)
+
+Soundness: ⊢ implies ⊨, proved by induction on length of proof
+
+Completeness: ⊨ implies ⊢, can be proven using consistency
diff --git a/content/advanced-logic-notes/lecture-1/index.md b/content/advanced-logic-notes/lecture-1/index.md
@@ -0,0 +1,70 @@
++++
+title = 'Lecture 1'
++++
+
+# Intro
+
+Basic model logic operators:
+- □: necessary, known, provable
+- ◇: possible, considered possible
+
+- ◇ φ ⇔ ¬□ ¬φ
+- □ φ ⇔ ¬◇ ¬φ
+
+# First-order propositional logic
+Includes variables, T, ⊥, not, and, or, implication.
+Proofs are given by structural induction.
+Precedence is ¬, then ∧∨, then →.
+
+a valuation v : Var → {0,1} maps propositional variables to truth values.
+
+the semantics of a formula under a valuation is defined with ⟦p⟧ᵥ = v(p), with p ∈ Var
+
+if ⟦φ⟧ᵥ = 1, we write v ⊨ φ (read "v models φ")
+- then, φ has a model, so φ is satisfiable
+
+If every model of all φᵢ is a model of ψ, we write φ₁,...,φn ⊨ ψ
+- then ψ is a semantic consequence of φ₁,...,φn
+
+If v ⊨ φ for all valuations of v, then ⊨ φ (φ is a tautology)
+
+Soundness: ⊢ implies ⊨, proved by induction on length of proof
+
+Completeness: ⊨ implies ⊢, can be proven using consistency
+
+# Basic modal logic
+E.g. "whatever is necessary is possible" == □φ → ◇φ
+
+□ can also mean "I know", e.g. "I know that someone appreciates me" == ∃x.□A(x, M)
+
+Loeb's formula: □ (□ p → p) → □ p
+
+Veridicality: □ φ → φ
+
+Truth s relative to current situation/world/environment:
+- formulas evaluated in given structure
+- necessity: truth in all accessible worlds
+- possibility: truth in some accessible world (at least one)
+
+## Frames
+A situation is set by a frame F = (W,R)
+- W ≠ ∅ set of possible worlds/states
+- R ⊆ W × W an accessibility/transition relation
+
+A frame could be (ℕ, <), or ({1,2,3,4}, {(1,2), (2,4), (1,3), (3,4), (2,2)})
+
+## Models
+model: pair M = (F, V)
+- a frame F = (W,R)
+- a valuation V : Var → W → {0,1}, or V : Var → P(W)
+
+pointed model: pair (M,w) of model M and w a world in M
+
+
+
+◇T holds if at least one successor.
+□⊥ holds if there is no successor.
+
+Dualities:
+- ◇ φ := ¬ □ ¬ φ
+- □ φ := ¬ ◇ ¬ φ
diff --git a/content/advanced-logic-notes/lecture-1/local-truth-definitions.png b/content/advanced-logic-notes/lecture-1/local-truth-definitions.png
Binary files differ.
