# Zulip Chat Archive

## Stream: new members

### Topic: defining wff

#### Patrick Thomas (Aug 03 2019 at 00:11):

I was wondering if the following definition can be formalized in Lean, and if so, how. I am thinking that a propositional variable might be defined as a natural number, but I am not sure how to introduce the connectives.

DEFINITION. The set of wffs is the intersection of all sets S of formulas such

that:

(i) p ∈ S for each propositional variable p.

(ii) For each formula A, if A ∈ S, then ~A ∈ S.

(iii) For all formulas A and B, if A ∈ S and B ∈ S, then [A ∨ B] ∈ S.

A wff is a member of the set of wffs.

I would like to use this definition in a formal proof of the following exercise:

Using the definition of the set of wffs, show that:

(a) Every formula consisting of a propositional variable standing alone is

a wff.

(b) If A is a wff, then ~A is a wff.

(c) If A and B are wffs, then [A ∨ B] is a wff.

#### Mario Carneiro (Aug 03 2019 at 00:27):

While it is possible to define wffs in this set-theoretic way, the much easier approach is to use an inductive type - this is what they are designed for. With that the theorem is trivial, as it is just the constructors of the inductive type

#### Floris van Doorn (Aug 03 2019 at 00:31):

Here is an example of using inductive types for this:

-- α is the type of propositional variables inductive wff (α : Type) : Type | var : α → wff | neg : wff → wff | or : wff → wff → wff local prefix `#` := wff.var local prefix `~` := wff.neg local infix ` ∨ ` := wff.or example {α} (p q : α) : wff α := #p ∨ ~ #q

#### Patrick Thomas (Aug 03 2019 at 00:40):

Thank you. I would still be interested in seeing how it might be done in the set-theoretic way, if you have a chance.

#### Floris van Doorn (Aug 03 2019 at 00:49):

In that case, I would define a character as a propositional variable or one of the 4 special characters (`~ [ ] ∨`

) and then define `S`

to be a set on the type of list of characters (`S`

is the intersection of all sets satisfying ...)

#### Patrick Thomas (Aug 03 2019 at 00:58):

I'm sorry, I'm not sure I understand.

#### Andrew Ashworth (Aug 03 2019 at 01:16):

It's a much more raw interpretation. Your formulas are sequences of `[ ] ~ \/ 1 2 3 4 5 6 7 8 9`

. Step 1 is to turn a sequence of digits into a var. Step 2 is to come up with a prop describing 1, 2, 3 in terms of this raw list of characters.

#### Floris van Doorn (Aug 03 2019 at 01:17):

import data.set.lattice noncomputable theory open sum -- Var is the type of propositional variables constant Var : Type def character := Var ⊕ fin 4 def lbracket : character := inr 0 def rbracket : character := inr 1 def neg : character := inr 2 def disj : character := inr 3 local notation `⟦` := lbracket local notation `⟧` := rbracket local notation `~` := neg local notation `∨` := disj def wff : set (list character) := ⋂₀ { S | (∀(p : Var), [inl p] ∈ S) ∧ (∀(A ∈ S), [ ~ ] ++ A ∈ S) ∧ ∀(A B ∈ S), [ ⟦ ] ++ A ++ [ ∨ ] ++ B ++ [ ⟧ ] ∈ S }

#### Patrick Thomas (Aug 03 2019 at 01:24):

It might take me a bit to go through this, but thank you!

Last updated: May 14 2021 at 02:15 UTC