defining wff

Stream: new members

[Patrick Thomas]

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]

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]

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]

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]

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]

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

[Andrew Ashworth]

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]

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]

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