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

andrejbauer

{-
  Weak excluded middle states that for every propostiion P, either ¬¬P or ¬P holds.

  We give a proof of weak excluded middle, relying just on basic facts about real numbers,
  which we carefully state, in order to make the dependence on them transparent.

  Some people might doubt the formalization. To convince yourself that there is no cheating, you should:

  * Carefully read the facts listed in the RealFacts below to see that these are all
    just familiar facts about the real numbers.

andrejbauer

{- Here is a short demonstration on how to use Agda's solvers that automatically
   prove equations. It seems quite impossible to find complete worked examples
   of how Agda solvers are used.

   Thanks go to @anormalform who helped out with these on Twitter, see
   https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng

   I welcome improvements and additions to this file.

   This file works with Agda 2.6.2.2 and standard-library-1.7.1