tnt.lean

-- Formalization of Hofstadter's "TNT" system

import init.data.list

namespace tnt

-- TNT terms and formulas -----------------------------------------------------

inductive term : Type
| zero : term
| var : string → term
| succ : term → term
| add : term → term → term
| mul : term → term → term

instance : has_zero term := ⟨term.zero⟩
instance : has_add term := ⟨term.add⟩
instance : has_mul term := ⟨term.mul⟩

inductive formula : Type
| eq : term → term → formula
| not : formula → formula
| and : formula → formula → formula
| or : formula → formula → formula
| implies : formula → formula → formula
| any : string → formula → formula
| all : string → formula → formula

-- Concepts -------------------------------------------------------------------

open term
open formula

-- True if the variable u occurs in the given term.
def occurs_in (u : string) : term → Prop
| zero := false
| (var v) := v = u
| (succ a) := occurs_in a
| (add a b) := occurs_in a ∨ occurs_in b
| (mul a b) := occurs_in a ∨ occurs_in b

-- True if the variable u occurs free in the given formula.
def free_in (u : string) : formula → Prop
| (eq a b) := occurs_in u a ∨ occurs_in u b
| (not a) := free_in a
| (and a b) := free_in a ∨ free_in b
| (or a b) := free_in a ∨ free_in b
| (implies a b) := free_in a ∨ free_in b
| (any v a) := if u = v then false else free_in a
| (all v a) := if u = v then false else free_in a

-- Search a term (the third argument) for all instances of the variable `u` and
-- replace them with the term `t`.
def subst_term (t : term) (u : string) : term → term
| zero := zero
| (var v) := if v = u then t else var v
| (succ a) := succ (subst_term a)
| (add a b) := subst_term a + subst_term b
| (mul a b) := subst_term a * subst_term b

-- Search a formula (the third argument) for all free uses of the variable `u`
-- and replace them with the term `t`.
--
-- This implements "proper substitution": bound uses of `u` are not replaced.
--
-- The real TNT rule for specialization instead does a brute force
-- search-and-replace, and prevents naming conflicts by requiring that "[the
-- term being inserted] contains no variables that are bound in [the formula]",
-- but that would be way more work for us. I think the difference is
-- superficial.
def subst (t : term) (u  : string) : formula → formula
| (eq a b) := eq (subst_term t u a) (subst_term t u b)
| (not p) := not (subst p)
| (and a b) := and (subst a) (subst b)
| (or a b) := or (subst a) (subst b)
| (implies a b) := implies (subst a) (subst b)
| f@(any v a) := if v = u then f else any v (subst a)
| f@(all v a) := if v = u then f else all v (subst a)


-- Proofs ---------------------------------------------------------------------

-- A proof is valid or not with respect to a list of premises.
--notation `env` := list formula
def env : Type := list formula

namespace env
  def as_list (e : env) : list formula := e
end env

-- Define TNT proofs as a Lean type.
inductive proof : env → formula → Type
-- Inference rules of Hofstadter's Propositional Calculus
--    Rule of Joining: If A and B are theorems, so is <A∧B>.
| join {e : env} {a b : formula} : proof e a → proof e b → proof e (and a b)
--    Rule of Separation: If <A∧B> is a theorem, then A and B are also theorems.
| separate_left {e : env} {a b : formula} : proof e (and a b) → proof e a
| separate_right {e : env} {a b : formula} : proof e (and a b) → proof e b
--    Double-Tilde Rule: The string ~~ can be deleted from any theorem to make
--    a new theorem. The string ~~ can be added into any theorem to make a new
--    theorem, provided the resulting string is well-formed.
-- (This formulation is not correct or sound; the type of f is too permissive)
| notnot_delete {e : env} {f : formula → formula} {a : formula} :
    proof e (f (not (not a))) → proof e (f a)
| notnot_add {e : env} {f : formula → formula} {a : formula} :
    proof e (f a) → proof e (f (not (not a)))
--    Fantasy Rule: If assuming A to be a theorem leads to B being a theorem,
--    then <A⊃B> is a theorem.
| fantasy {e : env} {a b : formula} : proof (a :: e) b → proof e (implies a b)
--    Carry-over Rule: Inside a fantasy, any theorem from the reality one level
--    higher can be brought in and used.
| carry_over {e : env} {a b : formula} : proof e b → proof (a :: e) b
--    Rule of Detachment: If A and <A⊃B> are theorems, then B is a theorem.
| detach {e : env} {a b : formula} : proof e a → proof e (implies a b) → proof e b
--    Contrapositive Rule: <A⊃B> and <~B⊃~A> are interchangeable.
| contrapositive_add {e : env} {a b : formula} :
    proof e (implies a b) → proof e (implies (not b) (not a))
| contrapositive_delete {e : env} {a b : formula} :
    proof e (implies (not b) (not a)) → proof e (implies a b)
--    DeMorgan's Rule: <~A∧~B> and ~<A∨B> are interchangeable.
| and_to_or {e : env} {a b : formula} :
    proof e (and (not a) (not b)) → proof e (not (or a b))
| or_to_and {e : env} {a b : formula} :
    proof e (not (or a b)) → proof e (and (not a) (not b))
--    Switcheroo Rule: <A∨B> and <~A⊃B> are interchangeable.
| or_to_implies {e : env} {a b : formula} : proof e (or a b) → proof e (implies (not a) b)
| implies_to_or {e : env} {a b : formula} : proof e (implies (not a) b) → proof e (or a b)
--
-- Inference rules of TNT
--    Axiom 1: ∀a:~Sa=0
| ax1 {e : env} {a : string} : proof e (all a (not (eq (succ (var a)) zero)))
--    Axiom 2: ∀a:(a+0)=a
| ax2 {e : env} {a : string} : proof e (all a (eq ((var a) + zero) (var a)))
--    Axiom 3: ∀a:∀b:(a+Sb)=S(a+b)
| ax3 {e : env} {a b : string} : proof e (all a (all b (eq ((var a) + (succ (var b)))
                                                           (succ ((var a) + (var b))))))
--    Axiom 4: ∀a:(a•0)=0
| ax4 {e : env} {a : string} : proof e (all a (eq ((var a) * zero) zero))
--    Axiom 5: ∀a:∀b:(a•Sb)=((a•b)+a)
| ax5 {e : env} {a b : string} : proof e (all a (all b (eq (var a * succ (var b))
                                                           ((var a * var b) + var a))))
--    Rule of Specification: If ∀u:A is a theorem then so are A and A{t/u} provided t contains no variables that are bound in A
-- (It is easier to just do proper substitution, sorry)
| specification_1 {e : env} {u : string} {a : formula} : proof e (all u a) → proof e a
| specification_2 {e : env} {u : string} {a : formula} (t : term) : proof e (all u a) → proof e (subst t u a)
--    Rule of Generalization: If A is a theorem in which u is free, then so is ∀u:A, provided u is not free in the premise of any fantasy containing A
| generalization {e : env} {u : string} {a : formula} : proof e a → (∀ f, f ∈ e.as_list → ¬free_in u f) → proof e (all u a)
--    Rule of Interchange: The strings ∀u:~ and ~∃u: are interchangeable anywhere inside a theorem to produce a new theorem
-- (Same problem as with the Double-Tilde Rule.)
| all_to_any {e : env} {u : string} {f : formula → formula} {a : formula} :
    proof e (f (all u (not a))) → proof e (f (not (any u a)))
| any_to_all {e : env} {u : string} {f : formula → formula} {a : formula} :
    proof e (f (not (any u a))) → proof e (f (all u (not a)))
--    Symmetry of Equality: If s=t is a theorem then so is t=s
| symm_eq {e : env} {s t : term} : proof e (eq s t) → proof e (eq t s)
--    Transitivity of Equality: If r=s and s=t are theorems then so is r=t
| trans_eq {e : env} {r s t : term} : proof e (eq r s) → proof e (eq s t) → proof e (eq r t)
--    Add S: If r=t is a theorem then so is Sr=St
| add_succ {e : env} {r t : term} : proof e (eq r t) → proof e (eq (succ r) (succ t))
--    Drop S: If Sr=St is a theorem then so is r=t
| drop_succ {e : env} {r t : term} : proof e (eq (succ r) (succ t)) → proof e (eq r t)
--    Rule of Induction: If A{0/u} and ∀u:<A⊃A{Su/u}> are both theorems, then so is ∀u:A
| induction {e : env} {a : formula} {u : string} :
    proof e (subst zero u a) →
    proof e (all u (implies a (subst (succ (var u)) u a))) →
    proof e (all u a)

example (e : env) : proof e (not (any "a" (eq (succ (var "a")) zero))) :=
  @proof.all_to_any e "a" id _ proof.ax1

end tnt