commit 160b714ff6f80a919ed860806d788bb9dde31ec0
parent e34c8bd4a764cdeac2426de3e31d38c17087f5b4
Author: Alex Balgavy <alex@balgavy.eu>
Date: Tue, 8 Feb 2022 18:39:43 +0100
Remove redundant file
Diffstat:
1 file changed, 0 insertions(+), 33 deletions(-)
diff --git a/content/advanced-logic-notes/lecture-1.md b/content/advanced-logic-notes/lecture-1.md
@@ -1,33 +0,0 @@
-+++
-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
