Formula

Difficulty: moderate — 4 definitions, 1 abbreviations, 0 lemmas, 0 theorems, 0 examples.

definition abbreviation
legend

The syntax and semantics of classical propositional logic: formulas built from atomic propositions and the four connectives negation, conjunction, disjunction, and implication, and the truth table each formula computes.

A propositional formula over a type \(\alpha\) of atomic propositions. Built from an atom, or from a smaller formula (or two) by one of the four connectives: negation, conjunction, disjunction, and implication.

Propositional.Formula (α : Type) : Type
Show details 
| Propositional.Formula.atom : {α : Type} → α → Propositional.Formula α
| Propositional.Formula.neg : {α : Type} → Propositional.Formula α → Propositional.Formula α
| Propositional.Formula.and : {α : Type} → Propositional.Formula α → Propositional.Formula α → Propositional.Formula α
| Propositional.Formula.or : {α : Type} → Propositional.Formula α → Propositional.Formula α → Propositional.Formula α
| Propositional.Formula.imp : {α : Type} → Propositional.Formula α → Propositional.Formula α → Propositional.Formula α

Outer dependencies: (none)

Lean core dependencies: Eq, HEq, Nat, Nat.ble, Nat.decEq, Not, PProd, PULift, PUnit, SizeOf, cond, dite, eq_of_heq

Used by: Propositional.Formula.Derivable, Propositional.Formula.Derivable.case_split, Propositional.Formula.Derivable.deduction, Propositional.Formula.Derivable.deduction_aux, Propositional.Formula.Derivable.provable_of_nil, Propositional.Formula.Derivable.weaken, Propositional.Formula.Provable, Propositional.Formula.SemanticEntails, Propositional.Formula.SemanticEntails.refl, Propositional.Formula.SemanticEntails.trans, Propositional.Formula.SyntacticEntails, Propositional.Formula.SyntacticEntails.refl, Propositional.Formula.SyntacticEntails.trans, Propositional.Formula.Tautology, Propositional.Formula.and_isConjunction, Propositional.Formula.bigAnd, Propositional.Formula.bigAnd_val, Propositional.Formula.bigOr, Propositional.Formula.bigOr_val, Propositional.Formula.case_split, Propositional.Formula.completeness, Propositional.Formula.dnf, Propositional.Formula.dnf_val, Propositional.Formula.eliminate, Propositional.Formula.exists_andOrNot_of_boolFun, Propositional.Formula.kalmar, Propositional.Formula.literal, Propositional.Formula.literal_val, Propositional.Formula.minterm, Propositional.Formula.minterm_val, Propositional.Formula.nand, Propositional.Formula.neg_isClassicalNegation, Propositional.Formula.or_isDisjunction, Propositional.Formula.provable_contrapose, Propositional.Formula.provable_deMorgan_or, Propositional.Formula.provable_dni, Propositional.Formula.provable_explosion, Propositional.Formula.provable_imp_iff_semanticDerive, Propositional.Formula.provable_imp_iff_syntacticDerive, Propositional.Formula.provable_lem, Propositional.Formula.provable_self_imp, Propositional.Formula.soundness, Propositional.Formula.starred, Propositional.Formula.val, Propositional.NandFormula.exists_nand_of_boolFun, Propositional.NandFormula.ofFormula, Propositional.NandFormula.ofFormula_val, Propositional.NandFormula.toFormula, Propositional.semanticBasis3, Propositional.syntacticBasis3

The Sheffer stroke (“not both”): the single connective from which every other connective can be built, shown later in this chapter.

Propositional.Formula.nand {α : Type} (φ ψ : Propositional.Formula α) : Propositional.Formula α
Show details 
fun {α} φ ψ => (φ.and ψ).neg

Complexity: 21 (size of the value term)

Outer dependencies: Propositional.Formula

Used by: Propositional.NandFormula.toFormula

The truth value of a formula under a valuation: the truth table, computed structurally. Each connective’s clause is definitionally its usual truth-table rule, so it needs no separate lemma to unfold — plain simp already knows it.

Propositional.Formula.val {α : Type} (v : Propositional.Valuation α) :
  Propositional.Formula α → Bool
Show details 
fun {α} v x => Propositional.Formula.brecOn x (Propositional.Formula.val._f v)

Complexity: 27 (size of the value term)

Outer dependencies: Propositional.Formula, Propositional.Valuation

Lean core dependencies: Bool, Bool.and, Bool.not, Bool.or, Eq, Eq.mpr, Eq.symm, PProd, PUnit, congrArg, id

Used by: Propositional.Formula.SemanticEntails, Propositional.Formula.SemanticEntails.refl, Propositional.Formula.SemanticEntails.trans, Propositional.Formula.Tautology, Propositional.Formula.bigAnd_val, Propositional.Formula.bigOr_val, Propositional.Formula.completeness, Propositional.Formula.dnf_val, Propositional.Formula.exists_andOrNot_of_boolFun, Propositional.Formula.kalmar, Propositional.Formula.literal_val, Propositional.Formula.minterm_val, Propositional.Formula.neg_isClassicalNegation, Propositional.Formula.or_isDisjunction, Propositional.Formula.provable_imp_iff_semanticDerive, Propositional.Formula.soundness, Propositional.Formula.starred, Propositional.NandFormula.exists_nand_of_boolFun, Propositional.NandFormula.ofFormula_val, Propositional.NandFormula.toFormula_val

A tautology: true under every valuation.

Propositional.Formula.Tautology {α : Type} (φ : Propositional.Formula α) : Prop
Show details 
fun {α} φ => ∀ (v : Propositional.Valuation α), Propositional.Formula.val v φ = true

Complexity: 23 (size of the value term)

Outer dependencies: Propositional.Formula

Inner dependencies: Propositional.Formula.val, Propositional.Valuation

Lean core dependencies: Bool, Eq

Used by: Propositional.Formula.completeness, Propositional.Formula.soundness

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionabbreviationdeclared elsewheredependencyproof dependency
legend