andrejbauer

(* The basic theory of Lawvere-Tierney operators and sheafification in logical form.

   This formalization is based on:

   Barbara Veit: A proof of the associated sheaf theorem by means of categorical logic,
   The Journal of Symbolic Logic , Volume 46 , Issue 1 , March 1981 , pp. 45–55
   DOI: https://doi.org/10.2307/2273255
*)

Require Import Utf8.

andrejbauer

module Myhill where

import Data.List (find)

type N = Integer

-- given injective maps `f, g : N → N` that witness 1-1 reductions `A ≤₁ B` and `B ≤₁ A`, respectively,
-- `myhill f g` computes the graph of a bijection `h : N → N` that witnesses `A ≡ B`, see
-- https://en.wikipedia.org/wiki/Myhill_isomorphism_theorem
myhill :: (N -> N) -> (N -> N) -> [(N,N)]

andrejbauer

(* A proof that there is a least closure operator which forces a given
   predicate to be true. The construction can be found in, e.g.,
   Martin Hyland's “Effective topos” paper, Proposition 16.3. *)

(* A closure operator on [Prop] is an idempotent, monotone, inflationary enodmap.

   One often requires additionally that the operator preserves conjunctions,
   in which case these are also called j-operators and Lawvere-Tierney topologies.
   We eschew the condition to obtain a slighly more general result, but we
   also show that the closure operator of interst happens to preserve conjunctions.

andrejbauer

(* A formalization of a classical propositional calculus a la user4035,
   see https://proofassistants.stackexchange.com/q/4443/169 and
   https://proofassistants.stackexchange.com/q/4468/169 ,
   with the following modifications:

   1) We use a set of assumptions rather than a list of assumptions.
   2) We use derivation trees to represent proofs instead of lists of formulas.

   Proofs-as-lists are used in Hilbert-style systems, whereas
   derivation trees are more common in natural-deduction style rules.

andrejbauer

-- A predicative version of Tarski's fixed-point theorem

open import Level
open import Data.Product

module Tarski where

  -- a complete preorder with carrier at level a, the preorder is at level b,
  -- and suprema indexed by sets from level c
  record CompletePreorder a b c : Setω where

andrejbauer

Experiments involving Miquel's theorem. Joint work with Finn Klein.

andrejbauer

# 
METHOD: TABLE
ENCODE: Unicode
PROMPT: LaTeX
VERSION: 1.0
DELIMITER: ,
VALIDINPUTKEY: ^,.?!:;"'/\()[]{}<>$%&@*01234567890123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz
TERMINPUTKEY: 
BEGINCHARACTER
alpha	α

andrejbauer

(* Post's theorem in computability theory states that a subset S ⊆ ℕ is
   decidable if both S and its complement ℕ \ S are semidecidable.
   Just how much classical logic is needed to prove the theorem, though?
   In this note we show that Markov's principle suffices.

   Rather than working with subsets of ℕ we work synthetically, with
   semidecidable and decidable truth values. (This is more general than
   the traditional Post's theorem.)
*)

andrejbauer

(*
   A formalization of first-order logic, theories and their models.
   As an example we formalize the language of ZF set theory and a a small fragment of ZF.
*)

(* A signature is given by function symbols, relation symbols, and their arities. *)
Structure Signature :=
  { funSym : Type (* names of function symbols *)
  ; funArity : funSym -> Type (* arities of function symbols *)
  ; relSym : Type (* names of relation symbols *)

andrejbauer

open import Data.Nat
open import Data.Product

module example where

  data SimpleTree (A : Set) : Set where
    empty : SimpleTree A
    leaf : A -> SimpleTree A
    node : A -> SimpleTree A -> SimpleTree A -> SimpleTree A