Practal — Practical Logic

Introduction

• Pick a book or paper, and formalize its ideas within the ITP system to build and further my understanding.
• Formalize my own notions and ideas (e.g. Local Lexing [7]) for the same reasons.

Use Case: Category Theory

structure Category =
  type Object 
  type Arrow  
  let dom : Arrow → Object
  let cod : Arrow → Object
  def HomSet(A : Object, B : Object) = 
    { f : Arrow | dom f = A ∧ cod f = B }
  let id : (x : Object) → HomSet(x, x)
  let then : (f : Arrow) → (g : Arrow | dom g = cod f) → 
             { h : Arrow | dom h = dom f ∧ cod h = cod g } 
  axiom identity : ∀ x : Arrow. (x then id (cod x)) = (id (dom x) then x) = x
  axiom associativity : ∀ e f g : Arrow. ((e then f) then g) = (e then (f then g)) 
end  

{ f : Arrow | dom f = A ∧ cod f = B }

(g : { g : Arrow | dom g = cod f })

cod e = dom f ∧ cod f = dom g

Nil Type For Expressing Undefinedness

let Arrow : Type
axiom ¬(nil : Arrow)

Function Subtyping

C ≤ A ∧ B ≤ D

∀ x : A. f x = g x 

A = C ∧ B ≤ D

Union, Intersection and Difference Types

A ≤ A ∪ B ∧ B ≤ A ∪ B

A ∩ B ≤ A ∧ A ∩ B ≤ B  

¬ (∃x : Null. true)

∀ A B : Type. ∀ a : A. (a : B) = (a : A ∩ B)
∀ A B : Type. ∀ b : B. (b : A) = (b : A ∩ B)
∀ A B : Type. ∀ a : A. a : A ∪ B
∀ A B : Type. ∀ b : B. b : A ∪ B

Type Extensionality

∀ A B : Type. (A = B) = ((∀ a : A. a : B) ∧ (∀ b : B. b : A))

Partial Functions

typealias A ↪ B = A → (B ∪ Nil)

A → B ≤ A ↪ B

Traditional Approach to Undefinedness

1/0 < 2

(α : Type) → (α ↪ ℙ) → ℙ

• If for all x : α we have P x = true then (∀ x : α. P x) = true, otherwise (∀ x : α. P x) = false.
• If there is x : α such that P x = true then (∃ x : α. P x) = true, otherwise (∃ x : α. P x) = false.

(α : Type) → (α ↪ ℙ) ↪ α

∀ x y z : ℝ. z = x / y ⟶ z ⋅ y = x

Defining Types

• via structure
• via typealias
• via typedef

structure

typealias

∀ A B : Type. (A ↪ B ) = (A → (B ∪ Nil))

typedef

typedef A ↪ B = A → (B ∪ Nil)

∀ A B : Type. (A ↪ B) ≠ (A → (B ∪ Nil))

Quotient Types

typedef ℚ = ℤ ⨯ (ℤ \ {0}) 
  identify (a, b) in ℚ with (c, d) in ℚ where a ⋅ d = c ⋅ b 
  identify z in ℤ with (z, 1) in ℚ

typedef ℚ = ℤ ⨯ (ℤ \ {0}) 
  identify (a, b) with (c, d) where a ⋅ d = c ⋅ b 
  identify z in ℤ with (z, 1)

typedef ℤ = ℕ ⨯ ℕ 
  identify (a, b) with (c, d) where a + d = c + b 
  identify n in ℕ with (n, 0)

typealias B = A

typedef B = A 
  identify a in A with a in B

Use Case: Set Theory

typealias Set (A : Type) = A → ℙ

structure ZF = 
  type Set
  let ∈ : Set → Set → ℙ
  let ∅ : Set
  let Un : Set → Set
  let Pow : Set → Set 
  let Repl : Set → (Set → Set) → Set 
  let Sep : Set → (Set → ℙ) → Set
  let Inf : Set 
  axiom Empty: ∀ x : Set. ¬ (x ∈ ∅)
  axiom Extensionality: ∀ x y : Set. (x = y) = (∀ z : Set. (z ∈ x) = (z ∈ y))
  axiom Union: ∀ z x : Set. (z ∈ Un x) = (∃ y : Set. z ∈ y ∧ y ∈ x)
  axiom Power: ∀ x y : Set. (y ∈ Pow x) = (∀ z : Set. z ∈ y ⟶ z ∈ x)
  axiom Replacement: ∀ f : Set → Set. ∀ y X : Set. y ∈ (Repl X f) = (∃ x : Set. x ∈ X ∧ y = f x) 
  axiom Separation: ∀ f : Set → ℙ. ∀ x X : Set. x ∈ (Sep X f) = (x ∈ X ∧ f x) 
  axiom Regularity: ∀ X : Set. X ≠ ∅ ⟶ (∃ x : Set. x ∈ X ∧ (∀ y : Set. y ∈ x ⟶ ¬ (y ∈ X))) 
  def UPair(x : Set, y : Set) = Repl (Pow (Pow ∅)) (λ z. if z = ∅ then x else y)
  def Singleton(x : Set) = UPair(x, x)
  def union(x : Set, y : Set) = Un (UPair(x, y))
  def Suc(x : Set) = union x (Singleton x)
  axiom Infinity: ∅ ∈ Inf ∧ (∀ x : Set. x ∈ Inf ⟶ Suc x ∈ Inf)
end

let 𝕌 : ZF

{ x : 𝕌.Set | x ∈ s }

Controlled Natural Language

Paraconsistency

Automation

Conclusion

References