## 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