showing that proofs are finite

Stream: new members

[Eduardo Freire]

Hello, I'm trying to prove that classical propositional logic is complete and have one remaining sorry that I'm stuck on which involves showing that proofs are finite. Here is the MWE:

import tactic

inductive prop_formula
| var : ℕ → prop_formula
| imp : prop_formula → prop_formula → prop_formula

inductive prop_thm : set prop_formula → prop_formula → Prop
| ax : ∀{Γ p}, p ∈ Γ → prop_thm Γ p
| imp_i : ∀{Γ p q}, prop_thm (Γ ∪ {p}) q → prop_thm Γ (p.imp q)

theorem fin_subset_proves_of_proves {Γ : set prop_formula} {φ : prop_formula} :
prop_thm Γ φ → ∃Δ, Δ ⊆ Γ ∧ set.finite Δ ∧ prop_thm Δ φ := sorry

In order to prove this I wanted to make a function assumptions_used : ∀Γ p, prop_thm Γ p → set prop_formula which gives me the smallest set of formulas in Γ needed to prove p. Here is my attempt:

def assumptions_used : ∀Γ p, prop_thm Γ p → set prop_formula
| Γ p (prop_thm.ax _ _ h) := {p}
| Γ p (prop_thm.imp_i _ q r h) := (assumptions_used (Γ ∪ {q}) r h) \ {q}

This gives me the error "induction tactic failed, recursor 'prop_thm.dcases_on' can only eliminate into Prop", which I don't know how to resolve. I have little experience with defining functions using the equation compiler so I wouldn't be surprised if this is nonsense. Do you have any hints or suggestions?

[Kyle Miller]

Proof irrelevance means that with prop_thm being Prop-valued, you can't do pattern matching to construct something Type-valued. The error message is telling you that you're only allowed to pattern match to construct something Prop-valued.

Maybe you might want this?

inductive prop_thm : set prop_formula → prop_formula → Type
| ax : ∀{Γ p}, p ∈ Γ → prop_thm Γ p
| imp_i : ∀{Γ p q}, prop_thm (Γ ∪ {p}) q → prop_thm Γ (p.imp q)

[Kyle Miller]

Then you can write nonempty (prop_thm Δ φ) when you want a Prop version.

[Eduardo Freire]

Oh that makes sense, seems like it works. Thanks!

[Eduardo Freire]

On a related note, is Tukey's lemma (or something similar) in mathlib?

[Matt Diamond]

@Eduardo Freire maybe https://leanprover-community.github.io/mathlib_docs/order/zorn.html?

[Eduardo Freire]

Yeah, initially I thought that Zorn's lemma would be harder to apply, but thinking about it its probably the same amount of work.
Nice to know that there is a place showing the several versions of it, thank you

[Matt Diamond]

no problem... btw, not sure if this is relevant but there's a proof of Hausdorff's Maximality Principle here: https://leanprover-community.github.io/mathlib_docs/order/chain.html

[Patrick Johnson]

Regarding the main question, assumptions_used is not really needed. You could define it using Kyle's suggestion and define a function that converts prop-valued prop_thm to type-valued prop_thm using choice (or just define type-valued version only), but it's easier to just use induction directly:

import tactic
import tactic.induction

inductive prop_formula
| var : ℕ → prop_formula
| imp : prop_formula → prop_formula → prop_formula

inductive prop_thm : set prop_formula → prop_formula → Prop
| ax : ∀{Γ p}, p ∈ Γ → prop_thm Γ p
| imp_i : ∀{Γ p q}, prop_thm (Γ ∪ {p}) q → prop_thm Γ (p.imp q)

lemma union_proves_of_proves {s t : set prop_formula} {p : prop_formula}
  (h : prop_thm s p) : prop_thm (s ∪ t) p :=
begin
  induction' h,
  { left, exact set.mem_union_left _ h },
  { right, rw [set.union_assoc, set.union_comm t, ←set.union_assoc], exact ih },
end

lemma fin_subset_proves_of_proves {Γ : set prop_formula} {φ : prop_formula}
  (h : prop_thm Γ φ) : ∃ (Δ : set prop_formula), Δ ⊆ Γ ∧ Δ.finite ∧ prop_thm Δ φ :=
begin
  induction' h,
  { use [{φ}, by rwa set.singleton_subset_iff, set.finite_singleton _],
    left, apply set.mem_singleton },
  { rcases ih with ⟨Δ, h₁, h₂, h₃⟩,
    use [Δ \ {φ}, by rwa [set.diff_subset_iff, set.union_comm], set.finite.diff h₂ _],
    right, rw set.diff_union_self, exact union_proves_of_proves h₃ },
end

[Eduardo Freire]

That is really helpful, I should be one application of Zorn's lemma away from proving the main result now, thanks!