5
$\begingroup$

I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is to prove in Lean that this substitution preserves validity and to use it as part of a proof checker for first order logic. I have these definitions in Lean:

import data.finset

/-
Term schemes.
var "x" : An object variable named "x". Ranges over the domain of each interpretation.
func 0 "c" [] : A constant named "c".
func n "f" [x1 ... xn] : A function named "f" of n terms (arguments).
-/
inductive term : Type
| var : string → term
| func (n : ℕ) : string → (fin n → term) → term

open term

/-
Formula schemes.
atom 0 "P" [] : A propositional variable named "P".
atom n "P" [x1 ... xn] : A predicate variable named "P" of n terms (arguments).
-/
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

open formula

/-
domain: A nonempty set D called the domain of the interpretation. The intention is that all terms have values in D.

nonempty: A proof that there is at least one element in the domain.

func: (n : ℕ, f : string) → (f_{M} : (terms : fin n → domain) → v : domain)
A mapping of each n-ary function symbol f to a function f_{M}.
n : The arity of the function symbol.
f : The function symbol.
f_{M} : The function that the function symbol is mapped to.
terms : fin n → domain : The n terms (arguments) of the function expressed as a finite function.
v : domain : The result of the function. An element in the domain.

pred: (n : ℕ, P : string) → (P_{M} : (terms : fin n → domain) → v : Prop)
A mapping of each n-ary predicate symbol P to a predicate P_{M}.
n : The arity of the predicate symbol.
P : The predicate symbol.
P_{M} : The predicate that the predicate symbol is mapped to.
terms : fin n → domain : The n terms (arguments) of the predicate expressed as a finite function.
v : Prop : The result of the predicate. True or false.
-/
structure interpretation (domain : Type) : Type :=
(nonempty : nonempty domain)
(func (n : ℕ) : string → (fin n → domain) → domain)
(pred (n : ℕ) : string → (fin n → domain) → Prop)


/-
The type of mappings of object variable names to elements of a domain.
-/
def valuation (D : Type) := string → D

/-
The function mapping each term to an element of a domain by a given interpretation and valuation.
-/
def eval_term (D : Type) (m : interpretation D) (v : valuation D) : term → D
| (var x) := v x
| (func n f terms) := m.func n f (fun i : fin n, eval_term (terms i))

notation a' ` ↦ `:25 v := fun f, function.update f a' v

def holds (D : Type) (m : interpretation D) : valuation D → formula → Prop
| _ bottom := false
| _ top := true
| v (atom n x terms) := m.pred n x (fun i : fin n, eval_term D m v (terms i))
| v (not p) := ¬ holds v p
| v (and p q) := holds v p ∧ holds v q
| v (or p q) := holds v p ∨ holds v q
| v (imp p q) := holds v p → holds v q
| v (iff p q) := holds v p ↔ holds v q
| v (forall_ x p) := ∀ a : D, holds ((x ↦ a) v) p
| v (exists_ x p) := ∃ a : D, holds ((x ↦ a) v) p

def is_valid (p : formula) : Prop :=
∀ D : Type, ∀ m : interpretation D, ∀ v : valuation D, holds D m v p

EDIT:

The immediate issue is that I don't understand the fundamental idea of what it means to substitute a predicate for a predicate. That is, I don't have an algorithm using any of the techniques for handling binders. If it is a propositional variable I believe it is only a name replacement, but I don't understand the case for general predicates. What is being replaced by what in the terms and why? A few basic examples would be very helpful. I'm having a hard time finding much of any kind of reference to it.

EDIT:

It appears that if P is a valid formula then uniformly replacing a formula Q for any predicate in P results in a valid formula as long as the free variables in Q do not become bound in the replacement: https://github.com/pthomas505/lean3/blob/cad06c04fbe96e14e1dc76822225a917ba29b76c/src/metalogic/pred.lean#L1176

I am a little confused by this, because I had expected there to be more conditions required, such as those described here: https://math.stackexchange.com/a/1374989/245129

UPDATE:

The sub_pred_formula function in the code below is my attempt to define the substitution in Haskell, but I think it is probably wrong. I would be really grateful if someone could help me fix it, if it is.

{-
References:

https://www.cambridge.org/core/books/handbook-of-practical-logic-and-automated-reasoning/EB6396296813CB562987E8C37AC4520D
https://www.cl.cam.ac.uk/~jrh13/atp/index.html
Harrison, J. (2009).
Handbook of Practical Logic and Automated Reasoning.
Cambridge: Cambridge University Press.
doi:10.1017/CBO9780511576430
-}


import Data.List
import Data.Set
import Data.Foldable


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


data Formula = Pred String [Term]
             | Not Formula
             | Imp Formula Formula
             | Forall String Formula
               deriving (Show, Eq)


{-
all_var_set t = The set of the names of all of the variables that occur in
the term t.
-}
all_var_set :: Term -> Data.Set.Set String
all_var_set (Var x) = Data.Set.singleton x
all_var_set (Func _ ts) = Data.Set.unions (Data.List.map all_var_set ts)


{-
free_var_set p = The set of the names of all of the variables that occur
free in the formula p.
-}
free_var_set :: Formula -> Data.Set.Set String
free_var_set (Pred _ ts) = Data.Set.unions (Data.List.map all_var_set ts)
free_var_set (Not p) = free_var_set p
free_var_set (Imp p q) = Data.Set.union (free_var_set p) (free_var_set q)
free_var_set (Forall x p) = Data.Set.delete x (free_var_set p)


{-
sub_var_term sigma t = The simultaneous substitution of each variable x
in t by sigma x.
-}
sub_var_term :: (String -> Term) -> Term -> Term
sub_var_term sigma (Var x) = sigma x
sub_var_term sigma (Func f ts) = Func f (Data.List.map (sub_var_term sigma) ts)


{-
variant x xs = If x is not in xs then x. If x is in xs then the string
obtained by appending a single quote to x until the resulting string is not in
xs.
-}
variant :: String -> Data.Set.Set String -> String
variant x xs = if Data.Set.member x xs then variant (x ++ "'") xs else x

{-
update_function f x y = The function that maps x to y and all other
values z to f z.
-}
update_function :: (Eq a) => (a -> b) -> a -> b -> (a -> b)
update_function f x y = \z -> if z == x then y else f z

{-
sub_var_formula sigma p = The simultaneous substitution of each free variable
x in p by sigma x. Each binding variable in p is replaced as needed to ensure
that no variable in sigma x becomes bound in the substitution.
-}
sub_var_formula :: (String -> Term) -> Formula -> Formula
sub_var_formula sigma (Pred p ts) =
  Pred p (Data.List.map (sub_var_term sigma) ts)
sub_var_formula sigma (Not p) =
  Not (sub_var_formula sigma p)
sub_var_formula sigma (Imp p q) =
  Imp (sub_var_formula sigma p) (sub_var_formula sigma q)
sub_var_formula sigma (Forall x p) =
  let free = Data.Set.difference (free_var_set p) (Data.Set.singleton x) in
  let x' = if Data.Foldable.any
             (\y -> Data.Set.member x (all_var_set (sigma y))) free
           then variant x
             (free_var_set
               (sub_var_formula (update_function sigma x (Var x)) p))
           else x
  in Forall x' (sub_var_formula (update_function sigma x (Var x')) p)


sub_single_var :: String -> Term -> Formula -> Formula
sub_single_var x t p =
  let sigma = update_function (\y -> Var y) x t in
  sub_var_formula sigma p

zip_check_length :: (a -> b -> c) -> [a] -> [b] -> [c]
zip_check_length _ [] [] = []
zip_check_length f (x : xs) (y : ys) = (f x y) : zip_check_length f xs ys
zip_check_length _ _ _ = error "zip_check_length"


-- uniform simultaneous replacement of the predicates in a formula by formulas

all_pred_set :: Formula -> Data.Set.Set (String, [Term])
all_pred_set (Pred p ts) = Data.Set.singleton (p, ts)
all_pred_set (Not p) = all_pred_set p
all_pred_set (Imp p q) = Data.Set.union (all_pred_set p) (all_pred_set q)
all_pred_set (Forall _ p) = all_pred_set p

zip_to_function :: (Eq a) => [a] -> [b] -> (a -> b) -> (a -> b)
zip_to_function [] [] f = f
zip_to_function (x:xs) (y:ys) f = zip_to_function xs ys (update_function f x y)
zip_to_function _ _ _ = error "zip_to_function"

zip_var_to_term :: [String] -> [Term] -> (String -> Term)
zip_var_to_term xs ts = zip_to_function xs ts (\x -> Var x)

sub_pred_formula_aux ::
  (String -> Term) -> ((String, [Term]) -> ([String], Formula)) -> Formula -> Formula
sub_pred_formula_aux sigma m (Pred p ts) =
  let (params, q) = m (p, ts) in
  let sigma' = zip_to_function params ts sigma in
  sub_var_formula sigma' q
sub_pred_formula_aux sigma m (Not p) =
  Not (sub_pred_formula_aux sigma m p)
sub_pred_formula_aux sigma m (Imp p q) =
  Imp (sub_pred_formula_aux sigma m p) (sub_pred_formula_aux sigma m q)
sub_pred_formula_aux sigma m (Forall x p) =
  let x' = if Data.Foldable.any
             (\r -> Data.Set.member x
               (Data.Set.difference (free_var_set (snd (m r))) (Data.Set.fromList (fst (m r)))))
             (all_pred_set p)
           then variant x (free_var_set
             (sub_pred_formula_aux (update_function sigma x (Var x)) m p))
           else x
  in Forall x' (sub_pred_formula_aux (update_function sigma x (Var x')) m p)

sub_pred_formula :: ((String, [Term]) -> ([String], Formula)) -> Formula -> Formula
sub_pred_formula m p = sub_pred_formula_aux (\x -> Var x) m p

sub_single_pred :: (String, [Term]) -> ([String], Formula) -> Formula -> Formula
sub_single_pred (p, ts) (params, q) r =
  let m = update_function (\(p', ts') -> ([], Pred p' ts')) (p, ts) (params, q) in
  sub_pred_formula m r



data Step = Modus_Ponens Int Int
          | Prop_1 Formula Formula
          | Prop_2 Formula Formula Formula
          | Prop_3 Formula Formula
          | Gen Int String
          | Pred_1 Formula Formula String
          | Pred_2 Formula String Term
          | Pred_3 Formula String
          | Eq_1 Term
          | Eq_2 String [Term] [Term]
          | Eq_3 String [Term] [Term]


check_step :: [Formula] -> Step -> [Formula]

-- |- p & |- (p -> q) => |- q
check_step context (Modus_Ponens p_index p_q_index) =
  let p = context !! p_index in
  let (Imp p' q) = context !! p_q_index in
  if p == p' then context ++ [q] else error "Modus_Ponens"

-- |- (p -> (q -> p))
check_step context (Prop_1 p q) =
  context ++ [(p `Imp` (q `Imp` p))]

-- |- ((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
check_step context (Prop_2 p q r) =
  context ++ [((p `Imp` (q `Imp` r)) `Imp` ((p `Imp` q) `Imp` (p `Imp` r)))]

-- |- ((~p -> ~q) -> (q -> p))
check_step context (Prop_3 p q) =
  context ++ [(((Not p) `Imp` (Not q)) `Imp` (q `Imp` p))]


-- |- p => |- (forall x. p)
check_step context (Gen p_index x) =
  let p = context !! p_index in
  context ++ [(Forall x p)]

-- |- ((forall x. (p -> q)) -> ((forall x. p) -> (forall x. q)))
check_step context (Pred_1 p q x) =
  context ++ [((Forall x (p `Imp` q)) `Imp` ((Forall x p) `Imp` (Forall x q)))]

-- |- ((forall x. p) -> (p [x -> t]))
check_step context (Pred_2 p x t) =
  context ++ [((Forall x p) `Imp` (sub_single_var x t p))]

-- |- (p -> (forall x. p)) provided x is not free in p
check_step context (Pred_3 p x) =
  if Data.Set.notMember x (free_var_set p)
  then context ++ [(p `Imp` (Forall x p))]
  else error "Pred_3"


-- |- t = t
check_step context (Eq_1 t) =
  context ++ [(Pred "Eq" [t, t])]

-- |- s1 = t1 -> ... -> sn = tn -> f(s1,..,sn) = f(t1,..,tn)
check_step context (Eq_2 f ss ts) =
  -- eqs = [s1 = t1, ..., sn = tn]
  let eqs = zip_check_length (\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
  context ++ [(Prelude.foldr Imp z eqs)]

-- |- s1 = t1 -> ... -> sn = tn -> P(s1,..,sn) -> P(t1,..,tn)
check_step context (Eq_3 p ss ts) =
  -- eqs = [s1 = t1, ..., sn = tn]
  let eqs = zip_check_length (\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
  context ++ [(Prelude.foldr Imp z eqs)]


check_step_list_aux :: [Formula] -> [Step] -> Formula
check_step_list_aux context [] = Data.List.last context
check_step_list_aux context (step : step_list) =
  let context' = check_step context step in
  check_step_list_aux context' step_list

check_step_list :: [Step] -> Formula
check_step_list step_list = check_step_list_aux [] step_list


example_1 = [
  (Prop_2 (Pred "P" []) ((Pred "P" []) `Imp` (Pred "P" [])) (Pred "P" [])),
  (Prop_1 (Pred "P" []) ((Pred "P" []) `Imp` (Pred "P" []))),
  (Modus_Ponens 1 0),
  (Prop_1 (Pred "P" []) (Pred "P" [])),
  (Modus_Ponens 3 2) ]
```
$\endgroup$
16
  • 1
    $\begingroup$ Are you familiar with any of the answers to proofassistants.stackexchange.com/questions/316/… ? $\endgroup$
    – mudri
    Jun 6 at 11:13
  • 2
    $\begingroup$ Another day, another victim of substitution lemmas. I know I am going to sound very arrogant an condescending, but if you're going to formalize logic you should not do it the way logic textbooks suggest. If you find yourself using string you've already set yourself up for a great deal of suffering. The people who know how to do this come from the area known as "programming language theory" – you should learn from them (us), see @mudri's suggestion. $\endgroup$ Jun 6 at 19:29
  • $\begingroup$ So, on a more positive note, please tell us in these comments what your background is and whether you're familiar with the techniques that mudri linked to. $\endgroup$ Jun 6 at 19:33
  • 1
    $\begingroup$ There seem to be three things you allude to in your most recent comment: renaming (substituting variables for variables), substitution (substituting terms in for variables), and a kind of find-and-replace (substituting terms in for other terms). If it's the latter you're thinking of, it's going to be somewhat more difficult to reason about than either of the former two, but should be doable. I'd still look to work around it by, for example, introducing a third term with a free variable, such that when you substitute terms in for that free variable, the result is the terms you're interested in. $\endgroup$
    – mudri
    Jun 10 at 11:10
  • 1
    $\begingroup$ In that case, you're using the wrong software to implement a proof assistant. You should be using a Real Programming Language, not another proof assistant. Do you know about lexers, parsers, type-checking algorithms, and other standard technology involved with implementation of a proof assistant? Those will come in handy. $\endgroup$ Jun 15 at 5:46

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.