## Stream: general

### Topic: ITP for FOL + ZFC

#### Patrick Thomas (Jan 03 2022 at 03:30):

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 (Jan 03 2022 at 04:07):

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 (Jan 03 2022 at 04:10):

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

#### Patrick Thomas (Jan 03 2022 at 17:24):

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 (Jan 03 2022 at 17:52):

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 (Jan 03 2022 at 17:53):

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

#### Patrick Thomas (Jan 03 2022 at 17:59):

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 (Jan 03 2022 at 18:09):

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

#### Reid Barton (Jan 03 2022 at 18:11):

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 (Jan 03 2022 at 18:28):

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 (Jan 03 2022 at 18:29):

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

#### Huỳnh Trần Khanh (Jan 03 2022 at 18:35):

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 (Jan 03 2022 at 18:38):

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 (Jan 03 2022 at 18:40):

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 (Jan 03 2022 at 18:43):

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 (Jan 03 2022 at 18:45):

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

#### Reid Barton (Jan 03 2022 at 18:46):

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 (Jan 03 2022 at 18:48):

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 (Jan 03 2022 at 18:48):

you probably want a newtype, not just a type alias

#### Reid Barton (Jan 03 2022 at 18:51):

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.

I see.

#### Reid Barton (Jan 03 2022 at 18:56):

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 (Jan 03 2022 at 18:58):

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 (Jan 03 2022 at 19:00):

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

#### Reid Barton (Jan 03 2022 at 19:00):

And you want to export Formula(..) too

#### Reid Barton (Jan 03 2022 at 19:00):

You will need it to apply axiom schemas

#### Reid Barton (Jan 03 2022 at 19:01):

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

Ok.

#### Patrick Thomas (Jan 04 2022 at 18:34):

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 (Jan 04 2022 at 18:39):

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 (Jan 04 2022 at 18:40):

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 (Jan 04 2022 at 18:41):

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 (Jan 04 2022 at 19:58):

I see. Thank you.

#### Patrick Thomas (Jan 04 2022 at 22:41):

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 (Jan 05 2022 at 04:08):

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 (Jan 05 2022 at 04:10):

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

#### Patrick Thomas (Jan 05 2022 at 04:14):

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 (Jan 05 2022 at 04:20):

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

#### Patrick Thomas (Jan 05 2022 at 06:44):

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 (Jan 05 2022 at 17:54):

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 (Jan 05 2022 at 18:32):

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 (Jan 05 2022 at 19:56):

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 (Jan 05 2022 at 22:02):

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

#### Trebor Huang (Jan 05 2022 at 22:03):

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 (Jan 05 2022 at 22:06):

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 (Jan 05 2022 at 22:09):

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 (Jan 05 2022 at 22:26):

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 (Jan 05 2022 at 22:29):

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 (Jan 05 2022 at 23:00):

Is the code correct as is?

#### Mario Carneiro (Jan 05 2022 at 23:26):

no, it gives an error at refl:

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

#### Patrick Thomas (Jan 05 2022 at 23:28):

I'm sorry, I meant the Haskell code.

#### Patrick Thomas (Jan 09 2022 at 01:43):

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?

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 (Jan 09 2022 at 01:44):

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

#### Patrick Thomas (Jan 09 2022 at 01:46):

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 (Jan 09 2022 at 01:48):

The full code for reference:
nd.hs

#### Trebor Huang (Jan 09 2022 at 07:02):

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

#### Trebor Huang (Jan 09 2022 at 07:03):

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 (Jan 09 2022 at 07:05):

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 (Jan 09 2022 at 08:00):

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

yep

#### Trebor Huang (Jan 09 2022 at 09:09):

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

#### Patrick Thomas (Jan 09 2022 at 15:38):

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 (Jan 09 2022 at 21:07):

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

#### Patrick Thomas (Jan 09 2022 at 21:38):

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 (Jan 10 2022 at 06:02):

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 (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 (Jan 10 2022 at 06:07):

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

#### Trebor Huang (Jan 10 2022 at 06:17):

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

#### Patrick Thomas (Jan 10 2022 at 06:18):

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

#### Trebor Huang (Jan 10 2022 at 06:35):

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

#### Patrick Thomas (Jan 10 2022 at 06:44):

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

#### Patrick Thomas (Jan 10 2022 at 06:45):

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

#### Trebor Huang (Jan 10 2022 at 06:55):

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

#### Trebor Huang (Jan 10 2022 at 06:56):

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

#### Patrick Thomas (Jan 10 2022 at 07:00):

I think I see. Thank you.

#### Patrick Thomas (Jan 11 2022 at 01:15):

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 (Jan 11 2022 at 01:43):

@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 (Jan 11 2022 at 01:48):

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

#### Patrick Thomas (Jan 11 2022 at 01:49):

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

#### Mario Carneiro (Jan 11 2022 at 01:54):

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

#### Patrick Thomas (Jan 11 2022 at 01:57):

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 (Jan 11 2022 at 01:58):

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 (Jan 11 2022 at 02:01):

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 (Jan 11 2022 at 02:02):

Or maybe identifier is a better term than name?

#### Mario Carneiro (Jan 11 2022 at 02:05):

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 (Jan 11 2022 at 02:05):

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

#### Patrick Thomas (Jan 11 2022 at 02:09):

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 (Jan 11 2022 at 02:10):

As in, x -> forall x.

lam 0, but yes

#### Mario Carneiro (Jan 11 2022 at 02:12):

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

#### Mario Carneiro (Jan 11 2022 at 02:13):

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

#### Patrick Thomas (Jan 11 2022 at 02:13):

Why would it already be zero?

#### Mario Carneiro (Jan 11 2022 at 02:14):

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

#### Mario Carneiro (Jan 11 2022 at 02:14):

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

#### Mario Carneiro (Jan 11 2022 at 02:15):

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 (Jan 11 2022 at 02:16):

You mean in going from named variables to de bruijn?

yes

#### Mario Carneiro (Jan 11 2022 at 02:17):

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

#### Patrick Thomas (Jan 11 2022 at 02:21):

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 (Jan 11 2022 at 02:23):

Just for each term right?

#### Patrick Thomas (Jan 11 2022 at 02:29):

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 (Jan 12 2022 at 06:35):

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

#### Patrick Thomas (Jan 12 2022 at 06:39):

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

#### Trebor Huang (Jan 12 2022 at 08:09):

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

#### Trebor Huang (Jan 12 2022 at 08:11):

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

#### Trebor Huang (Jan 12 2022 at 08:13):

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 (Jan 12 2022 at 08:14):

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.

Thank you.

#### Patrick Thomas (Jan 12 2022 at 15:38):

Oh, sorry, I meant using de bruijn indexes.

#### Trebor Huang (Jan 12 2022 at 15:48):

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)

I see.

#### Patrick Thomas (Jan 13 2022 at 01:12):

Am I better off than using locally nameless?

#### Mario Carneiro (Jan 13 2022 at 04:24):

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 (Jan 13 2022 at 04:39):

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 (Jan 13 2022 at 06:22):

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 (Jan 13 2022 at 06:24):

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 (Jan 13 2022 at 06:25):

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

#### Patrick Thomas (Jan 13 2022 at 14:36):

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

#### Patrick Thomas (Jan 14 2022 at 05:03):

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 (Jan 14 2022 at 05:17):

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 (Jan 14 2022 at 05:24):

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 (Jan 14 2022 at 06:27):

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 (Jan 14 2022 at 06:31):

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 (Jan 14 2022 at 07:13):

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 (Jan 14 2022 at 07:42):

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 (Jan 14 2022 at 07:49):

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 (Jan 14 2022 at 07:56):

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 (Jan 15 2022 at 03:26):

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 (Jan 15 2022 at 03:27):

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

#### Patrick Thomas (Jan 15 2022 at 03:27):

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 (Jan 15 2022 at 03:28):

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 (Jan 15 2022 at 03:34):

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 (Jan 15 2022 at 05:17):

• 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.

Thank you!

#### Patrick Thomas (Jan 15 2022 at 05:55):

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

#### Mario Carneiro (Jan 15 2022 at 05:58):

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 (Jan 15 2022 at 06:00):

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 (Jan 15 2022 at 06:00):

Completeness of propositional calculus is pretty easy

#### Patrick Thomas (Jan 15 2022 at 06:02):

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?

I mean not free

#### Mario Carneiro (Jan 15 2022 at 06:03):

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 (Jan 15 2022 at 06:04):

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

#### Mario Carneiro (Jan 15 2022 at 06:05):

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 (Jan 15 2022 at 06:08):

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 (Jan 15 2022 at 06:08):

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 (Jan 15 2022 at 06:09):

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

I am

sorry to confuse

No problem.

#### Mario Carneiro (Jan 15 2022 at 06:09):

the F variables don't really play a role here

#### Mario Carneiro (Jan 15 2022 at 06:10):

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 (Jan 15 2022 at 06:11):

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 (Jan 15 2022 at 06:14):

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 (Jan 15 2022 at 06:15):

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 (Jan 15 2022 at 06:15):

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 (Jan 15 2022 at 06:16):

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 (Jan 15 2022 at 06:17):

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

#### Mario Carneiro (Jan 15 2022 at 06:18):

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

#### Mario Carneiro (Jan 15 2022 at 06:20):

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

(deleted)

(deleted)

#### Patrick Thomas (Jan 15 2022 at 06:34):

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 (Jan 15 2022 at 06:40):

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

#### Trebor Huang (Jan 15 2022 at 06:41):

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

#### Patrick Thomas (Jan 15 2022 at 06:42):

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

Yes.

Hmm.

(deleted)

#### Patrick Thomas (Jan 15 2022 at 06:45):

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

Yep.

Hmm.

#### Trebor Huang (Jan 15 2022 at 06:46):

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 (Jan 15 2022 at 06:49):

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 (Jan 15 2022 at 06:50):

Yep, that's the crux of alpha equivalence.

#### Trebor Huang (Jan 15 2022 at 06:51):

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

#### Patrick Thomas (Jan 15 2022 at 06:52):

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

#### Patrick Thomas (Jan 15 2022 at 06:54):

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

#### Trebor Huang (Jan 15 2022 at 06:54):

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 (Jan 15 2022 at 06:55):

I see. A rule for alpha conversion?

#### Trebor Huang (Jan 15 2022 at 06:55):

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

#### Patrick Thomas (Jan 15 2022 at 07:01):

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 (Jan 15 2022 at 07:01):

Yes that's right.

#### Patrick Thomas (Jan 15 2022 at 07:02):

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

#### Trebor Huang (Jan 15 2022 at 07:05):

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

Cool! Thank you!

#### Trebor Huang (Jan 15 2022 at 07:06):

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 (Jan 15 2022 at 07:09):

Aside question: What does the octopus emoji mean?

#### Huỳnh Trần Khanh (Jan 15 2022 at 07:10):

It means congratulations.

#### Patrick Thomas (Jan 15 2022 at 07:11):

Huh. Ok. Thank you!

#### Yaël Dillies (Jan 15 2022 at 08:46):

"Impressive". It does a victory dance

#### Patrick Thomas (Jan 16 2022 at 00:39):

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.
-}

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 (Jan 16 2022 at 01:50):

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

#### Patrick Thomas (Jan 16 2022 at 01:52):

I see. Thank you.

#### Mario Carneiro (Jan 16 2022 at 01:55):

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 (Jan 16 2022 at 01:57):

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

#### Mario Carneiro (Jan 16 2022 at 01:59):

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

#### Mario Carneiro (Jan 16 2022 at 01:59):

pred_2 should also take a Scope

#### Mario Carneiro (Jan 16 2022 at 02:01):

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

#### Mario Carneiro (Jan 16 2022 at 02:02):

i.e. what you said for binders = 0

#### Patrick Thomas (Jan 16 2022 at 02:04):

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

#### Patrick Thomas (Jan 16 2022 at 02:05):

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

#### Mario Carneiro (Jan 16 2022 at 02:06):

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

#### Patrick Thomas (Jan 16 2022 at 02:08):

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

#### Patrick Thomas (Jan 16 2022 at 02:08):

That is the invariant?

#### Mario Carneiro (Jan 16 2022 at 02:09):

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 (Jan 16 2022 at 02:10):

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 (Jan 16 2022 at 02:11):

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

#### Mario Carneiro (Jan 16 2022 at 02:12):

similarly for every Formula and Theorem

Thank you.

#### Patrick Thomas (Jan 16 2022 at 02:15):

Does pred_3 also need to take a scope?

#### Mario Carneiro (Jan 16 2022 at 02:15):

No, that one specifically should not

#### Mario Carneiro (Jan 16 2022 at 02:16):

that's the not free condition we talked about

I see.

#### Patrick Thomas (Jan 16 2022 at 03:09):

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 (Jan 16 2022 at 07:25):

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

#### Patrick Thomas (Jan 16 2022 at 07:49):

{-
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.
-}

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 (Jan 16 2022 at 09:38):

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
| 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)

{-
(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)) &&
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) &&
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 (Jan 16 2022 at 11:43):

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 (Jan 16 2022 at 11:45):

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 (Jan 16 2022 at 11:46):

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 (Jan 16 2022 at 16:13):

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 (Jan 16 2022 at 16:39):

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 (Jan 16 2022 at 16:45):

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

#### Patrick Thomas (Jan 16 2022 at 16:57):

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 (Jan 16 2022 at 22:11):

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

#### Patrick Thomas (Jan 16 2022 at 22:47):

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 (Jan 16 2022 at 22:48):

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

#### Trebor Huang (Jan 17 2022 at 04:39):

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

#### Trebor Huang (Jan 17 2022 at 04:40):

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 (Jan 17 2022 at 04:43):

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

#### Patrick Thomas (Jan 17 2022 at 04:44):

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

#### Trebor Huang (Jan 17 2022 at 04:46):

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

#### Trebor Huang (Jan 17 2022 at 04:47):

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 (Jan 17 2022 at 04:50):

The alternative as Mario points out, is, eg

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

#### Patrick Thomas (Jan 17 2022 at 04:50):

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 (Jan 17 2022 at 04:52):

Would you happen to have a reference that includes it?

#### Trebor Huang (Jan 17 2022 at 04:52):

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 (Jan 17 2022 at 04:52):

What is the tree form?

#### Trebor Huang (Jan 17 2022 at 04:56):

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

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

#### Patrick Thomas (Jan 17 2022 at 04:57):

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

#### Patrick Thomas (Jan 17 2022 at 04:58):

So you don't have assumptions?

#### Trebor Huang (Jan 17 2022 at 04:58):

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

#### Patrick Thomas (Jan 17 2022 at 04:59):

Those aren't proofs of p and q?

#### Trebor Huang (Jan 17 2022 at 05:01):

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 (Jan 17 2022 at 05:02):

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

#### Patrick Thomas (Jan 17 2022 at 05:05):

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

#### Patrick Thomas (Jan 17 2022 at 05:07):

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

#### Patrick Thomas (Jan 17 2022 at 05:09):

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 (Jan 17 2022 at 05:09):

Just combine them.

#### Patrick Thomas (Jan 17 2022 at 05:10):

Forward instead of backwards reasoning I guess.

#### Patrick Thomas (Jan 17 2022 at 05:21):

Is this Sequent natural deduction?

#### Patrick Thomas (Jan 17 2022 at 05:39):

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

#### Patrick Thomas (Jan 17 2022 at 07:03):

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 (Jan 17 2022 at 07:04):

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

#### Patrick Thomas (Jan 17 2022 at 07:05):

Maybe. I'll take a look.

Thank you.

#### Patrick Thomas (Jan 17 2022 at 07:31):

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 (Jan 17 2022 at 08:13):

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 (Jan 17 2022 at 08:14):

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 (Jan 17 2022 at 16:52):

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

#### Patrick Thomas (Jan 17 2022 at 17:08):

How is it addressed in Lean and MetaMath?

#### Trebor Huang (Jan 17 2022 at 17:20):

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 (Jan 17 2022 at 17:35):

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

#### Patrick Thomas (Jan 17 2022 at 18:11):

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

#### Patrick Thomas (Jan 17 2022 at 19:45):

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 (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 (Jan 18 2022 at 00:15):

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 (Jan 18 2022 at 00:29):

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

#### Patrick Thomas (Jan 18 2022 at 00:30):

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

#### Patrick Thomas (Jan 18 2022 at 01:10):

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 (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 (Jan 18 2022 at 01:14):

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 (Jan 18 2022 at 01:35):

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 (Jan 18 2022 at 01:42):

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 (Jan 18 2022 at 01:47):

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 (Jan 18 2022 at 01:50):

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 (Jan 18 2022 at 02:02):

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 (Jan 18 2022 at 02:07):

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

#### Patrick Thomas (Jan 18 2022 at 02:22):

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

#### Patrick Thomas (Jan 18 2022 at 02:27):

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 (Jan 18 2022 at 03:10):

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 (Jan 18 2022 at 03:13):

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

#### Patrick Thomas (Jan 18 2022 at 03:15):

I see. Why is it a Maybe?

#### Mario Carneiro (Jan 18 2022 at 03:15):

We would define eq as PredDef "Eq" 2 Nothing

#### Mario Carneiro (Jan 18 2022 at 03:16):

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 (Jan 18 2022 at 03:16):

so even axiomatic term constructors like Eq need to have declarations

#### Patrick Thomas (Jan 18 2022 at 03:19):

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

#### Patrick Thomas (Jan 18 2022 at 03:21):

I'm guessing not?

#### Patrick Thomas (Jan 18 2022 at 03:24):

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 (Jan 18 2022 at 03:27):

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 (Jan 18 2022 at 03:28):

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

#### Patrick Thomas (Jan 18 2022 at 03:29):

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

#### Mario Carneiro (Jan 18 2022 at 03:30):

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 (Jan 18 2022 at 03:31):

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

#### Patrick Thomas (Jan 18 2022 at 03:35):

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

#### Patrick Thomas (Jan 18 2022 at 03:40):

Do Formula and Term get extended somehow?

#### Mario Carneiro (Jan 18 2022 at 03:42):

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

#### Mario Carneiro (Jan 18 2022 at 03:43):

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

#### Patrick Thomas (Jan 18 2022 at 03:46):

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

#### Patrick Thomas (Jan 18 2022 at 03:46):

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

#### Patrick Thomas (Jan 18 2022 at 03:48):

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

#### Patrick Thomas (Jan 18 2022 at 03:58):

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 (Jan 18 2022 at 04:05):

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 (Jan 18 2022 at 04:07):

With the conditions on the matching arity and admits?

#### Mario Carneiro (Jan 18 2022 at 04:08):

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

#### Mario Carneiro (Jan 18 2022 at 04:09):

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

#### Mario Carneiro (Jan 18 2022 at 04:09):

not sure what you mean by admits

#### Patrick Thomas (Jan 18 2022 at 04:10):

I think free for in your terminology.

#### Mario Carneiro (Jan 18 2022 at 04:10):

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

#### Mario Carneiro (Jan 18 2022 at 04:11):

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 (Jan 18 2022 at 04:20):

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 (Jan 18 2022 at 04:21):

Use the equality axioms?

#### Patrick Thomas (Jan 18 2022 at 04:22):

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

#### Patrick Thomas (Jan 18 2022 at 04:24):

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

#### Patrick Thomas (Jan 18 2022 at 04:26):

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

#### Patrick Thomas (Jan 18 2022 at 04:27):

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

#### Patrick Thomas (Jan 18 2022 at 04:29):

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

#### Mario Carneiro (Jan 18 2022 at 04:50):

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 (Jan 18 2022 at 04:58):

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 (Jan 18 2022 at 05:47):

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 (Jan 22 2022 at 06:20):

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 (Jan 22 2022 at 07:00):

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

#### Patrick Thomas (Jan 22 2022 at 17:29):

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

#### Mario Carneiro (Jan 22 2022 at 19:06):

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 (Jan 22 2022 at 19:14):

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 (Jan 22 2022 at 19:19):

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 (Jan 22 2022 at 19:23):

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

#### Trebor Huang (Jan 22 2022 at 19:23):

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

#### Patrick Thomas (Jan 22 2022 at 19:25):

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 (Jan 22 2022 at 19:35):

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

#### Patrick Thomas (Jan 22 2022 at 19:37):

There are currently no dependent types in Haskell, right?

#### Patrick Thomas (Jan 22 2022 at 19:40):

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 (Jan 22 2022 at 19:46):

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 (Jan 22 2022 at 19:47):

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

#### Patrick Thomas (Jan 22 2022 at 20:07):

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 (Jan 22 2022 at 20:09):

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 (Jan 22 2022 at 21:32):

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

#### Patrick Thomas (Jan 22 2022 at 22:36):

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

#### Patrick Thomas (Jan 23 2022 at 01:41):

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

#### Patrick Thomas (Jan 23 2022 at 02:24):

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

#### Mario Carneiro (Jan 23 2022 at 02:58):

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 (Jan 23 2022 at 03:05):

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 (Jan 23 2022 at 03:14):

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 (Jan 23 2022 at 03:16):

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 (Jan 23 2022 at 03:18):

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 (Jan 23 2022 at 03:19):

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

(deleted)

(deleted)

#### Trebor Huang (Jan 23 2022 at 09:18):

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.

(deleted)

#### Mario Carneiro (Jan 23 2022 at 15:19):

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 (Jan 23 2022 at 15:24):

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 (Jan 23 2022 at 15:37):

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 (Jan 23 2022 at 17:10):

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

#### Patrick Thomas (Jan 23 2022 at 19:52):

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 (Jan 23 2022 at 19:56):

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

#### Patrick Thomas (Jan 23 2022 at 20:07):

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 (Jan 23 2022 at 20:12):

Yes, that's right

#### Mario Carneiro (Jan 23 2022 at 20:12):

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

#### Mario Carneiro (Jan 23 2022 at 20:13):

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

#### Mario Carneiro (Jan 23 2022 at 20:15):

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 (Jan 23 2022 at 20:16):

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 (Jan 23 2022 at 20:18):

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 (Jan 23 2022 at 20:22):

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 (Jan 23 2022 at 20:23):

That happens automatically from the type signature

#### Mario Carneiro (Jan 23 2022 at 20:24):

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 (Jan 23 2022 at 20:24):

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

#### Mario Carneiro (Jan 23 2022 at 20:24):

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

#### Mario Carneiro (Jan 23 2022 at 20:25):

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 (Jan 23 2022 at 20:29):

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

#### Patrick Thomas (Jan 23 2022 at 20:32):

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

#### Patrick Thomas (Jan 23 2022 at 20:33):

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

#### Patrick Thomas (Jan 23 2022 at 20:35):

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

Thank you!!

#### Mario Carneiro (Jan 23 2022 at 20:46):

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 (Jan 23 2022 at 23:10):

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 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
-- how to return Var "P"?

#### Mario Carneiro (Jan 23 2022 at 23:14):

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

#### Mario Carneiro (Jan 23 2022 at 23:16):

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

Ahh. Thank you!

#### Mario Carneiro (Jan 23 2022 at 23:19):

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 (Jan 23 2022 at 23:21):

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 (Jan 23 2022 at 23:24):

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

#### Zhanrong Qiao (Jan 24 2022 at 00:35):

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 (Jan 24 2022 at 00:36):

(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 (Jan 24 2022 at 01:00):

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

(deleted)

#### Zhanrong Qiao (Jan 24 2022 at 01:24):

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 (Jan 24 2022 at 01:50):

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 (Jan 24 2022 at 01:51):

Since it has a Term s in the definition?

yes

Ok. Thank you.

#### Mario Carneiro (Jan 24 2022 at 01:57):

@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 (Jan 24 2022 at 02:03):

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 (Jan 24 2022 at 03:12):

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?

yes

#### Patrick Thomas (Jan 24 2022 at 03:21):

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

#### Mario Carneiro (Jan 24 2022 at 03:22):

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

Ok. Thank you!

#### Patrick Thomas (Jan 24 2022 at 03:40):

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?

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 (Jan 24 2022 at 03:47): Theorem (Imp (Pred "P" []) (Pred "P" [])) #### Patrick Thomas (Jan 24 2022 at 03:48): Frege_ST.hs #### Patrick Thomas (Jan 24 2022 at 03:49): Very cool! (If I did it right) :) #### Patrick Thomas (Jan 24 2022 at 03:54): Thank you!! #### Patrick Thomas (Jan 24 2022 at 04:11): 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 (Jan 24 2022 at 05:26): 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 (Jan 24 2022 at 05:27): 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 (Jan 24 2022 at 05:40): 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 (Jan 24 2022 at 05:43): 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 (Jan 24 2022 at 05:44): I'm soon going to run out of obvious flaws to poke at, so there's that #### Patrick Thomas (Jan 24 2022 at 05:44): :) #### Mario Carneiro (Jan 24 2022 at 05:45): 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 (Jan 24 2022 at 05:47): 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 (Jan 24 2022 at 05:48): 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 (Jan 24 2022 at 05:50): So it is unsound? #### Patrick Thomas (Jan 24 2022 at 05:50): All was for naught? #### Mario Carneiro (Jan 24 2022 at 05:51): It's why I'm generally dubious of the LCF style - every real world programming language is unsound for stupid reasons #### Mario Carneiro (Jan 24 2022 at 05:51): 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 (Jan 24 2022 at 05:52): I'm not sure what the alternative to LCF is? Isn't Lean and Coq LCF? #### Mario Carneiro (Jan 24 2022 at 05:54): 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 (Jan 24 2022 at 05:54): the "small trusted kernel" becomes everything behind the privacy barrier #### Mario Carneiro (Jan 24 2022 at 05:54): Lean and Coq are not LCF style in this sense #### Trebor Huang (Jan 24 2022 at 05:55): Lean and Coq explicitly stores the proof objects, so you get things like $(mp S (K S))$ #### Patrick Thomas (Jan 24 2022 at 05:56): I'm sorry, I'm not sure what that means. #### Patrick Thomas (Jan 24 2022 at 05:57): That is, stores the proof objects. #### Mario Carneiro (Jan 24 2022 at 05:57): 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 (Jan 24 2022 at 05:59): 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 (Jan 24 2022 at 06:00): 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 (Jan 24 2022 at 06:04): 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 (Jan 24 2022 at 06:06): 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 (Jan 24 2022 at 06:13): 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 (Jan 24 2022 at 06:16): 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 (Jan 24 2022 at 06:18): For example, P -> (P -> P) holds from an instantiation of prop_1 with p and p. #### Patrick Thomas (Jan 24 2022 at 06:19): And the verifier instantiates prop_1 with p and p and checks that it matches? #### Patrick Thomas (Jan 24 2022 at 06:39): Or something along the lines of what I was doing for natural deduction earlier? #### Zhanrong Qiao (Jan 24 2022 at 10:52): 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 (Jan 24 2022 at 10:55): 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 (Jan 24 2022 at 11:18): 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 (Jan 24 2022 at 12:47): @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 (Jan 24 2022 at 13:54): 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 (Jan 25 2022 at 07:04): 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 (Jan 25 2022 at 07:11): That's right. #### Patrick Thomas (Jan 25 2022 at 07:35): 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 (Jan 25 2022 at 07:36): That is, immutable with regards to checkStep. #### Patrick Thomas (Jan 25 2022 at 07:37): As in, no case in checkStep changes the definition context passed to it. #### Zhanrong Qiao (Jan 25 2022 at 13:05): 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 (Jan 25 2022 at 13:10): 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 (Jan 25 2022 at 13:12): 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 (Jan 25 2022 at 14:27): 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 (Jan 25 2022 at 14:27): Untitled.png #### Zhanrong Qiao (Jan 25 2022 at 14:38): 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 (Jan 25 2022 at 22:55): 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 (Jan 26 2022 at 01:50): (deleted) #### Patrick Thomas (Jan 26 2022 at 03:37): (deleted) #### Patrick Thomas (Jan 26 2022 at 03:45): Does this work for adding definitions? Test.hs #### Patrick Thomas (Jan 26 2022 at 03:58): 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 (Jan 26 2022 at 04:20): 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 (Jan 26 2022 at 04:26): (deleted) #### Patrick Thomas (Jan 26 2022 at 04:28): (deleted) #### Patrick Thomas (Jan 26 2022 at 04:35): 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 (Jan 26 2022 at 04:49): 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 (Jan 26 2022 at 04:53): 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 (Jan 26 2022 at 05:02): 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 (Jan 26 2022 at 05:13): (deleted) #### Patrick Thomas (Jan 27 2022 at 04:13): Does this fix the issue with the undefined references? Test.hs #### Mario Carneiro (Jan 27 2022 at 06:28): 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 (Jan 27 2022 at 14:44): 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 (Jan 27 2022 at 16:26): Actually, no, I'm not sure I have that right. At least not the part about changing the definition of Proof. #### Patrick Thomas (Jan 27 2022 at 16:42): 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 (Jan 27 2022 at 16:48): I'm not sure. Suggestions welcomed :) #### Mario Carneiro (Jan 27 2022 at 16:57): 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 (Jan 27 2022 at 16:59): basically the Formula expressions inside Justification are more like mini-programs for constructing a formula with guaranteed internal sharing #### Patrick Thomas (Jan 27 2022 at 17:03): When you say context, are you referring to the definition context? #### Patrick Thomas (Jan 27 2022 at 17:05): Also, what do you mean by guaranteed internal sharing? #### Zhanrong Qiao (Jan 27 2022 at 18:14): 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 (Jan 27 2022 at 18:24): To implement this we could store checked formulas in the context for reference #### Zhanrong Qiao (Jan 27 2022 at 18:26): 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 (Jan 27 2022 at 18:33): (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 (Jan 27 2022 at 18:48): I'm not sure if this is what he meant or not. #### Patrick Thomas (Jan 27 2022 at 22:20): I'm not sure that he is saying that the issue is related to not using de Bruijn indexes. #### Mario Carneiro (Jan 27 2022 at 22:39): No, de bruijn indices don't really affect this one way or another #### Mario Carneiro (Jan 27 2022 at 22:40): When I say context I mean the local context associating Ref -> CheckedFormula #### Patrick Thomas (Jan 27 2022 at 22:43): 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 (Jan 27 2022 at 22:43): 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 (Jan 27 2022 at 22:44): 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 (Jan 27 2022 at 22:45): if you make it too global then the ref numbers and the context gets big #### Mario Carneiro (Jan 27 2022 at 22:45): since it basically becomes a log of all expressions ever constructed #### Patrick Thomas (Jan 27 2022 at 22:46): Wait, so every formula gets added to the map from references to formulas, not just those specified by let? #### Mario Carneiro (Jan 27 2022 at 22:47): no, just the let ones, but you can have them stick around / not be scoped if you like #### Mario Carneiro (Jan 27 2022 at 22:47): for example you could require that every proof starts with a list of all let formulas and then the actual justification #### Mario Carneiro (Jan 27 2022 at 22:48): 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 (Jan 27 2022 at 22:50): What would be the drawback to doing that? #### Patrick Thomas (Jan 27 2022 at 22:51): I'm not sure what would delineate the start and end of a local context? #### Patrick Thomas (Jan 27 2022 at 22:52): How would that differ from what I added for definitions? #### Mario Carneiro (Jan 27 2022 at 22:52): 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 (Jan 27 2022 at 22:53): Does that mean you see a much bigger issue here? #### Mario Carneiro (Jan 27 2022 at 22:54): 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 (Jan 27 2022 at 22:55): 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 (Jan 27 2022 at 22:56): This is only a major issue if you have large terms, however. As Zhanrong said, long formulas are a niche issue #### Mario Carneiro (Jan 27 2022 at 22:56): It's more important to support this for proofs, since duplication there is much more common #### Mario Carneiro (Jan 27 2022 at 22:57): In DTT you can get very large terms or terms with high duplication, however #### Patrick Thomas (Jan 27 2022 at 22:58): DTT? #### Mario Carneiro (Jan 27 2022 at 22:58): dependent type theory, i.e. lean or coq style #### Mario Carneiro (Jan 27 2022 at 22:59): as opposed to FOL or HOL #### Patrick Thomas (Jan 27 2022 at 23:04): 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 (Jan 27 2022 at 23:07): Sorry, I'm not certain what a local context would look like. What would start and end it? #### Patrick Thomas (Jan 27 2022 at 23:08): Can you do the same thing with have statements and put them all at the beginning, like using earlier proofs? #### Patrick Thomas (Jan 27 2022 at 23:09): It doesn't seem like what I currently have doesn't have any support for using prior proofs? #### Mario Carneiro (Jan 27 2022 at 23:46): 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 (Jan 27 2022 at 23:56): Thank you. What makes ProofContext local? #### Patrick Thomas (Jan 27 2022 at 23:59): Does local mean initialized to be empty at the start of each checkProof? #### Patrick Thomas (Jan 28 2022 at 01:05): 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 (Jan 28 2022 at 02:47): Patrick Thomas said: Does local mean initialized to be empty at the start of each checkProof? Yes #### Mario Carneiro (Jan 28 2022 at 02:48): compared to Context which contains all the definitions, and is generally monotonic across a whole proof development #### Patrick Thomas (Jan 28 2022 at 03:29): checkProof is not the entirety of a whole proof development? #### Patrick Thomas (Jan 28 2022 at 03:31): 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 (Jan 28 2022 at 03:36): For example, something that reads like "A proof is a sequence of steps such that ..." #### Patrick Thomas (Jan 28 2022 at 04:26): If anyone has a pointer to one, that would be great. Thank you. #### Trebor Huang (Jan 28 2022 at 07:46): 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 (Jan 28 2022 at 12:18): One example that gets pretty close to covering the whole gamut of practical theory development is the OpenTheory spec #### Patrick Thomas (Jan 28 2022 at 15:37): 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 (Jan 28 2022 at 16:15): "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 (Jan 28 2022 at 18:22): Like, for example we have let binders in all major proof assistants...? #### Patrick Thomas (Jan 28 2022 at 18:25): I guess I meant more along the lines of how they are implemented. #### Zhanrong Qiao (Jan 28 2022 at 18:45): You mean, how are the representation and checking of let implemented? #### Patrick Thomas (Jan 28 2022 at 18:46): Yes, I think so. #### Zhanrong Qiao (Jan 28 2022 at 18:55): 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 (Jan 28 2022 at 18:57): 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 (Jan 28 2022 at 19:01): And when encountering Ref Int (or Ref String or Ref + whatever index type) just read the corresponding entry from the local context #### Patrick Thomas (Jan 28 2022 at 19:05): 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 (Jan 28 2022 at 19:06): That is, I don't see a way in the current system to have separate Theorem statements like in Lean. #### Patrick Thomas (Jan 28 2022 at 19:07): All of which fall under a global context. #### Zhanrong Qiao (Jan 28 2022 at 19:10): 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 (Jan 28 2022 at 19:13): 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 (Jan 28 2022 at 19:24): 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 (Jan 28 2022 at 19:25): No, I don't think I did. I'm wondering if I should have. #### Zhanrong Qiao (Jan 28 2022 at 19:31): (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 (Jan 28 2022 at 19:32): 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 (Jan 28 2022 at 19:46): I'm also wondering if a Hilbert system was the right approach. #### Zhanrong Qiao (Jan 28 2022 at 19:58): 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 (Jan 28 2022 at 20:23): Hmm. I wonder if let and have are something usually reserved for natural deduction. #### Patrick Thomas (Jan 28 2022 at 20:24): Same with local and global contexts. #### Patrick Thomas (Jan 28 2022 at 20:24): Or at least originate from it. #### Zhanrong Qiao (Jan 28 2022 at 20:29): In some sense yes? Natural deduction is indeed related to λ (through the Curry-Howard correspondence) which also binds some variable... #### Zhanrong Qiao (Jan 28 2022 at 20:30): let and have are related to the "cut rule" in sequent calculus in this way #### Patrick Thomas (Jan 28 2022 at 20:33): Interesting. I am familiar with the Curry-Howard correspondence, but not sequent calculus. #### Zhanrong Qiao (Jan 28 2022 at 20:36): 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 (Jan 28 2022 at 20:37): Hmm. What do have and let correspond to in natural deduction? #### Zhanrong Qiao (Jan 28 2022 at 20:38): The cut rule corresponds to "proving some lemma and then use it to prove the goal" in ND #### Patrick Thomas (Jan 28 2022 at 20:40): I see. Are there also local and global definitions? #### Zhanrong Qiao (Jan 28 2022 at 20:40): (deleted) #### Zhanrong Qiao (Jan 28 2022 at 20:40): 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 (Jan 28 2022 at 20:41): I see. Thank you! #### Patrick Thomas (Jan 29 2022 at 00:05): Is there a good reference for formalized natural deduction extended with definitions? #### Patrick Thomas (Jan 29 2022 at 01:02): What is the form of natural deduction that Lean corresponds to in the Curry-Howard correspondence? Is there a formalization for it? #### Patrick Thomas (Jan 29 2022 at 02:28): 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 (Jan 29 2022 at 02:40): Does the same problem occur in my implementation of exists elimination? #### Patrick Thomas (Jan 29 2022 at 06:15): 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 (Jan 29 2022 at 08:25): 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 (Jan 29 2022 at 09:37): 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 (Jan 29 2022 at 11:47): 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 (Jan 29 2022 at 16:53): 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 (Jan 29 2022 at 18:00): 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 (Jan 29 2022 at 18:02): 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 (Jan 29 2022 at 18:04): 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 (Jan 29 2022 at 18:17): 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 (Jan 29 2022 at 18:25): 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 (Jan 29 2022 at 19:18): 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 (Jan 29 2022 at 19:24): Why incidentally is it that mp requires proofs of p and q being well formed, and not p and p -> q? #### Mario Carneiro (Jan 29 2022 at 19:41): 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 (Jan 29 2022 at 19:45): 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 (Jan 29 2022 at 19:47): 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 (Jan 29 2022 at 19:53): 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 (Jan 29 2022 at 19:58): 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 (Jan 29 2022 at 20:04): 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 (Jan 29 2022 at 20:13): 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 (Jan 29 2022 at 20:15): 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 (Jan 29 2022 at 20:17): 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 (Jan 29 2022 at 20:17): each metamath database defines its set of valid sorts, it's not a closed list known to the verifier #### Mario Carneiro (Jan 29 2022 at 20:17): same thing for the syntax axioms #### Mario Carneiro (Jan 29 2022 at 20:20): As a result, the Justification grammar in metamath looks closer to this: data Justification = ApplyThm String [Justification] #### Patrick Thomas (Jan 29 2022 at 20:21): 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 (Jan 29 2022 at 20:22): yes #### Mario Carneiro (Jan 29 2022 at 20:22): those aren't metamath concepts per se #### Mario Carneiro (Jan 29 2022 at 20:23): 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 (Jan 29 2022 at 20:23): Oh, class as in class variable? #### Mario Carneiro (Jan 29 2022 at 20:23): class is actually more like second order terms, but it is used for both #### Mario Carneiro (Jan 29 2022 at 20:23): yes, it means ZFC class expression #### Mario Carneiro (Jan 29 2022 at 20:24): there is also setvar but this is only for set variables, as the name implies, not expressions #### Patrick Thomas (Jan 29 2022 at 20:28): Hmm. Thank you. I will try and see if I can extend what I have with what I think I understand. #### Patrick Thomas (Jan 29 2022 at 22:53): 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 (Jan 29 2022 at 22:54): the latter. There is one wff proof per variable appearing in the formula #### Mario Carneiro (Jan 29 2022 at 22:54): and they come in the same order as the variable declaration #### Patrick Thomas (Jan 29 2022 at 22:56): 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 (Jan 29 2022 at 22:56): no, they would be in the order a,b,c,d #### Mario Carneiro (Jan 29 2022 at 22:56): because that's the order they were defined at the top of the file #### Mario Carneiro (Jan 29 2022 at 22:57): pretty sure. It's mostly handled behind the scenes by the authoring tool, the user doesn't generally have to see it #### Patrick Thomas (Jan 29 2022 at 22:58): Hmm, that seems like it complicates my implementation, or I'm not sure how to handle it well. #### Patrick Thomas (Jan 29 2022 at 23:00): Do I lose anything by requiring wff proofs for what is passed exactly instead? #### Mario Carneiro (Jan 29 2022 at 23:03): 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 (Jan 29 2022 at 23:04): 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 (Jan 29 2022 at 23:07): 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 (Jan 29 2022 at 23:09): 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 (Jan 29 2022 at 23:10): I mean variables #### Mario Carneiro (Jan 29 2022 at 23:10): you don't have to unfold definitions, it is syntactically obvious what the variables in an expression are #### Patrick Thomas (Jan 29 2022 at 23:11): isn't a variable well formed by definition? Why do we need to check that it is well formed? #### Mario Carneiro (Jan 29 2022 at 23:11): 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 (Jan 29 2022 at 23:12): 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 (Jan 29 2022 at 23:13): 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 (Jan 29 2022 at 23:13): 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 (Jan 29 2022 at 23:13): or if the variables are numbered then you are checking that the numbers are less than the length of the list #### Patrick Thomas (Jan 29 2022 at 23:14): Because they are constrained by the constructors of Term and Formula? #### Mario Carneiro (Jan 29 2022 at 23:14): Well, your prover still isn't dealing with applying one theorem in another context (with substitution for the variables) #### Mario Carneiro (Jan 29 2022 at 23:15): the situation to avoid is that the substitution does not cover one of the variables appearing in the statement of the theorem #### Patrick Thomas (Jan 29 2022 at 23:16): You mean accidental bindings? #### Patrick Thomas (Jan 29 2022 at 23:17): The only context I have is the global context of definitions and proofs previously checked right? #### Mario Carneiro (Jan 29 2022 at 23:17): 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 (Jan 29 2022 at 23:19): 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 (Jan 29 2022 at 23:20): or you would just get a crash when you look up c in some map #### Mario Carneiro (Jan 29 2022 at 23:22): 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 (Jan 29 2022 at 23:25): So we are talking about when I have more than one proof, and proofs take hypothesis? #### Patrick Thomas (Jan 29 2022 at 23:26): I guess I'm confused, because I don't declare a list of variables at the beginning? #### Patrick Thomas (Jan 29 2022 at 23:27): I mean, in this Hilbert system there are no hypothesis right? #### Patrick Thomas (Jan 29 2022 at 23:28): So this would be an issue only if I allowed for them, say moved to natural deduction? #### Mario Carneiro (Jan 29 2022 at 23:33): 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 (Jan 29 2022 at 23:34): 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 (Jan 29 2022 at 23:39): 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 (Jan 29 2022 at 23:40): in metamath, yes #### Mario Carneiro (Jan 29 2022 at 23:40): in lean, yes as well #### Patrick Thomas (Jan 29 2022 at 23:40): Sorry, why is that again? #### Mario Carneiro (Jan 29 2022 at 23:41): 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 (Jan 29 2022 at 23:42): In HOL you can kind of get away with this by having a constructor of the form Var String Type #### Mario Carneiro (Jan 29 2022 at 23:43): 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 (Jan 29 2022 at 23:43): I didn't think FOL had types? I thought there was just one big domain of discourse? #### Mario Carneiro (Jan 29 2022 at 23:44): What about wff vs term? #### Patrick Thomas (Jan 29 2022 at 23:46): 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 (Jan 29 2022 at 23:46): right #### Mario Carneiro (Jan 29 2022 at 23:47): 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 (Jan 29 2022 at 23:47): that is, without the ability to prove propositional theorems you can't build up a toolbox of useful theorems like and.left #### Mario Carneiro (Jan 29 2022 at 23:48): 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 (Jan 29 2022 at 23:49): Would you call these something like proof schemes? #### Mario Carneiro (Jan 29 2022 at 23:49): yes #### Mario Carneiro (Jan 29 2022 at 23:49): in metamath everything is a scheme, it's a logic of schemes being deduced from other schemes #### Mario Carneiro (Jan 29 2022 at 23:50): which is why variable distinctness is a primitive notion #### Patrick Thomas (Jan 29 2022 at 23:50): 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 (Jan 29 2022 at 23:51): Like in the proof of p -> p I would declare p to be a formula variable. #### Mario Carneiro (Jan 29 2022 at 23:51): exactly #### Patrick Thomas (Jan 29 2022 at 23:53): 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 (Jan 29 2022 at 23:55): Because p has been declared to be a formula variable in the proof? #### Mario Carneiro (Jan 29 2022 at 23:55): well, they have to pass a formula for p #### Mario Carneiro (Jan 29 2022 at 23:55): so previously they had to have constructed that formula, with all the attendant checks #### Mario Carneiro (Jan 29 2022 at 23:57): 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 (Jan 29 2022 at 23:57): 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 (Jan 29 2022 at 23:59): So you would have a justification like, declared as term variable and a justification like declared as formula variable? #### Patrick Thomas (Jan 30 2022 at 00:01): 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 (Jan 30 2022 at 00:02): And the term and formula ones are meta variables? or schema variables? #### Mario Carneiro (Jan 30 2022 at 00:03): I think you can unify term variables and term metavariables in that scheme #### Patrick Thomas (Jan 30 2022 at 00:22): 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 (Jan 30 2022 at 00:24): 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 (Jan 30 2022 at 00:27): 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 (Jan 30 2022 at 00:34): Or is this not for the axiom schemes in my implementation, but for the proof schemes? #### Patrick Thomas (Jan 30 2022 at 00:35): Because in the axiom schemes for my implementation what needs to be passed in is already explicit. #### Patrick Thomas (Jan 30 2022 at 01:01): 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 (Jan 30 2022 at 01:03): Or would I even have data definitions for any kind of term, term scheme, formula or formula scheme? #### Patrick Thomas (Jan 30 2022 at 01:18): Like, how far off was I here: Hilbert_Linear_2.hs #### Mario Carneiro (Jan 30 2022 at 01:19): 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 (Jan 30 2022 at 01:20): Like in the code I just added? #### Mario Carneiro (Jan 30 2022 at 01:22): 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 (Jan 30 2022 at 01:26): Sorry, why is that? And why only for FormulaStep? #### Patrick Thomas (Jan 30 2022 at 01:27): Or do you mean have only one kind of step? #### Patrick Thomas (Jan 30 2022 at 01:28): Instead of ProofStep, FormulaStep and TermStep just have Step? #### Mario Carneiro (Jan 30 2022 at 01:28): yes, that #### Mario Carneiro (Jan 30 2022 at 01:29): 1 sec, example coming up #### Mario Carneiro (Jan 30 2022 at 01:38): 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 (Jan 30 2022 at 01:51): Very cool! Thank you! Would I also need steps for adding term scheme variables, and formula scheme variables? #### Mario Carneiro (Jan 30 2022 at 01:51): 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 (Jan 30 2022 at 01:52): You already have term and formula variables via the Pred and Var constructors #### Mario Carneiro (Jan 30 2022 at 01:52): you just need a mechanism to substitute into them #### Patrick Thomas (Jan 30 2022 at 01:54): I see. That mechanism being two more Step constructors? #### Mario Carneiro (Jan 30 2022 at 02:14): 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 (Jan 30 2022 at 02:17): 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 (Jan 30 2022 at 02:29): Sorry, what do the constructor arguments to ApplyThm represent? The name of a theorem, and ? #### Mario Carneiro (Jan 30 2022 at 02:39): The name of the theorem, the substitutions for term variables, the substitutions for predicate variables, and the list of hypotheses #### Mario Carneiro (Jan 30 2022 at 02:42): 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 (Jan 30 2022 at 02:50): 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 (Jan 30 2022 at 03:00): 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 (Jan 30 2022 at 03:03): I'm wondering if there is a missing call to substTerm or if it is implicit somewhere? #### Mario Carneiro (Jan 30 2022 at 03:08): 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 (Jan 30 2022 at 03:09): and then we would turn an occurrence like P(1, 2, 3) into 1 + 2 = 3 #### Mario Carneiro (Jan 30 2022 at 03:10): substTerm doesn't appear in the constructors I've shown, but it would appear in the Pred case, for example #### Mario Carneiro (Jan 30 2022 at 03:11): er... I guess I did that one #### Mario Carneiro (Jan 30 2022 at 03:12): yeah this probably doesn't typecheck, we should be using let args' = substTerm ts <$> args instead of let args' = go <> args #### Patrick Thomas (Jan 30 2022 at 03:20): 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 (Jan 30 2022 at 04:59): 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 (Jan 30 2022 at 05:02): Or no, maybe just replace each free variable with any term? #### Mario Carneiro (Jan 30 2022 at 05:51): 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 (Jan 30 2022 at 05:52): 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 (Jan 30 2022 at 05:53): You could replace x = y with x < y? #### Patrick Thomas (Jan 30 2022 at 05:54): Oh, or where you talking about the first sentence. #### Mario Carneiro (Jan 30 2022 at 05:58): For example, replacing forall x, P(x, y) with P(z, w) := x < z is bad because x will get captured #### Patrick Thomas (Jan 30 2022 at 05:59): 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 (Jan 30 2022 at 05:59): that example is a predicate of arity 2 #### Mario Carneiro (Jan 30 2022 at 06:01): 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 (Jan 30 2022 at 06:02): so that example would result in forall x', x < x' #### Patrick Thomas (Jan 30 2022 at 06:09): 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 (Jan 30 2022 at 06:10): 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 (Jan 30 2022 at 06:11): 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 (Jan 30 2022 at 06:14): 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 (Jan 30 2022 at 06:15): I am #### Mario Carneiro (Jan 30 2022 at 06:15): In the second version we lift the restriction on P, so you can put anything in for it #### Mario Carneiro (Jan 30 2022 at 06:15): instead of restricting the substitution, we sometimes rename the binder to avoid clashes #### Mario Carneiro (Jan 30 2022 at 06:16): in the first version we just reject if we would otherwise have to rename a binder #### Patrick Thomas (Jan 30 2022 at 06:16): 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 (Jan 30 2022 at 06:16): for example P := 0 < x #### Mario Carneiro (Jan 30 2022 at 06:17): The arity of P is determined by its use in the original theorem, here P -> forall x. P #### Mario Carneiro (Jan 30 2022 at 06:17): we're allowed to use an expression with free variables #### Mario Carneiro (Jan 30 2022 at 06:17): we might want to derive 0 < x -> forall x'. 0 < x here #### Mario Carneiro (Jan 30 2022 at 06:18): 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 (Jan 30 2022 at 06:20): 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 (Jan 30 2022 at 06:25): Wait, so what does P(x) mean? Is it the same as Pred "P" [Var "x"]? #### Patrick Thomas (Jan 30 2022 at 06:28): It seems not? The "x" in P(x) is some kind of binder? #### Mario Carneiro (Jan 30 2022 at 06:29): 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 (Jan 30 2022 at 06:31): well, technically "P" -> (["x"], i) where getFormula ctx i = e #### Patrick Thomas (Jan 30 2022 at 06:35): "P" -> (["x"], e) means we are replacing the variable x by e in P? #### Patrick Thomas (Jan 30 2022 at 06:36): Sorry, maybe it is easier to talk about outside of the code, which I am still trying to understand. #### Mario Carneiro (Jan 30 2022 at 06:36): It means we are replacing P(x) by e, and more generally P(t) by e[t/x] #### Mario Carneiro (Jan 30 2022 at 06:39): 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 (Jan 30 2022 at 06:40): 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 (Jan 30 2022 at 06:42): Thank you. #### Patrick Thomas (Jan 30 2022 at 06:43): Probably not tonight though. Have a good evening, or day depending on your time zone. #### Patrick Thomas (Jan 31 2022 at 04:36): Does this look correct for the propositional calculus case? Do the comments reflect a correct understanding? Thank you. Hilbert_Prop.hs #### Patrick Thomas (Jan 31 2022 at 04:38): 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 (Jan 31 2022 at 04:54): 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 (Jan 31 2022 at 04:57): So you don't have to replace every free variable in the formula scheme? I was wondering about that. #### Patrick Thomas (Jan 31 2022 at 04:58): Or I guess I read that backwards. You do have to? #### Patrick Thomas (Jan 31 2022 at 04:59): Did you mean (Data.Map.keysSet m) subset (allVar p)? #### Patrick Thomas (Jan 31 2022 at 05:08): 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 (Jan 31 2022 at 05:16): Thank you! #### Patrick Thomas (Jan 31 2022 at 05:51): Like this? Hilbert_Prop.hs #### Patrick Thomas (Feb 01 2022 at 02:09): 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 (Feb 01 2022 at 02:16): I don't think I ever suggested that? #### Mario Carneiro (Feb 01 2022 at 02:18): 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 (Feb 01 2022 at 02:20): 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 (Feb 01 2022 at 02:22): that example doesn't have the checkSteps function. The one earlier does and it uses last ps #### Patrick Thomas (Feb 01 2022 at 02:24): I see. I must have mixed together the code. Thank you. #### Patrick Thomas (Feb 01 2022 at 02:36): 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 (Feb 01 2022 at 08:41): yes #### Patrick Thomas (Feb 02 2022 at 02:53): Thank you. #### Patrick Thomas (Feb 02 2022 at 02:55): 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 (Feb 02 2022 at 03:02): Yes, they use named variables. You can use theorems to prove alpha conversion, there is no built in support for it #### Patrick Thomas (Feb 02 2022 at 03:05): I did not realize that was possible. What do you need to prove it, just FOL? #### Mario Carneiro (Feb 02 2022 at 03:16): It uses lemmas like http://us.metamath.org/mpeuni/cbvalv.html #### Mario Carneiro (Feb 02 2022 at 03:16): which follow from the FOL axiomatization #### Patrick Thomas (Feb 02 2022 at 03:23): Interesting. Is that due specifically to the axiomatization used by metamath that avoids substitution, or is that true generally? #### Patrick Thomas (Feb 02 2022 at 03:24): I guess I just expected that would have to be proved at the meta level. #### Mario Carneiro (Feb 02 2022 at 03:26): 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 (Feb 02 2022 at 03:26): The interesting observation is that it suffices to use theorems like that in lieu of built in alpha renaming #### Patrick Thomas (Feb 02 2022 at 03:27): That is cool. #### Mario Carneiro (Feb 02 2022 at 03:27): 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 (Feb 02 2022 at 03:28): you can use NF(x, ph) as a substitute for actual not-free constraints in lemmas that require it #### Mario Carneiro (Feb 02 2022 at 03:29): 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 (Feb 02 2022 at 03:32): 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 (Feb 02 2022 at 03:35): Cool. #### Patrick Thomas (Feb 02 2022 at 03:39): 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 (Feb 02 2022 at 03:41): Or are they in fact considered as meta theorems, and this allows you to move them down. #### Mario Carneiro (Feb 02 2022 at 03:43): No, there are predicate calculus theorems that have the object logic NF as a condition #### Mario Carneiro (Feb 02 2022 at 03:44): that is, the NF(x, ph) function I just mentioned #### Mario Carneiro (Feb 02 2022 at 03:44): for example NF(x, ph) -> ph -> ∀ x, ph is pretty easy to prove #### Mario Carneiro (Feb 02 2022 at 03:45): or NF(x, ph), ph -> ps |- ph -> ∀ x, ps #### Patrick Thomas (Feb 02 2022 at 03:48): But there are also predicate calculus theorems that have the meta logic NF as a condition? #### Mario Carneiro (Feb 02 2022 at 03:54): 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 (Feb 02 2022 at 03:55): I guess I meant in textbooks. #### Patrick Thomas (Feb 02 2022 at 03:56): 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 (Feb 02 2022 at 03:56): That there are lemmas in textbooks that use the meta logic (actual) version of it. #### Mario Carneiro (Feb 02 2022 at 03:58): Right. You take the textbook lemma, using the metalevel not-free constraint, and replace all instances of it with NF(x, ph) #### Mario Carneiro (Feb 02 2022 at 03:58): and that gives you a theorem that can be stated and proved in metamath #### Patrick Thomas (Feb 02 2022 at 03:59): Do the textbooks identify these as meta lemmas when they state them? #### Mario Carneiro (Feb 02 2022 at 04:00): In the textbooks these are all theorem schemes, since they usually have wff metavariables in them #### Patrick Thomas (Feb 02 2022 at 04:02): What is proved in metamath are theorem schemes too aren't they? #### Mario Carneiro (Feb 02 2022 at 04:04): Yes, but the scheme language is more restricted, to just substitution and distinctness #### Mario Carneiro (Feb 02 2022 at 04:05): anything beyond that has to be implemented inside the target language itself #### Patrick Thomas (Feb 02 2022 at 04:07): So meta, but not as meta? :) #### Mario Carneiro (Feb 02 2022 at 04:08): 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 (Feb 02 2022 at 04:10): For a more interesting example of an operation defined by recursion on formulas consider the double negation translation #### Patrick Thomas (Feb 02 2022 at 04:19): 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 (Feb 02 2022 at 04:21): yes #### Patrick Thomas (Feb 02 2022 at 04:22): 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 (Feb 02 2022 at 04:24): That's different than saying that the axiom schemes from one can be derived from the other and vice versa right? #### Patrick Thomas (Feb 02 2022 at 04:26): Because they are different at the meta level, so that wouldn't make sense. #### Mario Carneiro (Feb 02 2022 at 04:28): 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 (Feb 02 2022 at 04:30): 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 (Feb 02 2022 at 04:31): 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 (Feb 02 2022 at 04:32): the deduction theorem is one of these #### Patrick Thomas (Feb 02 2022 at 04:39): This gets confusing. #### Patrick Thomas (Feb 02 2022 at 04:47): So FOL schemes and metamath meta theorems are at the same level? How do you keep this all straight :) #### Patrick Thomas (Feb 02 2022 at 04:49): Is everything eventually embedded into a single higher level metalogic? #### Patrick Thomas (Feb 02 2022 at 04:51): That is, there is a single metalogic that can describe both FOL schemes and metamath metatheorems? #### Trebor Huang (Feb 02 2022 at 05:02): I think you shouldn't 'align' the levels of metamath and textbook FOL, that just gets confusing. #### Patrick Thomas (Feb 02 2022 at 05:05): 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 (Feb 02 2022 at 05:06): Or at least doesn't there have to be a single meta logic that can describe them both? #### Mario Carneiro (Feb 02 2022 at 05:09): 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 (Feb 02 2022 at 05:12): 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 (Feb 02 2022 at 05:17): I guess that makes sense. They would still want to show that they are doing the same FOL though right? #### Patrick Thomas (Feb 02 2022 at 05:17): Hence the proofs that they are equivalent at the object level. #### Mario Carneiro (Feb 02 2022 at 05:18): 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 (Feb 02 2022 at 05:21): 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 (Feb 02 2022 at 05:23): I guess if you can show that they are complete and the definition of complete makes sense. #### Patrick Thomas (Feb 02 2022 at 05:34): 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 (Feb 02 2022 at 05:34): sure that's true #### Mario Carneiro (Feb 02 2022 at 05:35): you can't really avoid that #### Mario Carneiro (Feb 02 2022 at 05:36): Any system of axioms comes with baseline assumptions. Without axioms you can't prove anything #### Mario Carneiro (Feb 02 2022 at 05:37): the best you can do is make sure the axioms are "obviously correct" #### Mario Carneiro (Feb 02 2022 at 05:38): or you can try not to engage with the question and use an off-the-shelf axiom system #### Patrick Thomas (Feb 02 2022 at 05:38): I see. Do the meta logics become increasingly simpler and more "obviously correct" the "higher" you go? #### Mario Carneiro (Feb 02 2022 at 05:39): they need not, it's up to you #### Patrick Thomas (Feb 02 2022 at 05:39): From what I have seen of the first level it appears to be about the same as the logic it is describing. #### Mario Carneiro (Feb 02 2022 at 05:40): but it is usually possible to have a PA-ish metalogic supporting an arbitrarily complicated object logic #### Patrick Thomas (Feb 02 2022 at 05:40): What does "PA-ish" mean? #### Mario Carneiro (Feb 02 2022 at 05:40): either peano arithmetic or a variation/subsystem of it #### Mario Carneiro (Feb 02 2022 at 05:41): like EFA (exponential function arithmetic) or PRA (primitive recursive arithmetic) #### Mario Carneiro (Feb 02 2022 at 05:42): if you try to make the system too weak it won't be able to support Godel's theorems #### Patrick Thomas (Feb 02 2022 at 05:45): The incompleteness theorems? #### Mario Carneiro (Feb 02 2022 at 05:45): yes #### Mario Carneiro (Feb 02 2022 at 05:47): 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 (Feb 02 2022 at 05:51): The argument that it is "obviously correct"? #### Mario Carneiro (Feb 02 2022 at 05:52): it's pretty hard to argue that PA is not obviously correct #### Mario Carneiro (Feb 02 2022 at 05:53): you have to have a strange idea of what numbers are to be able to contemplate the inconsistency of PA #### Patrick Thomas (Feb 02 2022 at 05:54): I'm not sure what you meant about run the argument with Robinson's Q. Which argument? #### Patrick Thomas (Feb 02 2022 at 05:55): And why do you want to be able to support Godel's theorems? #### Mario Carneiro (Feb 02 2022 at 06:00): the argument for Godel's incompleteness theorem, which involves constructing a provability assertion inside the weak metalogic #### Mario Carneiro (Feb 02 2022 at 06:01): 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 (Feb 02 2022 at 06:02): 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 (Feb 02 2022 at 06:03): and since ultimately we want to do mathematics in interesting and undecidable domains, this forms a bare minimum requirement on the metalogic #### Mario Carneiro (Feb 02 2022 at 06:06): 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 (Feb 02 2022 at 06:10): That makes sense. #### Patrick Thomas (Feb 02 2022 at 06:10): Although proving their own consistency sounds like a circular argument? #### Mario Carneiro (Feb 02 2022 at 06:11): It's not circular, since consistency of T is not a precondition of the proof #### Mario Carneiro (Feb 02 2022 at 06:12): in fact if T was inconsistent then T |- Con(T) would hold trivially #### Mario Carneiro (Feb 02 2022 at 06:12): 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 (Feb 02 2022 at 06:14): What does "in fact consistent" mean? #### Mario Carneiro (Feb 02 2022 at 06:15): in the case of Willard's axiom systems this is usually ensured by having the theory be a subsystem of PA #### Patrick Thomas (Feb 02 2022 at 06:16): Why does that mean "in fact"? #### Mario Carneiro (Feb 02 2022 at 06:16): What I mean is, it's consistent from an "external viewpoint", not merely in T's opinion #### Mario Carneiro (Feb 02 2022 at 06:17): since, as mentioned, if T was inconsistent it would prove its own consistency #### Mario Carneiro (Feb 02 2022 at 06:17): this is the "uninteresting case" of self-verification #### Mario Carneiro (Feb 02 2022 at 06:20): 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 (Feb 02 2022 at 06:24): You mean just from type theory? #### Patrick Thomas (Feb 02 2022 at 06:28): 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 (Feb 02 2022 at 06:29): And since we know we can always prove the consistency of T from T... #### Trebor Huang (Feb 02 2022 at 06:29): Lean proves Con(PA), but PA never proves Con(PA) #### Trebor Huang (Feb 02 2022 at 06:29): That's Goedel's incompleteness theorem. #### Trebor Huang (Feb 02 2022 at 06:30): Of course, unless PA is inconsistent, in which case PA proves anything by ex falso. #### Patrick Thomas (Feb 02 2022 at 06:36): It seems kind of oddly concrete that the level is arithmetic that the incompleteness theorem takes affect. #### Mario Carneiro (Feb 02 2022 at 06:37): That's the level where undecidability starts to pop up, for example in diophantine equations #### Patrick Thomas (Feb 02 2022 at 06:38): I guess I would have expected it to be more abstract, like some subset of the set theory axioms. #### Mario Carneiro (Feb 02 2022 at 06:38): 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 (Feb 02 2022 at 06:38): I see. #### Mario Carneiro (Feb 02 2022 at 06:38): The set theory axioms generally blow past this level pretty quickly #### Mario Carneiro (Feb 02 2022 at 06:39): once you have something that acts like a successor function like {x} you can usually already do all this stuff #### Trebor Huang (Feb 02 2022 at 06:39): One thing though: I don't immediately see how Lean proves Con(PA) without excluded middle, is there any reference? #### Mario Carneiro (Feb 02 2022 at 06:40): I was actually writing that up right now #### Mario Carneiro (Feb 02 2022 at 06:40): it's not too hard to see that it should be possible: nat has decidable equality #### Mario Carneiro (Feb 02 2022 at 06:41): plus Con(PA) is a negative statement so intuitionism doesn't get in the way much #### Trebor Huang (Feb 02 2022 at 06:41): Yeah I guess so, but it would be cool to see the complete proof done ;) #### Patrick Thomas (Feb 02 2022 at 06:44): 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 (Feb 02 2022 at 06:46): Not sure if I would understand it, but might be interesting to try to. #### Trebor Huang (Feb 02 2022 at 06:46): I think there's Meredith's work, which is mildly relevant(?) #### Mario Carneiro (Feb 02 2022 at 06:46): Something like http://us.metamath.org/mpeuni/natded.html? #### Patrick Thomas (Feb 02 2022 at 07:00): 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 (Feb 02 2022 at 07:09): 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 (Feb 02 2022 at 07:16): 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 (Feb 02 2022 at 07:17): But that's currently incomplete as I see it. You don't even have modus ponens, right? #### Mario Carneiro (Feb 02 2022 at 07:19): it's a bit annoying that the wikipedia article barely acknowledges this #### Patrick Thomas (Feb 02 2022 at 07:32): Thank you for the help! I'm going to sleep now :) #### Mario Carneiro (Feb 02 2022 at 08:23): 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 (Feb 03 2022 at 06:05): 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 (Feb 03 2022 at 06:09): No. The variables in the formula will be variables in the current context #### Patrick Thomas (Feb 03 2022 at 06:10): Ok. Thank you. #### Mario Carneiro (Feb 03 2022 at 06:14): 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 (Feb 03 2022 at 06:15): If you only have 0-ary formula and term variables then you only need one level of substitution #### Patrick Thomas (Feb 03 2022 at 06:21): 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 (Feb 03 2022 at 06:22): The question is whether you can substitute for those predicate variables of nonzero arity #### Mario Carneiro (Feb 03 2022 at 06:22): I assume you can, in which case you have the second order substitution process I mentioned #### Mario Carneiro (Feb 03 2022 at 06:23): This is second order logic "lite" #### Mario Carneiro (Feb 03 2022 at 06:23): since you don't have arbitrary quantification over those predicate variables #### Patrick Thomas (Feb 03 2022 at 06:25): 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 (Feb 03 2022 at 06:25): I'm trying to stick to just FOL for now. #### Mario Carneiro (Feb 03 2022 at 06:26): 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 (Feb 03 2022 at 06:27): Without such a mechanism it's not very useful to prove FOL schemes #### Mario Carneiro (Feb 03 2022 at 06:28): Basically the predicate variables aren't variables at all, they are constants #### Patrick Thomas (Feb 03 2022 at 06:31): Maybe it will be easier if I post what I have of the code so far. #### Patrick Thomas (Feb 03 2022 at 06:32): Let me clean it up a bit. #### Mario Carneiro (Feb 03 2022 at 06:33): What I'm saying is that if you can't substitute for predicate variables then they aren't variables #### Mario Carneiro (Feb 03 2022 at 06:33): that's what it means to be a variable #### Mario Carneiro (Feb 03 2022 at 06:34): Predicate constants are useful too, for example \in and < are predicate constants #### Mario Carneiro (Feb 03 2022 at 06:34): you wouldn't expect to be able to substitute them with expressions #### Patrick Thomas (Feb 03 2022 at 06:45): 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 (Feb 03 2022 at 06:47): 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 (Feb 03 2022 at 06:47): Yep. #### Mario Carneiro (Feb 03 2022 at 06:48): also protip you don't need to pass things that are fixed in the recursion to go #### Mario Carneiro (Feb 03 2022 at 06:48): like f_map and t_map #### Patrick Thomas (Feb 03 2022 at 06:49): Yeah, I started out thinking I might need to recursively descend for the propositional case and would need them. #### Patrick Thomas (Feb 03 2022 at 06:50): Or something like that. #### Mario Carneiro (Feb 03 2022 at 06:50): 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 (Feb 03 2022 at 06:51): What will be the drawbacks of not being able to do that? #### Patrick Thomas (Feb 03 2022 at 06:52): Are there things I can't prove, or will it just be lot harder to prove them? #### Mario Carneiro (Feb 03 2022 at 06:52): 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 (Feb 03 2022 at 06:53): 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 (Feb 03 2022 at 06:53): Yeah, that sounds like an issue. #### Patrick Thomas (Feb 03 2022 at 06:54): But I have to implement another level for every arity I want to support? #### Mario Carneiro (Feb 03 2022 at 06:55): 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 (Feb 03 2022 at 06:55): That handles arbitrary arity #### Mario Carneiro (Feb 03 2022 at 06:55): it doesn't handle third order variables but you don't have those anyway #### Patrick Thomas (Feb 03 2022 at 06:56): Wait, what is the difference between arity and order? #### Mario Carneiro (Feb 03 2022 at 06:57): • 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 (Feb 03 2022 at 06:58): An nth order variable takes (any number of) arguments of order n-1 #### Patrick Thomas (Feb 03 2022 at 07:01): Which order would a propositional variable be? P : Prop? #### Mario Carneiro (Feb 03 2022 at 07:02): 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 (Feb 03 2022 at 07:04): 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 (Feb 03 2022 at 07:05): but of course you can't code a nat -> Prop as a nat, that's cantor's theorem #### Patrick Thomas (Feb 03 2022 at 07:08): 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 (Feb 03 2022 at 07:11): 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 (Feb 03 2022 at 07:14): From the code it seems maybe you can substitute one predicate for another if there aritys match? #### Mario Carneiro (Feb 03 2022 at 07:15): that's certainly a necessary condition #### Mario Carneiro (Feb 03 2022 at 07:16): 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 (Feb 03 2022 at 07:16): obviously the number of lambda binders has to match the number of arguments to P #### Patrick Thomas (Feb 03 2022 at 07:17): I'm guessing there are also conditions to prevent free variable capture? #### Mario Carneiro (Feb 03 2022 at 07:26): 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 (Feb 03 2022 at 07:30): 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 (Feb 03 2022 at 07:33): 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 (Feb 03 2022 at 07:34): I'm not sure if I have ever seen that kind of substitution before. #### Mario Carneiro (Feb 03 2022 at 07:35): 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 (Feb 03 2022 at 07:35): we might beta reduce it later, resulting in more constraints / alpha renaming #### Mario Carneiro (Feb 03 2022 at 07:36): here we're trying to stick to first order so we always eliminate lambdas before they appear #### Patrick Thomas (Feb 03 2022 at 07:36): Free variables and parameters are not the same? What are parameters in my implementation, if I have any? #### Mario Carneiro (Feb 03 2022 at 07:36): hopefully my terminology is clear from the example #### Mario Carneiro (Feb 03 2022 at 07:37): a is a free variable, u is a parameter #### Mario Carneiro (Feb 03 2022 at 07:37): which is to say, it is a "bound variable" bound by the lambda #### Mario Carneiro (Feb 03 2022 at 07:37): even though we don't have any explicit lambda here #### Mario Carneiro (Feb 03 2022 at 07:39): in my code earlier, the parameters are the [String] in the M.Map String ([String], Int) of the formula substitution map #### Patrick Thomas (Feb 03 2022 at 07:39): Is there a dependent type here? There are both lambdas and a forall? #### Mario Carneiro (Feb 03 2022 at 07:40): 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 (Feb 03 2022 at 07:41): 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 (Feb 03 2022 at 07:42): lambda only appears at the top level here, the syntax is a list of variable names followed by a formula #### Mario Carneiro (Feb 03 2022 at 07:42): like ([u, v], ∀ b, u < a ∧ v < b) #### Patrick Thomas (Feb 03 2022 at 07:44): I mean, is there a parameter in the definition I have of Formula? Is it the variable name after the Forall? #### Mario Carneiro (Feb 03 2022 at 07:45): no, I'm using the term parameter just for the lambda-bound arguments #### Mario Carneiro (Feb 03 2022 at 07:45): the variables in a forall are just bound variables #### Mario Carneiro (Feb 03 2022 at 07:45): so b is a bound variable in the running example #### Patrick Thomas (Feb 03 2022 at 07:47): I guess I'm not sure what lambda bound means here. Do I have to extend the Formula def? #### Mario Carneiro (Feb 03 2022 at 07:47): no #### Mario Carneiro (Feb 03 2022 at 07:48): 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 (Feb 03 2022 at 07:49): 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 (Feb 03 2022 at 07:50): So you just decide which variables are going to be parameters when you decide to do a substitution? #### Mario Carneiro (Feb 03 2022 at 07:50): 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 (Feb 03 2022 at 07:51): you get to make a new formula substitution map any time you apply a lemma #### Mario Carneiro (Feb 03 2022 at 07:52): so the parameters can be different if you want #### Mario Carneiro (Feb 03 2022 at 07:52): the formula will usually be different too #### Patrick Thomas (Feb 03 2022 at 07:53): But it has to be a well formed formula right? #### Patrick Thomas (Feb 03 2022 at 07:53): Can we go step by step for what gets replaced by what? #### Patrick Thomas (Feb 03 2022 at 07:55): Suppose I have the predicate Pred "P" [Var (x), (Func "f" [Var "y"])] I guess. #### Patrick Thomas (Feb 03 2022 at 07:56): Although maybe that is not a proof scheme, so it doesn't work. #### Patrick Thomas (Feb 03 2022 at 07:58): 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 (Feb 03 2022 at 08:00): I'm sorry, maybe I need a more detailed paper or textbook or something. #### Patrick Thomas (Feb 03 2022 at 08:00): This kind of substitution is new to me, I think. #### Patrick Thomas (Feb 03 2022 at 08:11): 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 (Feb 03 2022 at 08:20): I changed x to f(x) in the example to emphasize that P is being applied to terms not variables #### Mario Carneiro (Feb 03 2022 at 08:21): u is a variable, but P(f(x), y) can have arbitrary terms there #### Mario Carneiro (Feb 03 2022 at 08:22): 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 (Feb 03 2022 at 08:22): < is a predicate constant #### Mario Carneiro (Feb 03 2022 at 08:23): definitions produce new predicate constants, and axiomatic constants like = are also constants #### Mario Carneiro (Feb 03 2022 at 08:24): The code that you wrote before for the Pred name ts case is appropriate for predicate constants #### Patrick Thomas (Feb 03 2022 at 08:27): Hmm. Ok. How would my data types change? What is an appropriate constructor for a predicate variable? #### Mario Carneiro (Feb 03 2022 at 08:28): same as constants #### Mario Carneiro (Feb 03 2022 at 08:28): the only difference is that variables are substituted and constants aren't #### Patrick Thomas (Feb 03 2022 at 08:29): So they can take arbitrary terms, not just Var? #### Mario Carneiro (Feb 03 2022 at 08:29): yes #### Mario Carneiro (Feb 03 2022 at 08:29): Mario Carneiro said: u is a variable, but P(f(x), y) can have arbitrary terms there #### Patrick Thomas (Feb 03 2022 at 08:32): How do you distinguish them in the code? I mean, I have no real data type for axiomatic constants right? #### Patrick Thomas (Feb 03 2022 at 08:35): Can we go more slowly through an example substitution using the notation from the code? #### Patrick Thomas (Feb 03 2022 at 08:38): Actually, I should probably go to sleep. Thank you for your patience. #### Mario Carneiro (Feb 03 2022 at 08:38): I don't really want to drag this out on a public channel #### Patrick Thomas (Feb 03 2022 at 08:39): Ok. #### Patrick Thomas (Feb 03 2022 at 08:39): Sorry. #### Patrick Thomas (Feb 03 2022 at 08:40): Thank you for your time. #### Mario Carneiro (Feb 03 2022 at 08:40): 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 (Feb 03 2022 at 08:41): I'm not against discussing this stuff for far longer than appropriate but I should probably moderate at some point #### Patrick Thomas (Feb 03 2022 at 08:42): :) Ok. I'll see what I can find for texts, papers first. #### Trebor Huang (Feb 03 2022 at 08:56): 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 (Feb 03 2022 at 08:57): 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 (Feb 03 2022 at 09:01): You definitely can't replace definitions, you might have used the definition in the proof #### Mario Carneiro (Feb 03 2022 at 09:02): You can't replace axiomatic constants either since they might be used in axioms (e.g. replace = with < in x = x) #### Mario Carneiro (Feb 03 2022 at 09:03): 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 (Jun 07 2022 at 01:43): 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? #### Patrick Thomas (Jun 09 2022 at 01:53): Should this theorem hold? #### Mario Carneiro (Jun 09 2022 at 03:41): 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 (Jun 09 2022 at 03:44): I see. So just is_valid P -> is_valid (sub_prop s P) holds? #### Patrick Thomas (Jun 09 2022 at 03:45): Ok. #### Patrick Thomas (Jun 09 2022 at 03:49): Thank you. #### Patrick Thomas (Jun 09 2022 at 03:53): Should s be of type string -> string or string -> formula? I'm guessing the latter, based on the propositional calculus case. #### Patrick Thomas (Jun 09 2022 at 05:06): Hmm, I need to check for variable capture then. #### Patrick Thomas (Jun 10 2022 at 05:07): 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 (Jun 15 2022 at 18:40): 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

Thank you!

#### Patrick Thomas (Jun 18 2022 at 16:43):

Is there an implementation in Lean or Haskell of the algorithm that Lean uses for the locally nameless representation?

#### Patrick Thomas (Jun 18 2022 at 16:46):

I would like to try to see how that translates to a representation for FOL.

#### Patrick Thomas (Jun 20 2022 at 21:54):

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 (Jun 20 2022 at 22:00):

I don't look forward to trying to prove things about them as they are :)

#### Patrick Thomas (Jul 09 2022 at 19:57):

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 (Jul 09 2022 at 19:57):

I have been having a hard time finding references to it, and I'm not sure why.

#### Patrick Thomas (Jul 09 2022 at 19:59):

My code base is here.

Last updated: Dec 20 2023 at 11:08 UTC