ITP for FOL + ZFC

Stream: general

[Patrick Thomas]

This is a translation of the core of the code for the interactive theorem prover described in "Handbook of Practical Logic and Automated Reasoning" by John Harrison [https://www.cl.cam.ac.uk/~jrh13/atp/index.html]. I'm wondering if I have done this correctly and if it can be extended for theorems in ZFC by adding the axioms for ZFC in the manner that I have added the first. Also, I am not certain if I am missing something, but the code for axiomExistsEq does not seem to match its 'x not free in t' comment.

import Data.List
import Prelude hiding (False, True)
import qualified Prelude (Bool(..))

data Formula a = False
               | True
               | Atom a
               | Not (Formula a)
               | And (Formula a) (Formula a)
               | Or (Formula a) (Formula a)
               | Imp (Formula a) (Formula a)
               | Iff (Formula a) (Formula a)
               | Forall String (Formula a)
               | Exists String (Formula a)
                 deriving (Show, Eq)

-- Func "c" [] : A constant named c
data Term = Var String
          | Func String [Term]
            deriving (Show, Eq)

-- Pred "P" [] : A propositional variable named P
data FOL = Pred String [Term]
           deriving (Show, Eq)

type Thm = Formula FOL


mkEq :: Term -> Term -> (Formula FOL)
mkEq s t = Atom (Pred "=" [s, t])

occursIn :: Term -> Term -> Bool
occursIn s t | s == t = Prelude.True
occursIn _ (Var _) = Prelude.False
occursIn s (Func _ args) = any (occursIn s) args

freeIn :: Term -> (Formula FOL) -> Bool
freeIn _ False = Prelude.False
freeIn _ True = Prelude.False
freeIn t (Atom (Pred _ args)) = any (occursIn t) args
freeIn t (Not p) = freeIn t p
freeIn t (And p q) = (freeIn t p) || (freeIn t q)
freeIn t (Or p q) = (freeIn t p) || (freeIn t q)
freeIn t (Imp p q) = (freeIn t p) || (freeIn t q)
freeIn t (Iff p q) = (freeIn t p) || (freeIn t q)
freeIn t (Forall y p) = (not (occursIn (Var y) t)) && (freeIn t p)
freeIn t (Exists y p) = (not (occursIn (Var y) t)) && (freeIn t p)

itList2 :: (t1 -> t2 -> t3 -> t3) -> [t1] -> [t2] -> t3 -> t3
itList2 _ [] [] b = b
itList2 f (h1 : t1) (h2 : t2) b = f h1 h2 (itList2 f t1 t2 b)
itList2 _ _ _ _ = error "itList2"


-- if |- p ==> q and |- p then |- q
modusPonens :: Thm -> Thm -> Thm
modusPonens (Imp p' q) p | p == p' = q
                         | otherwise = error "modusPonens: p != p'"
modusPonens _ _ = error "modusPonens: pattern match"

-- if |- p then |- forall x. p
gen :: String -> Thm -> Thm
gen x p = Forall x p

-- |- p ==> (q ==> p)
axiomAddImp :: (Formula FOL) -> (Formula FOL) -> Thm
axiomAddImp p q = Imp p (Imp q p)

-- |- (p ==> q ==> r) ==> (p ==> q) ==> (p ==> r)
axiomDistribImp :: (Formula FOL) -> (Formula FOL) -> (Formula FOL) -> Thm
axiomDistribImp p q r = Imp (Imp p (Imp q r)) (Imp (Imp p q) (Imp p r))

-- |- ((p ==> false) ==> false) ==> p
axiomDoubleNeg :: (Formula FOL) -> Thm
axiomDoubleNeg p = Imp (Imp (Imp p False) False) p

-- |- (forall x. p ==> q) ==> (forall x. p) ==> (forall x. q)
axiomAllImp :: String -> (Formula FOL) -> (Formula FOL) -> Thm
axiomAllImp x p q = Imp (Forall x (Imp p q)) (Imp (Forall x p) (Forall x q))

-- |- p ==> forall x. p [x not free in p]
axiomImpAll :: String -> (Formula FOL) -> Thm
axiomImpAll x p = if not (freeIn (Var x) p)
                  then (Imp p (Forall x p))
                  else error "axiomImpAll: variable free in formula"

-- |- exists x. x = t [x not free in t]
axiomExistsEq :: String -> Term -> Thm
axiomExistsEq x t = if not (occursIn (Var x) t)
                    then (Exists x (mkEq (Var x) t))
                    else error "axiomExistsEq: variable free in term"

-- |- t = t
axiomEqRefl :: Term -> Thm
axiomEqRefl t = mkEq t t

-- |- s1 = t1 ==> ... ==> sn = tn ==> f(s1,..,sn) = f(t1,..,tn)
axiomFunCong :: String -> [Term] -> [Term] -> Thm
axiomFunCong f lefts rights =
       itList2 (\s t p -> (Imp (mkEq s t) p)) lefts rights
               (mkEq (Func f lefts) (Func f rights))

-- |- s1 = t1 ==> ... ==> sn = tn ==> P(s1,..,sn) ==> P(t1,..,tn)
axiomPredCong :: String -> [Term] -> [Term] -> Thm
axiomPredCong p lefts rights =
       itList2 (\s t p -> (Imp (mkEq s t) p)) lefts rights
               (Imp (Atom (Pred p lefts)) (Atom (Pred p rights)))

-- |- (p <=> q) ==> p ==> q
axiomIffImp1 :: (Formula FOL) -> (Formula FOL) -> Thm
axiomIffImp1 p q = Imp (Iff p q) (Imp p q)

-- |- (p <=> q) ==> q ==> p
axiomIffImp2 :: (Formula FOL) -> (Formula FOL) -> Thm
axiomIffImp2 p q = Imp (Iff p q) (Imp q p)

-- |- (p ==> q) ==> (q ==> p) ==> (p <=> q)
axiomImpIff :: (Formula FOL) -> (Formula FOL) -> Thm
axiomImpIff p q = Imp (Imp p q) (Imp (Imp q p) (Iff p q))

-- |- true <=> (false ==> false)
axiomTrue :: Thm
axiomTrue = Iff True (Imp False False)

-- |- ~p <=> (p ==> false)
axiomNot :: (Formula FOL) -> Thm
axiomNot p = Iff (Not p) (Imp p False)

-- |- p /\ q <=> (p ==> q ==> false) ==> false
axiomAnd :: (Formula FOL) -> (Formula FOL) -> Thm
axiomAnd p q = Iff (And p q) (Imp (Imp p (Imp q False)) False)

-- |- p \/ q <=> ~(~p /\ ~q)
axiomOr :: (Formula FOL) -> (Formula FOL) -> Thm
axiomOr p q = Iff (Or p q) (Not (And (Not p) (Not q)))

-- |- (exists x. p) <=> ~(forall x. ~p)
axiomExists :: String -> (Formula FOL) -> Thm
axiomExists x p = Iff (Exists x p) (Not (Forall x (Not p)))

concl :: Thm -> (Formula FOL)
concl c = c


-- ZFC

mkElem :: Term -> Term -> (Formula FOL)
mkElem s t = Atom (Pred "in" [s, t])

-- |- forall x. forall y. forall z. (z \in x <==> z \in y) => (x = y)
axiomExtensionality :: String -> String -> String -> Thm
axiomExtensionality x y z = Imp (Forall x (Forall y (Forall z (Iff (mkElem (Var z) (Func x [])) (mkElem (Var z) (Func y [])))))) (mkEq (Var x) (Var y))


-- Derived

impRefl :: (Formula FOL) -> Thm
impRefl p = modusPonens (modusPonens (axiomDistribImp p (Imp p p) p) (axiomAddImp p (Imp p p))) (axiomAddImp p p)


-- Example: *Main> impRefl (Atom (Pred "P" []))

[Huỳnh Trần Khanh]

man this code is so cool!!! it's very clean and readable :heart_eyes: I have a suggestion though: you don't need to use String to represent bound variables :joy: in fact you can use something similar to de Bruijn indexing. this would simplify the implementation even more

[Patrick Thomas]

Thank you. It is pretty much just a direct translation from the book (I hope).

[Patrick Thomas]

It seems that FOL and set theory define different notions of predicates and functions, the latter being in terms of subsets of sets. How are these reconciled in FOL + ZFC?

[Reid Barton]

Well, these exist on different levels: a FOL predicate is a piece of syntax, while a subset in ZFC is something internal. So I'm not sure in what sense they could or should be reconciled. Of course they are related by some axioms, such as the axiom schema of separation.

[Reid Barton]

Note that in the context of ZFC, a "class" is really just a FOL predicate with one free variable.

[Patrick Thomas]

I guess my core question is, how can I create code in a similar manner as above, but for proving theorems in ZFC (or the set theory most often used in textbooks, I think it is ZFC?)

[Patrick Johnson]

Maybe you can find this helpful. It has been used to prove the independence of the continuum hypothesis.

[Reid Barton]

Patrick Thomas said:

I guess my core question is, how can I create code in a similar manner as above, but for proving theorems in ZFC (or the set theory most often used in textbooks, I think it is ZFC?)

In principle you just add the axioms of ZFC, and then the theorems you can prove from those axioms are the theorems of ZFC.
In practice, I guess you would pretty quickly learn the origin of the phrase "proof assistant".

[Huỳnh Trần Khanh]

you might want to take a look https://github.com/been-jamming/CORE been-jamming.github.io/CORE/

fair warning: code isn't production quality though

[Patrick Thomas]

How does the axiom of replacement get translated, since we do not have quantification over formulas in FOL?

[Huỳnh Trần Khanh]

Patrick Thomas said:

How does the axiom of replacement get translated, since we do not have quantification over formulas in FOL?

in CORE, a toy theorem prover I linked, it does allow quantification over formulas :joy: so maybe if you want a ZFC theorem prover that works you can just do whatever CORE does :joy: but I'm not an expert so I'm not sure whether that's an orthodox way of doing things or not

[Reid Barton]

Same way you implemented the rest of the axioms, which (like replacement) are actually axiom schemas--the quantification is at the meta level, not internal.

[Patrick Thomas]

Does the grammar get changed to this:

type Var = String

data Formula = False
             | True
             | Eq Var Var
             | In Var Var
             | Not Formula
             | And Formula Formula
             | Or Formula Formula
             | Imp Formula Formula
             | Iff Formula Formula
             | Forall Var Formula
             | Exists Var Formula
               deriving (Show, Eq)

type Thm = Formula

[Reid Barton]

Oh yes, you need to add the signature of the theory (here just the binary relation $\in$) to the language, and then maybe add axioms saying that it is preserved by replacing things by equal things?
I didn't notice before that the statement of axiomExtensionality was nonsense, it needs to be an axiom about $\in$, of course!

[Reid Barton]

I think it looks right now--since there aren't any function symbols, a "term" can only possibly be a variable.

[Reid Barton]

type Thm = Formula

Normally one would use something more robust than a type synonym to dissuade the user from treating an arbitrary formula as a theorem.

[Patrick Thomas]

Reid Barton said:

type Thm = Formula

Normally one would use something more robust than a type synonym to dissuade the user from treating an arbitrary formula as a theorem.

Yeah, I'm not sure how to do that in Haskell yet.

[Huỳnh Trần Khanh]

you probably want a newtype, not just a type alias

[Reid Barton]

The usual way is to put everything that can construct judgments (like Thm) in a single module, make Thm a newtype, export Thm and the field selector from that module, but don't export the constructor of Thm.

[Patrick Thomas]

I see.

[Reid Barton]

Then you have a guarantee that (barring the use of stuff like unsafeCoerce) the only way to construct values of type Thm is using the methods exported from that module, and so once you check that they really correspond to the axioms of whatever system you're interested in, then you know that any t :: Thm constructed anywhere in the program must be a valid theorem. This is the "LCF approach" as I understand it.

[Patrick Thomas]

Something like this?

import Prelude hiding (False, True)
import qualified Prelude (Bool(..))

module ITP (Theorem, modusPonens, etc.)

type Var = String

data Formula = False
             | True
             | Eq Var Var -- Var = Var
             | In Var Var -- Var ∈ Var
             | Not Formula -- ¬ Formula
             | And Formula Formula -- Formula ∧ Formula
             | Or Formula Formula -- Formula ∨ Formula
             | Imp Formula Formula -- Formula → Formula
             | Iff Formula Formula -- Formula ↔ Formula
             | Forall Var Formula -- ∀ Var. Formula
             | Exists Var Formula -- ∃ Var. Formula
               deriving (Show, Eq)

newtype Theorem = Theorem Formula

[Reid Barton]

Right, except you probably also want to export a function Theorem -> Formula, so that you can check what you proved

[Reid Barton]

And you want to export Formula(..) too

[Reid Barton]

You will need it to apply axiom schemas

[Reid Barton]

Of course for the moment there's no need to worry about any of this.

[Patrick Thomas]

Ok.

[Patrick Thomas]

I looked at the way that metamath implements the axiom schemes. I'm not sure I understand why the set variables are required to be distinct.
http://cn.metamath.org/mpeuni/mmset.html#staxioms

[Mario Carneiro]

In order for metamath expressions to act like standard FOL expressions, you usually want all textually distinct variables to have distinctness conditions, because otherwise you get bound variable collapse issues when \forall x, \exists y, P(x, y) becomes \forall x, \exists x, P(x, x) (which is equivalent to \forall x, \exists y, P(y, y))

[Mario Carneiro]

In some cases the distinctness is not required, but the safest thing is to assume it in the axioms and maybe prove the non-distinct version as a derived theorem

[Mario Carneiro]

Note that this is not distinctness in the sense that the set values are unequal (what you would write x != y in ZFC or lean), but rather that the variables are not the same variable

[Patrick Thomas]

I see. Thank you.

[Patrick Thomas]

Can the lambda calculus be formulated in such a way that the Curry–Howard correspondence has the same first order logic as that used with axiomatic set theory, that is, no functions and just the equality and member of predicates?

[Patrick Thomas]

Is this correct for the logic of ZFC?

type Var = String

data Formula = Not Formula -- ~ Formula
             | Imp Formula Formula -- Formula -> Formula
             | Forall Var Formula -- forall Var. Formula
             | Eq Var Var -- Var = Var
             | In Var Var -- Var \in Var
               deriving (Show, Eq)

newtype Theorem = Theorem Formula


subFor :: Var -> Var -> Formula -> Formula
subFor y x (Not p) = Not (subFor y x p)
subFor y x (Imp p q) = Imp (subFor y x p) (subFor y x q)
subFor y x (Forall z p) = if z /= x && z /= y then Forall z (subFor y x p) else error "subFor"
subFor y x (Eq s t) | x /= s && x /= t = Eq s t
                    | x == s && x /= t = Eq y t
                    | x /= s && x == t = Eq s y
                    | otherwise = Eq y y
subFor y x (In s t) | x /= s && x /= t = In s t
                    | x == s && x /= t = In y t
                    | x /= s && x == t = In s y
                    | otherwise = In y y


freeIn :: Var -> Formula -> Bool
freeIn x (Not p) = freeIn x p
freeIn x (Imp p q) = freeIn x p || freeIn x q
freeIn x (Forall y p) = x /= y && freeIn x p
freeIn x (Eq s t) = x == s || x == t
freeIn x (In s t) = x == s || x == t


-- Propositional calculus

-- |- (p -> (q -> p))
prop_1 :: Formula -> Formula -> Theorem
prop_1 p q = Theorem (Imp p (Imp q p))

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
prop_2 :: Formula -> Formula -> Formula -> Theorem
prop_2 p q r = Theorem (Imp (Imp p (Imp q r)) (Imp (Imp p q) (Imp p r)))

-- |- ((~p -> ~q) -> (q -> p))
prop_3 :: Formula -> Formula -> Theorem
prop_3 p q = Theorem (Imp (Imp (Not p) (Not q)) (Imp q p))

-- |- p & |- (p -> q) => |- q
mp :: Theorem -> Theorem -> Theorem
mp (Theorem p) (Theorem (Imp p' q)) = if p == p' then Theorem q else error "mp"
mp _ _ = error "mp"


-- Predicate calculus

-- |- p => |- forall x. p
gen :: Theorem -> Var -> Theorem
gen (Theorem p) x = Theorem (Forall x p)

-- |- ((forall x. (p -> q)) -> (forall x. p) -> (forall x. q))
pred_1 :: Var -> Formula -> Formula -> Theorem
pred_1 x p q = Theorem (Imp (Forall x (Imp p q)) (Imp (Forall x p) (Forall x q)))

-- |- (forall x. p -> p [y/x]) provided p admits y for x
pred_2 :: Var -> Var -> Formula -> Theorem
pred_2 x y p = Theorem (Imp (Forall x p) (subFor y x p))

-- |- (p -> forall x. p) provided x is not free in p
pred_3 :: Var -> Formula -> Theorem
pred_3 x p = if not (freeIn x p) then Theorem (Imp p (Forall x p)) else error "pred_3"


-- Equality

-- |- forall x. x = x
eq_1 :: Var -> Theorem
eq_1 x = Theorem (Forall x (Eq x x))

-- |- (x = y -> (x = z -> y = z))
eq_2 :: Var -> Var -> Var -> Theorem
eq_2 x y z = Theorem (Imp (Eq x y) (Imp (Eq x z) (Eq y z)))

-- |- (x = y -> (x \in z -> y \in z))
eq_3 :: Var -> Var -> Var -> Theorem
eq_3 x y z = Theorem (Imp (Eq x y) (Imp (In x z) (In y z)))

-- |- (x = y -> (z \in x -> z \in y))
eq_4 :: Var -> Var -> Var -> Theorem
eq_4 x y z = Theorem (Imp (Eq x y) (Imp (In z x) (In z y)))

[Patrick Thomas]

No, wait, I think the subFor function is wrong.

[Patrick Thomas]

Amended (I think).

type Var = String

data Formula = Not Formula -- ~ Formula
             | Imp Formula Formula -- Formula -> Formula
             | Forall Var Formula -- forall Var. Formula
             | Eq Var Var -- Var = Var
             | In Var Var -- Var \in Var
               deriving (Show, Eq)

newtype Theorem = Theorem Formula


subFor :: Var -> Var -> Formula -> Formula
subFor y x (Not p) = Not (subFor y x p)
subFor y x (Imp p q) = Imp (subFor y x p) (subFor y x q)
subFor y x (Forall z p) | z == x = Forall z p
                        | otherwise = if z /= y then Forall z (subFor y x p) else error "subFor"
subFor y x (Eq s t) | x /= s && x /= t = Eq s t
                    | x == s && x /= t = Eq y t
                    | x /= s && x == t = Eq s y
                    | otherwise = Eq y y
subFor y x (In s t) | x /= s && x /= t = In s t
                    | x == s && x /= t = In y t
                    | x /= s && x == t = In s y
                    | otherwise = In y y


freeIn :: Var -> Formula -> Bool
freeIn x (Not p) = freeIn x p
freeIn x (Imp p q) = freeIn x p || freeIn x q
freeIn x (Forall y p) = x /= y && freeIn x p
freeIn x (Eq s t) = x == s || x == t
freeIn x (In s t) = x == s || x == t


-- Propositional calculus

-- |- (p -> (q -> p))
prop_1 :: Formula -> Formula -> Theorem
prop_1 p q = Theorem (Imp p (Imp q p))

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
prop_2 :: Formula -> Formula -> Formula -> Theorem
prop_2 p q r = Theorem (Imp (Imp p (Imp q r)) (Imp (Imp p q) (Imp p r)))

-- |- ((~p -> ~q) -> (q -> p))
prop_3 :: Formula -> Formula -> Theorem
prop_3 p q = Theorem (Imp (Imp (Not p) (Not q)) (Imp q p))

-- |- p & |- (p -> q) => |- q
mp :: Theorem -> Theorem -> Theorem
mp (Theorem p) (Theorem (Imp p' q)) = if p == p' then Theorem q else error "mp"
mp _ _ = error "mp"


-- Predicate calculus

-- |- p => |- forall x. p
gen :: Theorem -> Var -> Theorem
gen (Theorem p) x = Theorem (Forall x p)

-- |- ((forall x. (p -> q)) -> (forall x. p) -> (forall x. q))
pred_1 :: Var -> Formula -> Formula -> Theorem
pred_1 x p q = Theorem (Imp (Forall x (Imp p q)) (Imp (Forall x p) (Forall x q)))

-- |- (forall x. p -> p [y/x]) provided p admits y for x
pred_2 :: Var -> Var -> Formula -> Theorem
pred_2 x y p = Theorem (Imp (Forall x p) (subFor y x p))

-- |- (p -> forall x. p) provided x is not free in p
pred_3 :: Var -> Formula -> Theorem
pred_3 x p = if not (freeIn x p) then Theorem (Imp p (Forall x p)) else error "pred_3"


-- Equality

-- |- forall x. x = x
eq_1 :: Var -> Theorem
eq_1 x = Theorem (Forall x (Eq x x))

-- |- (x = y -> (x = z -> y = z))
eq_2 :: Var -> Var -> Var -> Theorem
eq_2 x y z = Theorem (Imp (Eq x y) (Imp (Eq x z) (Eq y z)))

-- |- (x = y -> (x \in z -> y \in z))
eq_3 :: Var -> Var -> Var -> Theorem
eq_3 x y z = Theorem (Imp (Eq x y) (Imp (In x z) (In y z)))

-- |- (x = y -> (z \in x -> z \in y))
eq_4 :: Var -> Var -> Var -> Theorem
eq_4 x y z = Theorem (Imp (Eq x y) (Imp (In z x) (In z y)))

[Patrick Thomas]

Hmm, no, still wrong. Sorry for the spam.

[Patrick Thomas]

Is this correct for the logic of ZFC?

type Var = String

data Formula = Not Formula -- ~ Formula
             | Imp Formula Formula -- Formula -> Formula
             | Forall Var Formula -- forall Var. Formula
             | Eq Var Var -- Var = Var
             | In Var Var -- Var \in Var
               deriving (Show, Eq)

newtype Theorem = Theorem Formula


{-
An occurrence of a variable $v$ in a formula $P$ is bound if and only if
it occurs in a subformula of $P$ of the form $\forall v Q$. An occurrence
of $v$ in $P$ is free if and only if it is not a bound occurrence. The
variable $v$ is free or bound in $P$ according as it has a free or bound
 occurrence in $P$.

If $P$ is a formula, $v$ is a variable, and $t$ is a term, then $P(t/v)$ is
the result of replacing each free occurrence of $v$ in $P$ by an occurrence
of $t$.

If $v$ and $u$ are variables and $P$ is a formula, then $P$ admits $u$ for $v$
if and only if there is no free occurrence of $v$ in $P$ that becomes a
bound occurrence of $u$ in $P(u/v)$. If $t$ is a term, then $P$ admits $t$ for
$v$ if and only if $P$ admits for $v$ every variable in $t$.
-}

-- occursIn v p = v occurs in p
occursIn :: Var -> Formula -> Bool
occursIn v (Not p) = occursIn v p
occursIn v (Imp p q) = occursIn v p || occursIn v q
occursIn v (Forall _ p) = occursIn v p
occursIn v (Eq x y) = v == x || v == y
occursIn v (In x y) = v == x || v == y

-- freeIn v p = there exists an occurrence of v in p that is free.
freeIn :: Var -> Formula -> Bool
freeIn v (Not p) = freeIn v p
freeIn v (Imp p q) = freeIn v p || freeIn v q
freeIn v (Forall x p) = v /= x && freeIn v p
freeIn v (Eq x y) = v == x || v == y
freeIn v (In x y) = v == x || v == y

-- admitsFor p u v [] = p admits u for v = there is no free occurrence of
-- v in p that becomes a bound occurrence of u in p(u/v).
-- xs is the list of binding variables that p is in the scope of.
admitsFor :: Formula -> Var -> Var -> [Var] -> Bool
admitsFor (Not p) u v xs = admitsFor p u v xs
admitsFor (Imp p q) u v xs = admitsFor p u v xs && admitsFor q u v xs
admitsFor (Forall x p) u v xs = admitsFor p u v (x : xs)
admitsFor (Eq x y) u v xs = (v /= x || elem v xs || not (elem u xs)) &&
                            (v /= y || elem v xs || not (elem u xs))
admitsFor (In x y) u v xs = (v /= x || elem v xs || not (elem u xs)) &&
                            (v /= y || elem v xs || not (elem u xs))

-- subFor t v p = p(v/t) = the result of replacing each free occurrence of
-- v in P by an occurrence of t.
subFor :: Var -> Var -> Formula -> Formula
subFor t v (Not p) = Not (subFor t v p)
subFor t v (Imp p q) = Imp (subFor t v p) (subFor t v q)
subFor t v (Forall x p) | v == x = Forall x p
                        | otherwise = Forall x (subFor t v p)
subFor t v (Eq x y) | v == x && v == y = Eq t t
                    | v == x && v /= y = Eq t y
                    | v /= x && v == y = Eq x t
                    | otherwise = Eq x y
subFor t v (In x y) | v == x && v == y = In t t
                    | v == x && v /= y = In t y
                    | v /= x && v == y = In x t
                    | otherwise = In x y


-- Propositional calculus

-- |- (p -> (q -> p))
prop_1 :: Formula -> Formula -> Theorem
prop_1 p q = Theorem (Imp p (Imp q p))

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
prop_2 :: Formula -> Formula -> Formula -> Theorem
prop_2 p q r = Theorem (Imp (Imp p (Imp q r)) (Imp (Imp p q) (Imp p r)))

-- |- ((~p -> ~q) -> (q -> p))
prop_3 :: Formula -> Formula -> Theorem
prop_3 p q = Theorem (Imp (Imp (Not p) (Not q)) (Imp q p))

-- |- p & |- (p -> q) => |- q
mp :: Theorem -> Theorem -> Theorem
mp (Theorem p) (Theorem (Imp p' q)) = if p == p' then Theorem q else error "mp"
mp _ _ = error "mp"


-- Predicate calculus

-- |- p => |- forall v. p
gen :: Theorem -> Var -> Theorem
gen (Theorem p) v = Theorem (Forall v p)

-- |- ((forall v. (p -> q)) -> (forall v. p) -> (forall v. q))
pred_1 :: Var -> Formula -> Formula -> Theorem
pred_1 v p q = Theorem (Imp (Forall v (Imp p q)) (Imp (Forall v p) (Forall v q)))

-- |- (forall v. p -> p [t/v]) provided p admits t for v
pred_2 :: Var -> Var -> Formula -> Theorem
pred_2 t v p = if admitsFor p t v []
               then Theorem (Imp (Forall v p) (subFor t v p))
               else error "pred_2"

-- |- (p -> forall v. p) provided v is not free in p
pred_3 :: Var -> Formula -> Theorem
pred_3 v p = if not (freeIn v p)
             then Theorem (Imp p (Forall v p))
             else error "pred_3"


-- Equality

-- |- forall x. x = x
eq_1 :: Var -> Theorem
eq_1 x = Theorem (Forall x (Eq x x))

-- |- (x = y -> (x = z -> y = z))
eq_2 :: Var -> Var -> Var -> Theorem
eq_2 x y z = Theorem (Imp (Eq x y) (Imp (Eq x z) (Eq y z)))

-- |- (x = y -> (x \in z -> y \in z))
eq_3 :: Var -> Var -> Var -> Theorem
eq_3 x y z = Theorem (Imp (Eq x y) (Imp (In x z) (In y z)))

-- |- (x = y -> (z \in x -> z \in y))
eq_4 :: Var -> Var -> Var -> Theorem
eq_4 x y z = Theorem (Imp (Eq x y) (Imp (In z x) (In z y)))

[Trebor Huang]

This code is soooo cool! One thing: you can use pattern synonyms to define mkEq, and it will not only serve as a function but it can also be used to pattern match

[Patrick Thomas]

Thank you. It is in large part just a translation from the OCaml code in "Handbook of Practical Logic and Automated Reasoning" by John Harrison [https://www.cl.cam.ac.uk/~jrh13/atp/index.html].

[Patrick Thomas]

I'm not sure how the axioms change if I change to De Bruijn indexing or locally nameless variables. Do they? Do pred_2 and pred_3 change?

[Trebor Huang]

You are probably going to have to figure out several subtleties if you go to dBI

[Trebor Huang]

The tradition in first order logic is to use named variables, and there're lots of irks and quirks that are well-studied, like eigenvariables and stuff

[Trebor Huang]

This is because variables never go into context. In type theories like Lean's, there may be something like x : nat before the turnstile; In first order logic, only propositions ever do. Hilbert-style systems even don't allow anything to go "before the turnstile", in some sense

[Trebor Huang]

A lot of the weird restrictions on free variable occurence in FOL can be very well explained by writing them out in type theoretic (aka higher order logic) style, and realizing that they do no more than implicitly handling non-propositional terms in the context

[Mario Carneiro]

I don't think non-propositional terms themselves account for free variable restrictions. The analogue of free variable restrictions in type theory is scope restriction: an expression can only depend on the variables in scope (it carries its context with it, and can't be used in a context which does not extend the original). Also, substitution needs to know to avoid variables under a lambda

[Mario Carneiro]

Here's a standard example of scope violation:

example {α} : ∃ x : α, ∀ y : α, x = y :=
begin
  existsi _,
  intro y,
  refl
end

The proof by refl (to prove ?m = y) would work if not for the fact that ?m has a scope that does not include y

[Patrick Thomas]

Is the code correct as is?

[Mario Carneiro]

no, it gives an error at refl:

invalid apply tactic, failed to unify
  ?m_1 = y
with
  ?m_3 = ?m_3

[Patrick Thomas]

I'm sorry, I meant the Haskell code.

[Patrick Thomas]

I have code to define formulas with locally nameless variables and convert them to and from named variables, but I'm not sure how to define substitution for them, that is, the result of replacing one term by another in a formula. I'm not sure I understand the advantage of the locally nameless terms in this case, because if you are trying to replace a free variable by one that will become bound, then don't you still have to check and alpha convert for that?

-- Adapted from https://boarders.github.io/posts/locally-nameless/

import Prelude hiding (False, True)
import qualified Prelude (Bool(..))

import Data.List
import Data.Map


-- Func "c" [] : A constant named c
data Term a = Var a
            | Func String [Term a]
              deriving (Show, Eq)

data Formula a = False
               | True
               | Pred String [Term a]        -- Pred "P" [] : A propositional variable named P
               | Not (Formula a)             -- ~ Formula
               | And (Formula a) (Formula a) -- Formula /\ Formula
               | Or (Formula a) (Formula a)  -- Formula \/ Formula
               | Imp (Formula a) (Formula a) -- Formula -> Formula
               | Iff (Formula a) (Formula a) -- Formula <-> Formula
               | Forall a (Formula a)        -- forall Var. Formula
               | Exists a (Formula a)        -- exists Var. Formula
                 deriving (Show, Eq)


-- The type of named variables.
type NV = String


-- The type of locally nameless variables.
data LN = F String -- The name of a free variable or a binding variable.
        | B Int    -- The De Bruijn index of a bound variable.
          deriving (Eq, Show)


{-
Translates a named variable formula to a locally nameless formula.
Keeps the name of each free variable and binding variable. Changes the name of
each bound variable to its De Bruijn index.
-}
formulaToLN :: Formula NV -> Formula LN
formulaToLN formula = go Data.Map.empty formula
  where
    {-
    The mapping is from the name of each binding variable to its De Bruijn
    index at the current depth.
    -}
    go :: Data.Map.Map String Int -> Formula NV -> Formula LN
    go _ False = False
    go _ True = True
    go env (Pred name terms) = Pred name (Data.List.map (termToLN env) terms)
      where
        -- Translates a named variable term to a locally nameless term.
        {-
        The mapping is from the name of each binding variable to its De Bruijn
        index at the current depth.
        -}
        termToLN :: Data.Map.Map String Int -> Term NV -> Term LN
        termToLN env (Var name) =
          case Data.Map.lookup name env of
            {-
            The variable name is a key in the map. Therefore it has the same
            name as a binding variable. Therefore it is a bound variable.
            Then the De Bruijn index of the binding variable it matches is
            used.
            -}
            Just index -> Var (B index)
            {-
            The variable name is not a key in the map. Therefore it is a free
            variable. Then its name is kept.
            -}
            Nothing -> Var (F name)
        termToLN env (Func name terms) = Func name (Data.List.map (termToLN env) terms)
    go env (Not p) = Not (go env p)
    go env (And p q) = And (go env p) (go env q)
    go env (Or p q) = Or (go env p) (go env q)
    go env (Imp p q) = Imp (go env p) (go env q)
    go env (Iff p q) = Iff (go env p) (go env q)
    go env (Forall name p) =
      {-
      Since a binding variable has been gone under, the De Bruijn index of
      each binding variable at the current depth is increased by 1 and the
      De Bruijn index of the encountered binding variable at the current
      depth is set to 0.
      -}
      let env' = Data.Map.insert name 0 (Data.Map.map (+1) env) in
      Forall (F name) (go env' p) -- The name of the binding variable is kept.
    go env (Exists name p) =
      let env' = Data.Map.insert name 0 (Data.Map.map (+1) env) in
      Exists (F name) (go env' p) -- The name of the binding variable is kept.


-- Translates a locally nameless formula to a named variable formula.
formulaFromLN :: Formula LN -> Formula NV
formulaFromLN formula = go Data.Map.empty formula
  where
    {-
    The mapping is from the De Bruijn index of each binding variable at the
    current depth to its name.
    -}
    go :: Data.Map.Map Int String -> Formula LN -> Formula NV
    go _ False = False
    go _ True = True
    go env (Pred name terms) = Pred name (Data.List.map (termFromLN env) terms)
      where
        -- Translates a locally nameless term to a named variable term.
        {-
        The mapping is from the De Bruijn index of each binding variable at the
        current depth to its name.
        -}
        termFromLN :: Data.Map.Map Int String -> Term LN -> Term NV
        termFromLN env (Var v) =
          case v of
            -- This is a free variable.
            F name  -> Var name
            -- This is a bound variable.
            B index -> case Data.Map.lookup index env of
                         Just name -> Var name
                         Nothing -> error "Bound variable has no binder."
        termFromLN env (Func name terms) = Func name (Data.List.map (termFromLN env) terms)
    go env (Not p) = Not (go env p)
    go env (And p q) = And (go env p) (go env q)
    go env (Or p q) = Or (go env p) (go env q)
    go env (Imp p q) = Imp (go env p) (go env q)
    go env (Iff p q) = Iff (go env p) (go env q)
    go env (Forall v p) =
      case v of
        B _ -> error "Bound variable at binding site."
        {-
        Since a binding variable has been gone under, the
        De Bruijn index of each binding variable at the
        current depth is increased by 1 and the De Bruijn
        index of the encountered binding variable at the
        current depth is set to 0.
        -}
        F name -> let env' = Data.Map.insert 0 name (Data.Map.mapKeysMonotonic (+1) env) in
                             Forall name (go env' p)
    go env (Exists v p) =
      case v of
        B _ -> error "Bound variable at binding site."
        F name -> let env' = Data.Map.insert 0 name (Data.Map.mapKeysMonotonic (+1) env) in
                             Exists name (go env' p)

[Patrick Thomas]

Or do you only replace bound variables, even in the natural deduction rules?

[Patrick Thomas]

That is, the a[b/c] instances in these rules:

ForallIntro: (gamma |- p) (x not free in gamma) => (gamma |- forall x. p)
ForallElim: (gamma |- forall x. p) (p admits t for x) => (gamma |- p[t/x])
ExistsIntro: (gamma |- p) (p admits x for t) => (gamma |- exists x. p [x/t])
ExistsElim: (gamma |- exists x. p) (gamma, p [y/x] |- q) (y not free in q) (y not free in gamma) => (gamma |- q)
Substitution: (gamma |- s = t) => (gamma |- p = p [t/s])

[Patrick Thomas]

The full code for reference:
nd.hs

[Trebor Huang]

You can read the paper by Conor McBride on locally nameless. It's easily understandable, and demonstrates exactly how it is beneficial.

[Trebor Huang]

In particular, every time you move inside a binder, you generate a free name (which, remarkably, doesn't require a monad or anything whatsoever) and substitute every occurence of the variable being unbound.

[Trebor Huang]

And when you move out, you abstract one named variable into an unnamed one, and bind it. This pair of instantiate and abstract functions enables clean and intuitive manipulation.

[Stuart Presnell]

Is that McBride & McKinna, “I am not a Number—I am a Free Variable” (https://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf)?

[Trebor Huang]

yep

[Trebor Huang]

The functional pearl version is slightly better in terms of formatting and convention, but that's a matter of taste.

[Patrick Thomas]

In the lambda calculus you are only substituting for variables bound by a lambda, correct? But in the rules for natural deduction, you are also substituting for variables that are not bound (by a forall or exists), like in the ExistsElim and Substitution rules listed above?

[Patrick Thomas]

Can the natural deduction rules be derived from the axioms of the first system?

[Patrick Thomas]

Are there any forums that are more broadly dedicated to mathematical logic and,or its implementation in code that would be better suited to these kinds of questions? I only know of this and https://math.stackexchange.com/.

[Patrick Thomas]

Updated to full classical FOL + equality:

import Data.List


data Term a = Var a
            | Func String [Term a] -- Func "c" [] : A constant named "c" ; -- Func "f" [v] : A function named "f" of one variable v
              deriving (Show, Eq)

data Formula a = Pred String [Term a] -- Pred "P" [] : A propositional variable named "P" ; Pred "Eq" [s, t] : s = t
               | Not (Formula a)
               | Imp (Formula a) (Formula a)
               | Forall a (Formula a)
                 deriving (Show, Eq)

newtype Theorem a = Theorem (Formula a)
                    deriving (Show, Eq)

{-
From "First Order Mathematical Logic" by Angelo Margaris:

An occurrence of a variable $v$ in a formula $P$ is bound if and only if
it occurs in a subformula of $P$ of the form $\forall v Q$. An occurrence
of $v$ in $P$ is free if and only if it is not a bound occurrence. The
variable $v$ is free or bound in $P$ according as it has a free or bound
 occurrence in $P$.

If $P$ is a formula, $v$ is a variable, and $t$ is a term, then $P(t/v)$ is
the result of replacing each free occurrence of $v$ in $P$ by an occurrence
of $t$.

If $v$ and $u$ are variables and $P$ is a formula, then $P$ admits $u$ for $v$
if and only if there is no free occurrence of $v$ in $P$ that becomes a
bound occurrence of $u$ in $P(u/v)$. If $t$ is a term, then $P$ admits $t$ for
$v$ if and only if $P$ admits for $v$ every variable in $t$.
-}


-- occursInTerm v t = there exists an occurrence of v in t.
occursInTerm :: String -> Term String -> Bool
occursInTerm v (Var v') = v == v'
occursInTerm v (Func _ terms) = any (occursInTerm v) terms

-- freeIn v p = there exists an occurrence of v in p that is free.
freeIn :: String -> Formula String -> Bool
freeIn v (Pred _ terms) = any (occursInTerm v) terms
freeIn v (Not p) = freeIn v p
freeIn v (Imp p q) = freeIn v p || freeIn v q
freeIn v (Forall v' p) = v /= v' && freeIn v p


{-
subInFormula p t v = p(t/v) = the result of replacing each free occurrence of
v in p by an occurrence of t.
-}
subInFormula :: Formula String -> Term String -> String -> Formula String
subInFormula (Pred name terms) t v = Pred name (Data.List.map (\t' -> subInTerm t' t v) terms)
  where
    {-
    subInTerm s t v = the result of replacing each occurrence of v in s by
    an occurrence of t.
    -}
    subInTerm :: Term String -> Term String -> String -> Term String
    subInTerm (Var v') t v = if v == v' then t else Var v'
    subInTerm (Func name terms) t v = Func name (Data.List.map (\t' -> subInTerm t' t v) terms)
subInFormula (Not p) t v = Not (subInFormula p t v)
subInFormula (Imp p q) t v = Imp (subInFormula p t v) (subInFormula q t v)
subInFormula (Forall v' p) t v = if v == v' then Forall v' p else Forall v' (subInFormula p t v)


{-
admitsVar p u v = p admits u for v = there is no free occurrence of
v in p that becomes a bound occurrence of u in p(u/v).
-}
admitsVar :: Formula String -> String -> String -> Bool
admitsVar p u v = go p u v []
  where
    go :: Formula String -> String -> String -> [String] -> Bool
    go (Pred _ terms) u v binders = not (any (occursInTerm v) terms) || elem v binders || notElem u binders
    go (Not p) u v binders = go p u v binders
    go (Imp p q) u v binders = go p u v binders && go q u v binders
    go (Forall v' p) u v binders = go p u v (v' : binders)

{-
admitsTerm p t v = p admits for v every variable in t.
-}
admitsTerm :: Formula String -> Term String -> String -> Bool
admitsTerm p (Var u) v = admitsVar p u v
admitsTerm p (Func _ terms) v = all (\t -> admitsTerm p t v) terms


-- Propositional calculus

-- |- (p -> (q -> p))
prop_1 :: Formula String -> Formula String -> Theorem String
prop_1 p q = Theorem (Imp p (Imp q p))

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
prop_2 :: Formula String -> Formula String -> Formula String -> Theorem String
prop_2 p q r = Theorem (Imp (Imp p (Imp q r)) (Imp (Imp p q) (Imp p r)))

-- |- ((~p -> ~q) -> (q -> p))
prop_3 :: Formula String -> Formula String -> Theorem String
prop_3 p q = Theorem (Imp (Imp (Not p) (Not q)) (Imp q p))

-- |- p & |- (p -> q) => |- q
mp :: Theorem String -> Theorem String -> Theorem String
mp (Theorem p) (Theorem (Imp p' q)) = if p == p' then Theorem q else error "mp"
mp _ _ = error "mp"


-- Predicate calculus

-- |- p => |- forall v. p
gen :: Theorem String -> String -> Theorem String
gen (Theorem p) v = Theorem (Forall v p)

-- |- ((forall v. (p -> q)) -> (forall v. p) -> (forall v. q))
pred_1 :: String -> Formula String -> Formula String -> Theorem String
pred_1 v p q = Theorem (Imp (Forall v (Imp p q)) (Imp (Forall v p) (Forall v q)))

-- |- (forall v. p -> p [t/v]) provided p admits t for v
pred_2 :: String -> Formula String -> Term String -> Theorem String
pred_2 v p t = if admitsTerm p t v then Theorem (Imp (Forall v p) (subInFormula p t v)) else error "pred_2"

-- |- (p -> forall v. p) provided v is not free in p
pred_3 :: String -> Formula String -> Theorem String
pred_3 v p = if not (freeIn v p) then Theorem (Imp p (Forall v p)) else error "pred_3"


-- Equality

itList2 :: (t1 -> t2 -> t3 -> t3) -> [t1] -> [t2] -> t3 -> t3
itList2 _ [] [] b = b
itList2 f (h1 : t1) (h2 : t2) b = f h1 h2 (itList2 f t1 t2 b)
itList2 _ _ _ _ = error "itList2"

-- |- t = t
eq_1 :: Term String -> Theorem String
eq_1 t = Theorem (Pred "Eq" [t, t])

-- |- s1 = t1 ==> ... ==> sn = tn ==> f(s1,..,sn) = f(t1,..,tn)
eq_2 :: String -> [Term String] -> [Term String] -> Theorem String
eq_2 f lefts rights = Theorem (
       itList2 (\s t p -> (Imp (Pred "Eq" [s, t]) p)) lefts rights
               (Pred "Eq" [(Func f lefts), (Func f rights)])
       )

-- |- s1 = t1 ==> ... ==> sn = tn ==> P(s1,..,sn) ==> P(t1,..,tn)
eq_3 :: String -> [Term String] -> [Term String] -> Theorem String
eq_3 p lefts rights = Theorem (
       itList2 (\s t p -> (Imp (Pred "Eq" [s, t]) p)) lefts rights
               (Imp (Pred p lefts) (Pred p rights))
       )

[Patrick Thomas]

I'm not certain how this code gets changed if de Bruijn indexes are used instead, especially the axioms.

[Trebor Huang]

For dBI's you get rid of all the occurence-related stuff, so all the admits disappear. (Or rather, takes another form.)

[Patrick Thomas]

Why do they disappear, or what other form do they take?

[Trebor Huang]

You can change admitsTerm to a constant True, because with dBI, accidental binding never happens.

[Patrick Thomas]

So it is safe in the logic to make all alpha equivalent terms equal? (Which I think happens in dBI?)

[Patrick Thomas]

The substitution just changes to different alpha equivalent terms to avoid accidental bindings right?

[Trebor Huang]

There is no alpha equivalence with dBI, there is only strict equality.

[Trebor Huang]

Substitution don't need to care about accidental bindings, there are none.

[Patrick Thomas]

I think I see. Thank you.

[Patrick Thomas]

How do you check if an arbitrary variable is free in a formula using de Bruijn indexes? That is, how do you implement the freeIn function that is used in pred_3?

[Mario Carneiro]

@Patrick Thomas something like this:

freeIn :: Int -> Formula -> Bool
freeIn v (Pred _ terms) = any (occursInTerm v) terms
freeIn v (Not p) = freeIn v p
freeIn v (Imp p q) = freeIn v p || freeIn v q
freeIn v (Forall p) = freeIn (v + 1) p

[Patrick Thomas]

Should there be an underscore after Forall, ie, freeIn v (Forall _ p) = freeIn (v + 1) p?

[Patrick Thomas]

No, I guess there wouldn't be, would there.

[Mario Carneiro]

only if you want to track the variable name as metadata, it's not part of the main de bruijn implementation

[Patrick Thomas]

So if a standalone variable becomes bound, its "name" before becoming bound is irrecoverably lost, because it gets changed to the index of its new binder?

[Mario Carneiro]

In pure de bruijn there are no names to begin with, so nothing is lost. In locally nameless, the variable name is lost when you abstract a named variable, so you put it in the binder's metadata (the var_name field in src#expr.pi)

[Patrick Thomas]

I'm not sure I understand. If there are no names to begin with, how do you compare variables? The v in the function freeIn isn't the name?

[Patrick Thomas]

Or maybe identifier is a better term than name?

[Mario Carneiro]

If you want to consider the numbers in de bruijn variables as "names", then it's not true that they are lost when abstracting, they just get bumped up by 1

[Mario Carneiro]

free variables in de bruijn are represented as variables with numbers greater than the current binder depth

[Patrick Thomas]

But if the get bound, they are lost right? For example, we start out with the standalone variable "5". If we want to bind it, it becomes lam 1?

[Patrick Thomas]

As in, x -> forall x.

[Mario Carneiro]

lam 0, but yes

[Mario Carneiro]

If it's about to be bound then it should already be variable 0

[Mario Carneiro]

so all you have to do is put the lam constructor on

[Patrick Thomas]

Why would it already be zero?

[Mario Carneiro]

because you already know the order that variables will be bound and have arranged the free vars to come in that order

[Mario Carneiro]

if you can't do that then de bruijn doesn't have any extra advantages compared to locally nameless

[Mario Carneiro]

but for example if you are generating the term by traversing an expression from the outside in, it is not hard to arrange things so that you know what variable is the next one to be bound

[Patrick Thomas]

You mean in going from named variables to de bruijn?

[Mario Carneiro]

yes

[Mario Carneiro]

which is probably something you have to do if you are writing a proof assistant and users write terms with named variables

[Patrick Thomas]

Do you have to keep track of all of this as a global state for the entire proof, or just individually for each separate term?

[Patrick Thomas]

Just for each term right?

[Patrick Thomas]

Would this be a useful kernal for a proof assistant? What would its drawbacks be in comparison to others? Are there any advantages?

[Patrick Thomas]

How do gen and pred_3 get modified? Do you no longer specify which variable to bind with the forall?

[Patrick Thomas]

Is that going to break the logic, that you can no longer pick which variable to bind?

[Trebor Huang]

You still get to specify a name, because free variables have names.

[Trebor Huang]

For pred_3, since v is not free, it doesn't matter.

[Trebor Huang]

In McBride's terminology, if you want to generalize the variable with name "x" in p, you simply compute p1 = abstract "x" p, and then the resulting formula is just Forall p1

[Trebor Huang]

The rule of thumb: Free variables always have names, bound variables always have no name; The only exception is when a variable is in the process of becoming bound/free, in which case it is free but has no name.

[Patrick Thomas]

Thank you.

[Patrick Thomas]

Oh, sorry, I meant using de bruijn indexes.

[Trebor Huang]

Pure de Bruijn indexes are indeed more difficult, but if you do some free variable permutation it should still work out. (Disclaimer: I never wrote anything in pure dBI)

[Patrick Thomas]

I see.

[Patrick Thomas]

Am I better off than using locally nameless?

[Mario Carneiro]

The other way to handle free variables in pure de bruijn is to never abstract them. So for example let's say you have a haskell like setup where there are some global definitions and a lambda operator, then the global definitions can be free de bruijn variables with arbitrary values, and the local variables are all bound in some scope. Then for the bound variables you always use numbers 0, 1, 2, .. based on binder depth, and for the free variables it doesn't matter what number you use since they will never be abstracted

[Patrick Thomas]

I'm sorry, I'm not sure I follow what you mean. This is for a proof checker? This changes the axioms somehow?

[Mario Carneiro]

If you want to construct a bunch of terms in lambda calculus like this (FOL terms work just the same way)

app = \x y -> x y
foo = app (\x -> app x) app
bar = \x -> foo x

then you can do that by setting, say app = #0, foo = #1 and bar = #2 and you get the de bruijn terms:

app = lam (lam (#1 #0))
foo = #0 (lam (#1 #0)) #0
bar = lam (#2 #0)

[Mario Carneiro]

so in this example #0 (lam (#1 #0)) #0 references the free variable #0 which is app, and we're never going to abstract it so we could do the same thing if it was some other number; if app was instead #n then the term would be #n (lam (#(n+1) #0)) #n

[Mario Carneiro]

so this is handling global definitions and definitions with bound variables using only pure de bruijn, not locally nameless

[Patrick Thomas]

How do we know that we are never going to abstract app?

[Patrick Thomas]

In the "I am not a number - I am a free variable" paper (https://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf), what does being a closed expression mean in the sentence "From now on, outside of these operations, we maintain the invariant that Expr is only used for closed expressions and that Scopes have just one dangling index." I understand the usual meaning to be no free variables, but earlier they say "Meanwhile, instantiate image turns a scope into an expression by replacing the outer de Bruijn index (initially B 0) with image, which we presume is closed. Of course, F name is closed, so we can use instantiate (F name) to invert abstract name." but F name is a free variable right?

[Patrick Thomas]

Also, how does pred_3 get implemented in the manner described in the paper, if v is not free in p, and thus has no name to refer to and may not even occur in p.

[Patrick Thomas]

pred_3 is basically saying you can go from forall x. (x = y) to forall x. (forall x. (x = y)) right? But now x has two binders, and I don't see how that can be expressed in either de bruijn or the method of the paper.

[Trebor Huang]

No, x doesn't have two binders. The two x are different. And this axiom is but an awkward way we dealt with binders back in the day when dBI's were not invented.

[Trebor Huang]

I think it is really worth writing something McBride-style to reformulate FOL with locally nameless. I'll search for related literature when I'm free.

[Mario Carneiro]

Patrick Thomas said:

In the "I am not a number - I am a free variable" paper (https://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf), what does being a closed expression mean in the sentence "From now on, outside of these operations, we maintain the invariant that Expr is only used for closed expressions and that Scopes have just one dangling index."

They explain this sentence a bit more elsewhere:

For the most part, we shall pretend that Expr is the type of closed expressions—those with no ‘dangling’ bound variables pointing out of scope, and that Scope has one dangling bound variable, called B 0 at the top level.

So "closed" here means having no free B variables; free F variables are allowed

[Mario Carneiro]

The equivalent of pred_3 says that imp p (forall p) where p is an Expr, i.e. it is a "closed" expression containing no free B variables. There are no side conditions required because the closedness of p suffices, and this is ensured using typing and good discipline in the McBride formulation

[Mario Carneiro]

Trebor Huang said:

No, x doesn't have two binders. The two x are different. And this axiom is but an awkward way we dealt with binders back in the day when dBI's were not invented.

By the way, I'm still in favor of using named variables for theorem proving, I don't think that it is simply an outdated technology. The reason is because the abstract and instantiate operations are linear in the size of the expression, and locally nameless has you doing those operations all the time, to inspect an expression or really do anything at all with it. That means that most basic operations are somewhere around O(n^2) which isn't great.

What's more, that's O(n^2) in the tree form of the expression, meaning that if your expression has high duplication (which is very common in dependent type theory) then you can get an exponential blowup here. I believe it is possible to treat the expression in a DAG-like way, but it is quite difficult to do so because the same subexpression can mean different things depending on what binders it is under (the same numbers can refer to different binders), so caching the result of an analysis or transformation has to include a large amount of context and if you aren't careful you will end up having so many contexts that you are back to exponential time.

[Mario Carneiro]

Patrick Thomas said:

How do we know that we are never going to abstract app?

Because we always know, at the point we read an app token, whether it is referring to a free or bound variable. If we had an expression like

baz = \app -> app

then we would first encounter the app binder, record that app is local variable #0, and then when we see the reference to app later we use #0 (so the generated term is lam #0). By comparison, if we had

baz = \x -> app

we would record that x is local variable #0 (and the binder depth is 1), and when we see a reference to app we search the context, see that it is not present, but find app in the global context (with number #0), so we increment that by the binder depth and produce lam #1.

[Patrick Thomas]

Trebor Huang said:

No, x doesn't have two binders. The two x are different. And this axiom is but an awkward way we dealt with binders back in the day when dBI's were not invented.

The two x are different? Why? Is that an implied specification in the logic?

[Patrick Thomas]

To be honest, I'm not sure I understand what gen and pred_3 do differently, or how they are used.

[Patrick Thomas]

I think MetaMath avoids the issues of free and bound variables by somehow finding a set of axioms that don't require conditions involving them? And then these axioms that I have can somehow be derived from those? And vice versa maybe?

[Patrick Thomas]

Kind of an aside, but I can see coming up with a set of tautologies, or statements that are valid in every model (if I remember the terminology right), but how did they go about figuring out axioms that also made the theory complete, even for propositional calculus, let alone predicate calculus?

[Patrick Thomas]

Patrick Thomas said:

To be honest, I'm not sure I understand what gen and pred_3 do differently, or how they are used.

I mean, I think one (I'm not sure which) is used to do something like:
Let x be any set that satisfies some condition. Prove x has some property. Obtain that all sets under the condition have that property.
But I'm not sure about the other.

[Trebor Huang]

• The propositional axioms remain the same, which should be clear to you.
• gen goes from p to Forall (abstract v p), note that the Forall constructor does not take a variable name; instead it takes a Scope in McBride's terminology.
• pred_1 shouldn't be a problem.
• pred_2 goes from Forall p to instantiate t p, no additional check needed.
• pred_3 goes from p to Forall p, no check needed, no additional computation needed.

[Patrick Thomas]

Thank you!

[Patrick Thomas]

Now I just need to understand why that works for pred_3 :)

[Mario Carneiro]

In pred_3, p is an Expr, meaning that it has no free B variables and in particular no B 0. Therefore Forall p will introduce a bound variable which has no occurrences in p, which is what we want. No variable lifting is required because everything is numbered from the innermost quantifiers out.

[Mario Carneiro]

Regarding completeness of propositional and predicate calculus, I don't think they were easy theorems to find but the theory was all worked out in the 40s or so

[Mario Carneiro]

Completeness of propositional calculus is pretty easy

[Mario Carneiro]

See https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem

[Patrick Thomas]

Why do we want a bound variable that has no occurrence in p? Isn't the condition that it just not be free in p?

[Mario Carneiro]

I mean not free

[Mario Carneiro]

In de bruijn that means that outside the scope of binders there are no B's, under 1 binder there is only B 0, under 2 binders there are B 0 and B 1 and so on

[Mario Carneiro]

The haskell type system doesn't enforce this in McBride's presentation, so you have to just maintain it as a discipline

[Mario Carneiro]

similarly for Scope, which is like Expr except it allows B 0 outside binders, B 0, B 1 under 1 binder and so on

[Patrick Thomas]

So in the statement as given, v can not be free in p right/ So this means it either falls under the scope of a forall v p, or does not occur in p at all right?

[Mario Carneiro]

Patrick Thomas said:

Why do we want a bound variable that has no occurrence in p? Isn't the condition that it just not be free in p?

Actually de bruijn doesn't really make a distinction here. There are no B variables in p that would refer to the variable introduced in Forall p

[Patrick Thomas]

Wait, oops, sorry, I thought we were talking about locally nameless...

[Mario Carneiro]

I am

[Mario Carneiro]

sorry to confuse

[Patrick Thomas]

No problem.

[Mario Carneiro]

the F variables don't really play a role here

[Mario Carneiro]

The "v not free in p" condition is expressed by the fact that p is an Expr even though Forall normally takes a Scopeas its argument

[Mario Carneiro]

every Expr is a Scope, but not vice versa; the Scopes that are not Exprs are exactly those with a free occurrence of B 0

[Patrick Thomas]

Isn't that a different definition of free? The named variable version means is not in the scope of a forall v or v not occurring. The locally nameless is that that there is no B0. I think?

[Mario Carneiro]

remember that when I say B 0, I mean B 1 when under a binder, B 2 under two binders and so on. Anything that would be interpreted as referring to the outer Forall binder we're introducing

[Mario Carneiro]

We don't have to worry about name clashes with a "forall v" somewhere in the term because that's the whole point of de bruijn variables

[Mario Carneiro]

If you had something like forall v, v this would be rendered in LN as Forall (B 0), which does not contain any free B 0 (because the only variable that appears is under 1 binder, and is not B 1)

[Mario Carneiro]

on the other hand forall w, v would be Forall (B 1) which does contain a free B 0

[Mario Carneiro]

(in locally nameless you might also translate that as Forall (F "v") but let's suppose this is a Scope)

[Mario Carneiro]

In the latter case it still does not contain a free B 0, so we would be allowed to use the pred_3 rule and get Forall (F "v") -> Forall (Forall (F "v")) which would be rendered as forall x, v -> forall y, forall x, v

[Patrick Thomas]

(deleted)

[Patrick Thomas]

(deleted)

[Patrick Thomas]

In the named variable version, we can use pred_3 to get Forall x. (Pred P x) -> Forall x. Forall x. (Pred P x) right? What does this actually mean? Trebor says the two x are different?

[Trebor Huang]

In locally nameless that's Forall (Pred P (B 0)) -> Forall (Forall (Pred P (B 0))).

[Trebor Huang]

The variable x refers to the inner Forall, hence B 0.

[Patrick Thomas]

And the x in the named version is only bound by the inside forall x?

[Trebor Huang]

Yes.

[Patrick Thomas]

Hmm.

[Trebor Huang]

(deleted)

[Patrick Thomas]

So forall x, forall x, x is the same as forall y, forall x, x (in the named version)?

[Trebor Huang]

Yep.

[Patrick Thomas]

Hmm.

[Trebor Huang]

Think of the indices as lines connecting the nameless variable to the binders. So in this case, B 0 means "A nameless variable with a line connecting it to the inner Forall. And think of named variables in the usual way. Then, a Scope would have some dangling lines.

Then abstract just takes a variable name, searches for all occurences of that variable, make them nameless, and draw a bunch of lines from them, so if you put the result under a Forall, you just collect the dangling lines and connect the other side to the Forall.

instantiate takes a Scope, which has dangling lines, and replace the other end of the dangling lines with the expression you give.

[Patrick Thomas]

So (in the named version) is the 'v not free in p' condition the same as 'v does not occur in p', given that forall x, forall x, x is the same as forall y, forall x, x.

[Trebor Huang]

Yep, that's the crux of alpha equivalence.

[Trebor Huang]

You can change the variable names anyway you like, as long as they still refer to the same things.

[Patrick Thomas]

Why doesn't the named version just state "does not occur in" instead of "not free in"?

[Patrick Thomas]

I mean, could it? Would it be the same logic?

[Trebor Huang]

Some versions do that, but then you need to additionally state the rules to make variable changes like forall x. forall x. P(x) to forall y. forall x. P(x)

[Patrick Thomas]

I see. A rule for alpha conversion?

[Trebor Huang]

Yes. I think one of the papers linked from the metamath homepage discusses that, but I can't remember which.

[Patrick Thomas]

I think I might see then. If there is no dangling B0 in p (required if p is an expression), then forall p does not bind any variable that occurs in p, because it just binds dangling B0's?

[Trebor Huang]

Yes that's right.

[Patrick Thomas]

Hence it is equivalent to the named version, given alpha equivalence?

[Trebor Huang]

Yeah, actually it is very much like quotienting the alpha equivalence

[Patrick Thomas]

Cool! Thank you!

[Trebor Huang]

It's like how the set of irreducible fractions corresponds to the equivalence classes of fractions under a/b ~ c/d where ad = bc

[Patrick Thomas]

Aside question: What does the octopus emoji mean?

[Huỳnh Trần Khanh]

It means congratulations.

[Patrick Thomas]

Huh. Ok. Thank you!

[Yaël Dillies]

"Impressive". It does a victory dance

[Patrick Thomas]

Is this a correct translation?

{-
First order mathematical logic using locally nameless variables.

Modified from "Functional Pearl: I am not a Number—I am a Free Variable"
by Conor McBride and James McKinna.
https://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf
-}

import Data.List

{-
Func "c" [] : A constant named "c"
Func "f" [v] : A function named "f" of one variable v
-}
data Term = F String -- A free variable
          | B Int -- A De Bruijn indexed bound variable
          | Func String [Term]
            deriving (Show, Eq)

{-
Assumed not to have any bound variables out of scope.

Pred "P" [] : A propositional variable named "P"
Pred "Eq" [s, t] : s = t
-}
data Formula = Pred String [Term]
             | Not Formula
             | Imp Formula Formula
             | Forall Scope
               deriving (Show, Eq)

{-
May have bound variables indexed one greater than the number of binders
above it.
-}
newtype Scope = Scope Formula
                deriving (Show, Eq)

newtype Theorem = Theorem Formula
                  deriving (Show, Eq)

{-
abstract v p = The result of changing each free variable named v in the formula
p to a bound variable indexed one greater than the number of binders above it.
-}
abstract :: String -> Formula -> Scope
abstract v p = Scope (nameTo 0 v p) where
  nameTo :: Int -> String -> Formula -> Formula
  nameTo outer v (Pred name terms) = Pred name (Data.List.map (nameTo' outer v) terms) where
    nameTo' :: Int -> String -> Term -> Term
    nameTo' outer v (F v') = if v == v' then B outer else F v'
    nameTo' _ _ (B index) = B index
    nameTo' outer v (Func name terms) = Func name (Data.List.map (nameTo' outer v) terms)
  nameTo outer v (Not p) = Not (nameTo outer v p)
  nameTo outer v (Imp p q) = Imp (nameTo outer v p) (nameTo outer v q)
  nameTo outer v (Forall (Scope p)) = Forall (Scope (nameTo (outer + 1) v p))

{-
instantiate t (Scope p) = The result of replacing each bound variable in the
formula p that has an index one greater than the number of binders above it
by the term t.
-}
instantiate :: Term -> Scope -> Formula
instantiate t (Scope p) = replace 0 t p where
  replace :: Int -> Term -> Formula -> Formula
  replace outer t (Pred name terms) = Pred name (Data.List.map (replace' outer t) terms) where
    replace' :: Int -> Term -> Term -> Term
    replace' _ _ (F name) = F name
    replace' outer t (B index) = if outer == index then t else B index
    replace' outer t (Func name terms) = Func name (Data.List.map (replace' outer t) terms)
  replace outer t (Not p) = Not (replace outer t p)
  replace outer t (Imp p q) = Imp (replace outer t p) (replace outer t q)
  replace outer t (Forall (Scope p)) = Forall (Scope (replace (outer + 1) t p))

[Mario Carneiro]

FYI nameTo does not need the v argument and nameTo' does not need outer or v because they are already in scope

[Patrick Thomas]

I see. Thank you.

[Mario Carneiro]

t needs to be a closed term in instantiate for this implementation to be correct; I guess that's a precondition but it should be spelled out in the comment

[Patrick Thomas]

Closed in the sense of no bound variables with indexes greater than the number of binders they are under?

[Mario Carneiro]

pred_1 should take two Scopes, or else the quantifiers are useless

[Mario Carneiro]

pred_2 should also take a Scope

[Mario Carneiro]

@Patrick Thomas Closed in the sense of no bound variables at all

[Mario Carneiro]

i.e. what you said for binders = 0

[Patrick Thomas]

Should I make a check in the code for that each time a term is taken as an argument?

[Patrick Thomas]

No bound variables with indexes greater than 0, or just no bound variables altogether?

[Mario Carneiro]

Well, in LN this is an invariant, so you would only need it as a debug assertion

[Patrick Thomas]

A term shouldn't have any bound variables right? Since there are no binders in a term?

[Patrick Thomas]

That is the invariant?

[Mario Carneiro]

in LN there is only one interesting notion of closed: under k binders, no B n appears for n >= k (closed term, Term, Formula) or for n >= k + 1 (term/formula with one free variable, Scope). General open terms (no restriction on the B's) only appear in the definition of abstract and instantiate.

[Mario Carneiro]

For a Term to be closed that means it has no B variables at all though since there are no binders in the term grammar

[Mario Carneiro]

Every top level function you have there which has a Term in its type signature requires a closed term

[Mario Carneiro]

similarly for every Formula and Theorem

[Patrick Thomas]

Thank you.

[Patrick Thomas]

Does pred_3 also need to take a scope?

[Mario Carneiro]

No, that one specifically should not

[Mario Carneiro]

that's the not free condition we talked about

[Patrick Thomas]

I see.

[Patrick Thomas]

Is there a way to avoid putting the check for each term, formula, theorem and scope at each pattern match? Maybe a way to associate it with the data type?

[Mario Carneiro]

If you make checkBounds' a global function, you can define checkTerm as checkBounds' 0. Yes these are the invariants

[Patrick Thomas]

{-
Hilbert style first order mathematical logic with equality using locally nameless variables.

Modified from "Functional Pearl: I am not a Number—I am a Free Variable"
by Conor McBride and James McKinna.
https://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf
-}

import Data.List
import Control.Exception


{-
Func "c" [] : A constant named "c"
Func "f" [v] : A function named "f" of one variable v
-}
data Term = F String -- A named free variable
          | B Int -- A De Bruijn indexed bound variable
          | Func String [Term]
            deriving (Show, Eq)

{-
Pred "P" [] : A propositional variable named "P"
Pred "Eq" [s, t] : s = t
-}
data Formula = Pred String [Term]
             | Not Formula
             | Imp Formula Formula
             | Forall Scope
               deriving (Show, Eq)

newtype Scope = Scope Formula
                deriving (Show, Eq)

newtype Theorem = Theorem Formula
                  deriving (Show, Eq)


{-
abstract v p = The result of changing each free variable named v in the formula
p to a bound variable that has an index equal to the number of binders above it.
-}
abstract :: String -> Formula -> Scope
abstract v p = Scope (nameTo 0 v p) where
  nameTo :: Int -> String -> Formula -> Formula
  nameTo outer v (Pred name terms) = Pred name (Data.List.map (nameTo' outer v) terms) where
    nameTo' :: Int -> String -> Term -> Term
    nameTo' outer v (F v') = if v == v' then B outer else F v'
    nameTo' _ _ (B index) = B index
    nameTo' outer v (Func name terms) = Func name (Data.List.map (nameTo' outer v) terms)
  nameTo outer v (Not p) = Not (nameTo outer v p)
  nameTo outer v (Imp p q) = Imp (nameTo outer v p) (nameTo outer v q)
  nameTo outer v (Forall (Scope p)) = Forall (Scope (nameTo (outer + 1) v p))

{-
instantiate t (Scope p) = The result of replacing each bound variable that has
an index equal to the number of binders above it in the formula p by the term t.
-}
instantiate :: Term -> Scope -> Formula
instantiate t (Scope p) = replace 0 t p where
  replace :: Int -> Term -> Formula -> Formula
  replace outer t (Pred name terms) = Pred name (Data.List.map (replace' outer t) terms) where
    replace' :: Int -> Term -> Term -> Term
    replace' _ _ (F name) = F name
    replace' outer t (B index) = if outer == index then t else B index
    replace' outer t (Func name terms) = Func name (Data.List.map (replace' outer t) terms)
  replace outer t (Not p) = Not (replace outer t p)
  replace outer t (Imp p q) = Imp (replace outer t p) (replace outer t q)
  replace outer t (Forall (Scope p)) = Forall (Scope (replace (outer + 1) t p))

{-
checkTermBounds outer t = The index of each bound variable in term t is
less than outer.
-}
checkTermBounds :: Int -> Term -> Bool
checkTermBounds _ (F _) = True
checkTermBounds outer (B index) = index < outer
checkTermBounds outer (Func _ terms) = Data.List.all (checkTermBounds outer) terms

{-
checkFormulaBounds outer p = The index of each bound variable in formula p is
less than the number of binders above it plus outer.
-}
checkFormulaBounds :: Int -> Formula -> Bool
checkFormulaBounds outer (Pred _ terms) = Data.List.all (checkTermBounds outer) terms
checkFormulaBounds outer (Not p) = checkFormulaBounds outer p
checkFormulaBounds outer (Imp p q) = checkFormulaBounds outer p && checkFormulaBounds outer q
checkFormulaBounds outer (Forall (Scope p)) = checkFormulaBounds (outer + 1) p

{-
checkTerm t = There is no bound variable in t.
-}
checkTerm :: Term -> Bool
checkTerm t = checkTermBounds 0 t

{-
checkFormula p = The index of each bound variable in the formula p is
less than the number of binders above it.
-}
checkFormula :: Formula -> Bool
checkFormula p = checkFormulaBounds 0 p

{-
checkScope (Scope p) = The index of each bound variable in the formula p is
less than the number of binders above it plus one.
-}
checkScope :: Scope -> Bool
checkScope (Scope p) = checkFormulaBounds 1 p


-- Propositional calculus

-- |- (p -> (q -> p))
prop_1 :: Formula -> Formula -> Theorem
prop_1 p q =
  assert (all checkFormula [p, q]) $
  Theorem (p `Imp` (q `Imp` p))

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
prop_2 :: Formula -> Formula -> Formula -> Theorem
prop_2 p q r =
  assert (all checkFormula [p, q, r]) $
  Theorem ((p `Imp` (q `Imp` r)) `Imp` ((p `Imp` q) `Imp` (p `Imp` r)))

-- |- ((~p -> ~q) -> (q -> p))
prop_3 :: Formula -> Formula -> Theorem
prop_3 p q =
  assert (all checkFormula [p, q]) $
  Theorem (((Not p) `Imp` (Not q)) `Imp` (q `Imp` p))

-- |- p & |- (p -> q) => |- q
mp :: Theorem -> Theorem -> Theorem
mp (Theorem p) (Theorem (p' `Imp` q)) =
  assert (all checkFormula [p, p', q]) $
  if p == p' then Theorem q else error "mp"
mp _ _ = error "mp"


-- Predicate calculus

-- |- p => |- forall v. p
gen :: Theorem -> String -> Theorem
gen (Theorem p) v =
  assert (checkFormula p) $
  Theorem (Forall (abstract v p))

-- |- ((forall v. (p -> q)) -> (forall v. p) -> (forall v. q))
pred_1 :: Scope -> Scope -> Theorem
pred_1 (Scope p) (Scope q) =
  assert (all checkScope [(Scope p), (Scope q)]) $
  Theorem ((Forall (Scope (p `Imp` q))) `Imp` ((Forall (Scope p)) `Imp` (Forall (Scope q))))

-- |- (forall v. p -> p [t/v]) provided p admits t for v
pred_2 :: Scope -> Term -> Theorem
pred_2 p t =
  assert (checkScope p) $
  assert (checkTerm t) $
  Theorem ((Forall p) `Imp` (instantiate t p))

-- |- (p -> forall v. p) provided v is not free in p
pred_3 :: Formula -> Theorem
pred_3 p =
  assert (checkFormula p) $
  Theorem (p `Imp` (Forall (Scope p)))


-- Equality

-- |- t = t
eq_1 :: Term -> Theorem
eq_1 t =
  assert (checkTerm t) $
  Theorem (Pred "Eq" [t, t])

-- |- s1 = t1 ==> ... ==> sn = tn ==> f(s1,..,sn) = f(t1,..,tn)
eq_2 :: String -> [Term] -> [Term] -> Theorem
eq_2 f ss ts =
  assert (all checkTerm ss) $
  assert (all checkTerm ts) $
  if (Data.List.length ss == Data.List.length ts) then
  -- eqs = [s1 = t1, ..., sn = tn]
  let eqs = Data.List.zipWith (\s t -> (Pred "Eq" [s, t])) ss ts in
  -- z = f(s1,..,sn) = f(t1,..,tn)
  let z = Pred "Eq" [(Func f ss), (Func f ts)] in
  Theorem (Data.List.foldr Imp z eqs)
  else error "eq_2"

-- |- s1 = t1 ==> ... ==> sn = tn ==> P(s1,..,sn) ==> P(t1,..,tn)
eq_3 :: String -> [Term] -> [Term] -> Theorem
eq_3 p ss ts =
  assert (all checkTerm ss) $
  assert (all checkTerm ts) $
  if (Data.List.length ss == Data.List.length ts) then
  -- eqs = [s1 = t1, ..., sn = tn]
  let eqs = Data.List.zipWith (\s t -> (Pred "Eq" [s, t])) ss ts in
  -- z = P(s1,..,sn) ==> P(t1,..,tn)
  let z = (Pred p ss) `Imp` (Pred p ts) in
  Theorem (Data.List.foldr Imp z eqs)
  else error "eq_3"

[Patrick Thomas]

Am I on the right track here? This is an attempt at implementing a proof checker for natural deduction, but I am not sure I have the predicate and equality rules right. For example, in the exists introduction, are we substituting a variable in for a term?

--import Data.List


{-
Func "c" [] : A constant named "c"
Func "f" [v] : A function named "f" of one variable v
-}
data Term = Var String
          | Func String [Term]
            deriving (Show, Eq)

{-
Pred "P" [] : A propositional variable named "P"
Pred "Eq" [s, t] : s = t
-}
data Formula = Bottom -- False
             | Top -- True
             | Pred String [Term]
             | Not Formula
             | And Formula Formula
             | Or Formula Formula
             | Imp Formula Formula
             | Iff Formula Formula
             | Forall String Formula
             | Exists String Formula
               deriving (Show, Eq)

data Proof = Assumption
           | ImpIntro Proof
           | ImpElim Formula Proof Proof
           | AndIntro Proof Proof
           | AndElimLeft Formula Proof
           | AndElimRight Formula Proof
           | NotIntro Proof
           | NotElim Formula Proof Proof
           | OrIntroLeft Proof
           | OrIntroRight Proof
           | OrElim Formula Formula Proof Proof Proof
           | BottomElim Proof
           | TopIntro
           | IffIntro Proof Proof
           | IffElimLeft Formula Proof Proof
           | IffElimRight Formula Proof Proof
           | Contradiction Proof
           | ForallIntro Proof
           | ForallElim Formula Term String Proof
           | ExistsIntro Formula Term Proof
           | ExistsElim Formula String String Proof Proof
           | Reflexivity
           | Substitution Term Term Proof
             deriving (Show, Eq)

type Context = [Formula]


occursIn :: String -> Term -> Bool
occursIn v (Var name) = v == name
occursIn v (Func _ terms) = any (occursIn v) terms


-- freeIn v p = there exists an occurrence of v in p that is free.
freeIn :: String -> Formula -> Bool
freeIn _ Bottom = False
freeIn _ Top = False
freeIn v (Pred _ terms) = any (occursIn v) terms
freeIn v (Not p) = freeIn v p
freeIn v (And p q) = freeIn v p || freeIn v q
freeIn v (Or p q) = freeIn v p || freeIn v q
freeIn v (Imp p q) = freeIn v p || freeIn v q
freeIn v (Iff p q) = freeIn v p || freeIn v q
freeIn v (Forall x p) = v /= x && freeIn v p
freeIn v (Exists x p) = v /= x && freeIn v p


-- Placeholders
sub p _ _ = p
admits _ _ _ = True


-- isProofOf a (b, c) = a is a proof of b |- c
isProofOf :: Proof -> (Context, Formula) -> Bool

{-
Assumption:
(gamma |- p) if p is in gamma
-}
isProofOf Assumption (gamma, p) = elem p gamma


{-
Implication introduction:
(gamma, p |- q) => (gamma |- p -> q)
-}
isProofOf (ImpIntro sub_proof) (gamma, (Imp p q)) =
  isProofOf sub_proof ((p : gamma), q)

{-
Implication elimination:
(gamma |- p -> q) && (gamma |- p) => (gamma |- q)
-}
isProofOf (ImpElim p sub_proof_1 sub_proof_2) (gamma, q) =
  isProofOf sub_proof_1 (gamma, (Imp p q)) &&
  isProofOf sub_proof_2 (gamma, p)


{-
And introduction:
(gamma |- p) && (gamma |- q) => (gamma |- p /\ q)
-}
isProofOf (AndIntro sub_proof_1 sub_proof_2) (gamma, (And p q)) =
  isProofOf sub_proof_1 (gamma, p) &&
  isProofOf sub_proof_2 (gamma, q)

{-
And elimination left:
(gamma |- p /\ q) => (gamma |- p)
-}
isProofOf (AndElimLeft q sub_proof) (gamma, p) =
  isProofOf sub_proof (gamma, (And p q))

{-
And elimination right:
(gamma |- p /\ q) => (gamma |- q)
-}
isProofOf (AndElimRight p sub_proof) (gamma, q) =
  isProofOf sub_proof (gamma, (And p q))


{-
Not introduction:
(gamma, p |- False) => (gamma |- ~p)
-}
isProofOf (NotIntro sub_proof) (gamma, (Not p)) =
  isProofOf sub_proof ((p : gamma), Bottom)

{-
Not elimination:
(gamma |- ~p) && (gamma |- p) => (gamma |- False)
-}
isProofOf (NotElim p sub_proof_1 sub_proof_2) (gamma, Bottom) =
  isProofOf sub_proof_1 (gamma, (Not p)) &&
  isProofOf sub_proof_2 (gamma, p)


{-
Or introduction left:
(gamma |- p) => (gamma |- p \/ q)
-}
isProofOf (OrIntroLeft sub_proof) (gamma, (Or p _)) =
  isProofOf sub_proof (gamma, p)

{-
Or introduction right:
(gamma |- q) => (gamma |- p \/ q)
-}
isProofOf (OrIntroRight sub_proof) (gamma, (Or _ q)) =
  isProofOf sub_proof (gamma, q)

{-
Or elimination:
(gamma |- p \/ q) &&
(gamma, p |- r) &&
(gamma, q |- r) =>
(gamma |- r)
-}
isProofOf (OrElim p q sub_proof_1 sub_proof_2 sub_proof_3) (gamma, r) =
  isProofOf sub_proof_1 (gamma, (Or p q)) &&
  isProofOf sub_proof_2 ((p : gamma), r) &&
  isProofOf sub_proof_3 ((q : gamma), r)


{-
Bottom elimination:
(gamma |- False) => (gamma |- p)
-}
isProofOf (BottomElim sub_proof) (gamma, _) =
  isProofOf sub_proof (gamma, Bottom)


{-
Top introduction:
(gamma |- True)
-}
isProofOf TopIntro (_, Top) = True


{-
Iff introduction:
(gamma, p |- q) && (gamma, q |- p) => (gamma |- p <=> q)
-}
isProofOf (IffIntro sub_proof_1 sub_proof_2) (gamma, (Iff p q)) =
  isProofOf sub_proof_1 ((p : gamma), q) &&
  isProofOf sub_proof_2 ((q : gamma), p)

{-
Iff elimination left:
(gamma |- p <-> q) && (gamma |- p) => (gamma |- q)
-}
isProofOf (IffElimLeft p sub_proof_1 sub_proof_2) (gamma, q) =
  isProofOf sub_proof_1 (gamma, (Iff p q)) &&
  isProofOf sub_proof_2 (gamma, p)

{-
Iff elimination right:
(gamma |- p <-> q) && (gamma |- q) => (gamma |- p)
-}
isProofOf (IffElimRight q sub_proof_1 sub_proof_2) (gamma, p) =
  isProofOf sub_proof_1 (gamma, (Iff p q)) &&
  isProofOf sub_proof_2 (gamma, q)


{-
Contradiction:
(gamma, ~p |- False) => (gamma |- p)
-}
isProofOf (Contradiction sub_proof) (gamma, p) =
  isProofOf sub_proof (((Not p) : gamma), Bottom)


{-
Forall introduction:
(gamma |- p) &&
(x not free in gamma) =>
(gamma |- forall x. p)
-}
isProofOf (ForallIntro sub_proof) (gamma, (Forall x p)) =
  isProofOf sub_proof (gamma, p) &&
  not (any (freeIn x) gamma)

{-
Forall elimination:
(gamma |- forall x. p) &&
(p admits t for x) =>
(gamma |- p[t/x])
-}
isProofOf (ForallElim p t x sub_proof) (gamma, p') =
  isProofOf sub_proof (gamma, (Forall x p)) &&
  admits p t x &&
  p' == (sub p t x)


{-
Exists introduction:
(gamma |- p) &&
(p admits x for t) =>
(gamma |- exists x. p [x/t])
-}
isProofOf (ExistsIntro p t sub_proof) (gamma, (Exists x p')) =
  isProofOf sub_proof (gamma, p) &&
  admits p x t &&
  p' == (sub p x t)

{-
Exists elimination:
(gamma |- exists x. p) &&
(gamma, p [y/x] |- q) &&
(y not free in q) &&
(y not free in gamma) =>
(gamma |- q)
-}
isProofOf (ExistsElim p y x sub_proof_1 sub_proof_2) (gamma, q) =
  isProofOf sub_proof_1 (gamma, (Exists x p)) &&
  isProofOf sub_proof_2 (((sub p (Var y) x) : gamma), q) &&
  not (freeIn y q) &&
  not (any (freeIn y) gamma)


{-
Reflexivity:
(gamma |- t = t)
-}
isProofOf Reflexivity (_, (Pred "Eq" [t, t'])) = t == t'

{-
Substitution:
(gamma |- s = t) => (gamma |- p = p [t/s])
-}
isProofOf (Substitution s t sub_proof) (gamma, (Pred "Eq" [p, p'])) =
  isProofOf sub_proof (gamma, (Pred "Eq" [s, t])) &&
  p' == (sub p t s)

isProofOf _ (_, _) = False

[Mario Carneiro]

Your rule for ForallIntro is problematic because you don't have a weakening rule: you won't be able to prove e.g. x = x |- forall x. True. One way to fix it is instead of checking not (any (freeIn x) gamma) you filter out everything from gamma which has a free x in the subproof.

[Mario Carneiro]

Your rule for ExistsIntro is backwards. You still want "p admits t for x" but the substitution is in the hypothesis, not the conclusion:

Exists introduction:
(gamma |- p [t/x]) &&
(p admits t for x) =>
(gamma |- exists x. p)

[Mario Carneiro]

Alternatively you can just add a weakening rule Weakening gamma' subproof that checks that gamma' is a subset of the input context gamma

[Patrick Thomas]

Mario Carneiro said:

Your rule for ForallIntro is problematic because you don't have a weakening rule: you won't be able to prove e.g. x = x |- forall x. True. One way to fix it is instead of checking not (any (freeIn x) gamma) you filter out everything from gamma which has a free x in the subproof.

Hmm. I was attempting to interpret the statement in Logic and Proof (https://leanprover.github.io/logic_and_proof/first_order_logic.html#the-universal-quantifier) A(x) => Forall x. A(x) provided x is not free in any uncancelled hypothesis. Did I interpret it wrong, or did I miss something in the text?

[Patrick Thomas]

I guess I was not sure how "not free in any uncancelled hypothesis" should translate. I'm not sure what you mean by "filter out everything from gamma which has a free x in the subproof.".

[Patrick Thomas]

That is, how do you code a check for a variable being free in a subproof?

[Patrick Thomas]

Is it the same as checking "if x is a free variable in p, then x is not free in any formula in gamma"?

[Patrick Thomas]

I guess you write a function pattern matching on the Proof type?

[Patrick Thomas]

I'm confused though, doesn't the gamma hold all of the uncancelled hypothesis? So why is it not, according to "Logic and Proof", just a check that x is not free in gamma?

[Patrick Thomas]

Is there a missing axiom in "Logic and Proof"?

[Trebor Huang]

Usually logic books treat gamma as a set, but you used a list. That's the difference.

[Trebor Huang]

Some books treat it as a list, and additionally includes what's called structural rules. Removing some of those gives you substructural logcis like affine, relevant, linear, noncommutive etc.

[Patrick Thomas]

So I don't need a weakening rule if I use a set instead of a list?

[Patrick Thomas]

If so, I'm not sure I see why that solves the example Mario posted?

[Trebor Huang]

You do need an additional weakening rule, because the not free in gamma requirements do not respect weakening.

[Trebor Huang]

All the other rules respect weakening, so using only those rules, if gamma |- p is provable, then starting the proof all over again with gamma ++ delta instead still gives you a proof.

[Trebor Huang]

The alternative as Mario points out, is, eg

(gamma |- p)
=> (gamma ++ delta |- p)

[Patrick Thomas]

So regardless if gamma is a set or a list, I need a weakening rule, correct? I guess I can see why it might be needed, but I'm curious why I haven't seen it listed in what I have been able to find for predicate calculus in natural deduction.

[Patrick Thomas]

Would you happen to have a reference that includes it?

[Trebor Huang]

In pure propositional calculus you don't need it, as I argued above. In the "tree form" of natural deduction it is also not needed, because weakening is automatic.

[Patrick Thomas]

What is the tree form?

[Trebor Huang]

 p     q
-------
  p & q

Note that this proves p, q |- p & q, but the |- doesn't appear.

[Patrick Thomas]

Oh, I thought they were just implicit when I saw that.

[Patrick Thomas]

So you don't have assumptions?

[Trebor Huang]

You do, the assumptions are exactly the leaves of the derivation tree, p and q in this case.

[Patrick Thomas]

Those aren't proofs of p and q?

[Trebor Huang]

No.

To formulate this properly, you need the rule for conjunction to be

(gamma |- p) &&
(delta |- q) =>
(gamma ++ delta |- p and q)

Because the leaves of the tree sitting on p and q, respectively, are combined.

[Trebor Huang]

But you also need to use a set, because, well, leaves don't have an order.

[Patrick Thomas]

How would the proof for the example Mario gave work in that instance?

[Patrick Thomas]

Somehow combine x = x |- ? and |- forall x, true?

[Patrick Thomas]

I wonder if this is a better way to formulate it. I could use functions that take a proof of p and a proof of q and return a proof of p /\ q and not have to compare the gammas.

[Patrick Thomas]

Just combine them.

[Patrick Thomas]

Forward instead of backwards reasoning I guess.

[Patrick Thomas]

Is this Sequent natural deduction?

[Patrick Thomas]

What would the set of rules need to be to match the logic in lean?

[Patrick Thomas]

What I would like to have or create is a proof assistant for first order logic and axiomatic set theory, that has source code freely and publicly available (Mizar's doesn't seem to be?) that is easy to read and understand (probably preferably Haskell or similar), is close to standard texts or explains the reason for each deviation and why it is valid, and allows proofs to be constructed in a style such as

1. statement, justification from axiom ax_1 using substitutions p, q.
2. statement, justification from theorem th_1 using substitutions r, s and line 1.
3. statement, justification from rule_1 using substitutions t, u and line 2.
   I think meta math may be the closest to this?, but the last time I tried (admittedly some time ago) I couldn't figure out the gui assistant, and I couldn't find the api that I assumed it used to create my own. I also wish the axioms for the logic were closer to the standard texts, although I think I may understand why they are not. It would be cool if the standard texts could be derived from them and vice versa. I'm not sure if I can write proofs in it in the form shown above? I might not mind working on it to achieve this, if that is possible.
   The reason for the Haskell code is in part to help understand the logic rules more clearly, and in part an attempt at a start to create the above.

[Johan Commelin]

MM0 has a vscode extension. Maybe that solves your gui issues?

[Patrick Thomas]

Maybe. I'll take a look.

[Patrick Thomas]

Thank you.

[Patrick Thomas]

My initial impression is that it may be more complicated than I had hoped, maybe in part because it starts at a lower level? Nice tutorial video.

[Trebor Huang]

An aside: If you do that in Haskell and use the mechanisms of Haskell to create definitions, then during typechecking the definitions definitely will blow up exponentially. So you need something to prevent it from happening...

[Trebor Huang]

Like, if you implement a definition hierarchy as described in Metamath or Lean, it will get expanded all the way down when your checker tries to see if two terms are equal.

[Patrick Thomas]

So you need something in the axioms of the logic to handle definitions?

[Patrick Thomas]

How is it addressed in Lean and MetaMath?

[Trebor Huang]

Lean has the reducible/semireducible/opaque distinction, and other well-established stuff in type theory. Metamath does not have "definitions". Every new definition is actually little axioms, with additional checks which are detailed on the website.

[Patrick Thomas]

It looks like in mm0 definitions are part of the formal grammar.

[Patrick Thomas]

Is there a resource that explains more in depth the theory of definitions in mm0?

[Patrick Thomas]

Aside from issues of efficiency, just to ensure my understanding, is this a correct implementation of first order logic with equality? Especially the admitsVar and admitsTerm functions? Thank you.

{-
Hilbert style first order mathematical logic with equality using named variables.

Modified from "Handbook of Practical Logic and Automated Reasoning" by John Harrison.
https://www.cl.cam.ac.uk/~jrh13/atp/index.html
-}

import Data.List

{-
Func "c" [] : A constant named "c"
Func "f" [v] : A function named "f" of one variable v
-}
data Term = Var String
          | Func String [Term]
            deriving (Show, Eq)

{-
Pred "P" [] : A propositional variable named "P"
Pred "Eq" [s, t] : s = t
-}
data Formula = Pred String [Term]
             | Not Formula
             | Imp Formula Formula
             | Forall String Formula
               deriving (Show, Eq)

newtype Theorem = Theorem Formula
                  deriving (Show, Eq)

{-
From "First Order Mathematical Logic" by Angelo Margaris:

An occurrence of a variable $v$ in a formula $P$ is bound if and only if
it occurs in a subformula of $P$ of the form $\forall v Q$. An occurrence
of $v$ in $P$ is free if and only if it is not a bound occurrence. The
variable $v$ is free or bound in $P$ according as it has a free or bound
occurrence in $P$.

If $P$ is a formula, $v$ is a variable, and $t$ is a term, then $P(t/v)$ is
the result of replacing each free occurrence of $v$ in $P$ by an occurrence
of $t$.

If $v$ and $u$ are variables and $P$ is a formula, then $P$ admits $u$ for $v$
if and only if there is no free occurrence of $v$ in $P$ that becomes a
bound occurrence of $u$ in $P(u/v)$. If $t$ is a term, then $P$ admits $t$ for
$v$ if and only if $P$ admits for $v$ every variable in $t$.
-}

-- occursIn v t = there exists an occurrence of v in t.
occursIn :: String -> Term -> Bool
occursIn v (Var v') = v == v'
occursIn v (Func _ terms) = any (occursIn v) terms

-- freeIn v p = there exists an occurrence of v in p that is free.
freeIn :: String -> Formula -> Bool
freeIn v (Pred _ terms) = any (occursIn v) terms
freeIn v (Not p) = freeIn v p
freeIn v (Imp p q) = freeIn v p || freeIn v q
freeIn v (Forall v' p) = v /= v' && freeIn v p

{-
subIn p t v = p(t/v) = the result of replacing each free occurrence of
v in p by an occurrence of t.
-}
subIn :: Formula -> Term -> String -> Formula
subIn (Pred name terms) t v = Pred name (Data.List.map (\t' -> subInTerm t' t v) terms) where
  {-
  subInTerm t' t v = t'(t/v) = the result of replacing each occurrence of
  v in t' by an occurrence of t.
  -}
  subInTerm :: Term -> Term -> String -> Term
  subInTerm (Var v') t v = if v == v' then t else Var v'
  subInTerm (Func name terms) t v = Func name (Data.List.map (\t' -> subInTerm t' t v) terms)
subIn (Not p) t v = Not (subIn p t v)
subIn (Imp p q) t v = Imp (subIn p t v) (subIn q t v)
subIn (Forall v' p) t v = if v == v' then Forall v' p else Forall v' (subIn p t v)

{-
admitsVar p u v = p admits u for v = there is no free occurrence of
v in p that becomes a bound occurrence of u in p(u/v).
-}
admitsVar :: Formula -> String -> String -> Bool
admitsVar p u v = go p u v [] where
  go :: Formula -> String -> String -> [String] -> Bool
  go (Pred _ terms) u v binders = not (any (occursIn v) terms)
                               || elem v binders
                               || notElem u binders
  go (Not p) u v binders = go p u v binders
  go (Imp p q) u v binders = go p u v binders && go q u v binders
  go (Forall v' p) u v binders = go p u v (v' : binders)

{-
admitsTerm p t v = p admits for v every variable in t.
-}
admitsTerm :: Formula -> Term -> String -> Bool
admitsTerm p (Var u) v = admitsVar p u v
admitsTerm p (Func _ terms) v = all (\t -> admitsTerm p t v) terms


-- Propositional calculus

-- |- (p -> (q -> p))
prop_1 :: Formula -> Formula -> Theorem
prop_1 p q = Theorem (p `Imp` (q `Imp` p))

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
prop_2 :: Formula -> Formula -> Formula -> Theorem
prop_2 p q r = Theorem ((p `Imp` (q `Imp` r)) `Imp` ((p `Imp` q) `Imp` (p `Imp` r)))

-- |- ((~p -> ~q) -> (q -> p))
prop_3 :: Formula -> Formula -> Theorem
prop_3 p q = Theorem (((Not p) `Imp` (Not q)) `Imp` (q `Imp` p))

-- |- p & |- (p -> q) => |- q
mp :: Theorem -> Theorem -> Theorem
mp (Theorem p) (Theorem (p' `Imp` q)) = if p == p' then Theorem q else error "mp"
mp _ _ = error "mp"


-- Predicate calculus

-- |- p => |- forall v. p
gen :: Theorem -> String -> Theorem
gen (Theorem p) v = Theorem (Forall v p)

-- |- ((forall v. (p -> q)) -> (forall v. p) -> (forall v. q))
pred_1 :: String -> Formula -> Formula -> Theorem
pred_1 v p q = Theorem ((Forall v (p `Imp` q)) `Imp` ((Forall v p) `Imp` (Forall v q)))

-- |- (forall v. p -> p [t/v]) provided p admits t for v
pred_2 :: String -> Formula -> Term -> Theorem
pred_2 v p t = if admitsTerm p t v then Theorem ((Forall v p) `Imp` (subIn p t v)) else error "pred_2"

-- |- (p -> forall v. p) provided v is not free in p
pred_3 :: String -> Formula -> Theorem
pred_3 v p = if not (freeIn v p) then Theorem (p `Imp` (Forall v p)) else error "pred_3"


-- Equality

-- |- t = t
eq_1 :: Term -> Theorem
eq_1 t = Theorem (Pred "Eq" [t, t])

-- |- s1 = t1 ==> ... ==> sn = tn ==> f(s1,..,sn) = f(t1,..,tn)
eq_2 :: String -> [Term] -> [Term] -> Theorem
eq_2 f ss ts = if Data.List.length ss == Data.List.length ts then
               -- eqs = [s1 = t1, ..., sn = tn]
               let eqs = Data.List.zipWith (\s t -> (Pred "Eq" [s, t])) ss ts in
               -- z = f(s1,..,sn) = f(t1,..,tn)
               let z = Pred "Eq" [(Func f ss), (Func f ts)] in
               Theorem (Data.List.foldr Imp z eqs)
               else error "eq_2"

-- |- s1 = t1 ==> ... ==> sn = tn ==> P(s1,..,sn) ==> P(t1,..,tn)
eq_3 :: String -> [Term] -> [Term] -> Theorem
eq_3 p ss ts = if Data.List.length ss == Data.List.length ts then
               -- eqs = [s1 = t1, ..., sn = tn]
               let eqs = Data.List.zipWith (\s t -> (Pred "Eq" [s, t])) ss ts in
               -- z = P(s1,..,sn) ==> P(t1,..,tn)
               let z = (Pred p ss) `Imp` (Pred p ts) in
               Theorem (Data.List.foldr Imp z eqs)
               else error "eq_3"

[Mario Carneiro]

The theory of definitions in MM0 is described in the Metamath Zero paper (Fig. 3, p.11). It's basically a pared-down version of lean's defeq judgment: there is a proof rule that lets you replace an expression with one obtained by unfolding some definition inside the expression.

[Patrick Thomas]

Thank you. I saw that, but I had trouble following the notation, and I'm not familiar with multi sorted FOL.

[Patrick Thomas]

That is, I don't know if it being multi sorted is part of the notation.

[Patrick Thomas]

I guess I should add some context :)

{-
Hilbert style first order mathematical logic with equality using named variables.

Modified from "Handbook of Practical Logic and Automated Reasoning" by John Harrison.
https://www.cl.cam.ac.uk/~jrh13/atp/index.html
-}


{-
Func "c" [] : A constant named "c"
Func "f" [v] : A function named "f" of one variable v
-}
data Term = Var String
          | Func String [Term]
            deriving (Show, Eq)

{-
Pred "P" [] : A propositional variable named "P"
Pred "Eq" [s, t] : s = t
-}
data Formula = Pred String [Term]
             | Not Formula
             | Imp Formula Formula
             | Forall String Formula
               deriving (Show, Eq)

type Context = [Formula]

data Theorem = Theorem Context Formula
               deriving (Show, Eq)

{-
From "First Order Mathematical Logic" by Angelo Margaris:

An occurrence of a variable $v$ in a formula $P$ is bound if and only if
it occurs in a subformula of $P$ of the form $\forall v Q$. An occurrence
of $v$ in $P$ is free if and only if it is not a bound occurrence. The
variable $v$ is free or bound in $P$ according as it has a free or bound
occurrence in $P$.

If $P$ is a formula, $v$ is a variable, and $t$ is a term, then $P(t/v)$ is
the result of replacing each free occurrence of $v$ in $P$ by an occurrence
of $t$.

If $v$ and $u$ are variables and $P$ is a formula, then $P$ admits $u$ for $v$
if and only if there is no free occurrence of $v$ in $P$ that becomes a
bound occurrence of $u$ in $P(u/v)$. If $t$ is a term, then $P$ admits $t$ for
$v$ if and only if $P$ admits for $v$ every variable in $t$.
-}

-- occursIn v t = there exists an occurrence of v in t.
occursIn :: String -> Term -> Bool
occursIn v (Var v') = v == v'
occursIn v (Func _ terms) = any (occursIn v) terms

-- freeIn v p = there exists an occurrence of v in p that is free.
freeIn :: String -> Formula -> Bool
freeIn v (Pred _ terms) = any (occursIn v) terms
freeIn v (Not p) = freeIn v p
freeIn v (Imp p q) = freeIn v p || freeIn v q
freeIn v (Forall v' p) = v /= v' && freeIn v p

{-
subIn p t v = p(t/v) = the result of replacing each free occurrence of
v in p by an occurrence of t.
-}
subIn :: Formula -> Term -> String -> Formula
subIn (Pred name terms) t v = Pred name (map (\t' -> subInTerm t' t v) terms) where
  {-
  subInTerm t' t v = t'(t/v) = the result of replacing each occurrence of
  v in t' by an occurrence of t.
  -}
  subInTerm :: Term -> Term -> String -> Term
  subInTerm (Var v') t v = if v == v' then t else Var v'
  subInTerm (Func name terms) t v = Func name (map (\t' -> subInTerm t' t v) terms)
subIn (Not p) t v = Not (subIn p t v)
subIn (Imp p q) t v = Imp (subIn p t v) (subIn q t v)
subIn (Forall v' p) t v = if v == v' then Forall v' p else Forall v' (subIn p t v)

{-
admitsVar p u v = p admits u for v = there is no free occurrence of
v in p that becomes a bound occurrence of u in p(u/v).
-}
admitsVar :: Formula -> String -> String -> Bool
admitsVar p u v = go p u v [] where
  go :: Formula -> String -> String -> [String] -> Bool
  go (Pred _ terms) u v binders = not (any (occursIn v) terms)
                               || elem v binders
                               || notElem u binders
  go (Not p) u v binders = go p u v binders
  go (Imp p q) u v binders = go p u v binders && go q u v binders
  go (Forall v' p) u v binders = go p u v (v' : binders)

{-
admitsTerm p t v = p admits for v every variable in t.
-}
admitsTerm :: Formula -> Term -> String -> Bool
admitsTerm p (Var u) v = admitsVar p u v
admitsTerm p (Func _ terms) v = all (\t -> admitsTerm p t v) terms


-- Assumption

assume :: Context -> Formula -> Theorem
assume gamma p = if elem p gamma then Theorem gamma p else error "assume"


-- Propositional calculus

-- |- (p -> (q -> p))
prop_1 :: Context -> Formula -> Formula -> Theorem
prop_1 gamma p q = Theorem gamma (p `Imp` (q `Imp` p))

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
prop_2 :: Context -> Formula -> Formula -> Formula -> Theorem
prop_2 gamma p q r = Theorem gamma ((p `Imp` (q `Imp` r)) `Imp` ((p `Imp` q) `Imp` (p `Imp` r)))

-- |- ((~p -> ~q) -> (q -> p))
prop_3 :: Context -> Formula -> Formula -> Theorem
prop_3 gamma p q = Theorem gamma (((Not p) `Imp` (Not q)) `Imp` (q `Imp` p))

-- |- p & |- (p -> q) => |- q
mp :: Theorem -> Theorem -> Theorem
mp (Theorem gamma p) (Theorem gamma' (p' `Imp` q))
       = if gamma == gamma' && p == p' then Theorem gamma q else error "mp"
mp _ _ = error "mp"


-- Predicate calculus

-- |- p => |- forall v. p
gen :: Theorem -> String -> Theorem
gen (Theorem gamma p) v = Theorem gamma (Forall v p)

-- |- ((forall v. (p -> q)) -> (forall v. p) -> (forall v. q))
pred_1 :: Context -> String -> Formula -> Formula -> Theorem
pred_1 gamma v p q = Theorem gamma ((Forall v (p `Imp` q)) `Imp` ((Forall v p) `Imp` (Forall v q)))

-- |- (forall v. p -> p [t/v]) provided p admits t for v
pred_2 :: Context -> String -> Formula -> Term -> Theorem
pred_2 gamma v p t = if admitsTerm p t v then Theorem gamma ((Forall v p) `Imp` (subIn p t v)) else error "pred_2"

-- |- (p -> forall v. p) provided v is not free in p
pred_3 :: Context -> String -> Formula -> Theorem
pred_3 gamma v p = if not (freeIn v p) then Theorem gamma (p `Imp` (Forall v p)) else error "pred_3"


-- Equality

-- |- t = t
eq_1 :: Context -> Term -> Theorem
eq_1 gamma t = Theorem gamma (Pred "Eq" [t, t])

-- |- s1 = t1 ==> ... ==> sn = tn ==> f(s1,..,sn) = f(t1,..,tn)
eq_2 :: Context -> String -> [Term] -> [Term] -> Theorem
eq_2 gamma f ss ts = if length ss == length ts then
                     -- eqs = [s1 = t1, ..., sn = tn]
                     let eqs = zipWith (\s t -> (Pred "Eq" [s, t])) ss ts in
                     -- z = f(s1,..,sn) = f(t1,..,tn)
                     let z = Pred "Eq" [(Func f ss), (Func f ts)] in
                     Theorem gamma (foldr Imp z eqs)
                     else error "eq_2"

-- |- s1 = t1 ==> ... ==> sn = tn ==> P(s1,..,sn) ==> P(t1,..,tn)
eq_3 :: Context -> String -> [Term] -> [Term] -> Theorem
eq_3 gamma p ss ts = if length ss == length ts then
                     -- eqs = [s1 = t1, ..., sn = tn]
                     let eqs = zipWith (\s t -> (Pred "Eq" [s, t])) ss ts in
                     -- z = P(s1,..,sn) ==> P(t1,..,tn)
                     let z = (Pred p ss) `Imp` (Pred p ts) in
                     Theorem gamma (foldr Imp z eqs)
                     else error "eq_3"

[Patrick Thomas]

Do formulas in the context need to be closed, that is have no free variables? Or do the predicate rules have to add a check that a variable is not free in the context?

[Patrick Thomas]

For example, I could have:
x = 5 |- x = 5 from assume
x = 5 | forall x. x = 5 from gen
which I don't thing makes sense.

[Mario Carneiro]

Sorry, I got pulled away. Here's a variation on that definition schema that may fit better with your formulation:

data FuncDef = FuncDef {
  name :: String,
  arity :: Integer,
  defn :: Maybe ([String], Term) }

data PredDef = PredDef {
  name :: String,
  arity :: Integer,
  defn :: Maybe ([String], Formula) }

• A global context is a (Map String FuncDef, Map String PredDef) tracking definitions of functions and predicates.
• For a Term or Formula to be well formed, it must only use functions/predicates in the context and the arity must match.
• You can extend the context with a function if:
  • The function has not already been defined
  • The arity is nonnegative
  • The definition is either
    • not provided (it is an axiomatic term constructor), or
    • the [String] is a list of length arity, and the Term contains no free variables not in the list
• (similarly for predicates)

[Mario Carneiro]

For your last question, you normally wouldn't have a context in the hilbert-style axiomatization you are using. If you want to have one anyway, I would say that the formulas in the context should all be closed, and/or they are treated as universally quantified over everything. In such a situation, x = 5 |- forall x. x = 5 is a reasonable derivation

[Patrick Thomas]

You certainly don't have to apologize, I really appreciate any of your time.
That is what I had initially assumed, and then I was reminded of the deduction theorem, which while a meta theorem, seems to talk about a Hilbert system with a context?

[Patrick Thomas]

So then there is a rule to somehow allow a definition from this global context to be unfolded in a term or formula?

[Patrick Thomas]

What do [String] and Term and Formula represent, get used for, in the Maybes?

[Patrick Thomas]

The list of variables occurring in the Term and in the Formula?

[Patrick Thomas]

So name is the name of the function/predicate, arity is the number of variables in the function/predicate, [String] in def is the list of variables in the function/predicate, and Term/Formula in def is the actual Function or Formula we are giving a name to? What is the difference in the name in FuncDef and PredDef and the String in the global context?

[Mario Carneiro]

What is the difference in the name in FuncDef and PredDef and the String in the global context?

They are the same. You can probably do without name if you like, but it is nice to have it stored explicitly sometimes

[Mario Carneiro]

For example, we could define ne as PredDef "ne" 2 (Just (["x", "y"], Not (Pred "eq" [Var "x", Var "y"])))

[Patrick Thomas]

I see. Why is it a Maybe?

[Mario Carneiro]

We would define eq as PredDef "Eq" 2 Nothing

[Mario Carneiro]

You have to actually check that terms are well formed now, because you don't want definitions to reference themselves or future definitions

[Mario Carneiro]

so even axiomatic term constructors like Eq need to have declarations

[Patrick Thomas]

I see. So what happens to the definitions of Term and Formula? Do they change?

[Patrick Thomas]

I'm guessing not?

[Patrick Thomas]

How do these get used, and how does it avoid this:
"
An aside: If you do that in Haskell and use the mechanisms of Haskell to create definitions, then during typechecking the definitions definitely will blow up exponentially. So you need something to prevent it from happening...
"

[Mario Carneiro]

The blowup problem is avoided because if you have a definition of something complicated like Pred "IsPerfectoidSpace" [X] then it is represented as just that, not the thing it unfolds to

[Mario Carneiro]

things are only unfolded when you need it, via a new primitive unfolding rule

[Patrick Thomas]

Oh. I see. If you don't mind, what would that rule look like in my formulation?

[Mario Carneiro]

The unfolding rule says P(t1, ... tn) = p[t1/x1, ..., tn/xn] assuming the ti are free for xi in p and P(x1, ..., xn) := p

[Mario Carneiro]

although if you have substitution rules you can probably get away with just the equality P(x1, ..., xn) = p

[Patrick Thomas]

The := means the string p maps to the predicate/function P in the global context?

[Patrick Thomas]

Do Formula and Term get extended somehow?

[Mario Carneiro]

The other way around; P(x1, ..., xn) := p means lookup (snd globalCtx) P = PredDef P n (Just ([x1, ..., xn], p))

[Mario Carneiro]

Formula and Term are not extended, because we are reusing the Func and Pred constructors already in the grammar to represent definitions

[Patrick Thomas]

I'm sorry, would you mind giving an example of how ne is used inside a formula?

[Patrick Thomas]

That is, how would you construct a Formula that uses ne?

[Patrick Thomas]

Pred "ne" [Var "u", Var "v"]?

[Patrick Thomas]

Then to unfold it you look up "ne" in the map of predicates, check that its arity is equal to length [Var "u", Var "v"], check that x admits u and y admits v in Not (Pred "Eq" [Var "x", Var "y"]), then produce Theorem (Pred "Eq" [Pred "ne" [Var "u", Var "v"]], Not (Pred "Eq" [Var "u", Var "v"])])?

[Mario Carneiro]

Yes, that's how you construct it. To unfold it, you would use a rule unfold : String -> [Term] -> Theorem such that unfold "ne" [Var "u", Var "v"] = Theorem (Iff (Pred "ne" [Var "u", Var "v"]) (Not (Pred "Eq" [Var "u", Var "v"])))

[Patrick Thomas]

With the conditions on the matching arity and admits?

[Mario Carneiro]

The arity conditions exist on everything - to construct a Term in the first place you have to have the right arity

[Mario Carneiro]

one way to do this is to add a "smart constructor" for Pred

[Mario Carneiro]

not sure what you mean by admits

[Patrick Thomas]

I think free for in your terminology.

[Mario Carneiro]

ah yes, you need that for the version that does a substitution

[Mario Carneiro]

the simpler version can just have the type unfold : String -> Theorem and just uses the list of variables intrinsic to the predicate definition

[Patrick Thomas]

So in the simpler version you would just have Theorem (Iff (Pred "ne" [Var "x", Var "y"]) (Not (Pred "Eq" [Var "x", Var "y"])))? How would that then get used to replace the Pred "ne" [Var "u", Var "v"]

[Patrick Thomas]

Use the equality axioms?

[Patrick Thomas]

Then could you just as easily replace Term and Formula by Theorem in the global definition context?

[Patrick Thomas]

I guess, how does this differ from just adding definitions as axioms?

[Patrick Thomas]

I guess then because they would always be expanded, and then you would get the exponential blowup.

[Patrick Thomas]

But I guess you could still replace Term and Formula in the mapped to definition by the resulting Theorem?

[Patrick Thomas]

Or does having it done by the rule somehow ensure that the logic remains consistent?

[Mario Carneiro]

Patrick Thomas said:

Then could you just as easily replace Term and Formula by Theorem in the global definition context?

Sure, you could store it as a Theorem if you want.
Patrick Thomas said:

I guess, how does this differ from just adding definitions as axioms?

Because it's not just any axiom, it has a particular form, namely an equality between the new definition (fully applied to distinct variables) and some expression with no additional free variables. This is checked in the addTermDef : Context -> String -> [String] -> Term -> Context function

[Patrick Thomas]

I think I might see. I'll try to add it to my current code sometime in the next week or so and play around with it. Sorry to barrage you with questions, I'm not sure where else to ask. Thank you for your patience!

[Huỳnh Trần Khanh]

thank you for starting this thread too, I've had this question for quite a long time and this thread has been very insightful

[Patrick Thomas]

I added support for definitions using the algorithm from Mario. How does this look? Did I follow the algorithm correctly? Hilbert_NV_Def.hs

[Patrick Thomas]

Is that the right way to unfold the definition of a predicate?

[Patrick Thomas]

If I moved this to locally nameless variables would it be a practical kernel for a proof assistant?

[Mario Carneiro]

One danger of this approach for an LCF style kernel (i.e. everything in this module is made private except for the API and the user is allowed to call any API functions and should not be able to prove false) is that Term and Theorem have to be valid in a given Context but nothing enforces this. That means that I can prove foo <-> True in a context defining foo = True, and foo <-> False in a different context with foo = False, and then use mp and friends on both Theorems (since mp doesn't take a Context) to prove True <-> False and hence False

[Mario Carneiro]

Isabelle handles this by having a global context manager that can be queried to see whether two contexts (which are now IDs into the context manager state) are compatible (i.e. one is obtained by extension from another), and each Term and Theorem is tupled with the context in which it was constructed; any primitive rule which takes more than one Term/Formula/Theorem takes the union of the contexts involved and they must all be compatible.

Metamath handles this by making the context itself global state. Term and Theorem don't carry any context information but should be valid in the current context. There is no context branching in this model, but it makes validity checking a lot easier.

[Reid Barton]

In Haskell you could probably also use some kind of phantom type/GADT/singleton encoding (really what you want is a phantom dependent type)

[Patrick Thomas]

I'm not sure what a phantom dependent type is.

[Trebor Huang]

You can look it up on the Haskell wiki, the concept is quite simple.

[Patrick Thomas]

Would the metamath approach here be to make Theorem a (Context, Formula) pair and have mp check that the contexts are the same?

[Patrick Thomas]

Are you saying we would make the type of Theorem be dependent on Context?

[Patrick Thomas]

There are currently no dependent types in Haskell, right?

[Patrick Thomas]

What do you mean by a Term being valid in a given Context? I can see Theorem but I'm not sure I understand Term.

[Trebor Huang]

Are you saying we would make the type of Theorem be dependent on Context?

No.

There are currently no dependent types in Haskell, right?

No.

[Trebor Huang]

Uh, probably should be "it depends (no pun intended) on how dependent you want it to be"

[Patrick Thomas]

Patrick Thomas said:

Would the metamath approach here be to make Theorem a (Context, Formula) pair and have mp check that the contexts are the same?

Is this right?

[Patrick Thomas]

As I did here, but without the assumption rule? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ITP.20for.20FOL.20.2B.20ZFC/near/268331019

[Patrick Thomas]

I guess the basic question is, what is the simplest way to fix this?

[Patrick Thomas]

Does metamath zero use checks on free for and substitution for definitions?

[Patrick Thomas]

Updated code, but not sure how to fix definitions, and if the substitution can be removed with definitions.
Frege.hs

[Patrick Thomas]

Is the addition of definitions to this what is known as an extended Frege system?

[Mario Carneiro]

Patrick Thomas said:

Would the metamath approach here be to make Theorem a (Context, Formula) pair and have mp check that the contexts are the same?

No, in the metamath approach the Theorem is not tupled with a context but instead the context is available in a global data structure, and only grows monotonically (so Theorems can be created in past versions of the context but not "alternate history" versions). In Haskell the global state part is problematic, but something like ST should be sufficient to localize all the types to a given session, within which the context is stored in a STRef

[Mario Carneiro]

Patrick Thomas said:

Does metamath zero use checks on free for and substitution for definitions?

Not sure exactly what you mean. There are constraints on what you can unfold, for example you don't want a bound variable in the definition to capture a free variable in one of the parameters.

[Patrick Thomas]

I mean, I thought the axiom system of metamath was chosen in part to avoid the complexities of substitution, but it seems like they are reintroduced in adding definitions, for example, as you said, in the unfolding.

[Patrick Thomas]

I think what I meant in the previous comment was, could you simulate the global data structure by passing it in and out of each axiom scheme function.

[Patrick Thomas]

As an aside, is what I am trying to do here a waste of time :( I mean, if it could have been done, it would have?

[Patrick Thomas]

Or there are good reasons not to that I am unaware of yet?

[Patrick Thomas]

(deleted)

[Patrick Thomas]

(deleted)

[Trebor Huang]

As an aside, is what I am trying to do here a waste of time :( I mean, if it could have been done, it would have?

The exact combination of things you're doing probably hasn't. But each part of it has, so it's a great try-out-what-happens project, and uncovers some pitfalls / benefits along this path, I think.

[Trebor Huang]

(deleted)

[Mario Carneiro]

Patrick Thomas said:

I mean, I thought the axiom system of metamath was chosen in part to avoid the complexities of substitution, but it seems like they are reintroduced in adding definitions, for example, as you said, in the unfolding.

Metamath has substitution as a built in primitive: it's basically the rule that everything is built from. Where it differs from other systems is that metamath substitution is always direct but sometimes disallowed, whereas substitution in e.g. HOL is always allowed but sometimes requires bound variable renaming.

It is true, however, that adding definitions to metamath entails some additional knowledge about what it means to be a bound variable that is not present in traditional metamath. This is a fact I discovered when designing MM0. Metamath is able to sidestep the problem because it does not attempt to check conservativity of definitions - every definition is an axiom and you have to be careful not to accidentally introduce a free variable. The first version of these rules came about in the definition checker that is now part of set.mm CI, but when we turned it on we did actually discover a few typo'd definitions that could be used to prove a contradiction, so I've come to believe that it's an important part of the verifier even though it is not officially part of the metamath spec.

[Mario Carneiro]

Patrick Thomas said:

I think what I meant in the previous comment was, could you simulate the global data structure by passing it in and out of each axiom scheme function.

Yes, if you used a state monad you can simulate global state, but a public state monad is not good enough, because you can still snapshot an earlier state and roll back, meaning that you can capture some theorems made in an alternate timeline and use them to mess things up in a different one. ST avoids this problem because it actually uses mutable state, not just a simulation - there is no way to snapshot an old version of the state and roll back - and also types are guarded by the type variable denoting the arena for the state, which can be used to "brand" all the types like Term and Formula so that you can't start two separate sessions and share theorems created in one session with the other.

[Mario Carneiro]

Patrick Thomas said:

As an aside, is what I am trying to do here a waste of time :( I mean, if it could have been done, it would have?

It's certainly not a waste of time if you are learning. If you want to actually turn this into a product there are a bunch of other things to attend to, but you should know what your goals are and who your audience is. For example, I've been talking about protecting against API violations in the LCF style, but you should consider what your "threat model" is. Metamath is not designed as an LCF style system, which is to say that if you are working in the same codebase as the verifier then you can arbitrarily muck things up. Same thing for lean - you can "easily" bypass the kernel with some C++ code. These systems instead ensure security by parsing their own language, which is more limited / sandboxed in the things you can do.

But if you wanted to parse your own language, then clearly there is a bunch of missing stuff, like a parser and a grammar for that language, how you want to specify proofs, definitions, and so on. In the end, the "kernel" for such a prover might not be as well isolated as yours, because that can sometimes come with a performance penalty. Naturally if the kernel gets too big then people will start to question why it should be trustworthy, so you have to attend to that too. You have to somehow write the code such that it is easy to convince others that it is correct, and there are a variety of strategies for doing this.

Ultimately, the kernel is one of the smaller parts of making a useful verification system. It's probably the most logically interesting part, but there is a whole lot more beyond it.

[Patrick Thomas]

Thank you! I think I've got some studying to do on ST.

[Patrick Thomas]

I'm having trouble finding examples of this use case. I found examples where everything is done inside of runST, but not where runST calls other functions that take and return a STRef (if I am right and that is what I need to do?). Is the general idea that the type of Term, Formula, and Theorembecome dependent on a "thread id", and the axiom,rule functions take the "thread id" as a parameter and require that the Term, Formula and Theorems passed to them have that same "thread id"?

[Patrick Thomas]

And the STRef presumably created in the runST function somehow becomes contained to the "thread id" associated with that call of runST?

[Patrick Thomas]

If that is the general idea, how do you add the "thread id" (the variable s) to the datatypes and functions to do this? Is it with the forall somehow?

[Mario Carneiro]

Yes, that's right

[Mario Carneiro]

I think you can just declare Term as having a type parameter s

[Mario Carneiro]

even though it doesn't really use it in any interesting way

[Mario Carneiro]

There is one call to runST around the entire scope of the program. This represents one "proving session", within which you can add but not remove definitions. The only way to remove definitions is to exit the runST scope and start anew. You can also have two (unrelated) sessions going on in parallel, and the thread id s is being used to keep the two sessions separate

[Mario Carneiro]

You don't take and return an STRef, there is only one STRef s (Context s) in use which is passed to any functions that need to read or modify the context

[Mario Carneiro]

IIRC the syntax for type variables in data is just data Term s = Var String | Func String [Term s], you don't need forall

[Patrick Thomas]

I think I see. How do the functions, for example the ones that don't need to read or modify the context (all but the add definition and unfold definition functions) get associated with s and check that the terms, formulas, theorems passed to them match the same s? Is s passed to them from runST?

[Mario Carneiro]

That happens automatically from the type signature

[Mario Carneiro]

For example mp will have the type mp :: Theorem s -> Theorem s -> Theorem s which means that you can't use different s for the two inputs

[Mario Carneiro]

note that we're talking about different type variables here, not different inhabitants of one type s

[Mario Carneiro]

s itself is only a marker type, it has no content

[Mario Carneiro]

but if you have two theorems from two sessions they will have types Theorem s and Theorem t respectively where s and t are distinct type variables, so mp will not typecheck

[Patrick Thomas]

So, for example, how do you create an instance of Term s or Formula s in runST?

[Patrick Thomas]

You don't need an s to pass to the data constructor of Term s or Formula s?

[Patrick Thomas]

Or do you just leave the s out of the constructor definitions, expect for those that take a Formula or Term?

[Patrick Thomas]

Sorry, I guess I should have seen that in your example.

[Patrick Thomas]

Thank you!!

[Mario Carneiro]

The constructors Var and Func of Term s are private; using them you can construct whatever you like but the external API needs to use mkFunc instead, which will check that you only use functions in the context

[Patrick Thomas]

I'm a little uncertain how to implement the mkFunc. Here I want to read from a passed STRef but return a Term s. I can read from the STRef in a do block, but how do I then return a Term s? As a minimal example that expresses the same concept of what I think I need to do (maybe not?):

import Control.Monad.ST
import Data.STRef


data Term s = Var String
            | Func String [Term s]
              deriving (Show, Eq)


type Context s = Int

f :: STRef s (Context s) -> Term s
f ref = do
  x <- readSTRef ref
  -- how to return Var "P"?

[Mario Carneiro]

f :: STRef s (Context s) -> ST s (Term s)

[Mario Carneiro]

Alternatively, f can have the type Context s -> Term s and push the responsibility to read the context to the caller

[Patrick Thomas]

Ahh. Thank you!

[Mario Carneiro]

It's okay to let the user have access to objects of type Context s, because they can at worst hold on to old contexts (which are ancestors of the current one, so are still valid to use to construct terms). The only place where you have to be careful is the context extension function must use the latest context, not an old one, so it has to have a type like STRef s (Context s) -> FuncDef -> ST s ()

[Mario Carneiro]

in fact, you could also make a monad ThmM s a = ReaderT (STRef s (Context s)) (ST s) a and make the constructor private, so the user doesn't have to handle the STRef directly

[Patrick Thomas]

Hmm. I'm going to have to do some more reading. Thank you!

[Zhanrong Qiao]

Hello, recently I was also trying to make a "toy" theorem prover based on FOL + ZFC, also using Haskell (and maybe C++ in the future)... Just found this thread really helpful! I have a question though: are there some recommended ways to implement "in/definite descriptions"? I'm deciding between making them into inference rules (i.e. add defining axioms to context if conditions are met) and introducing some kind of "iota & epsilon operators" instead...

[Zhanrong Qiao]

(In case anyone is interested: I used locally nameless, contexts and natural deduction from the very beginning (which makes my verifier code (also this part) much longer and probably slower than Patrick's, but also seems to have avoided some problems you were discussing here), and I'm now (coincidentally) trying to implement definitions. I tried to think about the design in the previous months, and came up with some (still premature) ideas including "local definitions" that "interact with scope changes" like in this informal proof. The point is, in principle they can be lifted to the outermost scope, and the rules described here will become applicable (although still need to be modified to include the case of "partial" functions/predicates, i.e. definitions inside assume sections)...)

[Mario Carneiro]

Does def f open a new scope? As in you can later close the scope and any theorems about f become generalized forall f instead of being about a specific definition

[Zhanrong Qiao]

(deleted)

[Zhanrong Qiao]

No, as I wanted to make the definition of f generalizable (it can escape from any scopes); forall f (I use forallfunc f/n to indicate the type of f) is introduced using anyfunc f/n instead

[Patrick Thomas]

Mario Carneiro said:

It's okay to let the user have access to objects of type Context s, because they can at worst hold on to old contexts (which are ancestors of the current one, so are still valid to use to construct terms). The only place where you have to be careful is the context extension function must use the latest context, not an old one, so it has to have a type like STRef s (Context s) -> FuncDef -> ST s ()

Should FuncDef take an s? As in STRef s (Context s) -> FuncDef s -> ST s ()?

[Patrick Thomas]

Since it has a Term s in the definition?

[Mario Carneiro]

yes

[Patrick Thomas]

Ok. Thank you.

[Mario Carneiro]

@Zhanrong Qiao Regarding your question about indefinite description, wouldn't an iota/epsilon operator take you out of the FOL fragment? I see you have some 1.5 order variables going on so I might be wrong about this

[Mario Carneiro]

I think it would not be so bad to have a skolem operation in your language: something like any x { idef f :: p(x, f) } will introduce f(x) such that p(x, f(x)). That doesn't leave the first order world, and it doesn't have the drawbacks of long lived existential assumptions you get with a simple axiom of the form forall x. exists y. p(x,y) -> exists f. forall x. p(x, f(x)) (not to mention the second order issue here as well)

[Patrick Thomas]

I can't pull a Theorem s out of runST right? If I want to do something with it, like show it, do I need to do that in runST?

[Mario Carneiro]

yes

[Patrick Thomas]

I see. So the whole proof assistant basically runs inside of runST. Is that going to be an issue, do you think?

[Mario Carneiro]

It's probably kind of annoying in ghci, but it shouldn't be a problem for regular haskell programming

[Patrick Thomas]

Ok. Thank you!

[Patrick Thomas]

I can't do IO from inside ST though right? Do I have a function internal to runST that converts Theorem s to a String and somehow return the result of that out of runST?

[Patrick Thomas]

Yay!

ex_1 p = runST $ do
  ref <- newSTRef (Data.Map.empty, Data.Map.empty)
  addPredDefST ref (PredDef p 0 Nothing)
  c <- readSTRef ref
  let p' = mkPred c p []
  let s1 = prop_2 p' (p' `Imp` p') p'
  let s2 = prop_1 p' (p' `Imp` p')
  let s3 = mp s2 s1
  let s4 = prop_1 p' p'
  let concl = mp s4 s3
  return (show concl)

main :: IO ()
main = putStrLn (ex_1 "P")

[Patrick Thomas]

Theorem (Imp (Pred "P" []) (Pred "P" []))

[Patrick Thomas]

Frege_ST.hs

[Patrick Thomas]

Very cool! (If I did it right) :)

[Patrick Thomas]

Thank you!!

[Patrick Thomas]

So, um, I'm almost afraid to ask :), but is that right? Am I forgetting anything obvious that would make it unsound or incomplete or be an issue later?

[Mario Carneiro]

You should put it in a module and expose only the things that are supposed to be public, and ensure that the API is usable enough to prove theorems but not so permissive as to prove false

[Mario Carneiro]

That is, right now it is trivially unsound if we think of ex_1 as the user code because you can just write Theorem Bottom

[Patrick Thomas]

That was going to be my next step, that is putting it into a module and hiding what should be internal. I'm not sure how to go about the latter, that is ensure that the API is usable enough to prove theorems but not so permissive as to prove false, without trying to formally prove it, which is probably beyond what I am up for at this point, and may be impossible due to Godel?

[Mario Carneiro]

It's certainly very difficult to check that a kernel can't prove false with anything approaching absolute certainty. Even real world theorem provers have to deal with that every once in a while

[Mario Carneiro]

I'm soon going to run out of obvious flaws to poke at, so there's that

[Patrick Thomas]

:)

[Mario Carneiro]

Godel's theorem only comes up if you want to prove the soundness of your kernel using the kernel itself (or something axiomatically weaker than it). You could model this kernel in lean without too much trouble

[Patrick Thomas]

Soon? Does that mean you have more in mind :)
How hard would the proofs be once it was in lean? I can't imagine the ST monad would be easy?

[Mario Carneiro]

true, you would have to model haskell in order to get all that right, and once you did you would probably notice that the theorem is false because of e.g. unsafeCoerce

[Patrick Thomas]

So it is unsound?

[Patrick Thomas]

All was for naught?

[Mario Carneiro]

It's why I'm generally dubious of the LCF style - every real world programming language is unsound for stupid reasons

[Mario Carneiro]

But if you want to prove it sound anyway you can just blithely ignore these issues and assume sensible use of the API

[Patrick Thomas]

I'm not sure what the alternative to LCF is? Isn't Lean and Coq LCF?

[Mario Carneiro]

No, I mean LCF style in the sense of the HOL / ML-based systems: you have an abstract data type Theorem which may not even carry a proof object, and you use a privacy barrier to ensure that bad Theorem objects are not constructible

[Mario Carneiro]

the "small trusted kernel" becomes everything behind the privacy barrier

[Mario Carneiro]

Lean and Coq are not LCF style in this sense

[Trebor Huang]

Lean and Coq explicitly stores the proof objects, so you get things like $(mp S (K S))$

[Patrick Thomas]

I'm sorry, I'm not sure what that means.

[Patrick Thomas]

That is, stores the proof objects.

[Mario Carneiro]

the LCF style implies that the user will be writing code in the implementation language, hence you have a fundamental tension: it should be a real world language so that the implementation works, but real world languages don't have airtight privacy guarantees because that's not what they were intended for

[Trebor Huang]

In Lean, the proof of A -> B -> A /\ B can be printed out (try it!) to something like λ x y, <x, y> (sorry, unicode only partly works on my device).

[Trebor Huang]

But in your program (which is approximately LCF-style), you can't print "the proof". Such a thing doesn't even exist. You only have a Theorem which contains only the information of the theorem statement.

[Patrick Thomas]

Is the difference that in my program the proof is that a Theorem can be constructed, and in Lean the proof is that a given theorem passes a verifier test?

[Mario Carneiro]

it's a lot easier to control the grammar of your verifier language than it is to control what can be constructed, especially if you allow the user to be actively malicious and use the implementation language

[Patrick Thomas]

Is it possible to do that for what I was attempting? That is a hilbert system for FOL with equality and ZFC in Haskell?

[Patrick Thomas]

I'm not sure what it would look like. Would it take a proof as a series of user given justifications for each step, and check that those justifications all hold?

[Patrick Thomas]

For example, P -> (P -> P) holds from an instantiation of prop_1 with p and p.

[Patrick Thomas]

And the verifier instantiates prop_1 with p and p and checks that it matches?

[Patrick Thomas]

Or something along the lines of what I was doing for natural deduction earlier?

[Zhanrong Qiao]

Patrick Thomas said:

I'm not sure what it would look like. Would it take a proof as a series of user given justifications for each step, and check that those justifications all hold?

Yes, I think what Mario was saying is that you could make a data structure that stores proof steps, then your program could just take a data structure in some format and check if it's a valid proof, which does not rely on the type safety of the implementation language (also, proofs can then be constructed using another program written in arbitrary programming language for example). This is optional

[Zhanrong Qiao]

Mario Carneiro said:

Zhanrong Qiao Regarding your question about indefinite description, wouldn't an iota/epsilon operator take you out of the FOL fragment? I see you have some 1.5 order variables going on so I might be wrong about this

I thought epsilon operators and Skolem functions are the "same thing" (and the difference is just which one is more convenient)... In principle I could replace every occurrence of an epsilon operator by a definition of a Skolem function...?

[Zhanrong Qiao]

But yes I think the def/idef approach makes it easier to interface with first-order automated proving methods (they don't need to create definitions; no replacing are needed)

[Mario Carneiro]

@Zhanrong Qiao The difference in this case is that the idef is essentially a monomorphized epsilon operator: you stamp out a new definition every time the rule is invoked, rather than having a single higher order thing called "epsilon" to which you provide a lambda to get a choice function for a particular predicate

[Zhanrong Qiao]

Yes, I guess this is similar to thinking the invocations of the Axiom of Separation as instantiations of an axiom schema instead of applications of a second-order axiom... The syntactic rules are similar or the same but there can be different interpretations

[Patrick Thomas]

Zhanrong Qiao said:

Patrick Thomas said:

I'm not sure what it would look like. Would it take a proof as a series of user given justifications for each step, and check that those justifications all hold?

Yes, I think what Mario was saying is that you could make a data structure that stores proof steps, then your program could just take a data structure in some format and check if it's a valid proof, which does not rely on the type safety of the implementation language (also, proofs can then be constructed using another program written in arbitrary programming language for example). This is optional

Like this as a simple example?

{-
Func "c" [] : A constant named "c"
Func "f" [v] : A function named "f" of one variable v
-}
data Term = Var String
          | Func String [Term]
            deriving (Show, Eq)

{-
Pred "P" [] : A propositional variable named "P"
Pred "Eq" [s, t] : s = t
-}
data Formula = Bottom -- False
             | Top -- True
             | Pred String [Term]
             | Not Formula
             | And Formula Formula
             | Or Formula Formula
             | Imp Formula Formula
             | Iff Formula Formula
             | Forall String Formula
             | Exists String Formula
               deriving (Show, Eq)


data Justification = MP Step Step
                   | Prop_1 Formula Formula
                   | Prop_2 Formula Formula Formula
                   | Prop_3 Formula
                     deriving (Show, Eq)

type Assertion = Formula
type Step = (Assertion, Justification)


checkStep :: Step -> Bool

-- Propositional calculus

-- |- p & |- (p -> q) => |- q
checkStep (assertion, (MP step_1@(minor, _) step_2@(major, _))) =
  case major of
    (Imp p q) -> p == minor &&
                 q == assertion &&
                 checkStep step_1 &&
                 checkStep step_2
    _ -> error "mp"

-- |- (p -> (q -> p))
checkStep (assertion, Prop_1 p q) =
  assertion == (p `Imp` (q `Imp` p))

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
checkStep (assertion, Prop_2 p q r) =
  assertion == ((p `Imp` (q `Imp` r)) `Imp` ((p `Imp` q) `Imp` (p `Imp` r)))

-- |- (((p -> false) -> false) -> p)
checkStep (assertion, Prop_3 p) =
  assertion == (((p `Imp` Bottom) `Imp` Bottom) `Imp` p)


-- Example

-- |- p -> p

ex_1 p =
  let s1 = ((p `Imp` ((p `Imp` p) `Imp` p)) `Imp` ((p `Imp` (p `Imp` p)) `Imp` (p `Imp` p)), Prop_2 p (p `Imp` p) p) in
  let s2 = (p `Imp` ((p `Imp` p) `Imp` p), Prop_1 p (p `Imp` p)) in
  let s3 = ((p `Imp` (p `Imp` p)) `Imp` (p `Imp` p), MP s2 s1) in
  let s4 = (p `Imp` (p `Imp` p), Prop_1 p p) in
  let s5 = (p `Imp` p, MP s4 s3) in
  checkStep s5

[Trebor Huang]

That's right.

[Patrick Thomas]

Then I could also thread a separately verified immutable definition context through checkStep and add UnfoldFunc and UnfoldPred cases to the checkStep function?

[Patrick Thomas]

That is, immutable with regards to checkStep.

[Patrick Thomas]

As in, no case in checkStep changes the definition context passed to it.

[Zhanrong Qiao]

Patrick Thomas said:

Then I could also thread a separately verified immutable definition context through checkStep and add UnfoldFunc and UnfoldPred cases to the checkStep function?

Yes, you probably need to consider "assert x under definition context d" as a whole in checkStep... Then you probably need a "weakening" rule (adding definitions to context does not change the validity of the assertion, as long as the names used by the assertion don't get redefined etc)...

[Zhanrong Qiao]

Or you could disallow naming clashes when forming definition contexts, in this way you don't need to check for redefinitions in the weakening rule (I think I got weakening wrong in my implementations, I did not check for naming clash; will fix them later)

[Zhanrong Qiao]

But if you have a global context that 1. only allows adding more definitions but not removing definitions 2. disallows naming clash, then you no longer need to pass contexts into checkStep and weakening will be automatic

[Zhanrong Qiao]

Should I allow definitions to abstract over functions/predicates (like the subset function I imagined here)? This seems to be not even a part of second-order logic...

[Zhanrong Qiao]

Untitled.png

[Zhanrong Qiao]

I tried and it feels like the verifier code will become much messier with this (probably I have to start from some type theory...)

[Zhanrong Qiao]

Oh but I did not imagine any instances where we need more than one abstraction over (definable) functions/predicates in a formula. Probably I could still keep it simple...

[Patrick Thomas]

(deleted)

[Patrick Thomas]

(deleted)

[Patrick Thomas]

Does this work for adding definitions?
Test.hs

[Patrick Thomas]

I don't need to check that each function and predicate used in the proof is in the definition context do I? They just can't be unfolded if they are not?

[Patrick Thomas]

Zhanrong Qiao said:

But if you have a global context that 1. only allows adding more definitions but not removing definitions 2. disallows naming clash, then you no longer need to pass contexts into checkStep and weakening will be automatic

It seems that it would be easiest to not add definitions in the lines of the proof, and just require that they be given at the start. Then there is a single check that they are valid, and the context is only sent through the checkProofInContext function so that they can be unfolded as needed. Example code above.

[Patrick Thomas]

(deleted)

[Patrick Thomas]

(deleted)

[Patrick Thomas]

Should I allow a proof step for alpha conversion? Or change to locally nameless? I suppose I should do one or the other or proofs will become unwieldy?

[Mario Carneiro]

Patrick Thomas said:

For this non LCF version, I don't need to check that each function and predicate used in the proof is in the definition context do I? They just can't be unfolded if they are not?

This is not okay in definitions, at least. Because you can do def foo := bar (where bar is an undeclared nullary constant symbol) and then def bar := not foo (a regular definition) and suddenly you can unfold both foo and bar and get a contradiction

[Mario Carneiro]

It seems generally dubious to me to allow undefined references anywhere in a proof, but I think that under certain settings you can argue that if you use an undefined term constructor somewhere then it is effectively an opaque constant, and assuming it doesn't show up in the theorem statement you can generalize it and replace it with something more innocuous like the constant true function. (It does imply that your sorts are all nonempty, but in FOL this is usually the case anyway.)

[Mario Carneiro]

Zhanrong Qiao said:

Should I allow definitions to abstract over functions/predicates (like the subset function I imagined here)? This seems to be not even a part of second-order logic...

You might take some inspiration from metamath here. Metamath allows for the definition of functions that take second order variables, but no higher. If Set is the base sort (the collection of ZFC sets, for example), then first order variables (set variables) have type Set and second order variables (class and wff variables) have type Set -> ... -> Class or Set -> ... -> Prop (where we think of Class as Class := Set -> Prop). It is then possible to make definitions that accept any number of class and wff variables and produce a class or wff, for example the class abstraction operator (Set -> Prop) -> Class. However, there are no variables in this "third order" level, only concrete term constructors. subset : Class -> Class -> Prop would be in this category.

[Patrick Thomas]

(deleted)

[Patrick Thomas]

Does this fix the issue with the undefined references? Test.hs

[Mario Carneiro]

It does, but now you have the issue that you have to recheck subformulas many times. The usual way to fix this is to add some explicit DAG-like structure to your proof terms, so that if a subproof or subformula appears in two places it only has to be validated once. This can be done by adding a let-like construct: a way to extend the local context with a record "Ref 0 means P /\ Q", and then you can use Ref 0 to refer to this saved expression, and you know it is valid because it was checked when it was first entered into the context. The same thing applies to proofs, this is basically have statements. It is useful for both terms/formulas and proofs: for proofs, because proofs can be long and you don't want to duplicate them (and if there are duplicated subproofs in a duplicated proof it can blow up exponentially), and for terms/formulas because they have very high duplication within a proof, because all the core rules require some kind of subterm similarity (for example, P will necessarily be constructed at least twice, in both sides of a MP application proving P, (P -> Q) |- Q).

[Patrick Thomas]

Thank you. Does this mean for instance that instead of passing Terms, Formulas and Proofs to cases of checkProofInContext, you would pass Either Term Ref, Either Formula Ref and Either Proof Ref and also a local context mapping Ref to Terms, Formulas and Proofs? And you would change Proof to be one of Assertion Justification, Let Ref (Either Term Formula) or Have Ref Proof?

[Patrick Thomas]

Actually, no, I'm not sure I have that right. At least not the part about changing the definition of Proof.

[Patrick Thomas]

Maybe I should create a Step type that is either a (Assertion, Justification), a Let or a Have? And replace the checkProofInContext function with a CheckSteps function that takes the definition context, reference context and a list of Steps?

[Patrick Thomas]

I'm not sure. Suggestions welcomed :)

[Mario Carneiro]

You want Let and Have to be part of the Justification grammar itself, and similarly you want Ref to appear inside a Formula. This complicates formula equality testing though; one way would be to ensure as part of wellformedness checking that formulas in the context never contain Ref and formulas in the Justification have all the Refs substituted out before going in the context or being equality tested

[Mario Carneiro]

basically the Formula expressions inside Justification are more like mini-programs for constructing a formula with guaranteed internal sharing

[Patrick Thomas]

When you say context, are you referring to the definition context?

[Patrick Thomas]

Also, what do you mean by guaranteed internal sharing?

[Zhanrong Qiao]

Without de Brujin indexing, you recurse to check formulas without modifying it, so if you have a "certificate" that some formula is well-formed, then you also have "certificates" that all its subformulas are well-formed (though if you move into binders, there will be more free variables), so you could reuse the "certificates" (i.e. skip checking formulas that are subformulas of already-checked ones) i guess

[Zhanrong Qiao]

To implement this we could store checked formulas in the context for reference

[Zhanrong Qiao]

But if formulas in the context refer to each other, that could make equality testing slow, so Mario suggests to unfold their Refs before putting formulas into the context?

[Zhanrong Qiao]

(I'm not going to push for this level of optimization in checking for now... Will we encounter really long formulas in practice?)

[Patrick Thomas]

I'm not sure if this is what he meant or not.

[Patrick Thomas]

I'm not sure that he is saying that the issue is related to not using de Bruijn indexes.

[Mario Carneiro]

No, de bruijn indices don't really affect this one way or another

[Mario Carneiro]

When I say context I mean the local context associating Ref -> CheckedFormula

[Patrick Thomas]

What differentiates local and global contexts? The definition context is passed trough each instance of the proof checking function, so I guess that makes it global? What would be an example of a local context?

[Mario Carneiro]

by internal sharing, I mean that something like (x + x) + (x + x) will be represented as a DAG with 3 nodes x4 ⇉ x2 ⇉ x

[Mario Carneiro]

The map from refs to formulas can have whatever scope you like, but it generally makes most sense for it to be local to a given proof

[Mario Carneiro]

if you make it too global then the ref numbers and the context gets big

[Mario Carneiro]

since it basically becomes a log of all expressions ever constructed

[Patrick Thomas]

Wait, so every formula gets added to the map from references to formulas, not just those specified by let?

[Mario Carneiro]

no, just the let ones, but you can have them stick around / not be scoped if you like

[Mario Carneiro]

for example you could require that every proof starts with a list of all let formulas and then the actual justification

[Mario Carneiro]

that way you don't have to worry about scope checking, things just monotonically add to the context and then you throw the whole thing away at the end of the proof

[Patrick Thomas]

What would be the drawback to doing that?

[Patrick Thomas]

I'm not sure what would delineate the start and end of a local context?

[Patrick Thomas]

How would that differ from what I added for definitions?

[Mario Carneiro]

no major drawback, I suppose the numbers could get large if it's a big monolithic proof but it probably won't be your biggest issue anyway

[Patrick Thomas]

Does that mean you see a much bigger issue here?

[Mario Carneiro]

It's kind of like definitions, but transparent to the other rules. If r0 := p /\ p and r1 := p then you want r0 and r1 /\ p to be considered syntactically equal for the purposes of rules like MP

[Mario Carneiro]

Note that equality testing is still slow with this scheme, because in haskell you can't observe the pointer sharing so even if you have x4 ⇉ x2 ⇉ x and y4 ⇉ y2 ⇉ x checking that x4 = y4 requires checking x2 = y2 twice

[Mario Carneiro]

This is only a major issue if you have large terms, however. As Zhanrong said, long formulas are a niche issue

[Mario Carneiro]

It's more important to support this for proofs, since duplication there is much more common

[Mario Carneiro]

In DTT you can get very large terms or terms with high duplication, however

[Patrick Thomas]

DTT?

[Mario Carneiro]

dependent type theory, i.e. lean or coq style

[Mario Carneiro]

as opposed to FOL or HOL

[Patrick Thomas]

Mario Carneiro said:

It's more important to support this for proofs, since duplication there is much more common

You mean have statements?

[Patrick Thomas]

Sorry, I'm not certain what a local context would look like. What would start and end it?

[Patrick Thomas]

Can you do the same thing with have statements and put them all at the beginning, like using earlier proofs?

[Patrick Thomas]

It doesn't seem like what I currently have doesn't have any support for using prior proofs?

[Mario Carneiro]

A local context for holding terms, formulas, and proofs might look like this:

data ProofContext = ProofContext
  { terms :: Seq Term,
    fmlas :: Seq Formula,
   proofs :: Seq Assertion }

data Term = ...
  | Ref Int

data Formula = ...
  | Ref Int

data Justification = ...
  | Ref Int
  | LetTerm Term Justification
  | LetFormula Formula Justification
  | LetProof Proof Justification

checkProof :: Context -> ProofContext -> Proof -> Bool

[Patrick Thomas]

Thank you. What makes ProofContext local?

[Patrick Thomas]

Does local mean initialized to be empty at the start of each checkProof?

[Patrick Thomas]

Is there a formal definition of what a proof is in Hilbert FOL? For instance something that reads like "a proof is a sequence of steps each of which can refer to a previous step and must be of the form ....."

[Mario Carneiro]

Patrick Thomas said:

Does local mean initialized to be empty at the start of each checkProof?

Yes

[Mario Carneiro]

compared to Context which contains all the definitions, and is generally monotonic across a whole proof development

[Patrick Thomas]

checkProof is not the entirety of a whole proof development?

[Patrick Thomas]

I don't know why I didn't think of this before, but there is probably a formal description of this proof system (Hilbert FOL with equality and definitions) that I could be referencing and translating from?

[Patrick Thomas]

For example, something that reads like "A proof is a sequence of steps such that ..."

[Patrick Thomas]

If anyone has a pointer to one, that would be great. Thank you.

[Trebor Huang]

Logic books usually don't do that because that's too "software-engineerish". So you should probably look in proof assistant descriptions. I haven't really read about Mizar or HOL Light before, but I suppose you can find relevant design there.

Probably nobody has ever done this exact thing, so there won't be complete references, and you have to gather information from different sources.

[Mario Carneiro]

One example that gets pretty close to covering the whole gamut of practical theory development is the OpenTheory spec

[Patrick Thomas]

Thank you. I'm kind of surprised that no one has done this before, and I wonder if they had good reason and I am missing something. I was kind of expecting to find something in searches related to proof theory, but the closest I have come is the extended Frege system.

[Patrick Thomas]

"It does, but now you have the issue that you have to recheck subformulas many times. The usual way to fix this is to add some explicit DAG-like structure to your proof terms, so that if a subproof or subformula appears in two places it only has to be validated once."
For example, when you say the usual way, what does that mean? What references or examples do you draw from?

[Zhanrong Qiao]

Like, for example we have let binders in all major proof assistants...?

[Patrick Thomas]

I guess I meant more along the lines of how they are implemented.

[Zhanrong Qiao]

You mean, how are the representation and checking of let implemented?

[Patrick Thomas]

Yes, I think so.

[Zhanrong Qiao]

If I understood correctly, I guess in your example just extend Formula with a constructor Ref Int, and Justification with a constructor Let [Formula] Justification (the list can be seen as a mapping from Int to Formula, and probably using Map Int Formula is faster in Haskell? And the Justification argument is the scope of the Let) with the convention that there are no nested Lets.

[Zhanrong Qiao]

I guess that more commonly, a local context is kept when checking proofs, and upon encountering a Let String Formula Proof, check the Formula, temporarily push the entry (String, Formula) onto the top of the local context and check the Proof in the extended context (in this way there can be nested Lets)

[Zhanrong Qiao]

And when encountering Ref Int (or Ref String or Ref + whatever index type) just read the corresponding entry from the local context

[Patrick Thomas]

So a global context is common to all proofs? I guess I'm having trouble understanding what would constitute separate proofs, because in order to use one proof in another you have to check the "external" proof when you encounter a reference to it in another proof?

[Patrick Thomas]

That is, I don't see a way in the current system to have separate Theorem statements like in Lean.

[Patrick Thomas]

All of which fall under a global context.

[Zhanrong Qiao]

Lean seems to have a two-level hierarchy (just my feeling, I'm not sure if I'm correct, I have less experience in theorem proving than you...), in the "outer level" you use axiom, def, theorem etc. to introduce things, and the "inner level" is only relevant when checking individual terms, where you use let, λ etc. to introduce things (and these things will be removed once you go out of their scope)?

[Patrick Thomas]

That is how it appears to me as well. I don't have that much experience either. I'm wondering if that is what Mario means by a global and local context in my implementation.

[Zhanrong Qiao]

I don't think you made such a distinction in your implementation (I also did not, and I'm not even sure whether we need two levels of contexts...)

[Patrick Thomas]

No, I don't think I did. I'm wondering if I should have.

[Zhanrong Qiao]

(Probably this is for the sake of checking speed? After removing definitions from the context, you will need to check if the conclusion of a proof is still a well-formed formula, and if there are only two layers (here I mean a global one and one for the scope of a Let, with no nested Lets) this check will not be too often)

[Zhanrong Qiao]

But we still have nested lets and λs in Lean anyway (Lean's "inner level" context is more like a stack with multiple layers. Sorry if my wording is confusing...)

[Patrick Thomas]

I'm also wondering if a Hilbert system was the right approach.

[Zhanrong Qiao]

I (personally) think to make proofs appear natural, it's better to provide rules that allow making and discharging hypotheses directly (and anyway you can transform such proofs into Hilbert-style using the deduction theorem afterwards)... Metamath also supports this!

[Patrick Thomas]

Hmm. I wonder if let and have are something usually reserved for natural deduction.

[Patrick Thomas]

Same with local and global contexts.

[Patrick Thomas]

Or at least originate from it.

[Zhanrong Qiao]

In some sense yes? Natural deduction is indeed related to λ (through the Curry-Howard correspondence) which also binds some variable...

[Zhanrong Qiao]

let and have are related to the "cut rule" in sequent calculus in this way

[Patrick Thomas]

Interesting. I am familiar with the Curry-Howard correspondence, but not sequent calculus.

[Zhanrong Qiao]

Sequent calculus feels like "what we are actually thinking when writing down natural deduction proofs", and it works both forwards (from premises) and backwards (from goals); natural deduction is like working forwards only

[Patrick Thomas]

Hmm. What do have and let correspond to in natural deduction?

[Zhanrong Qiao]

The cut rule corresponds to "proving some lemma and then use it to prove the goal" in ND

[Patrick Thomas]

I see. Are there also local and global definitions?

[Zhanrong Qiao]

(deleted)

[Zhanrong Qiao]

I don't think so, they are often considered separately as an extension to FOL? (But in dependent type theory with C-H they are similar to let...)

[Patrick Thomas]

I see. Thank you!

[Patrick Thomas]

Is there a good reference for formalized natural deduction extended with definitions?

[Patrick Thomas]

What is the form of natural deduction that Lean corresponds to in the Curry-Howard correspondence? Is there a formalization for it?

[Patrick Thomas]

Mario Carneiro said:

Your rule for ForallIntro is problematic because you don't have a weakening rule: you won't be able to prove e.g. x = x |- forall x. True. One way to fix it is instead of checking not (any (freeIn x) gamma) you filter out everything from gamma which has a free x in the subproof.

Do you mean like:

Forall introduction:
Let gamma - {x} be the set of all the formulas in gamma for which x does not occur free. Then
(gamma - {x}|- p) =>
(gamma |- forall x. p)

[Patrick Thomas]

Does the same problem occur in my implementation of exists elimination?

[Patrick Thomas]

Is it natural deduction that Lean corresponds to in the C-H correspondence? If so, what are the exact rules of inference for it? What do let and have correspond to in it?

[Patrick Thomas]

Are have statements needed because my checker processes a proof as a tree, and in a tree you have to repeat the entirety of subproofs if you use them more than once? For example, would have statements no longer be needed if instead my checker processed the proof as a sequence of labelled steps, and the inference rules just used the labels to refer to previously checked steps?

[Patrick Thomas]

This could probably be made cleaner and faster, but for a thrown together example, does this eliminate the need for have statements?

import Data.Map
import Data.Set

{-
Func "c" [] : A constant named "c"
Func "f" [v] : A function named "f" of one variable v
-}
data Term = Var String
          | Func String [Term]
            deriving (Show, Eq)

{-
Pred "P" [] : A propositional variable named "P"
Pred "Eq" [s, t] : s = t
-}
data Formula = Bottom -- False
             | Top -- True
             | Pred String [Term]
             | Not Formula
             | And Formula Formula
             | Or Formula Formula
             | Imp Formula Formula
             | Iff Formula Formula
             | Forall String Formula
             | Exists String Formula
               deriving (Show, Eq)

type Assertion = Formula

data Justification = MP Int Int
                   | Prop_1 Formula Formula
                   | Prop_2 Formula Formula Formula
                   | Prop_3 Formula
                     deriving (Show, Eq)

type Step = (Assertion, Justification)

checkStep :: [Step] -> Step -> Bool

-- Propositional calculus

-- |- p & |- (p -> q) => |- q
checkStep checked (q, MP index_1 index_2) =
  let pq = fst (checked !! index_1) in
  let p = fst (checked !! index_2) in
  case pq of
    (Imp p' q') -> p == p' && q == q'
    _ -> error "mp"

-- |- (p -> (q -> p))
checkStep _ (assertion, Prop_1 p q) =
  assertion == (p `Imp` (q `Imp` p))

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
checkStep _ (assertion, Prop_2 p q r) =
  assertion == ((p `Imp` (q `Imp` r)) `Imp` ((p `Imp` q) `Imp` (p `Imp` r)))

-- |- (((p -> false) -> false) -> p)
checkStep _ (assertion, Prop_3 p) =
  assertion == (((p `Imp` Bottom) `Imp` Bottom) `Imp` p)


checkAll :: [Step] -> Bool
checkAll steps = go steps [] where
  go :: [Step] -> [Step] -> Bool
  go [] _ = True
  go (x:xs) previous = (checkStep previous x) && (go xs (previous ++ [x]))


-- Example

-- |- p -> p

ex_1 =
  let p = Pred "P" [] in
  let s0 = ((p `Imp` ((p `Imp` p) `Imp` p)) `Imp` ((p `Imp` (p `Imp` p)) `Imp` (p `Imp` p)), Prop_2 p (p `Imp` p) p) in
  let s1 = (p `Imp` ((p `Imp` p) `Imp` p), Prop_1 p (p `Imp` p)) in
  let s2 = ((p `Imp` (p `Imp` p)) `Imp` (p `Imp` p), MP 0 1) in
  let s3 = (p `Imp` (p `Imp` p), Prop_1 p p) in
  let s4 = (p `Imp` p, MP 2 3) in
  checkAll [s0, s1, s2, s3, s4]

[Trebor Huang]

Looks good.

But here's one thing where type theory is superior to usual FOL: In type theory, let and have are essentially the same thing except for syntactic differences. In FOL they have to be different: let for terms and have for proofs.

[Patrick Thomas]

Great! Thank you!
I think MetaMath has the user prove that each term and formula is valid? I'm not sure how their use in the proof is then checked.

[Mario Carneiro]

Patrick Thomas said:

Are have statements needed because my checker processes a proof as a tree, and in a tree you have to repeat the entirety of subproofs if you use them more than once? For example, would have statements no longer be needed if instead my checker processed the proof as a sequence of labelled steps, and the inference rules just used the labels to refer to previously checked steps?

Yes, that's correct. The same thing applies to terms, and here you gain the additional advantage that if every term is only constructed once then equality checking becomes O(1)

[Mario Carneiro]

Patrick Thomas said:

Mario Carneiro said:

It does, but now you have the issue that you have to recheck subformulas many times. The usual way to fix this is to add some explicit DAG-like structure to your proof terms, so that if a subproof or subformula appears in two places it only has to be validated once.

When you say the usual way, what do you mean? What references or examples do you draw from?

Besides my experience with poking around in different proof assistants, almost everything I've talked about in this thread has been incorporated as part of MM0, including the term deduplication trick I just mentioned. When you put it all together it has a really dramatic effect on performance

[Mario Carneiro]

Patrick Thomas said:

So a global context is common to all proofs? I guess I'm having trouble understanding what would constitute separate proofs, because in order to use one proof in another you have to check the "external" proof when you encounter a reference to it in another proof?

The global context should include also a list of checked proofs, which can then be referenced as part of new proofs. Both metamath and lean work like that.

[Mario Carneiro]

I know a few proof assistants that lack this "two level hierarchy", but they seem to be in the minority. In many of the HOLs, including HOL light, there is no explicit two-level thing; instead every theorem stands on its own and you "name" a theorem by assigning it to an OCaml variable. I think this was later found to be a bad idea, because it means you can't just enumerate over the theorems that exist like lean's environment.fold, nor can you get their user-provided names, which is problematic for, say, a proof exporter.

Lean does not have any context management keywords at the "global" level, unlike Zhanrong's language. I think these are avoided because they require you to keep the list of statements in a stack, which makes lookups more expensive, and if popping an assumption changes the type of statements then it can be expensive. I think Isabelle and Coq both have a module system, which amounts to hypotheses at the global level that can be discharged later, but I believe the scope checking entails walking all the theorems in the scope and I have heard rumors of long running Qed. statements, which is a baffling experience for users since it is weird that closing a scope should be expensive. Lean 3 has parameter which tries to simulate this behavior, but it isn't really type changing the theorems, it only makes them appear to have a different type inside the scope.

[Mario Carneiro]

Patrick Thomas said:

Great! Thank you!
I think MetaMath has the user prove that each term and formula is valid? I'm not sure how their use in the proof is then checked.

Every theorem comes with assumptions about each variable appearing in the theorem. So for example modus ponens which looks like |- P & |- (P -> Q) => |- Q actually has four assumptions: wff P, wff Q, |- Pand |- (P -> Q). So when you apply this theorem you make substitutions in for P and Q, say T. and x = x, and then you would have subproofs for wff T., wff x = x, |- T. and |- (T -> x = x). The wff T. proof is showing that T. is a well formed formula.

[Patrick Thomas]

Thank you!
Do you mean that you have additional steps, where each is an assertion that a term or formula is well formed with a justification potentially referring to previous steps for why that assertion holds, and when for example you need to pass a proof of p and q being well formed to mp, then you just pass the step label that asserts that p is well formed and the step label that asserts that q is well formed? So mp just takes four step labels? Do you interleave these steps with the steps for the axioms and inference rules, and add the justifications for being well formed to the list of justifications for the axioms and inference rules, or do you keep them separate and check all of the assertions of being well formed first?

[Patrick Thomas]

Why incidentally is it that mp requires proofs of p and q being well formed, and not p and p -> q?

[Mario Carneiro]

The well formedness steps are interleaved with the rest in the overall proof, but for each individual theorem all the well-formedness assumptions (called "floating hypotheses" or $f in metamath) precede the regular assumptions ("essential hypotheses" or $e in metamath) to that theorem.

[Mario Carneiro]

Patrick Thomas said:

Why incidentally is it that mp requires proofs of p and q being well formed, and not p and p -> q?

The $f hypotheses to a theorem are calculated automatically, by collecting all the variables that appear in the $e hypotheses and the theorem statement. This is somewhat analogous to what would happen in lean if you had variables p q r s t : Prop at the top of the file and then state theorem mp (min : p) (maj : p -> q) : q := ..., you will get four actual pis in the theorem statement, (p q : Prop) (min : p) (maj : p -> q). You don't need an assumption that p -> q is well formed because the theorem itself has the context to see that if p and q are well formed then so is p -> q, so even after substituting p and q we know it is well formed

[Mario Carneiro]

Note that in metamath proof assertions and well formedness assertions are on the same footing - wff p and |- p are just two different statements that can be proved

[Patrick Thomas]

I think I see. Somp in my implementation would still take four step labels, one for the assertion of wff p, one for wff q, one for |- p and one for |- p -> q? And the code for mp looks at the assertions at those step labels and checks that everything matches up?

[Patrick Thomas]

What makes a formula (or term?) well formed? That each occurring predicate and function is in the definitions table, and that each subformula (and subterm?) is well formed?

[Patrick Thomas]

Do you have justifications like AndWff Int Int, where the first Int is the label of a step that asserts that the left subformula of the /\ is well formed and the second is the label of a step that asserts that the right subformula is well formed?

[Mario Carneiro]

Yes. Each term constructor is introduced by an axiom that looks like wff (p -> q), which like other theorems inherits the assumptions wff p and wff q

[Mario Carneiro]

Patrick Thomas said:

What makes a formula (or term?) well formed? That each occurring predicate and function is in the definitions table, and that each subformula (and subterm?) is well formed?

In metamath, saying that a formula is well formed is the same as asserting the provability of wff fmla, in a context where you have wff hypotheses for every variable and have access to the syntax axioms like wff p & wff q => wff (p -> q)

[Mario Carneiro]

the distinction between formulas and terms is done here by having multiple constants that can appear in the first position: wff p vs class A

[Mario Carneiro]

each metamath database defines its set of valid sorts, it's not a closed list known to the verifier

[Mario Carneiro]

same thing for the syntax axioms

[Mario Carneiro]

As a result, the Justification grammar in metamath looks closer to this:

data Justification = ApplyThm String [Justification]

[Patrick Thomas]

Mario Carneiro said:

the distinction between formulas and terms is done here by having multiple constants that can appear in the first position: wff p vs class A

When you say term and formula here are you referring to what corresponds to Term and Formula in my implementation?

[Mario Carneiro]

yes

[Mario Carneiro]

those aren't metamath concepts per se

[Mario Carneiro]

but if you are doing FOL-ish things you will probably have something similar to terms and formulas, and in set.mm that's wff and class

[Patrick Thomas]

Oh, class as in class variable?

[Mario Carneiro]

class is actually more like second order terms, but it is used for both

[Mario Carneiro]

yes, it means ZFC class expression

[Mario Carneiro]

there is also setvar but this is only for set variables, as the name implies, not expressions

[Patrick Thomas]

Hmm. Thank you. I will try and see if I can extend what I have with what I think I understand.

[Patrick Thomas]

Mario Carneiro said:

Patrick Thomas said:

Why incidentally is it that mp requires proofs of p and q being well formed, and not p and p -> q?

The $f hypotheses to a theorem are calculated automatically, by collecting all the variables that appear in the $e hypotheses and the theorem statement. This is somewhat analogous to what would happen in lean if you had variables p q r s t : Prop at the top of the file and then state theorem mp (min : p) (maj : p -> q) : q := ..., you will get four actual pis in the theorem statement, (p q : Prop) (min : p) (maj : p -> q). You don't need an assumption that p -> q is well formed because the theorem itself has the context to see that if p and q are well formed then so is p -> q, so even after substituting p and q we know it is well formed

For the formulas passed to the axiom schemes, are you just checking that each formula passed is well formed? For example, passing p -> q and q -> r to the parameters p and q of prop_1, do they provide proofs that p -> q and q -> r are well formed, or that p, q and r are well formed? In the latter case, you would need to accept a variable number of proofs for wff and try to match them up?

[Mario Carneiro]

the latter. There is one wff proof per variable appearing in the formula

[Mario Carneiro]

and they come in the same order as the variable declaration

[Patrick Thomas]

So if the passed parameters were a -> (c -> d) and c -> b they would pass wff proofs in the order for a, c, d, b?

[Mario Carneiro]

no, they would be in the order a,b,c,d

[Mario Carneiro]

because that's the order they were defined at the top of the file

[Mario Carneiro]

pretty sure. It's mostly handled behind the scenes by the authoring tool, the user doesn't generally have to see it

[Patrick Thomas]

Hmm, that seems like it complicates my implementation, or I'm not sure how to handle it well.

[Patrick Thomas]

Do I lose anything by requiring wff proofs for what is passed exactly instead?

[Mario Carneiro]

Suppose you want to prove a -> b and b -> c implies a -> c. You need to know more than that a -> b and b -> c are well formed, you need a and b to be well formed to apply lemmas that recombine these variables in different ways

[Mario Carneiro]

The automatic variable construction in metamath is a front end thing. Behind the scenes it probably makes more sense to assume the list of variables is provided in some order and you just check that all the hypotheses use variables in that list

[Patrick Thomas]

When you say a variable in a hypothesis, are talking about subformulas or actually variables of the form Var x? What level do you break each formula down to that the user has to provide wff proofs for?

[Patrick Thomas]

Are we taking definitions into account here also, in that predicates and functions have to be defined in order to be considered well formed?

[Mario Carneiro]

I mean variables

[Mario Carneiro]

you don't have to unfold definitions, it is syntactically obvious what the variables in an expression are

[Patrick Thomas]

isn't a variable well formed by definition? Why do we need to check that it is well formed?

[Mario Carneiro]

For an expression to be well formed you have to be able to prove it is well formed. That proof uses syntax axioms, and you get one of those for every definition

[Mario Carneiro]

In this setting variables are not well formed by definition, well formedness means that the variable is among the list of variables permitted to appear in the statement

[Mario Carneiro]

in the metamath approach this is true by construction, but if you are given a list of variables separately then you have to check it

[Patrick Thomas]

Oh, but metamath is at a lower level then what I am doing right. In my implementation you can only construct wff, provided that the predicates and functions are defined?

[Mario Carneiro]

or if the variables are numbered then you are checking that the numbers are less than the length of the list

[Patrick Thomas]

Because they are constrained by the constructors of Term and Formula?

[Mario Carneiro]

Well, your prover still isn't dealing with applying one theorem in another context (with substitution for the variables)

[Mario Carneiro]

the situation to avoid is that the substitution does not cover one of the variables appearing in the statement of the theorem

[Patrick Thomas]

You mean accidental bindings?

[Patrick Thomas]

The only context I have is the global context of definitions and proofs previously checked right?

[Mario Carneiro]

like if you have syl: (a -> b) => (b -> c) => (a -> c) and you say "apply syl with a := 2 + 2" and don't say anything about b

[Mario Carneiro]

the metamath approach is to first gather up the variables in syl in order to get a,b,c, and then when you apply it you have to give 3 things x,y,z and then given two more things x -> y and y -> z you get x -> z. If the gathering of variables wasn't done correctly and, say, omitted c, then the downstream use would not substitute for it and you would get a scope error where c appears in the present theorem without any hypothesis about it

[Mario Carneiro]

or you would just get a crash when you look up c in some map

[Mario Carneiro]

Patrick Thomas said:

The only context I have is the global context of definitions and proofs previously checked right?

I mean another local context, i.e. you are proving an unrelated theorem from the one to be applied

[Patrick Thomas]

So we are talking about when I have more than one proof, and proofs take hypothesis?

[Patrick Thomas]

I guess I'm confused, because I don't declare a list of variables at the beginning?

[Patrick Thomas]

I mean, in this Hilbert system there are no hypothesis right?

[Patrick Thomas]

So this would be an issue only if I allowed for them, say moved to natural deduction?

[Mario Carneiro]

Sure, you can have them all exist a priori (as long as you only have one type, which is already not quite true since you have formulas and terms), but then you have to decide what to do about substitution in a theorem

[Mario Carneiro]

like, I want to be able to prove syl once (using the axioms) and use it later without having to replay the axioms

[Patrick Thomas]

I'm sorry, I'm not sure I am following. If I want to prove something, I need to declare what variables are allowed to appear in the proof?

[Mario Carneiro]

in metamath, yes

[Mario Carneiro]

in lean, yes as well

[Patrick Thomas]

Sorry, why is that again?

[Mario Carneiro]

you can't just use random variables that haven't been declared, because variables come with type information and a random letter has unknown type

[Mario Carneiro]

In HOL you can kind of get away with this by having a constructor of the form Var String Type

[Mario Carneiro]

but it's still dicey because you can have variables a: A and a: B and they should be treated as different (even after substituting B := A!)

[Patrick Thomas]

I didn't think FOL had types? I thought there was just one big domain of discourse?

[Mario Carneiro]

What about wff vs term?

[Patrick Thomas]

Oh. So like the p and q in the prop_1 scheme are variables of type formula and the t in the eq_refl scheme is a variable of type term?

[Mario Carneiro]

right

[Mario Carneiro]

If you don't do this, you won't be able to substitute in syl, which is a pretty big hit for a hilbert system

[Mario Carneiro]

that is, without the ability to prove propositional theorems you can't build up a toolbox of useful theorems like and.left

[Mario Carneiro]

In natural deduction it is not quite as bad because the axioms are a little closer to practice, but there are still plenty of useful propositional lemmas that aren't god given like and_assoc

[Patrick Thomas]

Would you call these something like proof schemes?

[Mario Carneiro]

yes

[Mario Carneiro]

in metamath everything is a scheme, it's a logic of schemes being deduced from other schemes

[Mario Carneiro]

which is why variable distinctness is a primitive notion

[Patrick Thomas]

That is, you are proving proof schemes, and when the user goes to use it they need to know what kind of variables to substitute in for which parameters?

[Patrick Thomas]

Like in the proof of p -> p I would declare p to be a formula variable.

[Mario Carneiro]

exactly

[Patrick Thomas]

So when the user passes an expression in for p, you have to break it done into all of the variables and then make sure that they recombine to form a formula?

[Patrick Thomas]

Because p has been declared to be a formula variable in the proof?

[Mario Carneiro]

well, they have to pass a formula for p

[Mario Carneiro]

so previously they had to have constructed that formula, with all the attendant checks

[Mario Carneiro]

that is, you have a formula foo which has already been validated and you put it in as p := foo in id : p -> p, which is done by traversing the expression p -> p and replacing occurrences of p with foo

[Mario Carneiro]

and that replacement doesn't have to validate anything, because p -> p is a valid formula and foo is a valid formula so foo -> foo is also valid

[Patrick Thomas]

So you would have a justification like, declared as term variable and a justification like declared as formula variable?

[Patrick Thomas]

But you also have a third type of variable, the one occurring as Var String in term, which I guess is an object variable?

[Patrick Thomas]

And the term and formula ones are meta variables? or schema variables?

[Mario Carneiro]

I think you can unify term variables and term metavariables in that scheme

[Patrick Thomas]

I'm sorry, I'm still not quite clear what I am checking if a formula is passed to an axiom scheme. I know it is a formula because they had to check it before hand right? In the check for that step of the proof, do I still need to gather all the variables that occur in the passed formulas and check that they are declared? Declared where? Wasn't that already done when it was checked that it was a formula?

[Patrick Thomas]

For reference, I am taking about what I need to check for example in the checkStep _ (assertion, Prop_1 p q) case of this code:
Hilbert_Linear.hs

[Patrick Thomas]

We are saying that the user has already checked that what is passed in for p and q are formulas right? But we also need to break these apart to determine that all of the variables occurring in the formulas that were passed are declared somewhere? Isn't that done when they verified they were formulas?

[Patrick Thomas]

Or is this not for the axiom schemes in my implementation, but for the proof schemes?

[Patrick Thomas]

Because in the axiom schemes for my implementation what needs to be passed in is already explicit.

[Patrick Thomas]

So should I rename my data definition for Term to TermScheme and add a constructor that takes the name of a term scheme variable, and change the definition of Formula to FormulaScheme and add a constructor that takes the name of a formula scheme variable? So each axiom scheme takes formula schemes and term schemes and returns proof schemes?

[Patrick Thomas]

Or would I even have data definitions for any kind of term, term scheme, formula or formula scheme?

[Patrick Thomas]

Like, how far off was I here:
Hilbert_Linear_2.hs

[Mario Carneiro]

Patrick Thomas said:

For reference, I am taking about what I need to check for example in the checkStep _ (assertion, Prop_1 p q) case of this code:
Hilbert_Linear.hs

In addition to what you already have, you need to check that p and q are valid formulas, or else you should have Ints passed in and refer to some already checked formulas in the local context

[Patrick Thomas]

Like in the code I just added?

[Mario Carneiro]

I would modify that code to remove the Formula from FormulaStep, and instead have the type of checked steps be different from the input

[Patrick Thomas]

Sorry, why is that? And why only for FormulaStep?

[Patrick Thomas]

Or do you mean have only one kind of step?

[Patrick Thomas]

Instead of ProofStep, FormulaStep and TermStep just have Step?

[Mario Carneiro]

yes, that

[Mario Carneiro]

1 sec, example coming up

[Mario Carneiro]

data Term = Var String
  deriving (Show, Eq)
data Formula = Imp Formula Formula
  deriving (Show, Eq)
data Proof = Proof Formula

data Step
  = IsVar String
  | IsImp Int Int
  | MP Int Int Int Int
  deriving (Show, Eq)

type LocalContext = ([Term], [Formula], [Proof])

pushTerm :: LocalContext -> Term -> LocalContext
pushTerm (ts, fs, ps) t = (ts ++ [t], fs, ps)
getTerm :: LocalContext -> Int -> Term
getTerm (ts, _, _) i = ts !! i

pushFormula :: LocalContext -> Formula -> LocalContext
pushFormula (ts, fs, ps) f = (ts, fs ++ [f], ps)
getFormula :: LocalContext -> Int -> Formula
getFormula (_, fs, _) i = fs !! i

pushProof :: LocalContext -> Proof -> LocalContext
pushProof (ts, fs, ps) p = (ts, fs, ps ++ [p])
getProof :: LocalContext -> Int -> Proof
getProof (_, fs, _) i = fs !! i

checkStep :: LocalContext -> Step -> LocalContext
checkStep ctx (IsVar v) = pushTerm ctx (Var v)
checkStep ctx (IsImp f g) = pushFormula ctx (Imp (getFormula ctx f) (getFormula ctx g))
checkStep ctx (MP p q h1 h2) =
  let Proof p' = getProof ctx h1 in
  let Proof (Imp p'' q') = getProof ctx h2 in
  if p == p' && p == p'' && q == q' then
    pushProof ctx (Proof q)
  else error "MP"

checkSteps :: [Step] -> Proof
checkSteps = go ([], [], []) where
  go (_, _, ps) [] = last ps
  go ctx (s:ss) = go ss (checkStep ctx s)

[Patrick Thomas]

Very cool! Thank you!
Would I also need steps for adding term scheme variables, and formula scheme variables?

[Mario Carneiro]

And an example use (imagine that Prop_1 and Prop_2 are defined similarly):

ex_1 = checkSteps [
  IsPred "P" [], -- f0 = p
  IsImp 0 0, -- f1 = p -> p
  IsImp 1 0, -- f2 = (p -> p) -> p
  IsImp 0 2, -- f3 = p -> ((p -> p) -> p)
  IsImp 0 1, -- f4 = p -> (p -> p)
  IsImp 4 1, -- f5 = (p -> (p -> p)) -> (p -> p)
  IsImp 3 5, -- f6 = (p -> ((p -> p) -> p)) -> ((p -> (p -> p)) -> (p -> p))
  Prop_2 0 1 0, -- p0 = |- (p -> ((p -> p) -> p)) -> ((p -> (p -> p)) -> (p -> p))
  Prop_1 0 1, -- p1 = |- p -> ((p -> p) -> p)
  MP 3 5 1 0, -- p2 = |- (p -> (p -> p)) -> (p -> p)
  Prop_1 0 0, -- p3 = |- p -> (p -> p)
  MP 0 0 3 2, -- p4 = |- p -> p
]

Probably you want to assert that this is a proof of p -> p at the end

[Mario Carneiro]

You already have term and formula variables via the Pred and Var constructors

[Mario Carneiro]

you just need a mechanism to substitute into them

[Patrick Thomas]

I see. That mechanism being two more Step constructors?

[Mario Carneiro]

Something like this:

data Term = Var String
  deriving (Show, Eq)
data Formula = Imp Formula Formula
  deriving (Show, Eq)
data Proof = Proof Formula

data Step
  = IsVar String
  | IsImp Int Int
  | ApplyThm String (M.Map String Int) (M.Map String ([String], Int)) [Int]
  deriving (Show, Eq)

type LocalContext = ([Term], [Formula], [Proof])
type GlobalContext = M.Map String ([Proof], Proof)

substTerm :: M.Map String Int -> Term -> Term
substTerm ts = go where
  go (Var v) = ts M.! v

substFormula :: LocalContext -> M.Map String Int -> M.Map String ([String], Int) -> Formula -> Formula
substFormula ctx ts fs = go where
  go (Imp f1 f2) = Imp (go f1) (go f2)
  go (Pred p args) =
    let (vs, i) = fs M.! p in
    let args' = go <$> args in
    if length args' == length vs then
      substFormula ctx (M.fromList (zip vs args')) [] (getFormula ctx i)
    else error "subst"

substProof :: LocalContext -> M.Map String Int -> M.Map String ([String], Int) -> Proof -> Proof
substProof ctx ts fs (Proof t) = Proof (substFormula ctx ts fs t)

checkStep :: GlobalContext -> LocalContext -> Step -> LocalContext
checkStep gctx ctx (ApplyThm th ts fs ps) =
  let (hs, concl) = gctx M.! th in
  let hs' = substProof lctx ts fs <$> hs in
  let concl' = substProof lctx ts fs concl in
  if length hs' == length ps &&
    all (\(h, p) -> let Proof h' = ctx !! p in h == h') (zip hs' ps)
  then pushProof ctx concl'
  else error "ApplyThm"

[Mario Carneiro]

Notice that you can eliminate Prop_1 and MP constructors from Step with this, by pre-seeding the GlobalContext with

initialContext = M.fromList [
  ("MP", (Proof [Pred "P" [], Imp (Pred "P" []) (Pred "Q" [])], Pred "Q" [])),
 ...
]

[Patrick Thomas]

Sorry, what do the constructor arguments to ApplyThm represent? The name of a theorem, and ?

[Mario Carneiro]

The name of the theorem, the substitutions for term variables, the substitutions for predicate variables, and the list of hypotheses

[Mario Carneiro]

Since you aren't tracking what variables appear in a theorem or ordering them when they go into the global context, these have to be given as maps from string. For predicate variables, the substitution is basically a lambda, since we might want to substitute for a predicate variable which has nonzero arity, and we need a secondary substFormula call to substitute into the lambda

[Patrick Thomas]

In the substitutions for predicate variables M.Map String ([String], Int) the first string is the name of a predicate being substituted into, and sorry, what are the list of strings and int? The names of the variables in the predicate to substitute in for? The arity?

[Patrick Thomas]

I'm guessing we need to check for accidental variable binding in all of these substitutions if this gets extended to predicate calculus?

[Patrick Thomas]

I'm wondering if there is a missing call to substTerm or if it is implicit somewhere?

[Mario Carneiro]

Patrick Thomas said:

In the substitutions for predicate variables M.Map String ([String], Int) the first string is the name of a predicate being substituted into, and sorry, what are the list of strings and int? The names of the variables in the predicate to substitute in for? The arity?

The list of strings are the lambda binders, and the int is a previously constructed formula from the local context. For example we might set P := \x y z -> x + y = z

[Mario Carneiro]

and then we would turn an occurrence like P(1, 2, 3) into 1 + 2 = 3

[Mario Carneiro]

substTerm doesn't appear in the constructors I've shown, but it would appear in the Pred case, for example

[Mario Carneiro]

er... I guess I did that one

[Mario Carneiro]

yeah this probably doesn't typecheck, we should be using let args' = substTerm ts <$> args instead of let args' = go <$> args

[Patrick Thomas]

I'll have to think more about what substituting for a predicate name means. I can see when the arity is zero, that it is just replacing it by a formula, like in the axiom schemes, but I'm not sure what it means when the arity is greater than zero.
I have a prior engagement to attend to, but thank you so much. This is really cool!

[Patrick Thomas]

So if you have a predicate such as such as Pred "P" [] in the proof scheme that you are substituting into, then you can replace it with any formula with no free variables right? What can you do when you have something like Pred "P" [Func "f" [Var "x"], Var "y"]? Replace it with any formula that has the same number of free variables?

[Patrick Thomas]

Or no, maybe just replace each free variable with any term?

[Mario Carneiro]

No, you can replace it with formulas with free variables, the variables just have to not get captured so there is some "free for t in x" side condition

[Mario Carneiro]

I haven't thought about the details but if you draw examples of the bad case it shouldn't be too hard to figure out

[Patrick Thomas]

You could replace x = y with x < y?

[Patrick Thomas]

Oh, or where you talking about the first sentence.

[Mario Carneiro]

For example, replacing forall x, P(x, y) with P(z, w) := x < z is bad because x will get captured

[Patrick Thomas]

So you can replace any predicate of arity 0 with any formula, given the side conditions on name capture? What can you do for arity > 0?

[Mario Carneiro]

that example is a predicate of arity 2

[Mario Carneiro]

Metamath has the ability to manually rename binders because they are subject to substitution. If you are treating them as binders, then you probably want to just alpha-rename the binder automatically instead of restricting the substitution

[Mario Carneiro]

so that example would result in forall x', x < x'

[Patrick Thomas]

I'm sorry, I got a little lost. I guess I am just trying to understand what can be substituted in for a predicate of arity 0 (a propositional variable) and what can be substituted in for a predicate of arity > 0.

[Mario Carneiro]

For the arity 0 special case, you can substitute any formula expression whose free variables are not bound in the context where the variable appears. So in P -> forall x. P, you can substitute any expression for P not containing a free x

[Mario Carneiro]

or in the alpha-renaming version, you can substitute any expression for P, but if P contains a free x then the x binder will be renamed to x' or something else not free in P

[Patrick Thomas]

In the second sentence are you still talking about the special case of arity = 0? Because then P wouldn't have a free x right?

[Mario Carneiro]

I am

[Mario Carneiro]

In the second version we lift the restriction on P, so you can put anything in for it

[Mario Carneiro]

instead of restricting the substitution, we sometimes rename the binder to avoid clashes

[Mario Carneiro]

in the first version we just reject if we would otherwise have to rename a binder

[Patrick Thomas]

I don't understand how P can have arity = 0 and have a free x. Wouldn't it have at least an arity of 1?

[Mario Carneiro]

for example P := 0 < x

[Mario Carneiro]

The arity of P is determined by its use in the original theorem, here P -> forall x. P

[Mario Carneiro]

we're allowed to use an expression with free variables

[Mario Carneiro]

we might want to derive 0 < x -> forall x'. 0 < x here

[Mario Carneiro]

We would use a nonzero arity when the theorem in question uses the predicate at multiple values, for example forall x. P(x) -> P(t)

[Mario Carneiro]

In this case, P(y) := 0 < x would require renaming the binder (and results in forall x'. 0 < x -> 0 < x), but P(x) := 0 < x is okay and does not rename the binder, resulting in forall x. 0 < x -> 0 < t. This is how you get deliberately captured variables

[Patrick Thomas]

Wait, so what does P(x) mean? Is it the same as Pred "P" [Var "x"]?

[Patrick Thomas]

It seems not? The "x" in P(x) is some kind of binder?

[Mario Carneiro]

In formulas, P(t) refers to Pred "P" [t] (where t is any term). When I write P(x) := e, I mean that the substitution map contains "P" -> (["x"], e)

[Mario Carneiro]

well, technically "P" -> (["x"], i) where getFormula ctx i = e

[Patrick Thomas]

"P" -> (["x"], e) means we are replacing the variable x by e in P?

[Patrick Thomas]

Sorry, maybe it is easier to talk about outside of the code, which I am still trying to understand.

[Mario Carneiro]

It means we are replacing P(x) by e, and more generally P(t) by e[t/x]

[Mario Carneiro]

perhaps you should study the code and come back with more pointed questions. (I don't guarantee the code is correct - I wrote it without actually compiling it so there are probably several errors)

[Patrick Thomas]

Ok, sorry. I'll see if I can put together what I think it would look like for just the propositional calculus, and then see what needs to change to extend it to the predicate calculus, if that makes sense?

[Patrick Thomas]

Thank you.

[Patrick Thomas]

Probably not tonight though. Have a good evening, or day depending on your time zone.

[Patrick Thomas]

Does this look correct for the propositional calculus case? Do the comments reflect a correct understanding? Thank you.
Hilbert_Prop.hs

[Patrick Thomas]

Sorry, the comment for GlobalContext should be changed to

{-
Monotonic.
A mapping of names to previously checked derivations.
name -> (ps, p) :
name : The name of a previously checked derivation.
ps : The list of proof schemes in the previously checked derivation.
p : The last proof scheme in the previously checked derivation.
-}

Hilbert_Prop.hs

[Mario Carneiro]

It looks good. The guard (Data.Map.keysSet m) == (allVar p) is overly strict, it suffices to use (allVar p) `subset` (Data.Map.keysSet m). Also it's possible to combine the guard and the substitution into one operation that replaces each free occurrence of a variable in p with the corresponding element of m (which will fail if it's not in the map)

[Patrick Thomas]

So you don't have to replace every free variable in the formula scheme? I was wondering about that.

[Patrick Thomas]

Or I guess I read that backwards. You do have to?

[Patrick Thomas]

Did you mean (Data.Map.keysSet m) `subset` (allVar p)?

[Patrick Thomas]

Nevermind, I think I see. You can have a mapping that has keys that do not appear in the formula but not vice versa. You do have to replace every free variable in the formula. I think?

[Patrick Thomas]

Thank you!

[Patrick Thomas]

Like this?
Hilbert_Prop.hs

[Patrick Thomas]

Out of curiosity, what is the advantage to storing the intermediate proof schemes in the global context at the end of a derivation instead of just the last proof scheme in the derivation?

[Mario Carneiro]

I don't think I ever suggested that?

[Mario Carneiro]

There are some advantages of being able to build multiple proof schemes out of one "derivation pool" / local context, but they are quite niche

[Patrick Thomas]

I think it was in your example code maybe? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ITP.20for.20FOL.20.2B.20ZFC/near/269903509

[Mario Carneiro]

that example doesn't have the checkSteps function. The one earlier does and it uses last ps

[Patrick Thomas]

I see. I must have mixed together the code. Thank you.

[Patrick Thomas]

If I move the last code example that I posted from propositional logic to predicate logic, do I understand correctly that applying a theorem will then require replacing each free term variable with a syntactically correct term scheme, taking into account potential free variable capture, in addition to the replacement of propositional variables (predicate variables of arity 0) that is already done in the current propositional case?

[Mario Carneiro]

yes

[Patrick Thomas]

Thank you.

[Patrick Thomas]

Is it correct that metamath and mm0 use named variables? If so, how is free variable capture handled? Is there a step that allows the user to explicitly alpha convert a formula scheme?

[Mario Carneiro]

Yes, they use named variables. You can use theorems to prove alpha conversion, there is no built in support for it

[Patrick Thomas]

I did not realize that was possible. What do you need to prove it, just FOL?

[Mario Carneiro]

It uses lemmas like http://us.metamath.org/mpeuni/cbvalv.html

[Mario Carneiro]

which follow from the FOL axiomatization

[Patrick Thomas]

Interesting. Is that due specifically to the axiomatization used by metamath that avoids substitution, or is that true generally?

[Patrick Thomas]

I guess I just expected that would have to be proved at the meta level.

[Mario Carneiro]

I don't think it's something special about the axiomatization: I mean it's a true theorem of FOL so as long as the axiomatization is something complete for FOL then that theorem should be provable

[Mario Carneiro]

The interesting observation is that it suffices to use theorems like that in lieu of built in alpha renaming

[Patrick Thomas]

That is cool.

[Mario Carneiro]

Same thing for the "not-free" predicate, which in metamath is a regular predicate defined as NF(x, ph) := (∃ x, ph) → (∀ x, ph)

[Mario Carneiro]

you can use NF(x, ph) as a substitute for actual not-free constraints in lemmas that require it

[Mario Carneiro]

This is not the usual not-free predicate defined in the metalogic, because for example NF(x, x = x) holds, but it is "just as good" from the point of view of provable theorems

[Mario Carneiro]

and there are lemmas that prove NF(x, ∀ x, ph) and NF(y, ph) -> NF(y, ∀ x, ph) and so on, so whenever a variable is not-free in an expression for an interesting reason (not just because it is not present in the expression), you can prove an NF lemma and then use a pred calc theorem that has an NF assumption

[Patrick Thomas]

Cool.

[Patrick Thomas]

So there are predicate calculus theorems that have the meta logic NF as a condition? How does that work without being able to do this? Wouldn't they have to jump to the level of meta theorems?

[Patrick Thomas]

Or are they in fact considered as meta theorems, and this allows you to move them down.

[Mario Carneiro]

No, there are predicate calculus theorems that have the object logic NF as a condition

[Mario Carneiro]

that is, the NF(x, ph) function I just mentioned

[Mario Carneiro]

for example NF(x, ph) -> ph -> ∀ x, ph is pretty easy to prove

[Mario Carneiro]

or NF(x, ph), ph -> ps |- ph -> ∀ x, ps

[Patrick Thomas]

But there are also predicate calculus theorems that have the meta logic NF as a condition?

[Mario Carneiro]

no, at least not in metamath. Theorems that would normally have an NF condition in FOL come in two flavors in metamath: either they have a disjointness requirement (not-present rather than not-free), or they have a NF condition. Not-present is stricter than not-free but is handled by metamath natively so it is easy to use, while NF is weaker than not-free and requires a subproof

[Patrick Thomas]

I guess I meant in textbooks.

[Patrick Thomas]

I thought maybe that is what you meant by "you can use NF(x, ph) as a substitute for actual not-free constraints in lemmas that require it".

[Patrick Thomas]

That there are lemmas in textbooks that use the meta logic (actual) version of it.

[Mario Carneiro]

Right. You take the textbook lemma, using the metalevel not-free constraint, and replace all instances of it with NF(x, ph)

[Mario Carneiro]

and that gives you a theorem that can be stated and proved in metamath

[Patrick Thomas]

Do the textbooks identify these as meta lemmas when they state them?

[Mario Carneiro]

In the textbooks these are all theorem schemes, since they usually have wff metavariables in them

[Patrick Thomas]

What is proved in metamath are theorem schemes too aren't they?

[Mario Carneiro]

Yes, but the scheme language is more restricted, to just substitution and distinctness

[Mario Carneiro]

anything beyond that has to be implemented inside the target language itself

[Patrick Thomas]

So meta, but not as meta? :)

[Mario Carneiro]

the scheme language in FOL is not rigidly defined, in principle you can do whatever you like by recursion on formulas, but generally includes at least not-free, proper substitution, alpha equality, and possibly the 3-ary not-free operation "y is free for x in t"

[Mario Carneiro]

For a more interesting example of an operation defined by recursion on formulas consider the double negation translation

[Patrick Thomas]

And everything that holds true at the object level using the usual axiom schemes holds true using metamath's restricted axiom schemes and vice versa?

[Mario Carneiro]

yes

[Patrick Thomas]

That's pretty cool. I would be interested in the proof, although I'm not sure I would be able to understand it.

[Patrick Thomas]

That's different than saying that the axiom schemes from one can be derived from the other and vice versa right?

[Patrick Thomas]

Because they are different at the meta level, so that wouldn't make sense.

[Mario Carneiro]

The axiom schemes of metamath should be true interpreted as FOL schemes, this is just soundness restated. The reverse doesn't work because unrestricted FOL schemes can't necessarily be expressed in metamath

[Patrick Thomas]

I see. Is that reverse direction at the same meta level and same idea as the deduction theorem showing that Hilbert and ND are equivalent?

[Mario Carneiro]

Some FOL schemes are mapped to metamath metatheorems, which is to say that each instance of the scheme corresponds to a metamath theorem

[Mario Carneiro]

the deduction theorem is one of these

[Patrick Thomas]

This gets confusing.

[Patrick Thomas]

So FOL schemes and metamath meta theorems are at the same level? How do you keep this all straight :)

[Patrick Thomas]

Is everything eventually embedded into a single higher level metalogic?

[Patrick Thomas]

That is, there is a single metalogic that can describe both FOL schemes and metamath metatheorems?

[Trebor Huang]

I think you shouldn't 'align' the levels of metamath and textbook FOL, that just gets confusing.

[Patrick Thomas]

They don't align? Don't they have to at some level in order to show that they are equivalent at the object level?

[Patrick Thomas]

Or at least doesn't there have to be a single meta logic that can describe them both?

[Mario Carneiro]

Metamath, like any formal system, has built in limits on what it can do natively. By contrast, mathematicians always dislike such restrictions and will "go meta" whenever they feel the need to. So the best you can hope for is to carve out a well defined subset of what mathematicians/logicians are doing and call it a formal system

[Mario Carneiro]

You can think of metamath like a traditional logic textbook written by someone who wanted to demonstrate that you can do FOL without defining not-free

[Patrick Thomas]

I guess that makes sense. They would still want to show that they are doing the same FOL though right?

[Patrick Thomas]

Hence the proofs that they are equivalent at the object level.

[Mario Carneiro]

well, most logic textbooks aren't too concerned with showing that they are equivalent to some other logic textbook. More important is that all the obviously true things can be derived

[Patrick Thomas]

I suppose that is true. I guess it would be easier if the axioms were more intuitive or obvious, which could also probably be said for the Hilbert axioms.

[Patrick Thomas]

I guess if you can show that they are complete and the definition of complete makes sense.

[Patrick Thomas]

Kind of an aside, but there is something that has always bothered me regarding meta logic. If I use a meta logic to prove that a logic is consistent (can not prove false and hence anything), how do I know that the meta logic I used is consistent? What if it is not, and I only proved that the logic is consistent because I can prove anything with the meta logic? Then don't I need a meta meta logic to prove that the meta logic is consistent and so on?

[Mario Carneiro]

sure that's true

[Mario Carneiro]

you can't really avoid that

[Mario Carneiro]

Any system of axioms comes with baseline assumptions. Without axioms you can't prove anything

[Mario Carneiro]

the best you can do is make sure the axioms are "obviously correct"

[Mario Carneiro]

or you can try not to engage with the question and use an off-the-shelf axiom system

[Patrick Thomas]

I see. Do the meta logics become increasingly simpler and more "obviously correct" the "higher" you go?

[Mario Carneiro]

they need not, it's up to you

[Patrick Thomas]

From what I have seen of the first level it appears to be about the same as the logic it is describing.

[Mario Carneiro]

but it is usually possible to have a PA-ish metalogic supporting an arbitrarily complicated object logic

[Patrick Thomas]

What does "PA-ish" mean?

[Mario Carneiro]

either peano arithmetic or a variation/subsystem of it

[Mario Carneiro]

like EFA (exponential function arithmetic) or PRA (primitive recursive arithmetic)

[Mario Carneiro]

if you try to make the system too weak it won't be able to support Godel's theorems

[Patrick Thomas]

The incompleteness theorems?

[Mario Carneiro]

yes

[Mario Carneiro]

You can run the argument with Robinson's Q, but since that system doesn't have induction, you need to do meta-induction to reason about it which means you have to step up another level

[Patrick Thomas]

The argument that it is "obviously correct"?

[Mario Carneiro]

it's pretty hard to argue that PA is not obviously correct

[Mario Carneiro]

you have to have a strange idea of what numbers are to be able to contemplate the inconsistency of PA

[Patrick Thomas]

I'm not sure what you meant about run the argument with Robinson's Q. Which argument?

[Patrick Thomas]

And why do you want to be able to support Godel's theorems?

[Mario Carneiro]

the argument for Godel's incompleteness theorem, which involves constructing a provability assertion inside the weak metalogic

[Mario Carneiro]

The systems that can prove Godel's theorems are "essentially undecidable", which is a good thing. Below that, you mostly have theories that are decidable, meaning that they can't model any interesting mathematics

[Mario Carneiro]

That is, a decidable theory can't be a metalogic for an undecidable theory because any question in the object logic can be reformulated as a question in the metalogic

[Mario Carneiro]

and since ultimately we want to do mathematics in interesting and undecidable domains, this forms a bare minimum requirement on the metalogic

[Mario Carneiro]

Although I should give an honorable mention to self-verifying theories, which live somewhere below Q (usually by not validating the totality of multiplication) and satisfying T |- Con(T)

[Patrick Thomas]

That makes sense.

[Patrick Thomas]

Although proving their own consistency sounds like a circular argument?

[Mario Carneiro]

It's not circular, since consistency of T is not a precondition of the proof

[Mario Carneiro]

in fact if T was inconsistent then T |- Con(T) would hold trivially

[Mario Carneiro]

Of course the interesting thing about self-verifying theories is that they are in fact consistent in addition to being able to prove they are consistent inside themselves

[Patrick Thomas]

What does "in fact consistent" mean?

[Mario Carneiro]

in the case of Willard's axiom systems this is usually ensured by having the theory be a subsystem of PA

[Patrick Thomas]

Why does that mean "in fact"?

[Mario Carneiro]

What I mean is, it's consistent from an "external viewpoint", not merely in T's opinion

[Mario Carneiro]

since, as mentioned, if T was inconsistent it would prove its own consistency

[Mario Carneiro]

this is the "uninteresting case" of self-verification

[Mario Carneiro]

Of course you can question the consistency of any theory, including PA, but you have to throw out the vast majority of mathematics in the world to take that position. I can prove Con(PA) in lean with no axioms

[Patrick Thomas]

You mean just from type theory?

[Patrick Thomas]

So are you basically using a sort of induction with the proof within T that T is consistent? That is, let each level of the meta logic just be T?

[Patrick Thomas]

And since we know we can always prove the consistency of T from T...

[Trebor Huang]

Lean proves Con(PA), but PA never proves Con(PA)

[Trebor Huang]

That's Goedel's incompleteness theorem.

[Trebor Huang]

Of course, unless PA is inconsistent, in which case PA proves anything by ex falso.

[Patrick Thomas]

It seems kind of oddly concrete that the level is arithmetic that the incompleteness theorem takes affect.

[Mario Carneiro]

That's the level where undecidability starts to pop up, for example in diophantine equations

[Patrick Thomas]

I guess I would have expected it to be more abstract, like some subset of the set theory axioms.

[Mario Carneiro]

I don't think it has to be arithmetical, but historically that's where it's easiest to state these types of theories

[Patrick Thomas]

I see.

[Mario Carneiro]

The set theory axioms generally blow past this level pretty quickly

[Mario Carneiro]

once you have something that acts like a successor function like {x} you can usually already do all this stuff

[Trebor Huang]

One thing though: I don't immediately see how Lean proves Con(PA) without excluded middle, is there any reference?

[Mario Carneiro]

I was actually writing that up right now

[Mario Carneiro]

it's not too hard to see that it should be possible: nat has decidable equality

[Mario Carneiro]

plus Con(PA) is a negative statement so intuitionism doesn't get in the way much

[Trebor Huang]

Yeah I guess so, but it would be cool to see the complete proof done ;)

[Patrick Thomas]

Along the same lines, is there a written, maybe formal, proof that the axioms of metamath are equivalent at the object level to say the axioms of ND?

[Patrick Thomas]

Not sure if I would understand it, but might be interesting to try to.

[Trebor Huang]

I think there's Meredith's work, which is mildly relevant(?)

[Mario Carneiro]

Something like http://us.metamath.org/mpeuni/natded.html?

[Patrick Thomas]

So I guess that shows that everything proven in ND can be proven from metamath. And the other way is shown because every axiom of metamath is a theorem of the Hilbert system, and the Hilbert system has been shown through the deduction theorem to be equivalent at the object level to ND?

[Mario Carneiro]

I found a way to cheat enough to make an easy proof of Con(PA):

inductive proof : Prop → Prop
prefix `⊢`:30 := proof
| refl (x : ℕ) : ⊢ x = x
| symm (x y : ℕ) : ⊢ x = y → ⊢ y = x
| trans (x y z : ℕ) : ⊢ x = y → ⊢ y = z → ⊢ x = z
| succ_inj (x y : ℕ) : ⊢ (x = y ↔ nat.succ x = nat.succ y)
| succ_ne_zero (x y : ℕ) : ⊢ nat.succ x ≠ 0
| induction (P : ℕ → Prop) : ⊢ (P 0 → (∀ x, P x → P x.succ) → ∀ x, P x)
| add_zero (a : ℕ) : ⊢ a + 0 = a
| add_succ (a b : ℕ) : ⊢ a + b.succ = (a + b).succ
| mul_zero (a : ℕ) : ⊢ a * 0 = 0
| mul_succ (a b : ℕ) : ⊢ a * b.succ = a * b + a
prefix `⊢`:30 := proof

theorem proof.sound {p} (h : ⊢ p) : p :=
begin
  induction h,
  case refl : x { exact rfl },
  case symm : x y h ih { exact ih.symm },
  case trans : x y z h₁ h₂ ih₁ ih₂ { exact ih₁.trans ih₂ },
  case succ_inj : x y { exact ⟨congr_arg _, nat.succ.inj⟩ },
  case succ_ne_zero : x y { exact nat.succ_ne_zero _ },
  case induction : P P0 Ps n { exact nat.rec_on n P0 Ps },
  case add_zero { exact rfl },
  case add_succ { exact rfl },
  case mul_zero { exact rfl },
  case mul_succ { exact rfl },
end

theorem con_pa : ¬ ⊢ 0 = 1 := λ h, absurd h.sound dec_trivial
#print axioms con_pa -- no axioms

[Trebor Huang]

That looks very much like how the Church's simple theory of types deals with propositions: There's no Curry-Howard correspondence, and there is a separate relation |- for proposition derivability, with separate axioms.

[Trebor Huang]

But that's currently incomplete as I see it. You don't even have modus ponens, right?

[Mario Carneiro]

it's a bit annoying that the wikipedia article barely acknowledges this

[Patrick Thomas]

Thank you for the help! I'm going to sleep now :)

[Mario Carneiro]

Okay, here's a slightly less cheating version, which embeds classical logic via the wff type, even though we aren't assuming any classical axioms on Prop

inductive wff
| eq : ℕ → ℕ → wff
| not : wff → wff
| imp : wff → wff → wff
| all : (ℕ → wff) → wff
infix ` ≃ `:60 := wff.eq
infixr ` ⇒ `:50 := wff.imp
prefix `~`:59 := wff.not
def wff.and (x y : wff) := ~(x ⇒ ~y)
infix ` && `:55 := wff.and
def wff.or (x y : wff) := ~x ⇒ y
infix ` || `:54 := wff.or
def wff.iff (x y : wff) := (x ⇒ y) && (y ⇒ x)
infix ` ⇔ `:53 := wff.iff
notation `𝔸` binders `, ` b:scoped := wff.all b

inductive proof : wff → Prop
prefix `⊢ `:30 := proof
| ax_1 (p q : wff) : ⊢ p ⇒ q ⇒ p
| ax_2 (p q r : wff) : ⊢ (p ⇒ q ⇒ r) ⇒ (p ⇒ q) ⇒ (p ⇒ r)
| ax_3 (p q : wff) : ⊢ (~p ⇒ ~q) ⇒ q ⇒ p
| mp (p q : wff) : ⊢ p ⇒ q → ⊢ p → ⊢ q
| gen (p : ℕ → wff) : (∀ x, ⊢ p x) → ⊢ 𝔸 x, p x
| ax_4 (p : ℕ → wff) (t : ℕ) : ⊢ (𝔸 x, p x) ⇒ p t
| ax_5 (p q : ℕ → wff) : ⊢ (𝔸 x, p x ⇒ q x) ⇒ (𝔸 x, p x) ⇒ (𝔸 x, q x)
| ax_6 (p : wff) : ⊢ p ⇒ (𝔸 x, p)
| refl (x : ℕ) : ⊢ x ≃ x
| symm (x y : ℕ) : ⊢ x ≃ y → ⊢ y ≃ x
| trans (x y z : ℕ) : ⊢ x ≃ y → ⊢ y ≃ z → ⊢ x ≃ z
| subst (x y : ℕ) (p : ℕ → wff) : ⊢ x ≃ y ⇒ p x ⇒ p y
| succ_inj (x y : ℕ) : ⊢ x ≃ y ⇔ x.succ ≃ y.succ
| succ_ne_zero (x y : ℕ) : ⊢ ~(x.succ ≃ 0)
| induction (P : ℕ → wff) : ⊢ (P 0 ⇒ (𝔸 x, P x ⇒ P x.succ) ⇒ 𝔸 x, P x)
| add_zero (a : ℕ) : ⊢ a + 0 ≃ a
| add_succ (a b : ℕ) : ⊢ a + b.succ ≃ (a + b).succ
| mul_zero (a : ℕ) : ⊢ a * 0 ≃ 0
| mul_succ (a b : ℕ) : ⊢ a * b.succ ≃ a * b + a
prefix `⊢ `:30 := proof

def wff.val : wff → Prop
| (x ≃ y) := x = y
| (~ x) := ¬ x.val
| (x ⇒ y) := x.val → y.val
| (wff.all p) := ∀ x, (p x).val

theorem wff.dne : ∀ x : wff, ¬¬x.val → x.val
| (x ≃ y) h := @decidable.of_not_not (x = y) _ h
| (~ x) h := not_of_not_not_not h
| (x ⇒ y) h := λ hx, y.dne $ λ hy, h $ λ hi, hy (hi hx)
| (wff.all p) h := λ x, (p x).dne $ λ hx, h $ λ ha, hx $ ha x

theorem proof.sound {p} (h : ⊢ p) : p.val :=
begin
  induction h,
  case ax_1 : p q { exact λ a b, a },
  case ax_2 : p q r { exact λ a b c, a c (b c) },
  case ax_3 : p q { exact λ a b, p.dne $ λ h, a h b },
  case mp : p q h₁ h₂ ih₁ ih₂ { exact ih₁ ih₂ },
  case gen : p h ih { exact ih },
  case ax_4 : p x { exact λ h, h x },
  case ax_5 : p q { exact λ a b x, a x (b x) },
  case ax_6 : p { exact λ h x, h },
  case refl : x { exact rfl },
  case symm : x y h ih { exact ih.symm },
  case trans : x y z h₁ h₂ ih₁ ih₂ { exact ih₁.trans ih₂ },
  case subst : x y p { exact λ (e:x=y) h, e ▸ h },
  case succ_inj : x y { exact λ h, h (congr_arg _) nat.succ.inj },
  case succ_ne_zero : x y { exact nat.succ_ne_zero _ },
  case induction : P { exact λ P0 Ps n, nat.rec_on n P0 Ps },
  case add_zero { exact rfl },
  case add_succ { exact rfl },
  case mul_zero { exact rfl },
  case mul_succ { exact rfl },
end

theorem con_pa : ¬ ⊢ 0 ≃ 1 := λ h, absurd h.sound (dec_trivial : 0 ≠ 1)
#print axioms con_pa -- no axioms

[Patrick Thomas]

Patrick Thomas said:

If I move the last code example that I posted from propositional logic to predicate logic, do I understand correctly that applying a theorem will then require replacing each free term variable with a syntactically correct term scheme, taking into account potential free variable capture, in addition to the replacement of propositional variables (predicate variables of arity 0) that is already done in the current propositional case?

If you substitute a formula in for a propositional variable, do you at the same time have to substitute in for each of the propositional variables and each of the free term variables in that formula? And so on recursively?

[Mario Carneiro]

No. The variables in the formula will be variables in the current context

[Patrick Thomas]

Ok. Thank you.

[Mario Carneiro]

there is some "second order subtitution" going on in the code for substituting into a second order variable, for example if we want to substitute P(x, y) := a < b + x into a theorem scheme like all z, ex w, P(z + 1, w) we have to substitute z + 1, w for x, y to get a < b + (z + 1) and then replace P(z + 1, w) with this a < b + (z + 1) formula in the original expression all z, ex w, P(z + 1, w) to get all z, ex w, a < b + (z + 1), but that's as far as it goes. (You would need third order substitution if the variables z and w could themselves be higher order objects appearing as z(u) in the expression.)

[Mario Carneiro]

If you only have 0-ary formula and term variables then you only need one level of substitution

[Patrick Thomas]

Mario Carneiro said:

If you only have 0-ary formula and term variables then you only need one level of substitution

I'm not sure if I do or not. I mean I have predicate variables which can have arbitrary arity. But are you maybe referring to higher order logics, that is beyond first order logic, where for example you can generalize over propositions?

[Mario Carneiro]

The question is whether you can substitute for those predicate variables of nonzero arity

[Mario Carneiro]

I assume you can, in which case you have the second order substitution process I mentioned

[Mario Carneiro]

This is second order logic "lite"

[Mario Carneiro]

since you don't have arbitrary quantification over those predicate variables

[Patrick Thomas]

I don't think I can. I mean you can substitute for the terms in them, but I don't have it that you can replace them entirely, which are different things right?

[Patrick Thomas]

I'm trying to stick to just FOL for now.

[Mario Carneiro]

Right I mean if you have a lemma like (all x, P(x) -> Q(x)) -> (all x, P(x)) -> (all x, Q(x)) and you say "I want to use this lemma with P(x) := 2 < x and Q(x) := 0 < x"

[Mario Carneiro]

Without such a mechanism it's not very useful to prove FOL schemes

[Mario Carneiro]

Basically the predicate variables aren't variables at all, they are constants

[Patrick Thomas]

Maybe it will be easier if I post what I have of the code so far.

[Patrick Thomas]

Let me clean it up a bit.

[Mario Carneiro]

What I'm saying is that if you can't substitute for predicate variables then they aren't variables

[Mario Carneiro]

that's what it means to be a variable

[Mario Carneiro]

Predicate constants are useful too, for example \in and < are predicate constants

[Mario Carneiro]

you wouldn't expect to be able to substitute them with expressions

[Patrick Thomas]

There are probably errors, but I think this gives the general idea:

{-
allVar t = The set of the names of all of the variables that occur in
the term t.
-}
allVar :: Term -> Data.Set.Set String
allVar (Var v) = Data.Set.singleton v
allVar (Func _ ts) = Data.Set.unions (Prelude.map allVar ts)

{-
allFreeVar p = The set of the names of all of the variables that occur
free in the formula p.
-}
allFreeVar :: Formula -> Data.Set.Set String
allFreeVar (Pred _ ts) = Data.Set.unions (Prelude.map allVar ts)
allFreeVar Bottom = Data.Set.empty
allFreeVar (Imp p q) = Data.Set.union (allFreeVar p) (allFreeVar q)
allFreeVar (Forall v p) = Data.Set.delete v (allFreeVar p)


{-

-}
subEachInForm :: Formula ->
                 Data.Map.Map String Term ->
                 Data.Map.Map String Formula ->
                 Formula

subEachInForm f t_map f_map = go Data.Set.empty f t_map f_map where
  go :: Data.Set.Set String ->
        Formula ->
        Data.Map.Map String Term ->
        Data.Map.Map String Formula ->
        Formula

  go binders (Pred name []) _ f_map =
    let f' = f_map ! name in
    if Data.Set.disjoint (allFreeVar f') binders
    then f'
    else error "free variable capture"

  go binders (Pred name ts) t_map _ =
        Pred name (Data.List.map (\t -> subEachInTerm binders t t_map) ts) where
          subEachInTerm :: Data.Set.Set String ->
                           Term ->
                           Data.Map.Map String Term ->
                           Term

          subEachInTerm (binders Var v) t_map =
            if v `Data.Set.member` binders then Var v else
            let t = t_map ! v in
            if Data.Set.disjoint (allVar t) binders
            then t
            else error "free variable capture"

          subEachInTerm binders (Func name ts) t_map =
            Func name (Data.List.map (\t -> subEachInTerm binders t t_map) ts)

  go _ Bottom _ _ = Bottom

  go binders (Imp p q) t_map f_map =
    Imp (subEachInForm binders p t_map f_map) (subEachInForm binders q t_map f_map)

  go binders (Forall v p) =
    Forall v (subEachInForm (Data.Set.insert v binders) p t_map f_map)

[Mario Carneiro]

shouldn't the last case

  go binders (Forall v p) =
    Forall v (subEachInForm (Data.Set.insert v binders) p t_map f_map)

be calling go recursively?

[Patrick Thomas]

Yep.

[Mario Carneiro]

also protip you don't need to pass things that are fixed in the recursion to go

[Mario Carneiro]

like f_map and t_map

[Patrick Thomas]

Yeah, I started out thinking I might need to recursively descend for the propositional case and would need them.

[Patrick Thomas]

Or something like that.

[Mario Carneiro]

This code is roughly what I expected. You aren't substituting for predicate variables, which means that you can't prove schemes over predicates and use them later

[Patrick Thomas]

What will be the drawbacks of not being able to do that?

[Patrick Thomas]

Are there things I can't prove, or will it just be lot harder to prove them?

[Mario Carneiro]

Mario Carneiro said:

Right I mean if you have a lemma like (all x, P(x) -> Q(x)) -> (all x, P(x)) -> (all x, Q(x)) and you say "I want to use this lemma with P(x) := 2 < x and Q(x) := 0 < x"

[Mario Carneiro]

In order to do this you would need to replay the proof in the specific case (all x, 2 < x -> 0 < x) -> (all x, 2 < x) -> (all x, 0 < x)

[Patrick Thomas]

Yeah, that sounds like an issue.

[Patrick Thomas]

But I have to implement another level for every arity I want to support?

[Mario Carneiro]

I refer you back to substFormula from https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ITP.20for.20FOL.20.2B.20ZFC/near/269903509

[Mario Carneiro]

That handles arbitrary arity

[Mario Carneiro]

it doesn't handle third order variables but you don't have those anyway

[Patrick Thomas]

Wait, what is the difference between arity and order?

[Mario Carneiro]

• x : nat : first order
• P : nat -> Prop: second order, arity 1
• P : nat -> nat -> Prop: second order, arity 2
• P : (nat -> Prop) -> Prop: third order, arity 1

[Mario Carneiro]

An nth order variable takes (any number of) arguments of order n-1

[Patrick Thomas]

Which order would a propositional variable be? P : Prop?

[Mario Carneiro]

I would usually refer to them as second order variables for consistency with the predicates, but you could also consider them as first order

[Mario Carneiro]

you can always code a proposition as a nat, using if p then 1 else 0, so it's possible to smuggle propositions when only first order / nat variables are allowed

[Mario Carneiro]

but of course you can't code a nat -> Prop as a nat, that's cantor's theorem

[Patrick Thomas]

Mario Carneiro said:

I refer you back to substFormula from https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ITP.20for.20FOL.20.2B.20ZFC/near/269903509

I'm sorry, I was having trouble following your code from earlier, so I thought it might make more sense to me to incrementally build my code up from prop logic and see what I needed to change.

[Patrick Thomas]

So, what are the rules to additionally substitute for a predicate variable of arity > 0? What can I substitute for what under what conditions?

[Patrick Thomas]

From the code it seems maybe you can substitute one predicate for another if there aritys match?

[Mario Carneiro]

that's certainly a necessary condition

[Mario Carneiro]

Think of it from the HOL perspective. We have a term like P(x, y) and we want to substitute a lambda like P := \lam u v -> foo into it

[Mario Carneiro]

obviously the number of lambda binders has to match the number of arguments to P

[Patrick Thomas]

I'm guessing there are also conditions to prevent free variable capture?

[Mario Carneiro]

Here's a fairly generic situation:

substitute
P(u, v) := ∀ b, u < a ∧ v < b
into
∀ x z, P(x, y)
to get
∀ x z, ∀ b, x < a ∧ y < b

• We start with an expression for P that has a a free variable (referring to something external) and b a bound variable, and the parameters u and v.
• In the final result, a should still be a free variable: therefore it must not clash with the binders it was placed under, namely x and z
• Additionally, x and y were not previously under the b binder but have been moved under it in the result, thus they also must not clash

[Mario Carneiro]

Basically any time we have an expression in an outer context with some free variables in it and we want to insert it somewhere under a binder, none of the free variables can clash with the binder

[Mario Carneiro]

This happens twice in the example, we took the expression λ u v, ∀ b, u < a ∧ v < b with free variable a and moved it under the binders ∀ x z, so a must not clash with x, z, and then we took the expressions x, y with free variables x, y and moved them under the binder ∀ b, so b must not clash with x, y

[Patrick Thomas]

I'm not sure if I have ever seen that kind of substitution before.

[Mario Carneiro]

In higher order logic we would only do the first part, substituting P := λ u v, ∀ b, u < a ∧ v < b and resulting in

∀ x z, (λ u v, ∀ b, u < a ∧ v < b)(x, y)

[Mario Carneiro]

we might beta reduce it later, resulting in more constraints / alpha renaming

[Mario Carneiro]

here we're trying to stick to first order so we always eliminate lambdas before they appear

[Patrick Thomas]

Free variables and parameters are not the same? What are parameters in my implementation, if I have any?

[Mario Carneiro]

hopefully my terminology is clear from the example

[Mario Carneiro]

a is a free variable, u is a parameter

[Mario Carneiro]

which is to say, it is a "bound variable" bound by the lambda

[Mario Carneiro]

even though we don't have any explicit lambda here

[Mario Carneiro]

in my code earlier, the parameters are the [String] in the M.Map String ([String], Int) of the formula substitution map

[Patrick Thomas]

Is there a dependent type here? There are both lambdas and a forall?

[Mario Carneiro]

Lambda isn't formally a part of the syntax, but we are substituting for a predicate so there is morally a lambda involved

[Mario Carneiro]

I've been writing these predicate substitutions as P(u, v) := ∀ b, u < a ∧ v < b or P := λ u v, ∀ b, u < a ∧ v < b

[Mario Carneiro]

lambda only appears at the top level here, the syntax is a list of variable names followed by a formula

[Mario Carneiro]

like ([u, v], ∀ b, u < a ∧ v < b)

[Patrick Thomas]

I mean, is there a parameter in the definition I have of Formula? Is it the variable name after the Forall?

[Mario Carneiro]

no, I'm using the term parameter just for the lambda-bound arguments

[Mario Carneiro]

the variables in a forall are just bound variables

[Mario Carneiro]

so b is a bound variable in the running example

[Patrick Thomas]

I guess I'm not sure what lambda bound means here. Do I have to extend the Formula def?

[Mario Carneiro]

no

[Mario Carneiro]

A predicate substitution consists of a variable to replace, P, a list of variables [u, v], and a formula ∀ b, u < a ∧ v < b

[Mario Carneiro]

Mario Carneiro said:

I've been writing these predicate substitutions as P(u, v) := ∀ b, u < a ∧ v < b or P := λ u v, ∀ b, u < a ∧ v < b

[Patrick Thomas]

So you just decide which variables are going to be parameters when you decide to do a substitution?

[Mario Carneiro]

Mario Carneiro said:

in my code earlier, the parameters are the [String] in the M.Map String ([String], Int) of the formula substitution map

[Mario Carneiro]

you get to make a new formula substitution map any time you apply a lemma

[Mario Carneiro]

so the parameters can be different if you want

[Mario Carneiro]

the formula will usually be different too

[Patrick Thomas]

But it has to be a well formed formula right?

[Patrick Thomas]

Can we go step by step for what gets replaced by what?

[Patrick Thomas]

Suppose I have the predicate Pred "P" [Var (x), (Func "f" [Var "y"])] I guess.

[Patrick Thomas]

Although maybe that is not a proof scheme, so it doesn't work.

[Patrick Thomas]

Can you substitute into predicates over arbitrary terms or just predicates of individual variables. Like I think I have only seen substitutions into things like P(x,y)?

[Patrick Thomas]

I'm sorry, maybe I need a more detailed paper or textbook or something.

[Patrick Thomas]

This kind of substitution is new to me, I think.

[Patrick Thomas]

Is there some kind of arbitrary predicate that we can only replace? We can't replace specific predicates like "x < y" with something like "x = y" right?

[Mario Carneiro]

I changed x to f(x) in the example to emphasize that P is being applied to terms not variables

[Mario Carneiro]

u is a variable, but P(f(x), y) can have arbitrary terms there

[Mario Carneiro]

Patrick Thomas said:

Is there some kind of arbitrary predicate that we can only replace? We can't replace specific predicates like "x < y" with something like "x = y" right?

Ah, yes you might need to distinguish these since you haven't been doing so thus far. There are predicate constants and predicate variables and you can only substitute for variables

[Mario Carneiro]

< is a predicate constant

[Mario Carneiro]

definitions produce new predicate constants, and axiomatic constants like = are also constants

[Mario Carneiro]

The code that you wrote before for the Pred name ts case is appropriate for predicate constants

[Patrick Thomas]

Hmm. Ok. How would my data types change? What is an appropriate constructor for a predicate variable?

[Mario Carneiro]

same as constants

[Mario Carneiro]

the only difference is that variables are substituted and constants aren't

[Patrick Thomas]

So they can take arbitrary terms, not just Var?

[Mario Carneiro]

yes

[Mario Carneiro]

Mario Carneiro said:

u is a variable, but P(f(x), y) can have arbitrary terms there

[Patrick Thomas]

How do you distinguish them in the code? I mean, I have no real data type for axiomatic constants right?

[Patrick Thomas]

Can we go more slowly through an example substitution using the notation from the code?

[Patrick Thomas]

Actually, I should probably go to sleep. Thank you for your patience.

[Mario Carneiro]

I don't really want to drag this out on a public channel

[Patrick Thomas]

Ok.

[Patrick Thomas]

Sorry.

[Patrick Thomas]

Thank you for your time.

[Mario Carneiro]

perhaps you should PM me or we can have a video discussion or something, I just don't want the hundreds of other people who read #general to deal with it if it isn't of general interest

[Mario Carneiro]

I'm not against discussing this stuff for far longer than appropriate but I should probably moderate at some point

[Patrick Thomas]

:) Ok. I'll see what I can find for texts, papers first.

[Trebor Huang]

Apart from efficiency concerns, there's actually no need to distinguish < as constants. They can be replaced, as long as you are also replacing them consistently in the axioms.

[Trebor Huang]

So declaring < as a constant serves only to say "hey, this thing is present in the axioms, so you can't just replace it without touching the axioms".

[Mario Carneiro]

You definitely can't replace definitions, you might have used the definition in the proof

[Mario Carneiro]

You can't replace axiomatic constants either since they might be used in axioms (e.g. replace = with < in x = x)

[Mario Carneiro]

That is, I think this only works if you don't have a concept of "global context" which is not subject to substitution

[Patrick Thomas]

Given this definition:

structure interpretation (domain : Type) : Type :=
(nonempty : nonempty domain)
(func (n : ℕ) : string → (fin n → domain) → domain)
(pred (n : ℕ) : string → (fin n → domain) → Prop)

If I have an instance m of interpretation and a function s : string -> string, is there a way to create a new instance m' of interpretation such that m'.nonempty = m.nonempty, m'.func = m.func and if m.pred = 0 p terms then m'.pred = 0 (s p) terms and is m.pred for n != 0?

I am trying to prove this: https://github.com/pthomas505/lean3/blob/ba0e7d74687a84729d8f0bf1db9c186c89c63937/src/metalogic/pred.lean#L1648

[Patrick Thomas]

Should this theorem hold?

[Mario Carneiro]

that theorem is only true in the forward direction. For example, P -> Q is not a tautology but a substitution instance of it is P -> P which is a tautology

[Patrick Thomas]

I see. So just is_valid P -> is_valid (sub_prop s P) holds?

[Patrick Thomas]

Ok.

[Patrick Thomas]

Thank you.

[Patrick Thomas]

Should s be of type string -> string or string -> formula? I'm guessing the latter, based on the propositional calculus case.

[Patrick Thomas]

Hmm, I need to check for variable capture then.

[Patrick Thomas]

I was wondering if anyone could help me figure out how to show that term and formula are instances of decidable_eq? If I add @[derive decidable_eq] in front of the definition of term I get:

invalid user defined recursor, motive result sort must be Prop or Type.{l} where l is a universe parameter

If I add it in front of the definition of formula I get:

mk_dec_eq_instance failed, failed to generate instance for
  Π (a b : fin n → term), decidable (a = b)

import data.finset

inductive term : Type
| var : string → term
| func (n : ℕ) : string → (fin n → term) → term

open term

inductive formula : Type
| bottom : formula
| top : formula
| atom (n : ℕ) : string → (fin n → term) → formula
| not : formula → formula
| and : formula → formula → formula
| or : formula → formula → formula
| imp : formula → formula → formula
| iff : formula → formula → formula
| forall_ : string → formula → formula
| exists_ : string → formula → formula

[Alex J. Best]

I don't know if the default derive handler can really be expected to do this. It relies on the fact that fin is a fintype naturally.
Here is a proof anyways, would be great if it can be improved but it is the best I could do

import data.finset

inductive term : Type
| var : string → term
| func (n : ℕ) : string → (fin n → term) → term


variables {p q : Prop}
def pi_decide [decidable p] (h : p → decidable q) : decidable (p ∧ q) :=
if hp : p then
  by haveI := h hp; exact
  if hq : q then is_true ⟨hp, hq⟩
  else is_false (assume h : p ∧ q, hq (and.right h))
else is_false (assume h : p ∧ q, hp (and.left h))

open term
instance : decidable_eq term
| (var s₁) (var s₂) := decidable_of_decidable_of_iff (by apply_instance : decidable (s₁ = s₂)) (by simp)
| (var s) (func n s' t) := is_false (by simp)
| (func n s' t) (var s) := is_false (by simp)
| (func n₁ s₁ t₁) (func n₂ s₂ t₂) := decidable_of_decidable_of_iff
  (begin
    apply' pi_decide,
    intro h,
    apply' and.decidable,
    rw fin.heq_fun_iff h,
    apply' fintype.decidable_forall_fintype,
    intro a,
    apply term.decidable_eq,
  end : decidable $ n₁ = n₂ ∧ s₁ = s₂ ∧ t₁ == t₂) (by simp)


#eval to_bool $ term.func 2 "f" (λ x, term.var "x") =
      term.func (1 + 1) "f" (λ x, term.var "y")

open term

@[derive decidable_eq]
inductive formula : Type
| bottom : formula
| top : formula
| atom (n : ℕ) : string → (fin n → term) → formula
| not : formula → formula
| and : formula → formula → formula
| or : formula → formula → formula
| imp : formula → formula → formula
| iff : formula → formula → formula
| forall_ : string → formula → formula
| exists_ : string → formula → formula

@Patrick Thomas

[Patrick Thomas]

Thank you!

[Patrick Thomas]

https://proofassistants.stackexchange.com/questions/1537/creating-a-proof-assistant-for-first-order-logic-in-haskell

[Patrick Thomas]

Is there an implementation in Lean or Haskell of the algorithm that Lean uses for the locally nameless representation?

[Patrick Thomas]

I would like to try to see how that translates to a representation for FOL.

[Patrick Thomas]

Is there a way to simplify these, for example if there exist definitions in mathlib that avoid the need to convert the fin function to a list?
https://github.com/pthomas505/lean3/blob/06c3f0981ed301f4c4e5c447cb648e33a17e2fcd/src/metalogic/pred.lean#L2593-L2702

[Patrick Thomas]

I don't look forward to trying to prove things about them as they are :)

[Patrick Thomas]

I'm trying to formalize the substitution of predicates as described here and then prove that this substitution preserves the validity of formulas. I'm wondering if anyone has any advice on how to go about doing this. Is there a proof somewhere, either formal or informal?

[Patrick Thomas]

I have been having a hard time finding references to it, and I'm not sure why.

[Patrick Thomas]

My code base is here.