commit 1c98cf9feaa8bc29d1e7b7a9e4fdc3430d182e74 parent c2fab7f260f7a290ffc497f43b74571529ec8e2c Author: Alex Balgavy <alex@balgavy.eu> Date: Thu, 5 Nov 2020 23:06:01 +0100 Logic and modelling notes Diffstat:
61 files changed, 729 insertions(+), 2898 deletions(-)
diff --git a/content/_index.md b/content/_index.md @@ -27,7 +27,7 @@ title = "Alex's university course notes" * [Intelligent Systems](is-notes/) * [Linear Algebra](lin-algebra-notes/) * [Software Design](https://thezeroalpha.github.io/softdesign-notes) -* [Logic & Modelling](https://thezeroalpha.github.io/logic-modelling-notes) +* [Logic & Modelling](logic-modelling-notes/) * [Databases](databases-notes) * [A Likelihood Approach to Statistics (Honors)](https://github.com/thezeroalpha/likelihood-notes/blob/master/notes.pdf) * [Human Computer Interaction](hci-notes/) diff --git a/content/logic-modelling-notes/The one-page cheat sheet.html b/content/logic-modelling-notes/The one-page cheat sheet.html @@ -1,146 +0,0 @@ -<html> -<head> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <title>The one-page cheat sheet</title> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -</head> -<body> - <a href="index.html">Index</a> - <hr> - <div class="content"> - -<div id="One-page cheat sheet"><h2 id="One-page cheat sheet" class="header"><a href="#One-page cheat sheet">One-page cheat sheet</a></h2></div> -<div id="One-page cheat sheet-Definitions"><h3 id="Definitions" class="header"><a href="#One-page cheat sheet-Definitions">Definitions</a></h3></div> -<ul> -<li> -Model is: - -<ul> -<li> -set A - domain - -<li> -interpretation operation for predicate and function symbols - -</ul> -<li> -satisfiable: some model & environment where it's true - -<li> -valid: true in all models and environments - -<li> -derivable: can be proven without global hypothesis - -<li> -tautology: true under any truth assignment (valid) - -<li> -soundness: ⊢ A → ⊨ A (from syntax to semantics) - -<li> -completeness: ⊨ A → ⊢ A (from semantics to syntax) - -<li> -partial order: antisymmetric, reflexive, transitive - -<ul> -<li> -memo technique -- p*<span id="One-page cheat sheet-Definitions-art"></span><strong id="art">art</strong>*ial means *<span id="One-page cheat sheet-Definitions-a"></span><strong id="a">a</strong>*ntisymmetric, *<span id="One-page cheat sheet-Definitions-r"></span><strong id="r">r</strong>*eflexive, *<span id="One-page cheat sheet-Definitions-t"></span><strong id="t">t</strong>*ransitive - -<li> -strict means irreflexive - -</ul> -<li> -total order: partial order & ∀ ab: R(a,b) ∨ R(b,a) - -<ul> -<li> -strict: ∀ ab: R(a,b) ∨ a = b ∨ R(b,a) - -</ul> -<li> -equivalence relation: has all three properties in the positive (symmetric, reflexive, transitive) - -</ul> - -<p> -environment is used to interpret free variables -</p> -<div id="One-page cheat sheet-Modal logic"><h3 id="Modal logic" class="header"><a href="#One-page cheat sheet-Modal logic">Modal logic</a></h3></div> -<ul> -<li> -□ Φ: true in world if true in all related worlds (if no related, true). - -<li> -◇ Φ: true in world if true in some related world (if no related, false). - -</ul> - -<p> -M,w ⊩ Φ: Φ true in world w of Kripke model M (true in model if true in every world) -</p> - -<p> -Φ valid in frame if true with every labelling. -</p> - -<p> -frame = Kripke - labels -</p> - -<div id="One-page cheat sheet-Metatheorems"><h3 id="Metatheorems" class="header"><a href="#One-page cheat sheet-Metatheorems">Metatheorems</a></h3></div> -<ul> -<li> -consistent: has a model - -<li> -syntactically consistent: can't derive ⊥ - -<li> -compactness: if Γ is consistent, every finite subset of Γ is also consistent - -</ul> - -<div id="One-page cheat sheet-Definability"><h3 id="Definability" class="header"><a href="#One-page cheat sheet-Definability">Definability</a></h3></div> -<p> -Model finiteness is undefinable. -</p> - -<p> -Model infiniteness is definable by a set of formulas. -</p> - -<p> -In predicate logic, only unreachability by n steps is definable, and only by a set of sentences. -</p> - -<div id="One-page cheat sheet-Decidability"><h3 id="Decidability" class="header"><a href="#One-page cheat sheet-Decidability">Decidability</a></h3></div> -<p> -Y ⊆ I decidable if program can tell for every i ∈ I whether i ∈ Y. I set, Y predicate on set. -</p> - -<p> -Undecidable: termination, PCP, validity, provability, satisfiability. -</p> - -<p> -Termination can be reduced to PCP, which can be reduced to validity. -</p> - -<p> -Incompleteness theorems: every non-trivial formal system is -</p> -<ul> -<li> -either incomplete (valid but not derivable) - -<li> -or inconsistent (doesn't have a model, or entails ⊥) - -</ul> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/The one-page cheat sheet.md b/content/logic-modelling-notes/The one-page cheat sheet.md @@ -0,0 +1,55 @@ ++++ +title = 'One-page cheat sheet' ++++ +# One-page cheat sheet +## Definitions +* Model is: + * set A - domain + * interpretation operation for predicate and function symbols +* satisfiable: some model & environment where it's true +* valid: true in all models and environments +* derivable: can be proven without global hypothesis +* tautology: true under any truth assignment (valid) +* soundness: ⊢ A → ⊨ A (from syntax to semantics) +* completeness: ⊨ A → ⊢ A (from semantics to syntax) +* partial order: antisymmetric, reflexive, transitive + * memo technique -- p**art**ial means **a**ntisymmetric, **r**eflexive, **t**ransitive + * strict means irreflexive +* total order: partial order & ∀ ab: R(a,b) ∨ R(b,a) + * strict: ∀ ab: R(a,b) ∨ a = b ∨ R(b,a) +* equivalence relation: has all three properties in the positive (symmetric, reflexive, transitive) + +environment is used to interpret free variables +## Modal logic +* □ Φ: true in world if true in all related worlds (if no related, true). +* ◇ Φ: true in world if true in some related world (if no related, false). + +M,w ⊩ Φ: Φ true in world w of Kripke model M (true in model if true in every world) + +Φ valid in frame if true with every labelling. + +frame = Kripke - labels + +## Metatheorems +* consistent: has a model +* syntactically consistent: can't derive ⊥ +* compactness: if Γ is consistent, every finite subset of Γ is also consistent + +## Definability +Model finiteness is undefinable. + +Model infiniteness is definable by a set of formulas. + +In predicate logic, only unreachability by n steps is definable, and only by a set of sentences. + +## Decidability +Y ⊆ I decidable if program can tell for every i ∈ I whether i ∈ Y. I set, Y predicate on set. + +Undecidable: termination, PCP, validity, provability, satisfiability. + +Termination can be reduced to PCP, which can be reduced to validity. + +Incompleteness theorems: every non-trivial formal system is +* either incomplete (valid but not derivable) +* or inconsistent (doesn't have a model, or entails ⊥) + diff --git a/content/logic-modelling-notes/_index.md b/content/logic-modelling-notes/_index.md @@ -0,0 +1,57 @@ ++++ +title = 'Logic and Modeling' ++++ + +# Logic and Modeling +Here's the [online book](http://avigad.github.io/logic_and_proof/propositional_logic.html). + +Also, [here's my Anki deck](logic-modelling.apkg). + +[The one-page cheat sheet](the-one-page-cheat-sheet). + +- [Propositional logic](propositional-logic) + - [Notation review](propositional-logic#notation-review) + - [Rules of inference](propositional-logic#rules-of-inference) + - [Forward and backward reasoning](propositional-logic#forward-and-backward-reasoning) + - [Proof by contradiction](propositional-logic#proof-by-contradiction) + - [Vocab definitions](propositional-logic#vocab-definitions) + - [Classical reasoning](propositional-logic#classical-reasoning) + - [Syntax vs Semantics](propositional-logic#syntax-vs-semantics) + - [Soundness and completeness](propositional-logic#soundness-and-completeness) +- [First order logic](first-order-logic) + - [Functions, predicates, relations](first-order-logic#functions-predicates-relations) + - [Quantifiers, binding](first-order-logic#quantifiers-binding) + - [Natural deduction rules](first-order-logic#natural-deduction-rules) + - [Relativization and sorts](first-order-logic#relativization-and-sorts) + - [Models](first-order-logic#models) + - [Interpreting formulas without quantifiers](first-order-logic#interpreting-formulas-without-quantifiers) + - [Interpretation of formulas with quantifiers and free variables](first-order-logic#interpretation-of-formulas-with-quantifiers-and-free-variables) + - [Interpreting terms in model with environment](first-order-logic#interpreting-terms-in-model-with-environment) + - [Semantical entailment in predicate logic](first-order-logic#semantical-entailment-in-predicate-logic) + - [Logical equivalence](first-order-logic#logical-equivalence) + - [Satisfiability, validity, consistency](first-order-logic#satisfiability-validity-consistency) + - [Translating into predicate logic](first-order-logic#translating-into-predicate-logic) + - [Rules for quantifiers and connectives](first-order-logic#rules-for-quantifiers-and-connectives) + - [Semantics of first order logic](first-order-logic#semantics-of-first-order-logic) +- [Sets](sets) + - [Relations](sets#relations) + - [Order types](sets#order-types) + - [Natural numbers & induction](sets#natural-numbers-induction) + - [Recursive definitions](sets#recursive-definitions) +- [Modal logic](modal-logic) + - [Truth in worlds](modal-logic#truth-in-worlds) + - [Truth in Kripke models](modal-logic#truth-in-kripke-models) + - [Semantic implication/entailment](modal-logic#semantic-implication-entailment) + - [Frames](modal-logic#frames) +- [Meta-Theorems of Predicate Logic](meta-theorems-of-predicate-logic) +- [Definability and Undefinability results](definability-and-undefinability-results) + - [for model cardinality](definability-and-undefinability-results#for-model-cardinality) + - [for reachability](definability-and-undefinability-results#for-reachability) + - [General overview](definability-and-undefinability-results#general-overview) +- [Decidability and Undecidability](decidability-and-undecidability) + - [Decision problems](decidability-and-undecidability#decision-problems) + - [Termination problem](decidability-and-undecidability#termination-problem) + - [Post's Correspondence Problem](decidability-and-undecidability#posts-correspondence-problem) + - [Undecidability of Validity and Provability](decidability-and-undecidability#undecidability-of-validity-and-provability) + - [Undecidability of Satisfiability](decidability-and-undecidability#undecidability-of-satisfiability) +- [Incompleteness theorem](incompleteness-theorem) diff --git a/content/logic-modelling-notes/addjs.sh b/content/logic-modelling-notes/addjs.sh @@ -1,10 +0,0 @@ -#!/usr/bin/env bash -if ! command -v vim; then - echo "Don't know how to do this without vim yet." - exit 1 -elif [ $# -ne 1 ]; then - echo "Need to pass the file as argument." - exit 1 -fi - -vim -c 'v/<head> <script/ s#<head>#<head> <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>' -c 'wq' $1 diff --git a/content/logic-modelling-notes/decidability-and-undecidability.html b/content/logic-modelling-notes/decidability-and-undecidability.html @@ -1,217 +0,0 @@ -<html> -<head> - <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> - <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> - <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> - <script> - document.addEventListener('DOMContentLoaded', function() { - document.querySelectorAll('pre.code').forEach(function(item) { - hljs.highlightBlock(item) - }) - }); - </script> - <title>decidability-and-undecidability</title> -</head> -<body> -<style type="text/css"> -nav a { - text-align: left; -} -nav #name { - text-align: right; - float: right; - font-style: italic; -} -</style> - <nav> - <a href="index.html">Index</a> - <span id="name">Alex Balgavy</span> - </nav> - <hr> - <div class="content"> - -<div id="Decidability and Undecidability"><h2 id="Decidability and Undecidability" class="header"><a href="#Decidability and Undecidability">Decidability and Undecidability</a></h2></div> -<div id="Decidability and Undecidability-Decision problems"><h3 id="Decision problems" class="header"><a href="#Decidability and Undecidability-Decision problems">Decision problems</a></h3></div> -<p> -Decision problem consists of set I and a predicate Y ⊆ I -</p> - -<p> -Examples: -</p> -<ul> -<li> -determine whether a number is prime: - -<ul> -<li> -input: natural number n - -<ul> -<li> -I = N - -</ul> -<li> -output: yes if n is prime, no otherwise - -<ul> -<li> -Y = { n ∈ N | n is prime } - -</ul> -</ul> -<li> -termination problem (whether a program terminates): - -<ul> -<li> -input: program P, input w - -<ul> -<li> -I = set of all pairs <program, input> - -</ul> -<li> -output: yes if P started with input w terminates, no otherwise - -<ul> -<li> -Y = { <P, w> | P terminates on input w } - -</ul> -</ul> -<li> -validity problem (determine whether a formula is valid): - -<ul> -<li> -input: formula Φ of predicate logic - -<ul> -<li> -I = set of formulas of predicate logic - -</ul> -<li> -output: yes if Φ is valid, no otherwise - -<ul> -<li> -Y = set of valid formulas in predicate logic - -</ul> -</ul> -</ul> - -<p> -A decision problem Y ⊆ I is decidable if there is a program that tells for every i ∈ I whether i ∈ Y. -</p> - -<div id="Decidability and Undecidability-Decision problems-Termination problem"><h4 id="Termination problem" class="header"><a href="#Decidability and Undecidability-Decision problems-Termination problem">Termination problem</a></h4></div> -<p> -This problem is undecidable. -</p> - -<p> -steps: -</p> -<ul> -<li> -T outputs yes on input <P, w> ⇔ P halts on input w - -<li> -Tself outputs yes on input P ⇔ P halts on input P - -<li> -Z halts on input P ⇔ P does not halt on input P - -<li> -Z halts on input Z ⇔ Z does not halt on input Z - -<li> -contradiction. - -</ul> - -<div id="Decidability and Undecidability-Decision problems-Post's Correspondence Problem"><h4 id="Post's Correspondence Problem" class="header"><a href="#Decidability and Undecidability-Decision problems-Post's Correspondence Problem">Post's Correspondence Problem</a></h4></div> -<p> -Given n pairs of words: <w1, v1> , ..., <wn, vn> -</p> - -<p> -are there indices \(i_1, i_2, ..., i_k\) (k ≥ 1) s.t. when concatenated, \(wi_1 wi_2 ... wi_k = vi_1 vi_2 ... vi_k \)? -</p> - -<p> -as a decision problem: -</p> -<ul> -<li> -\(PCP = \{ < <w_1, v_1>, ..., <w_k, v_k> > | k ≥ 1, w_i, v_i \; \text{binary words} \}\) - -<li> -Y = { i ∈ PCP | i has a solution } - -</ul> - -<p> -it's undecidable. -</p> - -<p> -the termination problem can be reduced to PCP -- there is a computable function r that maps instances of termination problem to instances of PCP such that it holds: \(P\text{ terminates on input w} \iff I_{<P, w>}\text{ has a solution}\) -</p> - -<p> -the validity problem in predicate logic is undecidable (no program that, given formula Φ, decides whether or not ⊨ Φ holds). PCP can be reduced to validity problem: -</p> -<ul> -<li> -I (instance of PCP) has a solution ⇔ ⊨ ΦI (instance of validity problem is valid) - -</ul> - -<p> -Then if we had program deciding validity for predicate logic, we would obtain PCP-solver. Not gonna work. -</p> - -<div id="Decidability and Undecidability-Undecidability of Validity and Provability"><h3 id="Undecidability of Validity and Provability" class="header"><a href="#Decidability and Undecidability-Undecidability of Validity and Provability">Undecidability of Validity and Provability</a></h3></div> -<p> -The validity problem in predicate logic is undecidable. -There cannot be a program that, given any formula Φ, decides whether or not ⊨Φ holds. -</p> - -<p> -The provability in predicate logic is undecidable. -There cannot be a program that, given any formula Φ, decides whether or not ⊢ Φ holds. -This follows from soundness and completeness theorem. -</p> - -<div id="Decidability and Undecidability-Undecidability of Satisfiability"><h3 id="Undecidability of Satisfiability" class="header"><a href="#Decidability and Undecidability-Undecidability of Satisfiability">Undecidability of Satisfiability</a></h3></div> -<p> -for sentences Φ it holds: -</p> -<ul> -<li> -Φ is unsatisfiable ⇔ ¬ Φ is valid - -<li> -Φ is satisfiable ⇔ ¬ Φ is not valid - -</ul> - -<p> -there's an easy reduction of validity problem to satisfiability problem. -</p> - -<p> -The relations ⊨ and ⊢ in predicate logic are undecidable. -</p> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/decidability-and-undecidability.md b/content/logic-modelling-notes/decidability-and-undecidability.md @@ -0,0 +1,73 @@ ++++ +template = 'page-math.html' +title = 'Decidability and Undecidability' ++++ + +# Decidability and Undecidability +## Decision problems +Decision problem consists of set I and a predicate Y ⊆ I + +Examples: +* determine whether a number is prime: + * input: natural number n + * I = N + * output: yes if n is prime, no otherwise + * Y = { n ∈ N | n is prime } +* termination problem (whether a program terminates): + * input: program P, input w + * I = set of all pairs <program, input> + * output: yes if P started with input w terminates, no otherwise + * Y = { <P, w> | P terminates on input w } +* validity problem (determine whether a formula is valid): + * input: formula Φ of predicate logic + * I = set of formulas of predicate logic + * output: yes if Φ is valid, no otherwise + * Y = set of valid formulas in predicate logic + +A decision problem Y ⊆ I is decidable if there is a program that tells for every i ∈ I whether i ∈ Y. + +### Termination problem +This problem is undecidable. + +steps: +* T outputs yes on input <P, w> ⇔ P halts on input w +* Tself outputs yes on input P ⇔ P halts on input P +* Z halts on input P ⇔ P does not halt on input P +* Z halts on input Z ⇔ Z does not halt on input Z +* contradiction. + +### Post's Correspondence Problem +Given n pairs of words: <w1, v1> , ..., <wn, vn> + +are there indices $i_1, i_2, ..., i_k$ (k ≥ 1) s.t. when concatenated, $wi_1 wi_2 ... wi_k = vi_1 vi_2 ... vi_k $? + +as a decision problem: +* $PCP = \{ < <w_1, v_1>, ..., <w_k, v_k> > | k ≥ 1, w_i, v_i \; \text{binary words} \}$ +* Y = { i ∈ PCP | i has a solution } + +it's undecidable. + +the termination problem can be reduced to PCP -- there is a computable function r that maps instances of termination problem to instances of PCP such that it holds: $P\text{ terminates on input w} \iff I_{<P, w>}\text{ has a solution}$ + +the validity problem in predicate logic is undecidable (no program that, given formula Φ, decides whether or not ⊨ Φ holds). PCP can be reduced to validity problem: +* I (instance of PCP) has a solution ⇔ ⊨ ΦI (instance of validity problem is valid) + +Then if we had program deciding validity for predicate logic, we would obtain PCP-solver. Not gonna work. + +## Undecidability of Validity and Provability +The validity problem in predicate logic is undecidable. +There cannot be a program that, given any formula Φ, decides whether or not ⊨Φ holds. + +The provability in predicate logic is undecidable. +There cannot be a program that, given any formula Φ, decides whether or not ⊢ Φ holds. +This follows from soundness and completeness theorem. + +## Undecidability of Satisfiability +for sentences Φ it holds: +* Φ is unsatisfiable ⇔ ¬ Φ is valid +* Φ is satisfiable ⇔ ¬ Φ is not valid + +there's an easy reduction of validity problem to satisfiability problem. + +The relations ⊨ and ⊢ in predicate logic are undecidable. + diff --git a/content/logic-modelling-notes/definability-and-undefinability-results.html b/content/logic-modelling-notes/definability-and-undefinability-results.html @@ -1,196 +0,0 @@ -<html> -<head> - <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> - <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> - <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> - <script> - document.addEventListener('DOMContentLoaded', function() { - document.querySelectorAll('pre.code').forEach(function(item) { - hljs.highlightBlock(item) - }) - }); - </script> - <title>definability-and-undefinability-results</title> -</head> -<body> -<style type="text/css"> -nav a { - text-align: left; -} -nav #name { - text-align: right; - float: right; - font-style: italic; -} -</style> - <nav> - <a href="index.html">Index</a> - <span id="name">Alex Balgavy</span> - </nav> - <hr> - <div class="content"> - -<div id="Definability and Undefinability results"><h2 id="Definability and Undefinability results" class="header"><a href="#Definability and Undefinability results">Definability and Undefinability results</a></h2></div> -<p> -expressible frame properties in predicate/modal logic: -</p> - -<p> -<img src="img/expressible-frame-properties.png" alt="Expressible frame properties" /> -</p> - -<div id="Definability and Undefinability results-for model cardinality"><h3 id="for model cardinality" class="header"><a href="#Definability and Undefinability results-for model cardinality">for model cardinality</a></h3></div> -<p> -model cardinality: -</p> - -<p> -<img src="img/model-cardinality-definition.png" alt="Model cardinality definition" /> -</p> - - -<p> -for all models M and all n ≥ 2 it holds that: -</p> -<ul> -<li> -M ⊨ Φn ⇔ A has at least n elements - -<li> -M ⊨ ψn ⇔ A has at most n elements - -<li> -M ⊨ Φn ∧ ψn ⇔ A has precisely n elements - -</ul> - -<p> -model infiniteness is definable by a set of formulas Δ: -</p> -<ul> -<li> -M ⊨ Δ ⇔ M has an infinite domain - -</ul> - -<p> -model finiteness is undefinable (single formula): -</p> -<ul> -<li> -there's no sentence ψ such that - -<li> -all M: M ⊨ ψ ⇔ M has a finite domain - -</ul> - -<p> -model finiteness is undefinable (set of formulas): -</p> -<ul> -<li> -there's no set of formulas Γ such that - -<li> -all M: M ⊨ Γ ⇔ M has a finite domain - -</ul> - -<p> -mode infiniteness is undefinable (single formula) -</p> -<ul> -<li> -there's no sentence ψ such that - -<li> -all M: M ⊨ ψ ⇔ M has infinite domain - -</ul> - -<div id="Definability and Undefinability results-for reachability"><h3 id="for reachability" class="header"><a href="#Definability and Undefinability results-for reachability">for reachability</a></h3></div> -<p> -"v is reachable via R from u". thinking of R as arrows, it means that there's a path from v to u. -</p> - -<p> -search for formulas χn that express reachability in n steps: -</p> - -<p> -Reachable in n steps: -</p> -<ol> -<li> -u = v - -<li> -R(u,v) - -<li> -∃x₁ (RU, x₁) ∧ R(x₁, v)) - -<li> -∃x₁ ∃x₂ (R(u, x₁) ∧ R(x₁, x₂) ∧ R(x₂, v)) - -<li> -.... - -</ol> - -<p> -shorthand: χ₂(c,d) denotes formula ∃x₁ (R(c, x₁) ∧ R(x₁, d)) -</p> - -<p> -<img src="img/theorem-for-reachability.png" alt="Theorem for reachability" /> -</p> - -<p> -reachability is undefinable: -</p> - -<p> -<img src="img/reachability-is-undefinable.png" alt="Reachability is undefinable" /> -</p> - - -<p> -Let R be a binary relation symbol. -</p> -<ol> -<li> -In predicate logic, reachability by R-steps is - -<ul> -<li> -not definable by a sentence - -<li> -not definable by a set of sentences - -</ul> -<li> -In predicate logic, unreachability by R-steps is - -<ul> -<li> -not definable by a single sentence - -<li> -definable by a set of sentences - -</ul> -</ol> - -<div id="Definability and Undefinability results-General overview"><h3 id="General overview" class="header"><a href="#Definability and Undefinability results-General overview">General overview</a></h3></div> -<p> -<img src="img/undefinability-results-overview.png" alt="Undefinability results overview" /> -</p> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/img/expressible-frame-properties.png b/content/logic-modelling-notes/definability-and-undefinability-results/expressible-frame-properties.png Binary files differ. diff --git a/content/logic-modelling-notes/definability-and-undefinability-results/index.md b/content/logic-modelling-notes/definability-and-undefinability-results/index.md @@ -0,0 +1,67 @@ ++++ +template = 'page-math.html' +title = 'Definability and Undefinability results' ++++ +# Definability and Undefinability results +expressible frame properties in predicate/modal logic: + + + +## for model cardinality +model cardinality: + + + + +for all models M and all n ≥ 2 it holds that: +* M ⊨ Φn ⇔ A has at least n elements +* M ⊨ ψn ⇔ A has at most n elements +* M ⊨ Φn ∧ ψn ⇔ A has precisely n elements + +model infiniteness is definable by a set of formulas Δ: +* M ⊨ Δ ⇔ M has an infinite domain + +model finiteness is undefinable (single formula): +* there's no sentence ψ such that +* all M: M ⊨ ψ ⇔ M has a finite domain + +model finiteness is undefinable (set of formulas): +* there's no set of formulas Γ such that +* all M: M ⊨ Γ ⇔ M has a finite domain + +mode infiniteness is undefinable (single formula) +* there's no sentence ψ such that +* all M: M ⊨ ψ ⇔ M has infinite domain + +## for reachability +"v is reachable via R from u". thinking of R as arrows, it means that there's a path from v to u. + +search for formulas χn that express reachability in n steps: + +Reachable in n steps: +1. u = v +2. R(u,v) +3. ∃x₁ (RU, x₁) ∧ R(x₁, v)) +4. ∃x₁ ∃x₂ (R(u, x₁) ∧ R(x₁, x₂) ∧ R(x₂, v)) +5. .... + +shorthand: χ₂(c,d) denotes formula ∃x₁ (R(c, x₁) ∧ R(x₁, d)) + + + +reachability is undefinable: + + + + +Let R be a binary relation symbol. +1. In predicate logic, reachability by R-steps is + * not definable by a sentence + * not definable by a set of sentences +2. In predicate logic, unreachability by R-steps is + * not definable by a single sentence + * definable by a set of sentences + +## General overview + + diff --git a/content/logic-modelling-notes/img/model-cardinality-definition.png b/content/logic-modelling-notes/definability-and-undefinability-results/model-cardinality-definition.png Binary files differ. diff --git a/content/logic-modelling-notes/img/reachability-is-undefinable.png b/content/logic-modelling-notes/definability-and-undefinability-results/reachability-is-undefinable.png Binary files differ. diff --git a/content/logic-modelling-notes/img/theorem-for-reachability.png b/content/logic-modelling-notes/definability-and-undefinability-results/theorem-for-reachability.png Binary files differ. diff --git a/content/logic-modelling-notes/img/undefinability-results-overview.png b/content/logic-modelling-notes/definability-and-undefinability-results/undefinability-results-overview.png Binary files differ. diff --git a/content/logic-modelling-notes/first-order-logic.html b/content/logic-modelling-notes/first-order-logic.html @@ -1,467 +0,0 @@ -<html> -<head> - <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> - <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> - <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> - <script> - document.addEventListener('DOMContentLoaded', function() { - document.querySelectorAll('pre.code').forEach(function(item) { - hljs.highlightBlock(item) - }) - }); - </script> - <title>first-order-logic</title> -</head> -<body> -<style type="text/css"> -nav a { - text-align: left; -} -nav #name { - text-align: right; - float: right; - font-style: italic; -} -</style> - <nav> - <a href="index.html">Index</a> - <span id="name">Alex Balgavy</span> - </nav> - <hr> - <div class="content"> - -<div id="First order logic"><h2 id="First order logic" class="header"><a href="#First order logic">First order logic</a></h2></div> -<div id="First order logic-Functions, predicates, relations"><h3 id="Functions, predicates, relations" class="header"><a href="#First order logic-Functions, predicates, relations">Functions, predicates, relations</a></h3></div> -<p> -functions: take different numbers of arguments, returns a result. e.g. \(mul(x,y)\), \(square(x)\) -</p> - -<p> -predicates, relations: takes one or more arguments, is either true or false. e.g. \(even(x)\), \(divides(x,y)\) -</p> - -<p> -formulas: say things. make assertions about objects in the domain. -</p> - -<div id="First order logic-Quantifiers, binding"><h3 id="Quantifiers, binding" class="header"><a href="#First order logic-Quantifiers, binding">Quantifiers, binding</a></h3></div> -<p> -Quantifiers: -</p> -<ul> -<li> -∀x: "for all x" - -<li> -∃x: "there exists an x" - -</ul> - -<p> -Generally bind tightly: ∀x P ∨ Q == (∀x P) ∨ Q -</p> - -<p> -free variable: variable that's not bound -</p> - -<p> -sentence: a formula that has no free variables -</p> - -<div id="First order logic-Quantifiers, binding-Natural deduction rules"><h4 id="Natural deduction rules" class="header"><a href="#First order logic-Quantifiers, binding-Natural deduction rules">Natural deduction rules</a></h4></div> - -<table> -<tr> -<th> -Universal quantification -</th> -<th> -Existential quantification -</th> -<th> -Equality -</th> -</tr> -<tr> -<td> -<img src="img/universal-introduction.png" alt="Universal introduction" /> -</td> -<td> -<img src="img/existential-introduction.png" alt="Existential introduction" /> -</td> -<td rowspan="2"> -<img src="img/equality-rules.png" alt="Equality rules" /> -</td> -</tr> -<tr> -<td> -<img src="img/universal-elimination.png" alt="Universal elimination" /> -</td> -<td> -<img src="img/existential-elimination.png" alt="Existential elimination" /> -</td> -</tr> -</table> - - -<div id="First order logic-Relativization and sorts"><h3 id="Relativization and sorts" class="header"><a href="#First order logic-Relativization and sorts">Relativization and sorts</a></h3></div> -<p> -You can use implication to relativize quantification (put it into a specific domain). -</p> - -<p> -Universal quantification, e.g. "every prime number greater than two is odd": -</p> - -<p> -∀x (prime(x) ∧ x > 2 → odd(x)) -</p> - -<p> -Existential quantification, e.g. "some woman is strong": -</p> - -<p> -∃x (woman(x) ∧ strong(x)) -</p> - -<p> -Remember to use ∧ with ∃, and not →. -</p> - -<div id="First order logic-Models"><h3 id="Models" class="header"><a href="#First order logic-Models">Models</a></h3></div> -<p> -Let F be a set of function symbols, P a set of predicate symbols. -</p> - -<p> -Model M for (F, P) consists of: -</p> -<ul> -<li> -non-empty set A ("domain", "universe") - -<li> -interpretation operation \((\cdot)^M\) for for symbols in F, P - -</ul> - -<p> -Universe A can be any non-empty set. -</p> - -<p> -only constraint: \(F^M\) and \(P^M\) have same number of arguments as F and P. -</p> - -<div id="First order logic-Interpreting formulas without quantifiers"><h3 id="Interpreting formulas without quantifiers" class="header"><a href="#First order logic-Interpreting formulas without quantifiers">Interpreting formulas without quantifiers</a></h3></div> -<p> -Truth definition for formula Φ without quantifiers and free variables in model M by induction on the structure of Φ: -</p> -<ul> -<li> -M ⊨ ¬Φ ↔ not: M ⊨ Φ ↔ M ⊭ Φ - -<li> -M ⊨ Æ∧ Ψ ↔ M ⊨ Φ and M ⊨ Ψ - -<li> -M ⊨ Φ ∨ Ψ ↔ M ⊨ Φ or M ⊨ Ψ - -<li> -M ⊨ Φ → Ψ : if M ⊨ Φ then M ⊨ Ψ - -<li> -M ⊨ P(t₁, .., tn) ↔ (\(t_1^M,\ldots,t_n^M) \in P^M\) - -</ul> - -<p> -Interpretation of terms \(t^M\): -</p> -<ul> -<li> -if t = c for constant c, then \(t^M = c^M\) - -<li> -if \(t = f(t_1,\ldots, t_n)\), then \(t^M = f^M(t_1^M,\ldots,t_n^M)\) - -</ul> - -<div id="First order logic-Interpretation of formulas with quantifiers and free variables"><h3 id="Interpretation of formulas with quantifiers and free variables" class="header"><a href="#First order logic-Interpretation of formulas with quantifiers and free variables">Interpretation of formulas with quantifiers and free variables</a></h3></div> -<p> -to interpret free variables, you use an environment. -</p> - -<p> -an environment <code>l: var → A</code> (look up function) interprets free variables in the domain -</p> - -<div id="First order logic-Interpreting terms in model with environment"><h3 id="Interpreting terms in model with environment" class="header"><a href="#First order logic-Interpreting terms in model with environment">Interpreting terms in model with environment</a></h3></div> -<p> -terms are built from variables, constants, function symbols -</p> -<ul> -<li> -variables are interpreted according to environment - -<li> -constants are interpreted according to \((\cdot)^M\) - -<li> -function symbols are interpreted according to \((\cdot)^M\) - -</ul> - - -<p> -Truth of formula Φ in model M with universe A with respect to environment e is defined by induction on the structure of Φ. -</p> - -<p> -Interpretation \(t^{M,l}\) of term t is -</p> - -\begin{align} -t^{M, l} = \begin{cases} - l(x) &&\text{if } t = x \text{ for a variable } x \\ - c^M &&\text{if } t = c \text{ for a constant } c \\ - f^M (t_1^{M, l}, \ldots, t_n^{M, l}) &&\text{if } t = f(t_1, \ldots, t_n) - \end{cases} -\end{align} -<p> -by induction on term structure. -</p> - -<p> -M ⊨l ∀x HI ↔ for all a ∈ A it holds that \( M \models_{l [x \to a]} \phi \) -</p> - -<p> -M ⊨l ∃x Φ ↔ for some a ∈ A it holds that \( M \models_{l [x \to a]} \phi \) -</p> - -<div id="First order logic-Semantical entailment in predicate logic"><h3 id="Semantical entailment in predicate logic" class="header"><a href="#First order logic-Semantical entailment in predicate logic">Semantical entailment in predicate logic</a></h3></div> -<p> -For all models M and all environments e, -such that M ⊨l Φ₁ and ... and M ⊨l Φn hold, -it also holds that M ⊨l ψ -</p> - -<div id="First order logic-Logical equivalence"><h3 id="Logical equivalence" class="header"><a href="#First order logic-Logical equivalence">Logical equivalence</a></h3></div> -<p> -Formulas φ and ψ are logically equivalent (φ ≡ ψ) if for all models M and environments l, M ⊨l φ ↔ M ⊨l ψ -</p> - -<p> -i.e. φ and ψ are true in precisely the same models when interpreted with the same environments. -</p> - -<p> -theorem: φ ≡ ψ ↔ φ ⊨ ψ and ψ ⊨ φ -</p> - -<div id="First order logic-Satisfiability, validity, consistency"><h3 id="Satisfiability, validity, consistency" class="header"><a href="#First order logic-Satisfiability, validity, consistency">Satisfiability, validity, consistency</a></h3></div> -<p> -Let φ be a formula, and Γ be a set of formulas. -</p> - -<p> -φ is satisfiable iff there is <em>some</em> model M and <em>some</em> environment l such that M ⊨l φ -</p> - -<p> -φ is valid iff M ⊨l φ holds for <em>all</em> models M and <em>all</em> environments l in which φ can be checked. -</p> - -<p> -Γ is consistent/satisfiable iff there is <em>some</em> model M and <em>some</em> environment l such tat M ⊨l ψ for all ψ ∈ Γ -</p> - -<p> -for all formulas φ, ψ: φ ≡ ψ means that φ ↔ ψ is valid -</p> - -<div id="First order logic-Translating into predicate logic"><h3 id="Translating into predicate logic" class="header"><a href="#First order logic-Translating into predicate logic">Translating into predicate logic</a></h3></div> -<p> -Example: "Marie and Jan are clever." -</p> - -<p> -Specification and model used: -</p> - -<p> -two predicates: -</p> -<ul> -<li> -CC(x): x is clever - -<li> -LL(x): x has learned logic - -</ul> - -<p> -two constants: -</p> -<ul> -<li> -m: Marie - -<li> -j: Jan - -</ul> - -<p> -model M: -</p> -<ul> -<li> -domain A = the set of all humans - -<li> -\(C^M\) = { x ∈ A | x is clever } - -<li> -\(LL^M\) = { x ∈ A | x has learned logic } - -<li> -\(j^M \)= Jan - -<li> -\(m^M\) = Marie - -</ul> - -<p> -Then: -</p> -<ul> -<li> -"Marie and Jan are clever": C(m) ∧ C(j) - -<li> -"Not everybody is clever": ¬∀x C(x) - -<li> -"Somebody has learned logic": ∃x LL(x) - -<li> -"Not everybody has learned logic, but Marie and Jan have": ¬∀x LL(x) ∧ LL(m) ∧ LL(j) - -</ul> - -<p> -∀ and →: -</p> -<ul> -<li> -∀x(LL(x) → C(x)): "everyone who has learned logic is clever" - -<li> -not the same as ∀x LL(x) → ∀x C(x): "if everyone has learned logic, everyone is clever" - -</ul> - -<p> -∃ and ∧: -</p> -<ul> -<li> -∃x(L(x) ∧ C(x)): "some logicians are clever" - -<li> -not the same as ∃x(L(x) → C(x)): "if someone is a logician, they are clever" - -</ul> - -<p> -Formulas with free variables express properties and relations: -</p> -<ul> -<li> -no free variables: a sentence - -<li> -one free variable: a property - -<li> -two or more free variables: a relation - -</ul> - -<div id="First order logic-Rules for quantifiers and connectives"><h3 id="Rules for quantifiers and connectives" class="header"><a href="#First order logic-Rules for quantifiers and connectives">Rules for quantifiers and connectives</a></h3></div> -<p> -If you move a negation around ∀, it becomes ∃, and vice versa. -</p> - -<p> -It also holds that: -</p> -<ul> -<li> -∀x(φ ∧ ψ) ≡ ∀x φ ∧ ∀x ψ - -<ul> -<li> -BUT in general doesn't hold for ∨ - -</ul> -<li> -∃x(φ ∨ ψ) ≡ ∃x φ ∨ ∃x ψ - -<ul> -<li> -BUT in general doesn't hold for ∧ - -</ul> -</ul> - -<p> -In general, you can't move quantifiers through an implication. -</p> - -<p> -Order of <em>repeated</em> ∀ or ∃ doesn't matter. But if you have <em>both</em> ∃ and ∀, the order is important. -</p> - -<div id="First order logic-Semantics of first order logic"><h3 id="Semantics of first order logic" class="header"><a href="#First order logic-Semantics of first order logic">Semantics of first order logic</a></h3></div> -<p> -Interpretation: specifying the meaning of a predicate symbol. -</p> -<ul> -<li> -unary predicate P: set of elements of domain D for which P is true. - -<li> -constant c: an element of domain D - -<li> -function f with arity n: function mapping n elements of domain D to another element of D - -<li> -relation R with arity n: set of n tuples of elements of domain D for which R is true - -</ul> - -<p> -You can find the truth value of sentences intuitively. -</p> - -<p> -Completeness: if formula A is logical consequence of set of sentences Γ, then A is provable from Γ. -</p> - -<p> -Soundness: if A is provable from Γ then A is true in any model of Γ -</p> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/img/equality-rules.png b/content/logic-modelling-notes/first-order-logic/equality-rules.png Binary files differ. diff --git a/content/logic-modelling-notes/img/existential-elimination.png b/content/logic-modelling-notes/first-order-logic/existential-elimination.png Binary files differ. diff --git a/content/logic-modelling-notes/img/existential-introduction.png b/content/logic-modelling-notes/first-order-logic/existential-introduction.png Binary files differ. diff --git a/content/logic-modelling-notes/first-order-logic/index.md b/content/logic-modelling-notes/first-order-logic/index.md @@ -0,0 +1,188 @@ ++++ +template = 'page-math.html' +title = 'First order logic' ++++ +# First order logic +## Functions, predicates, relations +functions: take different numbers of arguments, returns a result. e.g. $mul(x,y)$, $square(x)$ + +predicates, relations: takes one or more arguments, is either true or false. e.g. $even(x)$, $divides(x,y)$ + +formulas: say things. make assertions about objects in the domain. + +## Quantifiers, binding +Quantifiers: +* ∀x: "for all x" +* ∃x: "there exists an x" + +Generally bind tightly: ∀x P ∨ Q == (∀x P) ∨ Q + +free variable: variable that's not bound + +sentence: a formula that has no free variables + +### Natural deduction rules + +<table> +<tr><td>Universal quantification</td><td>Existential quantification</td><td>Equality</td></tr> +<tr><td><img alt="Universal introduction" src="universal-introduction.png"></td><td><img alt="Existential introduction" src="existential-introduction.png"></td><td rowspan="2"><img alt="Equality rules" src="equality-rules.png"></td></tr> +<tr><td><img alt="Universal elimination" src="universal-elimination.png"></td><td><img alt="Existential elimination" src="existential-elimination.png"></td></td></tr> +</table> + + +## Relativization and sorts +You can use implication to relativize quantification (put it into a specific domain). + +Universal quantification, e.g. "every prime number greater than two is odd": + +∀x (prime(x) ∧ x > 2 → odd(x)) + +Existential quantification, e.g. "some woman is strong": + +∃x (woman(x) ∧ strong(x)) + +Remember to use ∧ with ∃, and not →. + +## Models +Let F be a set of function symbols, P a set of predicate symbols. + +Model M for (F, P) consists of: +* non-empty set A ("domain", "universe") +* interpretation operation $(\cdot)^M$ for for symbols in F, P + +Universe A can be any non-empty set. + +only constraint: $F^M$ and $P^M$ have same number of arguments as F and P. + +## Interpreting formulas without quantifiers +Truth definition for formula Φ without quantifiers and free variables in model M by induction on the structure of Φ: +* M ⊨ ¬Φ ↔ not: M ⊨ Φ ↔ M ⊭ Φ +* M ⊨ Æ∧ Ψ ↔ M ⊨ Φ and M ⊨ Ψ +* M ⊨ Φ ∨ Ψ ↔ M ⊨ Φ or M ⊨ Ψ +* M ⊨ Φ → Ψ : if M ⊨ Φ then M ⊨ Ψ +* M ⊨ P(t₁, .., tn) ↔ ($t_1^M,\ldots,t_n^M) \in P^M$ + +Interpretation of terms $t^M$: +* if t = c for constant c, then $t^M = c^M$ +* if $t = f(t_1,\ldots, t_n)$, then $t^M = f^M(t_1^M,\ldots,t_n^M)$ + +## Interpretation of formulas with quantifiers and free variables +to interpret free variables, you use an environment. + +an environment `l: var → A` (look up function) interprets free variables in the domain + +## Interpreting terms in model with environment +terms are built from variables, constants, function symbols +* variables are interpreted according to environment +* constants are interpreted according to $(\cdot)^M$ +* function symbols are interpreted according to $(\cdot)^M$ + + +Truth of formula Φ in model M with universe A with respect to environment e is defined by induction on the structure of Φ. + +Interpretation $t^{M,l}$ of term t is + +$ +\begin{aligned} +t^{M, l} = \begin{cases} + l(x) &&\text{if } t = x \text{ for a variable } x \\\\ + c^M &&\text{if } t = c \text{ for a constant } c \\\\ + f^M (t_1^{M, l}, \ldots, t_n^{M, l}) &&\text{if } t = f(t_1, \ldots, t_n) + \end{cases} +\end{aligned} +$ + +by induction on term structure. + +M ⊨l ∀x HI ↔ for all a ∈ A it holds that $ M \models_{l [x \to a]} \phi $ + +M ⊨l ∃x Φ ↔ for some a ∈ A it holds that $ M \models_{l [x \to a]} \phi $ + +## Semantical entailment in predicate logic +For all models M and all environments e, +such that M ⊨l Φ₁ and ... and M ⊨l Φn hold, +it also holds that M ⊨l ψ + +## Logical equivalence +Formulas φ and ψ are logically equivalent (φ ≡ ψ) if for all models M and environments l, M ⊨l φ ↔ M ⊨l ψ + +i.e. φ and ψ are true in precisely the same models when interpreted with the same environments. + +theorem: φ ≡ ψ ↔ φ ⊨ ψ and ψ ⊨ φ + +## Satisfiability, validity, consistency +Let φ be a formula, and Γ be a set of formulas. + +φ is satisfiable iff there is _some_ model M and _some_ environment l such that M ⊨l φ + +φ is valid iff M ⊨l φ holds for _all_ models M and _all_ environments l in which φ can be checked. + +Γ is consistent/satisfiable iff there is _some_ model M and _some_ environment l such tat M ⊨l ψ for all ψ ∈ Γ + +for all formulas φ, ψ: φ ≡ ψ means that φ ↔ ψ is valid + +## Translating into predicate logic +Example: "Marie and Jan are clever." + +Specification and model used: + +two predicates: +* CC(x): x is clever +* LL(x): x has learned logic + +two constants: +* m: Marie +* j: Jan + +model M: +* domain A = the set of all humans +* $C^M$ = { x ∈ A | x is clever } +* $LL^M$ = { x ∈ A | x has learned logic } +* $j^M $= Jan +* $m^M$ = Marie + +Then: +* "Marie and Jan are clever": C(m) ∧ C(j) +* "Not everybody is clever": ¬∀x C(x) +* "Somebody has learned logic": ∃x LL(x) +* "Not everybody has learned logic, but Marie and Jan have": ¬∀x LL(x) ∧ LL(m) ∧ LL(j) + +∀ and →: +* ∀x(LL(x) → C(x)): "everyone who has learned logic is clever" +* not the same as ∀x LL(x) → ∀x C(x): "if everyone has learned logic, everyone is clever" + +∃ and ∧: +* ∃x(L(x) ∧ C(x)): "some logicians are clever" +* not the same as ∃x(L(x) → C(x)): "if someone is a logician, they are clever" + +Formulas with free variables express properties and relations: +* no free variables: a sentence +* one free variable: a property +* two or more free variables: a relation + +## Rules for quantifiers and connectives +If you move a negation around ∀, it becomes ∃, and vice versa. + +It also holds that: +* ∀x(φ ∧ ψ) ≡ ∀x φ ∧ ∀x ψ + * BUT in general doesn't hold for ∨ +* ∃x(φ ∨ ψ) ≡ ∃x φ ∨ ∃x ψ + * BUT in general doesn't hold for ∧ + +In general, you can't move quantifiers through an implication. + +Order of _repeated_ ∀ or ∃ doesn't matter. But if you have _both_ ∃ and ∀, the order is important. + +## Semantics of first order logic +Interpretation: specifying the meaning of a predicate symbol. +* unary predicate P: set of elements of domain D for which P is true. +* constant c: an element of domain D +* function f with arity n: function mapping n elements of domain D to another element of D +* relation R with arity n: set of n tuples of elements of domain D for which R is true + +You can find the truth value of sentences intuitively. + +Completeness: if formula A is logical consequence of set of sentences Γ, then A is provable from Γ. + +Soundness: if A is provable from Γ then A is true in any model of Γ + diff --git a/content/logic-modelling-notes/img/universal-elimination.png b/content/logic-modelling-notes/first-order-logic/universal-elimination.png Binary files differ. diff --git a/content/logic-modelling-notes/img/universal-introduction.png b/content/logic-modelling-notes/first-order-logic/universal-introduction.png Binary files differ. diff --git a/content/logic-modelling-notes/incompleteness-theorem.html b/content/logic-modelling-notes/incompleteness-theorem.html @@ -1,128 +0,0 @@ -<html> -<head> - <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> - <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> - <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> - <script> - document.addEventListener('DOMContentLoaded', function() { - document.querySelectorAll('pre.code').forEach(function(item) { - hljs.highlightBlock(item) - }) - }); - </script> - <title>incompleteness-theorem</title> -</head> -<body> -<style type="text/css"> -nav a { - text-align: left; -} -nav #name { - text-align: right; - float: right; - font-style: italic; -} -</style> - <nav> - <a href="index.html">Index</a> - <span id="name">Alex Balgavy</span> - </nav> - <hr> - <div class="content"> - -<div id="Incompleteness theorem"><h2 id="Incompleteness theorem" class="header"><a href="#Incompleteness theorem">Incompleteness theorem</a></h2></div> -<p> -Consider sets of function and predicate symbols: -</p> -<ul> -<li> -F = {0, S, +, ·} - -<li> -P = {<} - -</ul> - -<p> -with as intended model number theory N: -</p> -<ul> -<li> -domain of N is the natural numbers with 0 - -<li> -\(0^\mathbb{N} = 0\) - -<li> -\(S^\mathbb{N} (n) = n + 1\) - -<li> -\(+^\mathbb{N} (n,m) = n+m\) - -<li> -\(\mathbb{N}(n,m) = n \cdot m\) - -<li> -\(<^\mathbb{N} = \{ <n,m> | n,m \in \mathbb{N} \text{ such that }n < m \}\) - -</ul> - -<p> -One would like to have complete theory (deduction system) ⊢ for N that allows to derive all formulas that are true in N. -</p> - -<p> -First incompleteness theorem: -</p> -<ul> -<li> -every axiomatizable and sound theory ⊢ of first-order logic - -<li> -for number theory with language <F,P> - -<li> -is incomplete: - -<ul> -<li> -it contains sentences Φ that are true in N, but unprovable in ⊢: N ⊨ Φ, yet ⊬ Φ. - -</ul> -</ul> - - -<p> -Second incompleteness theorem: -</p> -<ul> -<li> -for every axiomatizable theory ⊢ of first-order logic - -<li> -for number theory with language <F,P> - -<li> -that is rich enough to express its own consistency by a sentence Φ⊢ - -<li> -it holds that either: - -<ul> -<li> -⊢ ⊥ (⊢ is inconsistent) - -<li> -⊬ Φ⊢ (hence ⊢ is incomplete) - -</ul> -<li> -so first-order theories (based on predicate logic) of number theory can't prove their own consistency - -</ul> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/incompleteness-theorem.md b/content/logic-modelling-notes/incompleteness-theorem.md @@ -0,0 +1,34 @@ ++++ +template = 'page-math.html' +title = 'Incompleteness theorem' ++++ +# Incompleteness theorem +Consider sets of function and predicate symbols: +* F = {0, S, +, ·} +* P = {<} + +with as intended model number theory N: +* domain of N is the natural numbers with 0 +* $0^\mathbb{N} = 0$ +* $S^\mathbb{N} (n) = n + 1$ +* $+^\mathbb{N} (n,m) = n+m$ +* $\mathbb{N}(n,m) = n \cdot m$ +* $<^\mathbb{N} = \{ <n,m> | n,m \in \mathbb{N} \text{ such that }n < m \}$ + +One would like to have complete theory (deduction system) ⊢ for N that allows to derive all formulas that are true in N. + +First incompleteness theorem: +* every axiomatizable and sound theory ⊢ of first-order logic +* for number theory with language <F,P> +* is incomplete: + * it contains sentences Φ that are true in N, but unprovable in ⊢: N ⊨ Φ, yet ⊬ Φ. + + +Second incompleteness theorem: +* for every axiomatizable theory ⊢ of first-order logic +* for number theory with language <F,P> +* that is rich enough to express its own consistency by a sentence Φ⊢ +* it holds that either: + * ⊢ ⊥ (⊢ is inconsistent) + * ⊬ Φ⊢ (hence ⊢ is incomplete) +* so first-order theories (based on predicate logic) of number theory can't prove their own consistency diff --git a/content/logic-modelling-notes/index.html b/content/logic-modelling-notes/index.html @@ -1,210 +0,0 @@ -<html> -<head> - <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> - <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> - <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> - <script> - document.addEventListener('DOMContentLoaded', function() { - document.querySelectorAll('pre.code').forEach(function(item) { - hljs.highlightBlock(item) - }) - }); - </script> - <title>index</title> -</head> -<body> -<style type="text/css"> -nav a { - text-align: left; -} -nav #name { - text-align: right; - float: right; - font-style: italic; -} -</style> - <nav> - <a href="index.html">Index</a> - <span id="name">Alex Balgavy</span> - </nav> - <hr> - <div class="content"> - - -<div id="Logic and Modeling"><h1 id="Logic and Modeling" class="header"><a href="#Logic and Modeling">Logic and Modeling</a></h1></div> -<p> -Here's the <a href="http://avigad.github.io/logic_and_proof/propositional_logic.html">online book</a>. -</p> - -<p> -Also, <a href="../../logic-modelling.apkg">here's my Anki deck</a>. -</p> - -<p> -<a href="The one-page cheat sheet.html">The one-page cheat sheet</a>. -</p> - -<ul> -<li> -<a href="propositional-logic.html#Propositional logic">Propositional logic</a> - -<ul> -<li> -<a href="propositional-logic.html#Propositional logic-Notation review">Notation review</a> - -<li> -<a href="propositional-logic.html#Propositional logic-Rules of inference">Rules of inference</a> - -<li> -<a href="propositional-logic.html#Propositional logic-Forward and backward reasoning">Forward and backward reasoning</a> - -<li> -<a href="propositional-logic.html#Propositional logic-Proof by contradiction">Proof by contradiction</a> - -<li> -<a href="propositional-logic.html#Propositional logic-Vocab definitions">Vocab definitions</a> - -<li> -<a href="propositional-logic.html#Propositional logic-Classical reasoning">Classical reasoning</a> - -<li> -<a href="propositional-logic.html#Propositional logic-Syntax vs Semantics">Syntax vs Semantics</a> - -<li> -<a href="propositional-logic.html#Propositional logic-Soundness and completeness">Soundness and completeness</a> - -</ul> -<li> -<a href="first-order-logic.html#First order logic">First order logic</a> - -<ul> -<li> -<a href="first-order-logic.html#First order logic-Functions, predicates, relations">Functions, predicates, relations</a> - -<li> -<a href="first-order-logic.html#First order logic-Quantifiers, binding">Quantifiers, binding</a> - -<ul> -<li> -<a href="first-order-logic.html#First order logic-Quantifiers, binding-Natural deduction rules">Natural deduction rules</a> - -</ul> -<li> -<a href="first-order-logic.html#First order logic-Relativization and sorts">Relativization and sorts</a> - -<li> -<a href="first-order-logic.html#First order logic-Models">Models</a> - -<li> -<a href="first-order-logic.html#First order logic-Interpreting formulas without quantifiers">Interpreting formulas without quantifiers</a> - -<li> -<a href="first-order-logic.html#First order logic-Interpretation of formulas with quantifiers and free variables">Interpretation of formulas with quantifiers and free variables</a> - -<li> -<a href="first-order-logic.html#First order logic-Interpreting terms in model with environment">Interpreting terms in model with environment</a> - -<li> -<a href="first-order-logic.html#First order logic-Semantical entailment in predicate logic">Semantical entailment in predicate logic</a> - -<li> -<a href="first-order-logic.html#First order logic-Logical equivalence">Logical equivalence</a> - -<li> -<a href="first-order-logic.html#First order logic-Satisfiability, validity, consistency">Satisfiability, validity, consistency</a> - -<li> -<a href="first-order-logic.html#First order logic-Translating into predicate logic">Translating into predicate logic</a> - -<li> -<a href="first-order-logic.html#First order logic-Rules for quantifiers and connectives">Rules for quantifiers and connectives</a> - -<li> -<a href="first-order-logic.html#First order logic-Semantics of first order logic">Semantics of first order logic</a> - -</ul> -<li> -<a href="sets.html#Sets">Sets</a> - -<ul> -<li> -<a href="sets.html#Sets-Relations">Relations</a> - -<ul> -<li> -<a href="sets.html#Sets-Relations-Order types">Order types</a> - -</ul> -<li> -<a href="sets.html#Sets-Natural numbers & induction">Natural numbers & induction</a> - -<li> -<a href="sets.html#Sets-Recursive definitions">Recursive definitions</a> - -</ul> -<li> -<a href="modal-logic.html#Modal logic">Modal logic</a> - -<ul> -<li> -<a href="modal-logic.html#Modal logic-Truth in worlds">Truth in worlds</a> - -<li> -<a href="modal-logic.html#Modal logic-Truth in Kripke models">Truth in Kripke models</a> - -<li> -<a href="modal-logic.html#Modal logic-Semantic implication/entailment">Semantic implication/entailment</a> - -<li> -<a href="modal-logic.html#Modal logic-Frames">Frames</a> - -</ul> -<li> -<a href="meta-theorems-of-predicate-logic.html#Meta-Theorems of Predicate Logic">Meta-Theorems of Predicate Logic</a> - -<li> -<a href="definability-and-undefinability-results.html#Definability and Undefinability results">Definability and Undefinability results</a> - -<ul> -<li> -<a href="definability-and-undefinability-results.html#Definability and Undefinability results-for model cardinality">for model cardinality</a> - -<li> -<a href="definability-and-undefinability-results.html#Definability and Undefinability results-for reachability">for reachability</a> - -<li> -<a href="definability-and-undefinability-results.html#Definability and Undefinability results-General overview">General overview</a> - -</ul> -<li> -<a href="decidability-and-undecidability.html#Decidability and Undecidability">Decidability and Undecidability</a> - -<ul> -<li> -<a href="decidability-and-undecidability.html#Decidability and Undecidability-Decision problems">Decision problems</a> - -<ul> -<li> -<a href="decidability-and-undecidability.html#Decidability and Undecidability-Decision problems-Termination problem">Termination problem</a> - -<li> -<a href="decidability-and-undecidability.html#Decidability and Undecidability-Decision problems-Post's Correspondence Problem">Post's Correspondence Problem</a> - -</ul> -<li> -<a href="decidability-and-undecidability.html#Decidability and Undecidability-Undecidability of Validity and Provability">Undecidability of Validity and Provability</a> - -<li> -<a href="decidability-and-undecidability.html#Decidability and Undecidability-Undecidability of Satisfiability">Undecidability of Satisfiability</a> - -</ul> -<li> -<a href="incompleteness-theorem.html#Incompleteness theorem">Incompleteness theorem</a> - -</ul> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/meta-theorems-of-predicate-logic.html b/content/logic-modelling-notes/meta-theorems-of-predicate-logic.html @@ -1,143 +0,0 @@ -<html> -<head> - <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> - <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> - <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> - <script> - document.addEventListener('DOMContentLoaded', function() { - document.querySelectorAll('pre.code').forEach(function(item) { - hljs.highlightBlock(item) - }) - }); - </script> - <title>meta-theorems-of-predicate-logic</title> -</head> -<body> -<style type="text/css"> -nav a { - text-align: left; -} -nav #name { - text-align: right; - float: right; - font-style: italic; -} -</style> - <nav> - <a href="index.html">Index</a> - <span id="name">Alex Balgavy</span> - </nav> - <hr> - <div class="content"> - -<div id="Meta-Theorems of Predicate Logic"><h2 id="Meta-Theorems of Predicate Logic" class="header"><a href="#Meta-Theorems of Predicate Logic">Meta-Theorems of Predicate Logic</a></h2></div> -<p> -Entailment syntactically (⊢) and semantically (⊨) -</p> -<ul> -<li> -Γ ⊢ ψ: there is natural deduction derivation of ψ that only uses premises in Γ - -<li> -Γ ⊨ ψ: for all M and l, if M ⊨l Φ for every Φ ∈ Γ, then M ⊨ ψ - -</ul> - -<p> -Soundness and completeness: -</p> -<ul> -<li> -Γ ⊢ Φ ⇔ Γ ⊨ Φ - -<li> -for all formulas Φ, every set Γ of formulas - -<li> -soundness (correctness): left-to-right (⇒) - -<li> -completeness: right-to-left (⇐) - -</ul> - -<p> -soundness theorem: -</p> -<ul> -<li> -Γ ⊢ Φ ⇒ Γ ⊨ Φ - -<li> -if there is natural deduction derivation of Φ from Γ, then there's no model M in which all formulas of Γ are true, but Φ is false - -<li> -"correct" means not possible to derive false conclusion Φ from true premises Γ - -<li> -prove by induction on derivation lengths - -</ul> - -<p> -completeness theorem: -</p> -<ul> -<li> -Γ ⊨ Φ ⇒ Γ ⊢ Φ - -<li> -derivations are strong enough to derive all valid semantic entailment statements - -<li> -"complete" means more derivation rules are not necessary - -<li> -proof is non-trivial - -</ul> - -<p> -consistency and syntactical consistency -</p> -<ul> -<li> -Γ is consistent ⇔ Γ is syntactically consistent - -<li> -Γ has a model ⇔ there is no derivation of ⊥ from Γ - -</ul> - -<p> -semantical consistency: -</p> -<ul> -<li> -set Γ of formulas is consistent if there is model M and environment l such that M ⊨ Φ for all Φ ∈ Γ - -</ul> - -<p> -syntactical consistency: -</p> -<ul> -<li> -set Γ of formulas is syntactically consistent if Γ ⊬ ⊥ - -</ul> - -<p> -compactness theorem: -</p> -<ul> -<li> -Γ is consistent ⇔ every finite subset Γ₀ ⊆ Γ si consistent - -</ul> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/meta-theorems-of-predicate-logic.md b/content/logic-modelling-notes/meta-theorems-of-predicate-logic.md @@ -0,0 +1,40 @@ ++++ +template = 'page-math.html' +title = 'Meta-Theorems of Predicate Logic' ++++ +# Meta-Theorems of Predicate Logic +Entailment syntactically (⊢) and semantically (⊨) +* Γ ⊢ ψ: there is natural deduction derivation of ψ that only uses premises in Γ +* Γ ⊨ ψ: for all M and l, if M ⊨l Φ for every Φ ∈ Γ, then M ⊨ ψ + +Soundness and completeness: +* Γ ⊢ Φ ⇔ Γ ⊨ Φ +* for all formulas Φ, every set Γ of formulas +* soundness (correctness): left-to-right (⇒) +* completeness: right-to-left (⇐) + +soundness theorem: +* Γ ⊢ Φ ⇒ Γ ⊨ Φ +* if there is natural deduction derivation of Φ from Γ, then there's no model M in which all formulas of Γ are true, but Φ is false +* "correct" means not possible to derive false conclusion Φ from true premises Γ +* prove by induction on derivation lengths + +completeness theorem: +* Γ ⊨ Φ ⇒ Γ ⊢ Φ +* derivations are strong enough to derive all valid semantic entailment statements +* "complete" means more derivation rules are not necessary +* proof is non-trivial + +consistency and syntactical consistency +* Γ is consistent ⇔ Γ is syntactically consistent +* Γ has a model ⇔ there is no derivation of ⊥ from Γ + +semantical consistency: +* set Γ of formulas is consistent if there is model M and environment l such that M ⊨ Φ for all Φ ∈ Γ + +syntactical consistency: +* set Γ of formulas is syntactically consistent if Γ ⊬ ⊥ + +compactness theorem: +* Γ is consistent ⇔ every finite subset Γ₀ ⊆ Γ si consistent + diff --git a/content/logic-modelling-notes/modal-logic.html b/content/logic-modelling-notes/modal-logic.html @@ -1,174 +0,0 @@ -<html> -<head> - <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> - <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> - <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> - <script> - document.addEventListener('DOMContentLoaded', function() { - document.querySelectorAll('pre.code').forEach(function(item) { - hljs.highlightBlock(item) - }) - }); - </script> - <title>modal-logic</title> -</head> -<body> -<style type="text/css"> -nav a { - text-align: left; -} -nav #name { - text-align: right; - float: right; - font-style: italic; -} -</style> - <nav> - <a href="index.html">Index</a> - <span id="name">Alex Balgavy</span> - </nav> - <hr> - <div class="content"> - -<div id="Modal logic"><h2 id="Modal logic" class="header"><a href="#Modal logic">Modal logic</a></h2></div> -<p> -modal logic allows reasoning about dynamics -- futures, knowledge, beliefs, etc. -</p> - -<p> -modalities (unary connectives): -</p> -<ul> -<li> -□ (box): sure, always, has to be, knows, guaranteed (kinda like ∀) - -<li> -◇ (diamond): possibly, sometimes, maybe, believes is possible, possible result (kinda like ∃) - -</ul> - -<p> -Kripke model <code>M = (W, R, L)</code> consists of: -</p> -<ul> -<li> -W worlds - -<li> -R accessibility relation - -<li> -L labeling function: which propositional letters are true in which world (<code>w ⊩ p ↔ p ∈ L(w)</code>) - -</ul> - -<p> -Kripke models define truth <em>per world</em>. -</p> - -<p> -<img src="img/kripke-model-and-graph.png" alt="Kripke model and graph" /> -</p> - -<div id="Modal logic-Truth in worlds"><h3 id="Truth in worlds" class="header"><a href="#Modal logic-Truth in worlds">Truth in worlds</a></h3></div> -<p> -<code>M, w ⊩ Φ</code> means formula Φ is true in world w of Kripke model M. -</p> - -<p> -◇ Φ is true in world w if there exists a world w' such that R(w, w') and Φ is true in w'. -</p> - -<p> -□ Φ is true in world w if Φ is true in all worlds w' with R(w, w'). special case when world has no outgoing edge, ◇ Φ never holds and □ Φ always holds. -</p> - -<div id="Modal logic-Truth in Kripke models"><h3 id="Truth in Kripke models" class="header"><a href="#Modal logic-Truth in Kripke models">Truth in Kripke models</a></h3></div> -<p> -Φ is true in Kripke model <code>M = (W, R, L)</code> (i.e. M ⊨ Φ), iff x ⊩ Φ for every world x ∈ W. -</p> - -<p> -all propositional tautologies also hold in modal logic. -</p> - -<div id="Modal logic-Semantic implication/entailment"><h3 id="Semantic implication/entailment" class="header"><a href="#Modal logic-Semantic implication/entailment">Semantic implication/entailment</a></h3></div> -<p> -M,w ⊨ ψ in every world w in every Kripke model where M,w ⊨ Φ₁, ..., M,w ⊨ Φn. -</p> - -<p> -modal validity: ⊨ ψ if in every world w in ever Kripke model M holds M,w ⊨ ψ. -</p> - -<p> -modal logical equivalence: <code>Φ ≡ ψ</code> if <code>M,w ⊨ Φ ↔ M,w ⊨ ψ</code>. in other words, Φ ≡ ψ ↔ Φ ⊨ ψ and ψ ⊨ Φ. -</p> - -<div id="Modal logic-Frames"><h3 id="Frames" class="header"><a href="#Modal logic-Frames">Frames</a></h3></div> -<p> -frame: Kripke model without labeling. <code>F = (W,R)</code>, W worlds, R accessibility relation -</p> - -<p> -Φ is valid in frame F (i.e. F ⊨ Φ) if for <em>every</em> labeling L, Kripke model M = (W,R,L) makes Φ true. -</p> - -<p> -Correspondence of formulas and frame properties -</p> -<ul> -<li> -reflexive: - -<ul> -<li> -F ⊨ □ p → p - -<li> -F ⊨ p → ◇ p - -</ul> -<li> -symmetric: - -<ul> -<li> -F ⊨ q → □ ◇ q - -<li> -F ⊨ ◇ □ p → p - -</ul> -<li> -transitive: - -<ul> -<li> -F ⊨ □ p → □ □ p - -<li> -F ⊨ ◇ ◇ p → ◇ p - -</ul> -<li> -serial: - -<ul> -<li> -F ⊨ ◇ T - -<li> -F ⊨ □ p → ◇ p - -</ul> -<li> -functional: □ p ↔ ◇ p - -</ul> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/modal-logic/index.md b/content/logic-modelling-notes/modal-logic/index.md @@ -0,0 +1,59 @@ ++++ +template = 'page-math.html' +title = 'Modal logic' ++++ +# Modal logic +modal logic allows reasoning about dynamics -- futures, knowledge, beliefs, etc. + +modalities (unary connectives): +* □ (box): sure, always, has to be, knows, guaranteed (kinda like ∀) +* ◇ (diamond): possibly, sometimes, maybe, believes is possible, possible result (kinda like ∃) + +Kripke model `M = (W, R, L)` consists of: +* W worlds +* R accessibility relation +* L labeling function: which propositional letters are true in which world (`w ⊩ p ↔ p ∈ L(w)`) + +Kripke models define truth _per world_. + + + +## Truth in worlds +`M, w ⊩ Φ` means formula Φ is true in world w of Kripke model M. + +◇ Φ is true in world w if there exists a world w' such that R(w, w') and Φ is true in w'. + +□ Φ is true in world w if Φ is true in all worlds w' with R(w, w'). special case when world has no outgoing edge, ◇ Φ never holds and □ Φ always holds. + +## Truth in Kripke models +Φ is true in Kripke model `M = (W, R, L)` (i.e. M ⊨ Φ), iff x ⊩ Φ for every world x ∈ W. + +all propositional tautologies also hold in modal logic. + +## Semantic implication/entailment +M,w ⊨ ψ in every world w in every Kripke model where M,w ⊨ Φ₁, ..., M,w ⊨ Φn. + +modal validity: ⊨ ψ if in every world w in ever Kripke model M holds M,w ⊨ ψ. + +modal logical equivalence: `Φ ≡ ψ` if `M,w ⊨ Φ ↔ M,w ⊨ ψ`. in other words, Φ ≡ ψ ↔ Φ ⊨ ψ and ψ ⊨ Φ. + +## Frames +frame: Kripke model without labeling. `F = (W,R)`, W worlds, R accessibility relation + +Φ is valid in frame F (i.e. F ⊨ Φ) if for _every_ labeling L, Kripke model M = (W,R,L) makes Φ true. + +Correspondence of formulas and frame properties +* reflexive: + * F ⊨ □ p → p + * F ⊨ p → ◇ p +* symmetric: + * F ⊨ q → □ ◇ q + * F ⊨ ◇ □ p → p +* transitive: + * F ⊨ □ p → □ □ p + * F ⊨ ◇ ◇ p → ◇ p +* serial: + * F ⊨ ◇ T + * F ⊨ □ p → ◇ p +* functional: □ p ↔ ◇ p + diff --git a/content/logic-modelling-notes/img/kripke-model-and-graph.png b/content/logic-modelling-notes/modal-logic/kripke-model-and-graph.png Binary files differ. diff --git a/content/logic-modelling-notes/propositional-logic.html b/content/logic-modelling-notes/propositional-logic.html @@ -1,276 +0,0 @@ -<html> -<head> - <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> - <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> - <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> - <script> - document.addEventListener('DOMContentLoaded', function() { - document.querySelectorAll('pre.code').forEach(function(item) { - hljs.highlightBlock(item) - }) - }); - </script> - <title>propositional-logic</title> -</head> -<body> -<style type="text/css"> -nav a { - text-align: left; -} -nav #name { - text-align: right; - float: right; - font-style: italic; -} -</style> - <nav> - <a href="index.html">Index</a> - <span id="name">Alex Balgavy</span> - </nav> - <hr> - <div class="content"> - -<div id="Propositional logic"><h2 id="Propositional logic" class="header"><a href="#Propositional logic">Propositional logic</a></h2></div> -<div id="Propositional logic-Notation review"><h3 id="Notation review" class="header"><a href="#Propositional logic-Notation review">Notation review</a></h3></div> -<ul> -<li> -<code>A, B, C</code> -- propositions - -<li> -<code>A ∧ B</code> -- conjunction ("and") - -<li> -<code>A ∨ B</code> -- disjunction ("or") - -<li> -<code>A → B</code> -- implication ("if A then B") - -<li> -<code>A ↔ B</code> -- bi-implication ("A iff B") - -<li> -<code>¬ A</code> -- negation ("not A") - -<li> -<code>⊥</code> -- false, falsum, nonsense, bullshit, the middle finger - -</ul> - -<div id="Propositional logic-Rules of inference"><h3 id="Rules of inference" class="header"><a href="#Propositional logic-Rules of inference">Rules of inference</a></h3></div> -<p> -"C is a logical consequence of A and B": -</p> - -<p> -<img src="img/logical-consequence.png" alt="Logical consequence" /> -</p> - - -<table> -<tr> -<th> -Implication -</th> -<th> -Conjunction -</th> -<th> -Negation -</th> -<th> -Disjunction -</th> -<th> -Bi-implication ("if and only if") -</th> -</tr> -<tr> -<td> -<img src="img/implication-elimination.png" alt="Implication elimination" /> -</td> -<td> -<img src="img/conjunction-introduction.png" alt="Conjunction introduction" /> -</td> -<td> -<img src="img/negation-hypothetical-reasoning.png" alt="Negation hypothetical reasoning" /> -</td> -<td> -<img src="img/disjunction-introduction.png" alt="Disjunction introduction" /> -</td> -<td> -<img src="img/bi-implication-introduction.png" alt="Bi-implication introduction" /> -</td> -</tr> -<tr> -<td> -<img src="img/hypothesis.png" alt="Hypothesis" /> -</td> -<td> -<img src="img/and-elimination.png" alt="And elimination" /> -</td> -<td> -<img src="img/negation-elimination.png" alt="Negation elimination" /> -</td> -<td> -<img src="img/disjunction-elimination.png" alt="Disjunction elimination" /> -</td> -<td> -<img src="img/bi-implication-elimination.png" alt="Bi-implication elimination" /> -</td> -</tr> -</table> - -<p> -Truth and falsity: from false, you can conclude anything, and from nothing, you can conclude true. -</p> - -<p> -<img src="img/falsum-elimination.png" alt="Falsum elimination" />, <img src="img/truth-introduction.png" alt="Truth introduction" /> -</p> - -<p> -You can also derive this conjunction rule: -</p> - -<p> -<img src="img/conjunction-negation-rule.png" alt="Conjunction negation rule" /> -</p> - -<div id="Propositional logic-Forward and backward reasoning"><h3 id="Forward and backward reasoning" class="header"><a href="#Propositional logic-Forward and backward reasoning">Forward and backward reasoning</a></h3></div> -<p> -Backward reasoning: looking at the goal and seeing what rules need to be applied ("bottom-up") -</p> - -<p> -Forward reasoning: starting at some hypotheses/assumptions -</p> - -<p> -The general heuristic is to always work backwards, as much as possible. Only once you get stuck should you work from your assumptions or hypotheses. -</p> - -<p> -If all else fails, try proof by contradiction. -</p> - -<div id="Propositional logic-Proof by contradiction"><h3 id="Proof by contradiction" class="header"><a href="#Propositional logic-Proof by contradiction">Proof by contradiction</a></h3></div> -<p> -Suppose a negation of a formula is true, prove that it's impossible, thereby proving the original formula. -</p> - -<p> -<img src="img/proof-by-contradiction.png" alt="Proof by contradiction" /> -</p> - -<p> -RAA stands for <em>"reductio ad absurdum"</em> -</p> - -<div id="Propositional logic-Vocab definitions"><h3 id="Vocab definitions" class="header"><a href="#Propositional logic-Vocab definitions">Vocab definitions</a></h3></div> -<ul> -<li> -derivable: a formula φ is "derivable" if we can prove φ with no global hypotheses (bottom line is φ, everything is closed). Then we write ⊢ φ. - -<li> -φ is derivable from hypotheses ψ₁..ψn if we can compute φ assuming ψ₁..ψn - -<li> -formulas φ and ψ are logically equivalent if ⊢ φ ↔ ψ - -</ul> - -<div id="Propositional logic-Classical reasoning"><h3 id="Classical reasoning" class="header"><a href="#Propositional logic-Classical reasoning">Classical reasoning</a></h3></div> -<p> -Principles: -</p> -<ul> -<li> -Proof by contradiction: assume the contradiction, and show false, thereby proving the original. - -<li> -Double negation elimination: ¬ ¬ A ↔ A. - -<li> -Contrapositive: if A → B, then ¬ B → ¬ A - -</ul> - -<p> -A general heuristic: -</p> -<ol> -<li> -Work backward from the conclusion, using introduction rules. - -<li> -When you run out of stuff to do, work forward with elimination rules. - -<li> -If you get stuck, - -</ol> -<blockquote> -<img src="img/go-go-proof-by-contradiction.jpg" alt="Proof by contradiction meme" style="width:20%" /> -</blockquote> -<blockquote> -(meme credit goes to Geo) -</blockquote> - -<div id="Propositional logic-Syntax vs Semantics"><h3 id="Syntax vs Semantics" class="header"><a href="#Propositional logic-Syntax vs Semantics">Syntax vs Semantics</a></h3></div> -<p> -Syntax: -</p> -<ul> -<li> -derivation, proofs - -<li> -Γ ⊢ A ("A is derivable from hypotheses in Γ") - -</ul> - -<p> -Semantics: -</p> -<ul> -<li> -truth and falsity - -<li> -truth assignment says which propositional letters are true - -<li> -valuation says which formulas are true - -</ul> - -<div id="Propositional logic-Soundness and completeness"><h3 id="Soundness and completeness" class="header"><a href="#Propositional logic-Soundness and completeness">Soundness and completeness</a></h3></div> -<p> -provable: if there is a formal proof of a formula (syntactic) -</p> - -<p> -tautology/valid: if true under any truth assignment (semantic) -</p> - -<p> -soundness: if a formula is provable, it is valid (if ⊢ A, then ⊨ A) -</p> - -<p> -completeness: if a formula is valid, it is provable (if ⊨ A, then ⊢ A) -</p> - -<p> -Proving soundness is easier than proving completeness. -</p> - -<p> -A is a logical consequence of Γ if, given any truth assignment that makes every formula in Γ true, A is true. -</p> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/img/and-elimination.png b/content/logic-modelling-notes/propositional-logic/and-elimination.png Binary files differ. diff --git a/content/logic-modelling-notes/img/bi-implication-elimination.png b/content/logic-modelling-notes/propositional-logic/bi-implication-elimination.png Binary files differ. diff --git a/content/logic-modelling-notes/img/bi-implication-introduction.png b/content/logic-modelling-notes/propositional-logic/bi-implication-introduction.png Binary files differ. diff --git a/content/logic-modelling-notes/img/conjunction-introduction.png b/content/logic-modelling-notes/propositional-logic/conjunction-introduction.png Binary files differ. diff --git a/content/logic-modelling-notes/img/conjunction-negation-rule.png b/content/logic-modelling-notes/propositional-logic/conjunction-negation-rule.png Binary files differ. diff --git a/content/logic-modelling-notes/img/disjunction-elimination.png b/content/logic-modelling-notes/propositional-logic/disjunction-elimination.png Binary files differ. diff --git a/content/logic-modelling-notes/img/disjunction-introduction.png b/content/logic-modelling-notes/propositional-logic/disjunction-introduction.png Binary files differ. diff --git a/content/logic-modelling-notes/img/falsum-elimination.png b/content/logic-modelling-notes/propositional-logic/falsum-elimination.png Binary files differ. diff --git a/content/logic-modelling-notes/img/go-go-proof-by-contradiction.jpg b/content/logic-modelling-notes/propositional-logic/go-go-proof-by-contradiction.jpg Binary files differ. diff --git a/content/logic-modelling-notes/img/hypothesis.png b/content/logic-modelling-notes/propositional-logic/hypothesis.png Binary files differ. diff --git a/content/logic-modelling-notes/img/implication-elimination.png b/content/logic-modelling-notes/propositional-logic/implication-elimination.png Binary files differ. diff --git a/content/logic-modelling-notes/propositional-logic/index.md b/content/logic-modelling-notes/propositional-logic/index.md @@ -0,0 +1,93 @@ ++++ +template = 'page-math.html' +title = 'Propositional logic' ++++ +# Propositional logic +## Notation review +* `A, B, C` -- propositions +* `A ∧ B` -- conjunction ("and") +* `A ∨ B` -- disjunction ("or") +* `A → B` -- implication ("if A then B") +* `A ↔ B` -- bi-implication ("A iff B") +* `¬ A` -- negation ("not A") +* `⊥` -- false, falsum, nonsense, bullshit, the middle finger + +## Rules of inference +"C is a logical consequence of A and B": + + + + +<table> +<tr><th>Implication</th><th>Conjunction</th><th>Negation</th><th>Disjunction</th><th>Bi-implication ("if and only if")</th></tr> +<tr><td><img alt="Hypothesis" src="hypothesis.png"></td><td><img alt="Conjunction introduction" src="conjunction-introduction.png"></td> <td><img alt="Negation hypothetical reasoning" src="negation-hypothetical-reasoning.png"></td><td><img alt="Disjunction introduction" src="disjunction-introduction.png"></td><td><img alt="Bi-implication introduction" src="bi-implication-introduction.png"></td></tr> +<tr><td><img alt="Implication elimination" src="implication-elimination.png"></td><td><img alt="And elimination" src="and-elimination.png"></td><td><img alt="Negation elimination" src="negation-elimination.png"></td><td><img alt="Disjunction elimination" src="disjunction-elimination.png"></td><td><img alt="Bi-implication elimination" src="bi-implication-elimination.png"></td></tr> +</table> + +Truth and falsity: from false, you can conclude anything, and from nothing, you can conclude true. + +,  + +You can also derive this conjunction rule: + + + +## Forward and backward reasoning +Backward reasoning: looking at the goal and seeing what rules need to be applied ("bottom-up") + +Forward reasoning: starting at some hypotheses/assumptions + +The general heuristic is to always work backwards, as much as possible. Only once you get stuck should you work from your assumptions or hypotheses. + +If all else fails, try proof by contradiction. + +## Proof by contradiction +Suppose a negation of a formula is true, prove that it's impossible, thereby proving the original formula. + + + +RAA stands for _"reductio ad absurdum"_ + +## Vocab definitions +* derivable: a formula φ is "derivable" if we can prove φ with no global hypotheses (bottom line is φ, everything is closed). Then we write ⊢ φ. +* φ is derivable from hypotheses ψ₁..ψn if we can compute φ assuming ψ₁..ψn +* formulas φ and ψ are logically equivalent if ⊢ φ ↔ ψ + +## Classical reasoning +Principles: +* Proof by contradiction: assume the contradiction, and show false, thereby proving the original. +* Double negation elimination: ¬ ¬ A ↔ A. +* Contrapositive: if A → B, then ¬ B → ¬ A + +A general heuristic: +1. Work backward from the conclusion, using introduction rules. +2. When you run out of stuff to do, work forward with elimination rules. +3. If you get stuck, + + + +(meme credit goes to Geo) + +## Syntax vs Semantics +Syntax: +- derivation, proofs +- Γ ⊢ A ("A is derivable from hypotheses in Γ") + +Semantics: +- truth and falsity +- truth assignment says which propositional letters are true +- valuation says which formulas are true + +## Soundness and completeness +provable: if there is a formal proof of a formula (syntactic) + +tautology/valid: if true under any truth assignment (semantic) + +soundness: if a formula is provable, it is valid (if ⊢ A, then ⊨ A) + +completeness: if a formula is valid, it is provable (if ⊨ A, then ⊢ A) + +Proving soundness is easier than proving completeness. + +A is a logical consequence of Γ if, given any truth assignment that makes every formula in Γ true, A is true. + diff --git a/content/logic-modelling-notes/img/logical-consequence.png b/content/logic-modelling-notes/propositional-logic/logical-consequence.png Binary files differ. diff --git a/content/logic-modelling-notes/img/negation-elimination.png b/content/logic-modelling-notes/propositional-logic/negation-elimination.png Binary files differ. diff --git a/content/logic-modelling-notes/img/negation-hypothetical-reasoning.png b/content/logic-modelling-notes/propositional-logic/negation-hypothetical-reasoning.png Binary files differ. diff --git a/content/logic-modelling-notes/img/proof-by-contradiction.png b/content/logic-modelling-notes/propositional-logic/proof-by-contradiction.png Binary files differ. diff --git a/content/logic-modelling-notes/img/truth-introduction.png b/content/logic-modelling-notes/propositional-logic/truth-introduction.png Binary files differ. diff --git a/content/logic-modelling-notes/sets.html b/content/logic-modelling-notes/sets.html @@ -1,189 +0,0 @@ -<html> -<head> - <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> - <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> - <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> - <link rel="Stylesheet" type="text/css" href="style.css" /> - <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> - <script> - document.addEventListener('DOMContentLoaded', function() { - document.querySelectorAll('pre.code').forEach(function(item) { - hljs.highlightBlock(item) - }) - }); - </script> - <title>sets</title> -</head> -<body> -<style type="text/css"> -nav a { - text-align: left; -} -nav #name { - text-align: right; - float: right; - font-style: italic; -} -</style> - <nav> - <a href="index.html">Index</a> - <span id="name">Alex Balgavy</span> - </nav> - <hr> - <div class="content"> - -<div id="Sets"><h2 id="Sets" class="header"><a href="#Sets">Sets</a></h2></div> -<p> -Recap from logic and sets: -</p> -<ul> -<li> -empty set Ø = {x | false} - -<li> -universal set U = {x | true} - -<li> -union A ∪ B = {x | x ∈ A or x ∈ B} - -<li> -intersection A ∩ B = {x | x ∈ A and x ∈ B} - -<li> -complement Ā = {x | x ∉ A} - -<li> -difference A \ B = {x | x ∈ A and x ∉ B} - -</ul> - -<p> -Theorems: -</p> -<ul> -<li> -A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) - -<li> -(A \ B) \ C = A \ (B ∪ C) - -</ul> - -<div id="Sets-Relations"><h3 id="Relations" class="header"><a href="#Sets-Relations">Relations</a></h3></div> -<p> -definitions of properties: -</p> -<ul> -<li> -reflexive: ∀x R(x,x) - -<li> -symmetric: ∀x ∀y (R(x,y) → R(y,x)) - -<li> -transitive: ∀x ∀y ∀z ((R(x,y) ∧ R(y,z)) → R(x,z)) - -<li> -serial: ∀x ∃y R(x,y) - -<li> -functional: ∀x ∃y (R(x,y) ∧ ∀z (R(x,z) → z=y)) - -</ul> - -<div id="Sets-Relations-Order types"><h4 id="Order types" class="header"><a href="#Sets-Relations-Order types">Order types</a></h4></div> -<p> -partial order: -</p> -<ul> -<li> -reflexive - -<li> -transitive - -<li> -antisymmetric - -</ul> - -<p> -total order: -</p> -<ul> -<li> -partial order - -<li> -∀ a,b (R(a,b) ∨ R(b,a)) - -</ul> - -<p> -strict partial order: partial order but irreflexive -</p> - -<p> -strict total order: -</p> -<ul> -<li> -strict partial order - -<li> -∀ a,b (R(a,b) ∨ (a=b) ∨ R(b,a)) - -</ul> - -<p> -equivalence relation: -</p> -<ul> -<li> -reflexive (∀a, a ≡ A) - -<li> -symmetric - -<li> -transitive - -</ul> - -<div id="Sets-Natural numbers & induction"><h3 id="Natural numbers & induction" class="header"><a href="#Sets-Natural numbers & induction">Natural numbers & induction</a></h3></div> -<p> -Set of natural numbers is N ∈ (0,∞) -</p> - -<p> -Principle of induction: let P be a property of natural numbers. Suppose P holds for zero, and whenever P holds for a natural number n, then it holds for its successor n+1. Then P holds for every natural number. -</p> - -<p> -As a natural deduction rule: -</p> - -<p> -<img src="img/induction-natural-deduction-rule.png" alt="Induction natural deduction rule" /> -</p> - -<div id="Sets-Recursive definitions"><h3 id="Recursive definitions" class="header"><a href="#Sets-Recursive definitions">Recursive definitions</a></h3></div> -<p> -Let A be any set, suppose a is in A, and g: N × A → A. Then there is a unique function f satisfying: -</p> -<ul> -<li> -f(0) = a - -<li> -f(n+1) = g(n, f(n)) - -</ul> - -<p> -Typically to prove something about a recursively defined function is to use induction. -</p> - - </div> -</body> -</html> diff --git a/content/logic-modelling-notes/sets/index.md b/content/logic-modelling-notes/sets/index.md @@ -0,0 +1,62 @@ ++++ +template = 'page-math.html' +title = 'Sets' ++++ +# Sets +Recap from logic and sets: +* empty set Ø = {x | false} +* universal set U = {x | true} +* union A ∪ B = {x | x ∈ A or x ∈ B} +* intersection A ∩ B = {x | x ∈ A and x ∈ B} +* complement Ā = {x | x ∉ A} +* difference A \ B = {x | x ∈ A and x ∉ B} + +Theorems: +* A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) +* (A \ B) \ C = A \ (B ∪ C) + +## Relations +definitions of properties: +* reflexive: ∀x R(x,x) +* symmetric: ∀x ∀y (R(x,y) → R(y,x)) +* transitive: ∀x ∀y ∀z ((R(x,y) ∧ R(y,z)) → R(x,z)) +* serial: ∀x ∃y R(x,y) +* functional: ∀x ∃y (R(x,y) ∧ ∀z (R(x,z) → z=y)) + +### Order types +partial order: +* reflexive +* transitive +* antisymmetric + +total order: +* partial order +* ∀ a,b (R(a,b) ∨ R(b,a)) + +strict partial order: partial order but irreflexive + +strict total order: +* strict partial order +* ∀ a,b (R(a,b) ∨ (a=b) ∨ R(b,a)) + +equivalence relation: +* reflexive (∀a, a ≡ A) +* symmetric +* transitive + +## Natural numbers & induction +Set of natural numbers is N ∈ (0,∞) + +Principle of induction: let P be a property of natural numbers. Suppose P holds for zero, and whenever P holds for a natural number n, then it holds for its successor n+1. Then P holds for every natural number. + +As a natural deduction rule: + + + +## Recursive definitions +Let A be any set, suppose a is in A, and g: N × A → A. Then there is a unique function f satisfying: +* f(0) = a +* f(n+1) = g(n, f(n)) + +Typically to prove something about a recursively defined function is to use induction. + diff --git a/content/logic-modelling-notes/img/induction-natural-deduction-rule.png b/content/logic-modelling-notes/sets/induction-natural-deduction-rule.png Binary files differ. diff --git a/content/logic-modelling-notes/src/The one-page cheat sheet.wiki b/content/logic-modelling-notes/src/The one-page cheat sheet.wiki @@ -1,52 +0,0 @@ -== One-page cheat sheet == -=== Definitions === -* Model is: - * set A - domain - * interpretation operation for predicate and function symbols -* satisfiable: some model & environment where it's true -* valid: true in all models and environments -* derivable: can be proven without global hypothesis -* tautology: true under any truth assignment (valid) -* soundness: ⊢ A → ⊨ A (from syntax to semantics) -* completeness: ⊨ A → ⊢ A (from semantics to syntax) -* partial order: antisymmetric, reflexive, transitive - * memo technique -- p**art**ial means **a**ntisymmetric, **r**eflexive, **t**ransitive - * strict means irreflexive -* total order: partial order & ∀ ab: R(a,b) ∨ R(b,a) - * strict: ∀ ab: R(a,b) ∨ a = b ∨ R(b,a) -* equivalence relation: has all three properties in the positive (symmetric, reflexive, transitive) - -environment is used to interpret free variables -=== Modal logic === -* □ Φ: true in world if true in all related worlds (if no related, true). -* ◇ Φ: true in world if true in some related world (if no related, false). - -M,w ⊩ Φ: Φ true in world w of Kripke model M (true in model if true in every world) - -Φ valid in frame if true with every labelling. - -frame = Kripke - labels - -=== Metatheorems === -* consistent: has a model -* syntactically consistent: can't derive ⊥ -* compactness: if Γ is consistent, every finite subset of Γ is also consistent - -=== Definability === -Model finiteness is undefinable. - -Model infiniteness is definable by a set of formulas. - -In predicate logic, only unreachability by n steps is definable, and only by a set of sentences. - -=== Decidability === -Y ⊆ I decidable if program can tell for every i ∈ I whether i ∈ Y. I set, Y predicate on set. - -Undecidable: termination, PCP, validity, provability, satisfiability. - -Termination can be reduced to PCP, which can be reduced to validity. - -Incompleteness theorems: every non-trivial formal system is -* either incomplete (valid but not derivable) -* or inconsistent (doesn't have a model, or entails ⊥) - diff --git a/content/logic-modelling-notes/src/decidability-and-undecidability.wiki b/content/logic-modelling-notes/src/decidability-and-undecidability.wiki @@ -1,69 +0,0 @@ -%template math -== Decidability and Undecidability == -=== Decision problems === -Decision problem consists of set I and a predicate Y ⊆ I - -Examples: - * determine whether a number is prime: - * input: natural number n - * I = N - * output: yes if n is prime, no otherwise - * Y = { n ∈ N | n is prime } - * termination problem (whether a program terminates): - * input: program P, input w - * I = set of all pairs <program, input> - * output: yes if P started with input w terminates, no otherwise - * Y = { <P, w> | P terminates on input w } - * validity problem (determine whether a formula is valid): - * input: formula Φ of predicate logic - * I = set of formulas of predicate logic - * output: yes if Φ is valid, no otherwise - * Y = set of valid formulas in predicate logic - -A decision problem Y ⊆ I is decidable if there is a program that tells for every i ∈ I whether i ∈ Y. - -==== Termination problem ==== -This problem is undecidable. - -steps: - * T outputs yes on input <P, w> ⇔ P halts on input w - * Tself outputs yes on input P ⇔ P halts on input P - * Z halts on input P ⇔ P does not halt on input P - * Z halts on input Z ⇔ Z does not halt on input Z - * contradiction. - -==== Post's Correspondence Problem ==== -Given n pairs of words: <w1, v1> , ..., <wn, vn> - -are there indices $i_1, i_2, ..., i_k$ (k ≥ 1) s.t. when concatenated, $wi_1 wi_2 ... wi_k = vi_1 vi_2 ... vi_k $? - -as a decision problem: - * $PCP = \{ < <w_1, v_1>, ..., <w_k, v_k> > | k ≥ 1, w_i, v_i \; \text{binary words} \}$ - * Y = { i ∈ PCP | i has a solution } - -it's undecidable. - -the termination problem can be reduced to PCP -- there is a computable function r that maps instances of termination problem to instances of PCP such that it holds: $P\text{ terminates on input w} \iff I_{<P, w>}\text{ has a solution}$ - -the validity problem in predicate logic is undecidable (no program that, given formula Φ, decides whether or not ⊨ Φ holds). PCP can be reduced to validity problem: - * I (instance of PCP) has a solution ⇔ ⊨ ΦI (instance of validity problem is valid) - -Then if we had program deciding validity for predicate logic, we would obtain PCP-solver. Not gonna work. - -=== Undecidability of Validity and Provability === -The validity problem in predicate logic is undecidable. -There cannot be a program that, given any formula Φ, decides whether or not ⊨Φ holds. - -The provability in predicate logic is undecidable. -There cannot be a program that, given any formula Φ, decides whether or not ⊢ Φ holds. -This follows from soundness and completeness theorem. - -=== Undecidability of Satisfiability === -for sentences Φ it holds: - * Φ is unsatisfiable ⇔ ¬ Φ is valid - * Φ is satisfiable ⇔ ¬ Φ is not valid - -there's an easy reduction of validity problem to satisfiability problem. - -The relations ⊨ and ⊢ in predicate logic are undecidable. - diff --git a/content/logic-modelling-notes/src/definability-and-undefinability-results.wiki b/content/logic-modelling-notes/src/definability-and-undefinability-results.wiki @@ -1,64 +0,0 @@ -%template math -== Definability and Undefinability results == -expressible frame properties in predicate/modal logic: - -{{local:../img/expressible-frame-properties.png|Expressible frame properties}} - -=== for model cardinality === -model cardinality: - -{{local:../img/model-cardinality-definition.png|Model cardinality definition}} - - -for all models M and all n ≥ 2 it holds that: - * M ⊨ Φn ⇔ A has at least n elements - * M ⊨ ψn ⇔ A has at most n elements - * M ⊨ Φn ∧ ψn ⇔ A has precisely n elements - -model infiniteness is definable by a set of formulas Δ: - * M ⊨ Δ ⇔ M has an infinite domain - -model finiteness is undefinable (single formula): - * there's no sentence ψ such that - * all M: M ⊨ ψ ⇔ M has a finite domain - -model finiteness is undefinable (set of formulas): - * there's no set of formulas Γ such that - * all M: M ⊨ Γ ⇔ M has a finite domain - -mode infiniteness is undefinable (single formula) - * there's no sentence ψ such that - * all M: M ⊨ ψ ⇔ M has infinite domain - -=== for reachability === -"v is reachable via R from u". thinking of R as arrows, it means that there's a path from v to u. - -search for formulas χn that express reachability in n steps: - -Reachable in n steps: - 1. u = v - 2. R(u,v) - 3. ∃x₁ (RU, x₁) ∧ R(x₁, v)) - 4. ∃x₁ ∃x₂ (R(u, x₁) ∧ R(x₁, x₂) ∧ R(x₂, v)) - 5. .... - -shorthand: χ₂(c,d) denotes formula ∃x₁ (R(c, x₁) ∧ R(x₁, d)) - -{{local:../img/theorem-for-reachability.png|Theorem for reachability}} - -reachability is undefinable: - -{{local:../img/reachability-is-undefinable.png|Reachability is undefinable}} - - -Let R be a binary relation symbol. - 1. In predicate logic, reachability by R-steps is - * not definable by a sentence - * not definable by a set of sentences - 2. In predicate logic, unreachability by R-steps is - * not definable by a single sentence - * definable by a set of sentences - -=== General overview === -{{local:../img/undefinability-results-overview.png|Undefinability results overview}} - diff --git a/content/logic-modelling-notes/src/first-order-logic.wiki b/content/logic-modelling-notes/src/first-order-logic.wiki @@ -1,181 +0,0 @@ -%template math -== First order logic == -=== Functions, predicates, relations === -functions: take different numbers of arguments, returns a result. e.g. $mul(x,y)$, $square(x)$ - -predicates, relations: takes one or more arguments, is either true or false. e.g. $even(x)$, $divides(x,y)$ - -formulas: say things. make assertions about objects in the domain. - -=== Quantifiers, binding === -Quantifiers: - * ∀x: "for all x" - * ∃x: "there exists an x" - -Generally bind tightly: ∀x P ∨ Q == (∀x P) ∨ Q - -free variable: variable that's not bound - -sentence: a formula that has no free variables - -==== Natural deduction rules ==== - -| Universal quantification | Existential quantification | Equality | -|----------------------------------------------------------------------|--------------------------------------------------------------------------|------------------------------------------------------| -| {{local:../img/universal-introduction.png|Universal introduction}} | {{local:../img/existential-introduction.png|Existential introduction}} | {{local:../img/equality-rules.png|Equality rules}} | -| {{local:../img/universal-elimination.png|Universal elimination}} | {{local:../img/existential-elimination.png|Existential elimination}} | \/ | - - -=== Relativization and sorts === -You can use implication to relativize quantification (put it into a specific domain). - -Universal quantification, e.g. "every prime number greater than two is odd": - -∀x (prime(x) ∧ x > 2 → odd(x)) - -Existential quantification, e.g. "some woman is strong": - -∃x (woman(x) ∧ strong(x)) - -Remember to use ∧ with ∃, and not →. - -=== Models === -Let F be a set of function symbols, P a set of predicate symbols. - -Model M for (F, P) consists of: - * non-empty set A ("domain", "universe") - * interpretation operation $(\cdot)^M$ for for symbols in F, P - -Universe A can be any non-empty set. - -only constraint: $F^M$ and $P^M$ have same number of arguments as F and P. - -=== Interpreting formulas without quantifiers === -Truth definition for formula Φ without quantifiers and free variables in model M by induction on the structure of Φ: - * M ⊨ ¬Φ ↔ not: M ⊨ Φ ↔ M ⊭ Φ - * M ⊨ Æ∧ Ψ ↔ M ⊨ Φ and M ⊨ Ψ - * M ⊨ Φ ∨ Ψ ↔ M ⊨ Φ or M ⊨ Ψ - * M ⊨ Φ → Ψ : if M ⊨ Φ then M ⊨ Ψ - * M ⊨ P(t₁, .., tn) ↔ ($t_1^M,\ldots,t_n^M) \in P^M$ - -Interpretation of terms $t^M$: - * if t = c for constant c, then $t^M = c^M$ - * if $t = f(t_1,\ldots, t_n)$, then $t^M = f^M(t_1^M,\ldots,t_n^M)$ - -=== Interpretation of formulas with quantifiers and free variables === -to interpret free variables, you use an environment. - -an environment `l: var → A` (look up function) interprets free variables in the domain - -=== Interpreting terms in model with environment === -terms are built from variables, constants, function symbols - * variables are interpreted according to environment - * constants are interpreted according to $(\cdot)^M$ - * function symbols are interpreted according to $(\cdot)^M$ - - -Truth of formula Φ in model M with universe A with respect to environment e is defined by induction on the structure of Φ. - -Interpretation $t^{M,l}$ of term t is - -{{$%align% -t^{M, l} = \begin{cases} - l(x) &&\text{if } t = x \text{ for a variable } x \\ - c^M &&\text{if } t = c \text{ for a constant } c \\ - f^M (t_1^{M, l}, \ldots, t_n^{M, l}) &&\text{if } t = f(t_1, \ldots, t_n) - \end{cases} -}}$ -by induction on term structure. - -M ⊨l ∀x HI ↔ for all a ∈ A it holds that $ M \models_{l [x \to a]} \phi $ - -M ⊨l ∃x Φ ↔ for some a ∈ A it holds that $ M \models_{l [x \to a]} \phi $ - -=== Semantical entailment in predicate logic === -For all models M and all environments e, -such that M ⊨l Φ₁ and ... and M ⊨l Φn hold, -it also holds that M ⊨l ψ - -=== Logical equivalence === -Formulas φ and ψ are logically equivalent (φ ≡ ψ) if for all models M and environments l, M ⊨l φ ↔ M ⊨l ψ - -i.e. φ and ψ are true in precisely the same models when interpreted with the same environments. - -theorem: φ ≡ ψ ↔ φ ⊨ ψ and ψ ⊨ φ - -=== Satisfiability, validity, consistency === -Let φ be a formula, and Γ be a set of formulas. - -φ is satisfiable iff there is _some_ model M and _some_ environment l such that M ⊨l φ - -φ is valid iff M ⊨l φ holds for _all_ models M and _all_ environments l in which φ can be checked. - -Γ is consistent/satisfiable iff there is _some_ model M and _some_ environment l such tat M ⊨l ψ for all ψ ∈ Γ - -for all formulas φ, ψ: φ ≡ ψ means that φ ↔ ψ is valid - -=== Translating into predicate logic === -Example: "Marie and Jan are clever." - -Specification and model used: - -two predicates: - * CC(x): x is clever - * LL(x): x has learned logic - -two constants: - * m: Marie - * j: Jan - -model M: - * domain A = the set of all humans - * $C^M$ = { x ∈ A | x is clever } - * $LL^M$ = { x ∈ A | x has learned logic } - * $j^M $= Jan - * $m^M$ = Marie - -Then: - * "Marie and Jan are clever": C(m) ∧ C(j) - * "Not everybody is clever": ¬∀x C(x) - * "Somebody has learned logic": ∃x LL(x) - * "Not everybody has learned logic, but Marie and Jan have": ¬∀x LL(x) ∧ LL(m) ∧ LL(j) - -∀ and →: - * ∀x(LL(x) → C(x)): "everyone who has learned logic is clever" - * not the same as ∀x LL(x) → ∀x C(x): "if everyone has learned logic, everyone is clever" - -∃ and ∧: - * ∃x(L(x) ∧ C(x)): "some logicians are clever" - * not the same as ∃x(L(x) → C(x)): "if someone is a logician, they are clever" - -Formulas with free variables express properties and relations: - * no free variables: a sentence - * one free variable: a property - * two or more free variables: a relation - -=== Rules for quantifiers and connectives === -If you move a negation around ∀, it becomes ∃, and vice versa. - -It also holds that: - * ∀x(φ ∧ ψ) ≡ ∀x φ ∧ ∀x ψ - * BUT in general doesn't hold for ∨ - * ∃x(φ ∨ ψ) ≡ ∃x φ ∨ ∃x ψ - * BUT in general doesn't hold for ∧ - -In general, you can't move quantifiers through an implication. - -Order of _repeated_ ∀ or ∃ doesn't matter. But if you have _both_ ∃ and ∀, the order is important. - -=== Semantics of first order logic === -Interpretation: specifying the meaning of a predicate symbol. - * unary predicate P: set of elements of domain D for which P is true. - * constant c: an element of domain D - * function f with arity n: function mapping n elements of domain D to another element of D - * relation R with arity n: set of n tuples of elements of domain D for which R is true - -You can find the truth value of sentences intuitively. - -Completeness: if formula A is logical consequence of set of sentences Γ, then A is provable from Γ. - -Soundness: if A is provable from Γ then A is true in any model of Γ - diff --git a/content/logic-modelling-notes/src/incompleteness-theorem.wiki b/content/logic-modelling-notes/src/incompleteness-theorem.wiki @@ -1,31 +0,0 @@ -%template math -== Incompleteness theorem == -Consider sets of function and predicate symbols: - * F = {0, S, +, ·} - * P = {<} - -with as intended model number theory N: - * domain of N is the natural numbers with 0 - * $0^\mathbb{N} = 0$ - * $S^\mathbb{N} (n) = n + 1$ - * $+^\mathbb{N} (n,m) = n+m$ - * $\mathbb{N}(n,m) = n \cdot m$ - * $<^\mathbb{N} = \{ <n,m> | n,m \in \mathbb{N} \text{ such that }n < m \}$ - -One would like to have complete theory (deduction system) ⊢ for N that allows to derive all formulas that are true in N. - -First incompleteness theorem: - * every axiomatizable and sound theory ⊢ of first-order logic - * for number theory with language <F,P> - * is incomplete: - * it contains sentences Φ that are true in N, but unprovable in ⊢: N ⊨ Φ, yet ⊬ Φ. - - -Second incompleteness theorem: - * for every axiomatizable theory ⊢ of first-order logic - * for number theory with language <F,P> - * that is rich enough to express its own consistency by a sentence Φ⊢ - * it holds that either: - * ⊢ ⊥ (⊢ is inconsistent) - * ⊬ Φ⊢ (hence ⊢ is incomplete) - * so first-order theories (based on predicate logic) of number theory can't prove their own consistency diff --git a/content/logic-modelling-notes/src/index.wiki b/content/logic-modelling-notes/src/index.wiki @@ -1,58 +0,0 @@ -%% vim: relativenumber nospell spelllang=en_us spellcapcheck= -%template math -%% let g:vimwiki_wikilocal_vars[1]['path_html'] = expand('%:p:h').'/../' -%% let g:vimwiki_wikilocal_vars[1]['template_path'] = '/Users/alex/Dropbox/vimwiki/templates/' - -= Logic and Modeling = -Here's the [[http://avigad.github.io/logic_and_proof/propositional_logic.html|online book]]. - -Also, [[local:../logic-modelling.apkg|here's my Anki deck]]. - -[[The one-page cheat sheet]]. - -- [[propositional-logic#Propositional logic|Propositional logic]] - - [[propositional-logic#Propositional logic#Notation review|Notation review]] - - [[propositional-logic#Propositional logic#Rules of inference|Rules of inference]] - - [[propositional-logic#Propositional logic#Forward and backward reasoning|Forward and backward reasoning]] - - [[propositional-logic#Propositional logic#Proof by contradiction|Proof by contradiction]] - - [[propositional-logic#Propositional logic#Vocab definitions|Vocab definitions]] - - [[propositional-logic#Propositional logic#Classical reasoning|Classical reasoning]] - - [[propositional-logic#Propositional logic#Syntax vs Semantics|Syntax vs Semantics]] - - [[propositional-logic#Propositional logic#Soundness and completeness|Soundness and completeness]] -- [[first-order-logic#First order logic|First order logic]] - - [[first-order-logic#First order logic#Functions, predicates, relations|Functions, predicates, relations]] - - [[first-order-logic#First order logic#Quantifiers, binding|Quantifiers, binding]] - - [[first-order-logic#First order logic#Quantifiers, binding#Natural deduction rules|Natural deduction rules]] - - [[first-order-logic#First order logic#Relativization and sorts|Relativization and sorts]] - - [[first-order-logic#First order logic#Models|Models]] - - [[first-order-logic#First order logic#Interpreting formulas without quantifiers|Interpreting formulas without quantifiers]] - - [[first-order-logic#First order logic#Interpretation of formulas with quantifiers and free variables|Interpretation of formulas with quantifiers and free variables]] - - [[first-order-logic#First order logic#Interpreting terms in model with environment|Interpreting terms in model with environment]] - - [[first-order-logic#First order logic#Semantical entailment in predicate logic|Semantical entailment in predicate logic]] - - [[first-order-logic#First order logic#Logical equivalence|Logical equivalence]] - - [[first-order-logic#First order logic#Satisfiability, validity, consistency|Satisfiability, validity, consistency]] - - [[first-order-logic#First order logic#Translating into predicate logic|Translating into predicate logic]] - - [[first-order-logic#First order logic#Rules for quantifiers and connectives|Rules for quantifiers and connectives]] - - [[first-order-logic#First order logic#Semantics of first order logic|Semantics of first order logic]] -- [[sets#Sets|Sets]] - - [[sets#Sets#Relations|Relations]] - - [[sets#Sets#Relations#Order types|Order types]] - - [[sets#Sets#Natural numbers & induction|Natural numbers & induction]] - - [[sets#Sets#Recursive definitions|Recursive definitions]] -- [[modal-logic#Modal logic|Modal logic]] - - [[modal-logic#Modal logic#Truth in worlds|Truth in worlds]] - - [[modal-logic#Modal logic#Truth in Kripke models|Truth in Kripke models]] - - [[modal-logic#Modal logic#Semantic implication/entailment|Semantic implication/entailment]] - - [[modal-logic#Modal logic#Frames|Frames]] -- [[meta-theorems-of-predicate-logic#Meta-Theorems of Predicate Logic|Meta-Theorems of Predicate Logic]] -- [[definability-and-undefinability-results#Definability and Undefinability results|Definability and Undefinability results]] - - [[definability-and-undefinability-results#Definability and Undefinability results#for model cardinality|for model cardinality]] - - [[definability-and-undefinability-results#Definability and Undefinability results#for reachability|for reachability]] - - [[definability-and-undefinability-results#Definability and Undefinability results#General overview|General overview]] -- [[decidability-and-undecidability#Decidability and Undecidability|Decidability and Undecidability]] - - [[decidability-and-undecidability#Decidability and Undecidability#Decision problems|Decision problems]] - - [[decidability-and-undecidability#Decidability and Undecidability#Decision problems#Termination problem|Termination problem]] - - [[decidability-and-undecidability#Decidability and Undecidability#Decision problems#Post's Correspondence Problem|Post's Correspondence Problem]] - - [[decidability-and-undecidability#Decidability and Undecidability#Undecidability of Validity and Provability|Undecidability of Validity and Provability]] - - [[decidability-and-undecidability#Decidability and Undecidability#Undecidability of Satisfiability|Undecidability of Satisfiability]] -- [[incompleteness-theorem#Incompleteness theorem|Incompleteness theorem]] diff --git a/content/logic-modelling-notes/src/meta-theorems-of-predicate-logic.wiki b/content/logic-modelling-notes/src/meta-theorems-of-predicate-logic.wiki @@ -1,37 +0,0 @@ -%template math -== Meta-Theorems of Predicate Logic == -Entailment syntactically (⊢) and semantically (⊨) - * Γ ⊢ ψ: there is natural deduction derivation of ψ that only uses premises in Γ - * Γ ⊨ ψ: for all M and l, if M ⊨l Φ for every Φ ∈ Γ, then M ⊨ ψ - -Soundness and completeness: - * Γ ⊢ Φ ⇔ Γ ⊨ Φ - * for all formulas Φ, every set Γ of formulas - * soundness (correctness): left-to-right (⇒) - * completeness: right-to-left (⇐) - -soundness theorem: - * Γ ⊢ Φ ⇒ Γ ⊨ Φ - * if there is natural deduction derivation of Φ from Γ, then there's no model M in which all formulas of Γ are true, but Φ is false - * "correct" means not possible to derive false conclusion Φ from true premises Γ - * prove by induction on derivation lengths - -completeness theorem: - * Γ ⊨ Φ ⇒ Γ ⊢ Φ - * derivations are strong enough to derive all valid semantic entailment statements - * "complete" means more derivation rules are not necessary - * proof is non-trivial - -consistency and syntactical consistency - * Γ is consistent ⇔ Γ is syntactically consistent - * Γ has a model ⇔ there is no derivation of ⊥ from Γ - -semantical consistency: - * set Γ of formulas is consistent if there is model M and environment l such that M ⊨ Φ for all Φ ∈ Γ - -syntactical consistency: - * set Γ of formulas is syntactically consistent if Γ ⊬ ⊥ - -compactness theorem: - * Γ is consistent ⇔ every finite subset Γ₀ ⊆ Γ si consistent - diff --git a/content/logic-modelling-notes/src/modal-logic.wiki b/content/logic-modelling-notes/src/modal-logic.wiki @@ -1,56 +0,0 @@ -%template math -== Modal logic == -modal logic allows reasoning about dynamics -- futures, knowledge, beliefs, etc. - -modalities (unary connectives): - * □ (box): sure, always, has to be, knows, guaranteed (kinda like ∀) - * ◇ (diamond): possibly, sometimes, maybe, believes is possible, possible result (kinda like ∃) - -Kripke model `M = (W, R, L)` consists of: - * W worlds - * R accessibility relation - * L labeling function: which propositional letters are true in which world (`w ⊩ p ↔ p ∈ L(w)`) - -Kripke models define truth _per world_. - -{{local:../img/kripke-model-and-graph.png|Kripke model and graph}} - -=== Truth in worlds === -`M, w ⊩ Φ` means formula Φ is true in world w of Kripke model M. - -◇ Φ is true in world w if there exists a world w' such that R(w, w') and Φ is true in w'. - -□ Φ is true in world w if Φ is true in all worlds w' with R(w, w'). special case when world has no outgoing edge, ◇ Φ never holds and □ Φ always holds. - -=== Truth in Kripke models === -Φ is true in Kripke model `M = (W, R, L)` (i.e. M ⊨ Φ), iff x ⊩ Φ for every world x ∈ W. - -all propositional tautologies also hold in modal logic. - -=== Semantic implication/entailment === -M,w ⊨ ψ in every world w in every Kripke model where M,w ⊨ Φ₁, ..., M,w ⊨ Φn. - -modal validity: ⊨ ψ if in every world w in ever Kripke model M holds M,w ⊨ ψ. - -modal logical equivalence: `Φ ≡ ψ` if `M,w ⊨ Φ ↔ M,w ⊨ ψ`. in other words, Φ ≡ ψ ↔ Φ ⊨ ψ and ψ ⊨ Φ. - -=== Frames === -frame: Kripke model without labeling. `F = (W,R)`, W worlds, R accessibility relation - -Φ is valid in frame F (i.e. F ⊨ Φ) if for _every_ labeling L, Kripke model M = (W,R,L) makes Φ true. - -Correspondence of formulas and frame properties - * reflexive: - * F ⊨ □ p → p - * F ⊨ p → ◇ p - * symmetric: - * F ⊨ q → □ ◇ q - * F ⊨ ◇ □ p → p - * transitive: - * F ⊨ □ p → □ □ p - * F ⊨ ◇ ◇ p → ◇ p - * serial: - * F ⊨ ◇ T - * F ⊨ □ p → ◇ p - * functional: □ p ↔ ◇ p - diff --git a/content/logic-modelling-notes/src/propositional-logic.wiki b/content/logic-modelling-notes/src/propositional-logic.wiki @@ -1,89 +0,0 @@ -%template math -== Propositional logic == -=== Notation review === -* `A, B, C` -- propositions -* `A ∧ B` -- conjunction ("and") -* `A ∨ B` -- disjunction ("or") -* `A → B` -- implication ("if A then B") -* `A ↔ B` -- bi-implication ("A iff B") -* `¬ A` -- negation ("not A") -* `⊥` -- false, falsum, nonsense, bullshit, the middle finger - -=== Rules of inference === -"C is a logical consequence of A and B": - -{{local:../img/logical-consequence.png|Logical consequence}} - - -| Implication | Conjunction | Negation | Disjunction | Bi-implication ("if and only if") | -|------------------------------------------------------------------------|--------------------------------------------------------------------------|----------------------------------------------------------------------------------------|--------------------------------------------------------------------------|--------------------------------------------------------------------------------| -| {{local:../img/implication-elimination.png|Implication elimination}} | {{local:../img/conjunction-introduction.png|Conjunction introduction}} | {{local:../img/negation-hypothetical-reasoning.png|Negation hypothetical reasoning}} | {{local:../img/disjunction-introduction.png|Disjunction introduction}} | {{local:../img/bi-implication-introduction.png|Bi-implication introduction}} | -| {{local:../img/hypothesis.png|Hypothesis}} | {{local:../img/and-elimination.png|And elimination}} | {{local:../img/negation-elimination.png|Negation elimination}} | {{local:../img/disjunction-elimination.png|Disjunction elimination}} | {{local:../img/bi-implication-elimination.png|Bi-implication elimination}} | - -Truth and falsity: from false, you can conclude anything, and from nothing, you can conclude true. - -{{local:../img/falsum-elimination.png|Falsum elimination}}, {{local:../img/truth-introduction.png|Truth introduction}} - -You can also derive this conjunction rule: - -{{local:../img/conjunction-negation-rule.png|Conjunction negation rule}} - -=== Forward and backward reasoning === -Backward reasoning: looking at the goal and seeing what rules need to be applied ("bottom-up") - -Forward reasoning: starting at some hypotheses/assumptions - -The general heuristic is to always work backwards, as much as possible. Only once you get stuck should you work from your assumptions or hypotheses. - -If all else fails, try proof by contradiction. - -=== Proof by contradiction === -Suppose a negation of a formula is true, prove that it's impossible, thereby proving the original formula. - -{{local:../img/proof-by-contradiction.png|Proof by contradiction}} - -RAA stands for _"reductio ad absurdum"_ - -=== Vocab definitions === -* derivable: a formula φ is "derivable" if we can prove φ with no global hypotheses (bottom line is φ, everything is closed). Then we write ⊢ φ. -* φ is derivable from hypotheses ψ₁..ψn if we can compute φ assuming ψ₁..ψn -* formulas φ and ψ are logically equivalent if ⊢ φ ↔ ψ - -=== Classical reasoning === -Principles: - * Proof by contradiction: assume the contradiction, and show false, thereby proving the original. - * Double negation elimination: ¬ ¬ A ↔ A. - * Contrapositive: if A → B, then ¬ B → ¬ A - -A general heuristic: - 1. Work backward from the conclusion, using introduction rules. - 2. When you run out of stuff to do, work forward with elimination rules. - 3. If you get stuck, - - {{local:../img/go-go-proof-by-contradiction.jpg|Proof by contradiction meme|style="width:20%"}} - - (meme credit goes to Geo) - -=== Syntax vs Semantics === -Syntax: -- derivation, proofs -- Γ ⊢ A ("A is derivable from hypotheses in Γ") - -Semantics: -- truth and falsity -- truth assignment says which propositional letters are true -- valuation says which formulas are true - -=== Soundness and completeness === -provable: if there is a formal proof of a formula (syntactic) - -tautology/valid: if true under any truth assignment (semantic) - -soundness: if a formula is provable, it is valid (if ⊢ A, then ⊨ A) - -completeness: if a formula is valid, it is provable (if ⊨ A, then ⊢ A) - -Proving soundness is easier than proving completeness. - -A is a logical consequence of Γ if, given any truth assignment that makes every formula in Γ true, A is true. - diff --git a/content/logic-modelling-notes/src/sets.wiki b/content/logic-modelling-notes/src/sets.wiki @@ -1,59 +0,0 @@ -%template math -== Sets == -Recap from logic and sets: - * empty set Ø = {x | false} - * universal set U = {x | true} - * union A ∪ B = {x | x ∈ A or x ∈ B} - * intersection A ∩ B = {x | x ∈ A and x ∈ B} - * complement Ā = {x | x ∉ A} - * difference A \ B = {x | x ∈ A and x ∉ B} - -Theorems: - * A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) - * (A \ B) \ C = A \ (B ∪ C) - -=== Relations === -definitions of properties: - * reflexive: ∀x R(x,x) - * symmetric: ∀x ∀y (R(x,y) → R(y,x)) - * transitive: ∀x ∀y ∀z ((R(x,y) ∧ R(y,z)) → R(x,z)) - * serial: ∀x ∃y R(x,y) - * functional: ∀x ∃y (R(x,y) ∧ ∀z (R(x,z) → z=y)) - -==== Order types ==== -partial order: - * reflexive - * transitive - * antisymmetric - -total order: - * partial order - * ∀ a,b (R(a,b) ∨ R(b,a)) - -strict partial order: partial order but irreflexive - -strict total order: - * strict partial order - * ∀ a,b (R(a,b) ∨ (a=b) ∨ R(b,a)) - -equivalence relation: - * reflexive (∀a, a ≡ A) - * symmetric - * transitive - -=== Natural numbers & induction === -Set of natural numbers is N ∈ (0,∞) - -Principle of induction: let P be a property of natural numbers. Suppose P holds for zero, and whenever P holds for a natural number n, then it holds for its successor n+1. Then P holds for every natural number. - -As a natural deduction rule: - -{{local:../img/induction-natural-deduction-rule.png|Induction natural deduction rule}} - -=== Recursive definitions === -Let A be any set, suppose a is in A, and g: N × A → A. Then there is a unique function f satisfying: - * f(0) = a - * f(n+1) = g(n, f(n)) - -Typically to prove something about a recursively defined function is to use induction. - diff --git a/content/logic-modelling-notes/style.css b/content/logic-modelling-notes/style.css @@ -1,45 +0,0 @@ -@charset 'UTF-8'; - -body { - margin: 0px; - padding: 1em; - background: #f3f2ed; - font-family: 'Lato', sans-serif; - font-size: 12pt; - font-weight: 300; - color: #8A8A8A; - padding-left: 50px; -} -h1 { - margin: 0px; - padding: 0px; - font-weight: 300; - text-align: center; -} -ul.toc li { - margin: 8px 0; -} -h3.name { - font-style: italic; - text-align: center; - font-weight: 300; - font-size: 20px; -} -a { - color: #D1551F; -} -a:hover { - color: #AF440F; -} -strong { - font-weight: 700; - color: #2A2A2A; -} -td,th,table { - border: 1px solid #AAA; - border-collapse: collapse; -} -th,td { - padding: 0.5em; -} -
