Proof, Truth, and Computation

intuitionistic logic and foundations

(talk notes)

the crisis in our foundations

hilbert, brouwer, and the rise of intuitionism

$$\{x : x \notin x \}$$

what were people so worried about anyway

some notation: inference

$$Γ ⊢_c A$$
$$\vdash_c \text{ is } \textit{classical entailment}$$
$$A \text{ is a } \textit{proposition}$$
$$Γ \text{ is a } \textit{context}$$

syntax and semantics

syntactic: provides proof

   "sense"

semantic: preserves truth

    "meaning"

$$Γ ⊢_c A$$
$$Γ ⊨_c A$$

soundness and completeness

soundness:

   every syntactic formula is semantically meaningful

completeness:

    every semantic formula is syntactically provable

$$Γ ⊢_c A ⇒ Γ ⊨_c A$$
$$Γ ⊨_c A ⇒ Γ ⊢_c A$$

hilbert's programme

I should like to eliminate once and for all the questions regarding the foundations of mathematics, by turning every mathematical proposition into a formula that can be concretely exhibited and strictly derived, thus recasting mathematical definitions and inferences in such a way that they are unshakeable. I believe that I can attain this goal completely with my proof theory...

brouwer's intuitionism

...separating mathematics from mathematical language and hence from the phenomena of language described by theoretical logic, recognizing that intuitionistic mathematics is an essentially language-less activity of the mind, having its origin in the perception of a move of time...

$$Γ ⊢_i A ↝ \text{a \textit{proof} of } A$$
$$Γ ⊢_i A \land B ↝ \text{a proof of } A \textit{ and } \text{a proof of } B$$
$$Γ ⊢_i A \lor B ↝ \text{a proof of } A \textit{ or } \text{a proof of } B$$
$$Γ ⊢_i ∀x.A↝ f : [x' : X] → A[x↦x']$$
$$Γ ⊢_i ∃x.A ↝ (x' : X, p : A[x↦x'])$$
$$Γ ⊢_i A ⇒ B↝ \text{ a proof of } B, \text{ assuming } A$$
$$Γ ⊢_i \lnot A ↝ \text{ a proof there is } \textit{no proof} \text{ of } A$$

heyting semantics

proof, not truth!

$$\nvdash_i A \lor \lnot A$$

constructive mathematics

a proof must be witnessed

constructivism: what do you lose?

a whole lot!

Taking the principle of excluded middle from the mathematician would be the same, proscribing the telescope to the astronomer or to the boxer the use of his fists. To prohibit existence statements and the principle of excluded middle is tantamount to relinquishing the science of mathematics altogether. For, compared with the immense expanse of modern mathematics, what would the wretched remnants mean, the isolated results, incomplete and unrelated, that the intuitionists naïve obtained without the use of the logical e-axiom ?

 

linv

need a choose definition

(related to double negation)

rinv

need the axiom of choice

noncomputable
def linv [Inhabited α] (f : α → β) : β → α :=
  fun b : β =>
  	if ex : (∃ a : α, f a = b) then
      choose ex
    else
      default
sorry
$$↣⇒ f^{-1}∘f = id_A$$
$$↠⇒f∘f^{-1} = id_B$$
open Classical

so why would you do this?

  1. it is a more intuitive notion of proof
  2. computational interpretations! more later
  3. you can still do nonconstructive mathematics (!!!)

intuitionistic logic is not less powerful (just add axioms)!

it provides better distinctions

the axiom of decidability

a proof of A or a proof of no proof of A

$$\text{Excluded Middle } \vdash_i A \lor \lnot A$$

a proof you can trust

inductive ℕ : Type
  | zero : ℕ
  | suc  : ℕ → ℕ

propositions as types

  • ∧ : logical conjunction
  • ∨ : logical disjunction
  • ⊐ : intuitionistic implication
  • ∀ : universal quantification
  • ∃ : existential quantification
  • ☐ : modal necessity
  • ◇ : modal possibility
  • 1 : tautology
  • 0 : falsehood
  • ¬ : logical negation
  • ⇁ : intuitionistic negation

the curry-howard correspondence

  • × : product type, struct, tuple
  • + : sum type, union, enum
  • → : function type
  • Π : dependent product type
  • Σ : dependent sum type
  • various - extremely useful
  • various - extremely useful
  • ⊤ : top type, any
  • ⊥ : bottom type, never
  • not computable!
  • function to ⊥

types

logic

in an ideal world:

  • peer review catches mistakes in proofs
  • mathematics built upon a solid, concrete, justifiable foundation

in the real world:

  • Wiles's (correct) proof of Fermat's Last Theorem spans 129 pages
  • Inter-universal Teichmüller theory (!!)

math is hard

mechanization: novel results

  • sphere packing in     three-dimensional space
  • New Foundations is consistent in ZFC (!!)
  • Liquid Tensor project: condensed mathematics 
  • math-comp (Coq)
  • mathlib (Lean)
  • 1lab.dev (Agda)

existing results

proof assistants work

problems that can occur:

  • accidentally using escape hatches (sorry)
  • mistakes in the theoretical model (logic)
  • bugs in the implementation (kernel)
  • mistakes in the type (proposition)
  • but: bugs in the proof will be caught

these are few, and quantifiable!

these systems are cool

also useful!

and make us think deeply about axioms

takeaway:

resources

on logic


on proof


toki.la/cumc

i'm running a course on Lean!

  • spring 2024, pending approval
  • first half: theory of proof assistants
  • second half: usage of proof assistants

 

toki.la/proof-assistants

double negation embedding

  • there is no proof there is no proof of A
  • there is no proof A is undecidable
  • A is not definitely decidable
$$Γ \vdash_{C} A \implies Γ \vdash_{I} \neg \neg A$$

thanks to

SPLab, Yanze, Alex, Markus

the vicious circle

$$\{x : x \notin x\}$$
$$\text{this sentence is not provable}$$
$$\exists x: \bot$$