class PropNeg (α : Type u) : Type u

• neg : α → α

def «term~_» : Lean.ParserDescr

Equations

• «term~_» = Lean.ParserDescr.node `«term~_» 58 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~ ") (Lean.ParserDescr.cat `term 58))

class PropImp (α : Type u) : Type u

• imp : α → α → α

def «term_⇒_» : Lean.TrailingParserDescr

Equations

• «term_⇒_» = Lean.ParserDescr.trailingNode `«term_⇒_» 55 56 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇒ ") (Lean.ParserDescr.cat `term 55))

class PropOr (α : Type u) : Type u

• or : α → α → α

def «term_⩒_» : Lean.TrailingParserDescr

Equations

• «term_⩒_» = Lean.ParserDescr.trailingNode `«term_⩒_» 56 57 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⩒ ") (Lean.ParserDescr.cat `term 56))

class PropAnd (α : Type u) : Type u

• and : α → α → α

def «term_⩑_» : Lean.TrailingParserDescr

Equations

• «term_⩑_» = Lean.ParserDescr.trailingNode `«term_⩑_» 57 58 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⩑ ") (Lean.ParserDescr.cat `term 57))

class PropIff (α : Type u) : Type u

• iff : α → α → α

def «term_⇔_» : Lean.TrailingParserDescr

Equations

• «term_⇔_» = Lean.ParserDescr.trailingNode `«term_⇔_» 55 56 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇔ ") (Lean.ParserDescr.cat `term 56))

class PropNotation (α : Type u) extends Top α, Bot α, PropNeg α, PropImp α, PropOr α, PropAnd α, PropIff α : Type u

Typeclass for propositional notations.

• top : α
• bot : α
• neg : α → α
• imp : α → α → α
• or : α → α → α
• and : α → α → α
• iff : α → α → α

class ClassicalPropNotation (α : Type u) : Type u

For classical logic, only ⊥ and ⇒ need to be defined; other notations are derived as follows:

• Negation ~ p = p ⇒ ⊥.
• True ⊤ = ~ ⊥.
• Disjunction (or) p ⩒ q = ~ p ⇒ q.
• Conjunction (and) p ⩑ q = ~ (p ⇒ ~ q).
• Iff p ⇔ q = (p ⇒ q) ⩑ (q ⇒ p).

• false : α
• imp : α → α → α

instance ClassicalPropNotation.instBot {α : Type u} [ClassicalPropNotation α] : Bot α

Equations

• ClassicalPropNotation.instBot = { bot := ClassicalPropNotation.false }

instance ClassicalPropNotation.instPropImp {α : Type u} [ClassicalPropNotation α] : PropImp α

Equations

• ClassicalPropNotation.instPropImp = { imp := ClassicalPropNotation.imp }

instance ClassicalPropNotation.instPropNeg {α : Type u} [ClassicalPropNotation α] : PropNeg α

Equations

• ClassicalPropNotation.instPropNeg = { neg := fun (p : α) => p ⇒ ⊥ }

instance ClassicalPropNotation.instTop {α : Type u} [ClassicalPropNotation α] : Top α

Equations

• ClassicalPropNotation.instTop = { top := ~ ⊥ }

instance ClassicalPropNotation.instPropOr {α : Type u} [ClassicalPropNotation α] : PropOr α

Equations

• ClassicalPropNotation.instPropOr = { or := fun (p q : α) => ~ p ⇒ q }

instance ClassicalPropNotation.instPropAnd {α : Type u} [ClassicalPropNotation α] : PropAnd α

Equations

• ClassicalPropNotation.instPropAnd = { and := fun (p q : α) => ~ (p ⇒ ~ q) }

instance ClassicalPropNotation.instPropIff {α : Type u} [ClassicalPropNotation α] : PropIff α

Equations

• ClassicalPropNotation.instPropIff = { iff := fun (p q : α) => (p ⇒ q) ⩑ (q ⇒ p) }

instance ClassicalPropNotation.instPropNotation {α : Type u} [ClassicalPropNotation α] : PropNotation α

Equations

• One or more equations did not get rendered due to their size.

theorem ClassicalPropNotation.true_def {α : Type u} [ClassicalPropNotation α] : ⊤ = ~ ⊥

theorem ClassicalPropNotation.neg_def {α : Type u} [ClassicalPropNotation α] {p : α} : ~ p = p ⇒ ⊥

theorem ClassicalPropNotation.or_def {α : Type u} [ClassicalPropNotation α] {p q : α} : p ⩒ q = ~ p ⇒ q

theorem ClassicalPropNotation.and_def {α : Type u} [ClassicalPropNotation α] {p q : α} : p ⩑ q = ~ (p ⇒ ~ q)

theorem ClassicalPropNotation.iff_def {α : Type u} [ClassicalPropNotation α] {p q : α} : p ⇔ q = (p ⇒ q) ⩑ (q ⇒ p)