Based on a part of a series of lectures given by Prof. R. Ramanujam The Institute of Mathematical Sciences, Chennai.
From what I understood. May be terribly wrong.
Corrections appreciated!
We need to define the language precisely, unambiguously and with as few logical resources as possible.
Given multiplication, we can implement divides like
b divides a = (∃k a = kb)
TODO: Implement subtraction using addition.
a - b = a + (a * (b-1))
TODO: Implement addition using subtraction.
a + b = a - (0 - b)
TODO: Implement multiplication using addition.
a * b = a + (a * (b-1))
TODO: Implement exponentiation using multiplication.
a ^ b = a * (a ^ (b-1))
A predicate prime() could be defined as
prime(p) :: (k divides p) → ((k = 1) ∨ (k = p)) = ∀k ∈ ℕ (∃n ∈ ℕ (p = nk) → ((k = 1) ∨ (k = p)))
(1 divides p) and (p divides p)
A predicate even() could be defined as
even(n) :: ∀n ∀a ∃b (n = ab) → (a = 2)
or just using addition like
even(n) :: ∀n ∃m (n = m + m)
Similarly, a predicate odd() could be defined as
odd(n) :: ¬(∀n ∃m n = m + m)
m < n could be defined like
<(m,n) :: ∀m ∈ ℕ ∀n ∈ ℕ ∃k ∈ ℕ (n = m + k)
Sir has done it as
∃k (n = m + k) ∧ (k ≠ 0)
m > n could be defined like
∃k (n+k = m) ∧ (k ≠ 0)
or just define it in terms of < as
>(m,n) :: <(n,m) Logicians don't like 'operator overloading' kind of stuff. Because it creates lot of sources of confusion. We need a precise meaning.
Predicate to check whether a number is zero:
zero(n) :: ∀k ∈ ℕ (k + n = n)
Can we define plus(n,m) using <(n,m) (ie, can addition be defined using order)?
No. Why?
Because addition returns a number, whereas order returns a truth value.
Gottlobe Frege
Tarski
Dense linear order
aka:
We wanna deal with statements that are true or false.
Note: RDBMS can be described using a first order language.
(Signature of a) Language of (Peano) arithmetic:
L = (R, F, C)
where
C = {0} // zeroF = {Succ, +, ^, x, ..}R = {<, =, ..} // Predicate symbolsThe predicates give a (Boolean?) truth value. Whereas the functions give another term.
Language of graphs:
C = ∅F = ∅R = {E²} // E is set of edgesThe predicate E(x,y) could mean there is a directed edge from vertex x to vertex y.
Then ∀y E(x,y) means that the vertex x is connected to all other vertices in the graph.
¬( ∃y E(x,y) ) :: the statement 'for some vertex y, there is an edge from vertex x to vertex y' is false.
That means ∀y ¬E(x,y) ie, the outdegree of the vertex x is zero.
Language of orders:
C = ∅F = ∅R = {<²} // < is the orderingLanguage of sets:
C = ∅F = ∅R = {∈²} // ∈ is the membership functionHere we could define x ⊆ t as:
X ⊆ Y ≡ ∀Z ((Z ∈ X) → (Z ∈ Y))
Language of groups:
C = ∅F = {dot}R = ∅We don't even need an explicit identity element, we can define it in terms of dot like
∃x ∀y (x•y = y and y•x = y)
A first order language (FOL) is defined by its parameters.
Specifies the formulas (ie, how formulas can be formed)
Using the syntax we can see if a formula is well-formed.
Can find parsing errors?
A structure. An inductive structure.
L = (R, F, C)
where
R: A (countable) set or predicate (or relation) symbols each of which has an arity. (Examples: < (binary), ∈ (binary), prime(x) (unary)).F: A (countable) set of function symbols each of which has an arity.C: A (countable) set of Constant symbols (not constants. Symbols denoting constants. Could 'zero' which stands for 0)Then there are:
Terms(L): Terms of the language LVars(L): Set of variablesNote: R = F = C = ∅ is an empty language.
R ≠ ∅, F ≠ ∅, C ≠ ∅R ≠ ∅, F = C = ∅F ≠ ∅, R = C = ∅Equations
x = y x = y + 5 (plus comes from F and 3 comes from C
x, y x, y+5
And regarding predicate/relational symbols,
∀rᵏ ∈ R with arity k and t₁, t₂, .., tₖ ∈ Terms(L), then r(t₁, t₂, ..., tₖ) is a primitive statement.
Like
(x + y) ∈ Terms(L) and f(g(y,x)) ∈ Terms(L), then (x + y) < f(g(y,x))
Combine primitive statements to build more (using connectives).
If α, β are statements then so are:
Propositional logic (or Boolean logic??) connectives:
α ∧ β (conjunction): a binary connectiveα ∨ β (disjunction): a binary connectiveα → β (implies. aka ⊃): a binary connectiveα ↔︎ β (iff. ie, equivalence. aka ≡): a binary connective¬α (negation): a unary connectiveQuantifiers (the x ∈ V is substituted in place of variables in α):
∀x α (universal quantifier)∃x α (existential quantifier)For example, the following is a statement
∀x ∀y (α ∧ β)
Because, α and β are statements.
That means α ∧ β is also a statement.
That in turn means ∀y (α ∧ β) is a statement,
which in turn means ∀x ∀y (α ∧ β) is a statement.
A countable set of variables associated with the FOL language.
BNF: Backus-Naur Form
L = (R, F, C) V = set of variables
t ∈ Terms(L) ::=
| c ∈ C |
| v ∈ V |
| fᵏ(t₁, t₂, .. , tₖ), fᵏ ∈ F |
α, β ∈ Φ(L) ::=
| t₁ = t₂ ⎫ atomic formulas |
| rᵏ(t₁, t₂, .. , tₖ), rᵏ ∈ R ⎭ |
| ¬α |
| α ∧ β |
| α ∨ β |
| α → β |
| α ≡ β |
| ∀x α |
| ∃x α |
The '::=' denotes an inductive definition.
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z)∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) is a formula.
This can be broken down like
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
---------------------------------
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
------------------------------
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
---------------------------
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
--
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
--
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
-------
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
--
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
--
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
-------
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
--
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
--
∀x ∀y ∀z (x < y) ∧ (y < z) → (x < z) ✓
ie,
∀x
┃
∀y
┃
∀z
┃
→
┃
┏━━━━━┻━━━━━━┓
┃ ┃
∧ ┃
┃ ┃
┏━━━━┻━━━┓ ┃
┃ ┃ ┃
< < <
┃ ┃ ┃
┏━━┻━━┓ ┏━━┻━━┓ ┏━━┻━━┓
x y y z x z
∀x x < ∃y∀x x < ∃y is not a formula.
This can be broken down like
∀x (x < ∃y) ✓
--------
∀x (x) < ∃y) ✓
---
∀x (x) < ∃y) ✗
ie,
∀x
┃
<
┃
┏━━┻━━┓
x ✗ ERROR
because ∃y by itself is not a member of Terms(L).
∴ (∀x x < ∃y) is not a formula.
ααRunning time: O(n) because we need to visit all nodes at least once.
TODO: Write a recurrence relation for it.
TODO: Write algorithm to check if a string/formula is in FO formula.
Terms(L) =
| fᵏ(t₁, …, tₖ) ∈ F // ie, a k-ary function |
| v ∈ V |
| c ∈ C |
Can be represented as a tree whose:
Formulas(L) = // given any two terms ∈ Terms(L), we can say they are equal
| t₁ = t₂ |
// if we already have k terms ∈ Terms(L) and there is a relation symbol // (or predicate symbol??) r ∈ R of arity k
| rᵏ(t₁, …, tₖ) ∈ R |
| ∀α β ∈ Formulas(L), α ∨ β |
| ∀α β ∈ Formulas(L), α ∧ β |
| ∀α β ∈ Formulas(L), α → β |
| ∀α β ∈ Formulas(L), α ≡ β |
| ∀x Formulas(L), ¬ α |
| ∀α β ∈ Formulas(L), ∀x α |
| ∀α β ∈ Formulas(L), ∃x α |
Can be represented as a tree whose:
|α| = number of nodes in the tree representation of α.
Assign meaning to the structure that we defined using the syntax.
We decide this meaning. Like setting the context. :-)
So we know what is true and what is wrong.
For example,
∀x ∀y, prime(x) → odd(x)
is false for x=2.
'mostly true', but still not true.
But,
∀x ∀y, prime(x) → green(x)
makes no sense (ie, sounds meaningless). How can a number be of a certain colour… :-)
But this could be meaningful depending on the semantics that we define.
And what about
large( pow(10, pow(10, pow(10))) )
Is it true?
It depends on our definition large().
Try
large(x) → large(x - 1)
If we defined large(x) as
large(x) =
| x >= 1000 => true
| otherwise => false
and x was 1000, it would be false.
(Again,) the truth value depends on our definition of large().
But if had just said
∀x, large(x) → large(x-1)
large(x) is true for any value of x, because it says ∀x.
So even large(-1000) would be true.
Vague predicate: difficult to say whether the statement is true or false.
Another example,
∀x ∃y, x = y²
is false, if x and y are natural numbers but true if they are real numbers.
ie, it is true in some structure.
Truth depends on the underlying structure.
Truth is a relation (between structures and sentences) here, not something like a judgement.
Not a judgement.
Simply a relation between structures and sentences (sentences aka statements)
structure ⊨ sentence // or ⊨ (structure, sentence)
S = (D, I)
where:
Examples:
| Language | Structure |
|---|---|
| Arithmetic | Number line (ie, the set of all real numbers??) |
| Groups | Set of all groups |
| Graphs | Set of all graphs |
| Orders | Set on which the order is imposed |
Structure for a language L = an L- structure.
From where the elements come from.
Interprets the symbols.
I = (IR, IF, IC)
where:
Every constant symbol is also an element of the domain.
So,
IC: C → D
Each function symbol is a k-ary function. ie, its arity is k.
IF: fᵏ ↦ (Dᵏ → D)
ie, a function of arity k takes k elements of the domain and produces a mapping to a single element of the domain.
For example, fᵏ could be a plus function of arity 2 defined on ℕ, in which it would be f²: (ℕxℕ → ℕ)
where each predicate/relation symbol is of arity k.
IR: rᵏ ↦ (Dᵏ → {0, 1})
0 means false and 1 means true here.
In
∀x ∀y, x = y
the domain consists of just one element (since there cannot be two elements with same value) or it could be empty.
So here, the domain has at most 1 element.
Simplest atomic formula is equality??
Like
x³ + y³ = z³
where t₁ = x³ + y³ and t₂ = z³
(and + is addition, x³ is x * x * x, etc)
After assigning values to variables and functions, we can evaluate the terms!
Suppose D is ℝ, ᵏ: ℝᵏ → ℝ and +: ℝ² → ℝ.
M = (S, π)
where
S: structureπ: V → D: Assignment. ie, assigns variables to values in the domainπ is also known as an environment / valuation.
We can extend (or 'lift') this π to a π^ like
π^: Terms(L) → D
because once we get the assignment map for the variables, we can use it to evaluate the terms as well since the terms use variables.
Each term t ∈ Terms(L) is evaluated to produce an element in the domain D.
∀c ∈ C, π^(c) = IC(c)∀v ∈ V, π^(v) = IV(v)∀f ∈ F, π^(f(t₁,.., tₖ)) = IF(f)(π^(t₁), ..., π^(t₁))About the last one, the terms given as argument of f are all evaluated (by applying π^) to produce values in D. These resultant values are then given as the argument of the function given as the interpretation of f.
If an α satisfies a model M, we say M ⊨ α. ie, M makes α true.
A relation between models and formulas (ie, (M x Formulas) → 𝔹).
Model for a language L is an L-model.
M ⊨ α is between the class of all L-models and all formulas in L.
Programming languages are built compositionally.
Most formal languages are built compositionally.
Logic is closely related to linguisitcs.
But logic insists of compositional semantics: meanings given compositionally.
And natural language is highly non-compositional.
M ⊨ t₁ = t₂ iff π^(t₁) = π^(t₂)
Here, t₁ = t₂ is something that is something in L where π^(t₁) = π^(t₂) is in the domain D.
M ⊨ rᵏ(t₁, ..., tₖ) iff IP(r)(π^(t₁), ..., π^(tₖ)) // a map from Dᵏ → {0, 1}
0 means it's in the relation and 1 means otherwise.
.
Now α = ¬β,
M ⊨ ¬β iff M ⊭ β
.
M ⊨ α ∧ β iff (M ⊨ α) and (M ⊨ β)
The 'and' here is in the meta-language.
.
M ⊨ α ∨ β iff (M ⊨ α) or (M ⊨ β)
The 'or' here is the mathematical OR. (Why???)
Implication
M ⊨ α → β iff whenever M ⊨ α, we also have (M ⊨ β)
ie, (M ⊨ α) ∧ (M ⊭ β) is not possible.
Equivalence
M ⊨ α ≡ β iff M ⊨ α exactly when M ⊨ β
ie, following are impossible:
(M ⊨ α) ∧ (M ⊭ β)(M ⊭ α) ∧ (M ⊨ β)Universal quantifier
M ⊨ ∀x α iff for all d ∈ D.
∀x means ∀d, d ∈ D. Every possible value in the domain.
Substitute all occurrences of x in α with terms defined over D. We can't just substitute elements in D.
The definition is like C → D not D → C.
So we can't say something like
M ⊨ α[x/d]
Existential quantifier
M ⊨ ∃x, α iff
TODO: Given an M and a formula α, is M ⊨ α true? (Algorithm: Truth definition)
| Video 3 |
M ⊨ α iff M ⊭ α
Only one of the two can (actually, must) be true, but not both (in an 'exclusive or' fashion).
M ⊨ ¬α iff M ⊭ α
M ⊨ α ∨ β iff M ⊨ α or M ⊨ β
M ⊨ α ∧ β iff M ⊨ α and M ⊨ β
M ⊨ α → β iff whenever M ⊨ α then also M ⊨ β
M ⊨ α ≡ β iff succeeds only when both α and β are equivalent. Either both are true or both are false.
M ⊭ α ∨ β iff M ⊭ α and M ⊭ β
M ⊭ α ∧ β iff M ⊭ α or M ⊭ β
M ⊭ α → β iff M ⊨ α and M ⊭ β (ie, fails when 'the premise holds but the conclusion doesn't' which is same as 'the assumption holds, but the conclusion doesn't')
vacuously true: α → b when ¬α
Let Γ be a set of formulas
and α is a formula.
Γ ⊨ α
Named after Leon Henkin
{P} C {Q}
------------------
{P * R} C {Q * R}
Can add more to the heap without disturbing. Provided R doesn't tamper with C.
I suppose this rule, which makes a separation between sub-parts of heaps distinct, is the reason why it is called 'separation logic'.
∀ and ∃∃!x)There exists one and only one x.
This can actually be implement using ∀ and ∃ itself.
∃!x α(x) ≡ ∃x(α(x) and ∀y α(y) → y=x)
So we don't really need a separate ∃!x.
∄x
An x doesn't exist.
Can be implemented using ∀ and ∃ like
∄x α(x) ≡ ∀x ¬α(x)
x: α(x) is true for most x but not all.xxLemma is like a 'minor-theorem' that is used to prove a theorem.
ie, a minor result whose sole purpose is to help proving a theorem.
Lemma is a helper to a theorem.
Axiom is what is known to be (or assumed to be) true and hence doesn't need a proof.
Theorem is something that we prove using axioms.
Corollary is something that can be derived trivially from a theorem.
"a quick consequence of a [sic] theorem that was proven" Ref: [1] and 1.
p → qp → q ≡ ¬p ∨ q
→ and ↦f: x ↦ y means that f is a function which takes a value x and produces y.
Whereas f: X → Y says that f is a function taking the set X as its domain and results in a value in Y.
So, I guess it means that ↦ works with values themselves and → works with sets.
Reference: https://math.stackexchange.com/a/1751201
If a variable is not quantified, it is a free variable?
For example, in
∀x, x ∧ y
y is a free variable (and x is a bound variable). The sentence is equivalent to saying
∀x ∃y, x ∧ y
We can say something about the truth value of the sentence only after fixing y.
(Then we can pick an x value and see if it is true??)
There is a slight difference.
Formulas can have variables floating around (free variables) as in
∀x, x = y // y is floating
Statements / sentences have no free variables. All variables are bound as in
∀x ∀y, x = y
= and ≡= is a stricter form of ≡.
≡ only says equivalent, not equal.
Whereas = says equal. One and the same.
For example in modular arithmetic (source: https://www.quora.com/What-are-the-differences-between-%E2%89%A1-and-symbols-in-mathematics-and-logic),
26 ≡ 2 mod 4 // 26 has remainder 2 when divided by 4
26 ≡ 2 mod 8 // 26 has remainder 2 when divided by 8
means that both 26 and 2 give the same remainder when divided by 4.
That doesn't mean 26=4 or 26=8.
∀x P(x, y), how do we know what kind of value y is? Is it ∀y or ∃y or something else?Like
a ∨ bc ∨ abd
Like
(a ∨ b)(c ∨ abd)
p → q ≡ ¬p ∨ q
https://math.stackexchange.com/a/2935038