Zulip Chat Archive

Stream: new members

Topic: defining wff


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 ...)

view this post on Zulip Patrick Thomas (Aug 03 2019 at 00:58):

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

view this post on Zulip 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.

view this post on Zulip 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 }

view this post on Zulip 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