how do I say "a sentence is a theorem of a theory" in lean?

Stream: maths

[Bulhwi Cha]

Bulhwi Cha said:

A user of a Korean-speaking philosophy discussion forum said, "You didn't prove that ∃ (x : Being), isGod x ∧ inReality x is not a theorem of a theory whose axioms are the premises of St. Anselm's argument (and the axioms of Lean's type theory)."

How can I construct a theory T and state that a proposition φ is not a theorem of T in Lean?

[Bulhwi Cha]

Of course, the first step is "Learn proof theory and model theory."

[Alistair Tucker]

In your case you just need to demonstrate that for some instantiation of your class the proposition is false. E.g. for Anselm Nat with Conceivable := fun _ => True there is provably no x such that IsMax x Conceivable.

[Bulhwi Cha]

Thank you, Alistair Tucker. Here's my attempt:

section

local instance : Anselm ℤ where
  conceivable := fun _ ↦ True
  inUnderstanding := fun _ ↦ True
  inReality := fun
    | .ofNat _ => True
    | .negSucc _ => False
  lt_of_inUnderstanding_not_inReality_inReality {_ _ : ℤ} := by
    repeat (first | simp | split <;> simp [not_true, not_false])
    rename_i n _ m
    calc
      -(n + 1) < (0 : ℤ) := Int.negSucc_lt_zero n
      0 ≤ ↑m := Int.zero_le_ofNat m
  isMax_conceivable_inUnderstanding := by simp
  exists_conceivable_and_inReality := by exists 0

private theorem not_exists_int_isGod : ¬ ∃ (a : ℤ), isGod a := by
  intro hex
  rcases hex with ⟨god, _hcg, hleg⟩
  have god_lt_succ_god : god < god + 1 := Int.lt_succ god
  have succ_god_le_god : god + 1 ≤ god := hleg (god + 1) trivial
  exact not_le_of_lt god_lt_succ_god succ_god_le_god

end