Logic notes

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!

Languages of logic

Desirable properties

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.

First order logic

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

The predicates give a (Boolean?) truth value. Whereas the functions give another term.

Language of graphs:

The 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:

Language of sets:

Here we could define x ⊆ t as:

X ⊆ Y ≡ ∀Z ((Z ∈ X) → (Z ∈ Y))

Language of groups:

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.

Syntax

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

Then there are:

Note: R = F = C = ∅ is an empty language.

Statements

Primitive statements

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))

Compound statements

Combine primitive statements to build more (using connectives).

If α, β are statements then so are:

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.

Variables

A countable set of variables associated with the FOL language.

BNF: Backus-Naur Form

Syntax of FOL using BNF

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.

Examples: Syntax of language of order

∀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.

Algorithm to parse the syntax tree

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.

Term

Terms(L) =

fᵏ(t₁, …, tₖ) ∈ F // ie, a k-ary function
v ∈ V
c ∈ C

Can be represented as a tree whose:

Formula Φ(L)

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 α.

Semantics

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.

Truth

Not a judgement.

Simply a relation between structures and sentences (sentences aka statements)

structure ⊨ sentence   // or ⊨ (structure, sentence)

Structure

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.

Domain

From where the elements come from.

Interpretation

Interprets the symbols.

I = (IR, IF, IC)

where:

Interpretation of constant symbols (IC)

Every constant symbol is also an element of the domain.

So,

IC: C → D

Interpretation of function symbols

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ℕ → ℕ)

Interpretation for predicate/relational symbols

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.

Formulas

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 +: ℝ² → ℝ.

Model (M)

M = (S, π)

where

π 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.

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.

Atomic formulas

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.

.

  1. .

    Now α = ¬β,

    M ⊨ ¬β iff M ⊭ β

  2. .

    M ⊨ α ∧ β iff (M ⊨ α) and (M ⊨ β)

    The 'and' here is in the meta-language.

  3. .

    M ⊨ α ∨ β iff (M ⊨ α) or (M ⊨ β)

    The 'or' here is the mathematical OR. (Why???)

  4. Implication

    M ⊨ α → β iff whenever M ⊨ α, we also have (M ⊨ β)

    ie, (M ⊨ α) ∧ (M ⊭ β) is not possible.

  5. Equivalence

    M ⊨ α ≡ β iff M ⊨ α exactly when M ⊨ β

    ie, following are impossible:

    • (M ⊨ α) ∧ (M ⊭ β)
    • (M ⊭ α) ∧ (M ⊨ β)

  6. 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]

  7. 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 ¬α

Consequence relation

Let Γ be a set of formulas

and α is a formula.

Γ ⊨ α

Henkin construction

Named after Leon Henkin

Separation logic

Frame rule

   {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'.

Interesting to note

Possible quantifiers other than ∀ and ∃

Uniqueness (∃!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.

Non-existence

∄x

An x doesn't exist.

Can be implemented using ∀ and ∃ like

∄x α(x) ≡ ∀x ¬α(x)

Some quantifiers that we can't code up easily (if at all)

Some terms

Difference between theorem and lemma

Lemma 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.

Difference between axiom and 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.

Difference between corollary and theorem

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.

Another form of p → q

p → q ≡ ¬p ∨ q

Difference between → 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

Free variable

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??)

Difference between statement/sentence and formula

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

Difference between = 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.

Dbts

CNF and DNF

Conjunctive Normal Form

Like

a ∨ bc ∨ abd

Disjunctive Normal Form

Like

(a ∨ b)(c ∨ abd)

p → q ≡ ¬p ∨ q

  1. https://math.stackexchange.com/a/2935038
    ↩︎