making my own logic system. Look at these sexy ass rules:
∀-Introduction:
a1,...,an (j) (Ot -> ∮t) & Ot
...
a1,...,an (k) (∀v)∮v & Ov j ∀I
Where t isn’t in any of the formulae on lines a1,...,an and v is a variable not already in ∮t, replaces every occurrence of t in ∮t. Also O ∈ℨ.
∀-Elimination:
a1,...,an (j) (∀v)∮v & Ov
...
a1,...,an (k) (Ot -> ∮t) & Ot j ∀E
Where t replaces every occurrence of v in ∮v and O ∈ℨ
∐-Introduction:
a1,...,an (j) Ot & ∮t
...
a1,...,an (k) (∐v)∮v & Ov j ∐I
Where v, a new variable, replaces at least one occurrence of t in ∮t. Also O ∈ℨ.
∐-Elimination:
a1,...,an (i) (∐v)∮v & Ov
...
a1,...,an (j) Ot & ∮t Assumption
...
b1,...,bu (k) ℭ
...
X (m) ℭ i,j,k ∐E
Where t is not in ℭ, (∐v)∮v or any of the formulae at lines b1,..,bu other than j. X = {a1,..,an} ∪ {b1,...,bu}/j; t replaces every occurrence of v in ∮v. Also O ∈ℨ.
